Relaciones lógicas

Las relaciones lógicas son un método de prueba empleado en la semántica de los lenguajes de programación para demostrar que dos semánticas denotacionales son equivalentes.

Para describir el proceso, denotemos las dos semánticas por${\displaystyle [\![\cdot ]\!]_{i}}$, dónde${\displaystyle i\in \{1,2\}}$. Para cada tipo${\displaystyle A}$, existe una relación asociada particular${\displaystyle \sim }$entre${\displaystyle [\![A]\!]_{1}}$y${\displaystyle [\![A]\!]_{2}}$. Esta relación se define de tal manera que para cada frase del programa${\displaystyle M}$, las dos denotaciones están relacionadas:${\displaystyle [\![M]\!]_{1}\sim [\![M]\!]_{2}}$Otra propiedad de esta relación es que las denotaciones relacionadas para los tipos básicos son equivalentes en cierto sentido, generalmente iguales. La conclusión es que ambas denotaciones exhiben un comportamiento equivalente en los términos básicos, por lo que son equivalentes.

https://www.cs.uoregon.edu/research/summerschool/summer16/notes/AhmedLR.pdf

https://www.cs.uoregon.edu/research/summerschool/summer13/lectures/ahmed-1.pdf

• POPLmark Reloaded : Pruebas que involucran relaciones lógicas utilizadas como referencia para asistentes de prueba .