Teorías unificadoras de la programación

Las Teorías Unificadoras de Programación ( UTP ) en informática se ocupan de la semántica de programas . Muestra cómo la semántica denotacional , la semántica operativa y la semántica algebraica pueden combinarse en un marco unificado para la especificación formal , el diseño y la implementación de programas y sistemas informáticos .

El libro de este título de CAR Hoare y He Jifeng se publicó en la Serie Internacional de Ciencias de la Computación de Prentice Hall en 1998 y ahora está disponible gratuitamente en la web. ^[1]

Teorias

La base semántica de la UTP es el cálculo de predicados de primer orden , ampliado con construcciones de punto fijo de la lógica de segundo orden. Siguiendo la tradición de Eric Hehner , los programas son predicados en UTP y no existe distinción entre programas y especificaciones a nivel semántico. En palabras de Hoare :

Un programa de computadora se identifica con el predicado más fuerte que describe cada observación relevante que se puede hacer del comportamiento de una computadora que ejecuta ese programa. ^[2]

En lenguaje UTP, una teoría es un modelo de un paradigma de programación particular. Una teoría UTP se compone de tres ingredientes:

• un alfabeto , que es un conjunto de nombres de variables que denotan los atributos del paradigma que puede observar una entidad externa;
• una firma , que es el conjunto de construcciones del lenguaje de programación intrínsecas al paradigma; y
• un conjunto de condiciones de salud , que definen el espacio de los programas que encajan dentro del paradigma. Estas condiciones de salud se expresan típicamente como transformadores de predicados idempotentes monótonos .

El refinamiento del programa es un concepto importante en la UTP. Un programa se refina si y sólo si cada observación que se puede hacer es también una observación de . La definición de refinamiento es común en todas las teorías UTP: ${\displaystyle P_{1}}$ ${\displaystyle P_{2}}$ ${\displaystyle P_{2}}$ ${\displaystyle P_{1}}$

${\displaystyle P_{1}\sqsubseteq P_{2}\quad {\text{if and only if}}\quad \left[P_{2}\Rightarrow P_{1}\right]}$

donde denota ^[3] el cierre universal de todas las variables del alfabeto. ${\displaystyle \left[X\right]}$

Relaciones

La teoría UTP más básica es el cálculo de predicados alfabetizado, que no tiene restricciones alfabéticas ni condiciones de salubridad. La teoría de las relaciones es un poco más especializada, ya que el alfabeto de una relación puede consistir únicamente en:

• variables no decoradas ( ), modelando una observación del programa al inicio de su ejecución; y ${\displaystyle v}$
• variables primadas ( ), modelando una observación del programa en una etapa posterior de su ejecución. ${\displaystyle v'}$

Algunas construcciones del lenguaje común se pueden definir en la teoría de las relaciones de la siguiente manera:

• La sentencia skip, que no altera el estado del programa de ninguna manera, se modela como la identidad relacional:

${\displaystyle \mathbf {skip} \equiv v'=v}$

• La asignación de valor a una variable se modela estableciendo y manteniendo constantes todas las demás variables (indicadas por ): ${\displaystyle E}$ ${\displaystyle a}$ ${\displaystyle a'}$ ${\displaystyle E}$ ${\displaystyle u}$

${\displaystyle a:=E\equiv a'=E\land u'=u}$

• La composición secuencial de dos programas es simplemente una composición relacional de estado intermedio:

${\displaystyle P_{1};P_{2}\equiv \exists v_{0}\bullet P_{1}[v_{0}/v']\land P_{2}[v_{0}/v]}$

• La elección no determinista entre programas es su mayor límite inferior:

${\displaystyle P_{1}\sqcap P_{2}\equiv P_{1}\lor P_{2}}$

• La elección condicional entre programas se escribe utilizando notación infija:

${\displaystyle P_{1}\triangleleft C\triangleright P_{2}\equiv (C\land P_{1})\lor (\lnot C\land P_{2})}$

• Una semántica para la recursividad viene dada por el punto menos fijo de un transformador de predicado monótono : ${\displaystyle \mu \mathbf {F} }$ ${\displaystyle \mathbf {F} }$

${\displaystyle \mu X\bullet \mathbf {F} (X)\equiv \sqcap \left\{X\mid \mathbf {F} (X)\sqsubseteq X\right\}}$

Referencias

1. Hoare, COCHE ; Jifeng, He (1 de abril de 1998). Teorías unificadoras de la programación. Prentice Hall. pag. 320.ISBN​ 978-0-13-458761-5. Consultado el 17 de septiembre de 2014 .
2. Hoare, CAR (abril de 1984). "Programación: ¿brujería o ciencia?". Software IEEE . 1 (2): 5–16. doi :10.1109/MS.1984.234042. S2CID  375578.
3. Dijkstra, Edsger W .; Scholten, Carel S. (1990). Cálculo de predicados y semántica de programas . Textos y Monografías en Informática. Saltador. ISBN 0-387-96957-8.

Otras lecturas

• Woodcock, Jim ; Cavalcanti, Ana (2004). "Un tutorial de introducción a los diseños en teorías unificadoras de programación" (PDF) . Métodos formales integrados . Apuntes de conferencias sobre informática , páginas. vol. 2999. Saltador. págs. 40–66. doi :10.1007/978-3-540-24756-2_4. ISBN 978-3-540-21377-2.
• Cavalcanti, Ana; Woodcock, Jim (2006). "Un tutorial de introducción a CSP en la unificación de teorías de programación" (PDF) . Técnicas de Refinamiento en Ingeniería de Software . Apuntes de conferencias sobre informática. vol. 3167. Saltador. págs. 220–268. doi :10.1007/11889229_6. ISBN 978-3-540-46253-8.

enlaces externos

• Sitio web del libro UTP
• Libro UTP en Archive.org