Teorías unificadoras de la programación

Las Teorías Unificadoras de la Programación ( UTP , por sus siglas en inglés) en informática abordan la semántica de los programas . Muestran cómo la semántica denotacional , la semántica operacional 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 con este título de CAR Hoare y He Jifeng ^{[ 1 ]} fue publicado en la Prentice Hall International Series in Computer Science en 1998 y se ha puesto a disposición gratuitamente en la web. ^{[ 2 ]}

En 2006 se inició una serie de simposios de la UTP. ^{[ 3 ]}

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

Un programa informático 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. ^{[ 4 ]}

En la jerga de 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 pueden ser observados por una entidad externa;
• una firma , que es el conjunto de construcciones del lenguaje de programación intrínsecas al paradigma; y
• una colección de condiciones de salud , que definen el espacio de programas que se ajustan al paradigma. Estas condiciones de salud se expresan típicamente como transformadores de predicados idempotentes monótonos .

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

${\displaystyle P_{1}\sqsubseteq P_{2}\quad {\text{si y solo si}}\quad \left[P_{2}\Rightarrow P_{1}\right]}$

dónde${\displaystyle \left[X\right]}$denota ^{[ 5 ]} el cierre universal de todas las variables en el alfabeto.

La teoría UTP más básica es el cálculo de predicados alfabetizados, que no tiene restricciones de alfabeto ni condiciones de salud. La teoría de relaciones es un poco más especializada, ya que el alfabeto de una relación puede constar únicamente de:

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

En la teoría de las relaciones, algunas construcciones lingüísticas comunes pueden definirse de la siguiente manera:

• La instrucción 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${\displaystyle E}$a una variable${\displaystyle a}$se modela como configuración${\displaystyle a'}$a${\displaystyle E}$y manteniendo todas las demás variables (denotadas por${\displaystyle u}$) constante:

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

• La composición secuencial de dos programas es simplemente la composición relacional de un 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 la 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 recursión viene dada por el punto fijo mínimo.${\displaystyle \mu \mathbf {F} }$de un transformador de predicados monótono${\displaystyle \mathbf {F} }$:

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

• Woodcock, Jim ; Cavalcanti, Ana (2004). «Introducción tutorial a los diseños en Teorías Unificadoras de la Programación» (PDF) . Métodos Formales Integrados . Notas de Clase en Ciencias de la Computación , páginas. Vol.  2999. Springer. pp. 40–66 . doi : 10.1007/978-3-540-24756-2_4 . ISBN  978-3-540-21377-2.
• Cavalcanti, Ana; Woodcock, Jim (2006). «Una introducción tutorial a CSP en Unifying Theories of Programming» (PDF) . Refinement Techniques in Software Engineering . Lecture Notes in Computer Science. Vol.  3167. Springer. pp. 220–268 . doi : 10.1007/11889229_6 . ISBN  978-3-540-46253-8.

• Sitio web de libros de UTP
• Libro de UTP en Archive.org
• Libro de UTP en la Biblioteca Abierta del Archivo de Internet