Teorías unificadas de la programación

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

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

Teorías

La base semántica de la UTP es el cálculo de predicados de primer orden, aumentado con construcciones de punto fijo a partir de la lógica de segundo orden. Siguiendo la tradición de Eric Hehner, los programas son predicados en el UTP, y no hay 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 sobre el comportamiento de una computadora que ejecuta ese programa.

En el 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 de lenguaje de programación intrínsecas al paradigma; y
• una colección de condiciones de salubridad, que definen el espacio de programas que se ajustan al paradigma. Estas condiciones de salubridad generalmente se expresan como transformadores monotónicos de predicados idempotentes .

El refinamiento de un 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 el cierre universal de todas las variables en el alfabeto.

Relaciones

La teoría UTP más básica es el cálculo del predicado 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 solo en:

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

Algunas construcciones de lenguaje comunes se pueden definir en la teoría de las relaciones de la siguiente manera:

• La declaración de omisión, 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 mantener 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 solo 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 usando 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 ${\displaystyle \mu \mathbf {F} }$ de un transformador predicado monotónico ${\displaystyle \mathbf {F} }$ :

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

Referencias

1. Hoare, C. A. R.; Jifeng, He (1 de abril de 1998). Unifying Theories of Programming. Prentice Hall College Division. p. 320. ISBN 978-0-13-458761-5. Consultado el 17 de septiembre de 2014. 

Otras lecturas

• Jim Woodcock y Ana Cavalcanti. Una introducción tutorial a los diseños con UTP. En Integrated Formal Methods, volumen 2999 de Lecture Notes in Computer Science, páginas 40–66. Springer Berlin / Heidelberg, 2004. ISBN 978-3-540-21377-2. doi 10.1007/978-3-540-24756-2_4   paper
• Ana Cavalcanti y Jim Woodcock. Una introducción tutorial a CSP en UTP. En Refinement Techniques in Software Engineering, volumen 3167 de Lecture Notes in Computer Science, páginas 220–268. Springer Berlin / Heidelberg, 2006. doi 10.1007/11889229_6   paper

Enlaces externos

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