Semántica de transformación de predicados

La semántica de transformación de predicados es una extensión de Lógica de Floyd-Hoare ideada por Edsger Dijkstra y extendida y refinada por otros investigadores. Esta extensión fue presentada por Dijkstra en sus artículos titulados "Guarded commands, nondeterminacy and formal derivation of programs" ("Comandos guardados, no-determinismo y derivación formal de programas"). Consiste en un método para definir la semántica de un lenguaje de programación imperativa mediante la asignación a cada comando del correspondiente transformador de predicados. Un transformador de predicados es una función total entre dos predicados del conjunto de estados de un programa.

El transformador de predicados canónico de la programación imperativa secuencial es el conocido normalmente como "weakest precondition" (precondición más débil) wp(S,R). Aquí S denota una secuencia de comandos y R un predicada llamado "postcondición". El resultado de su aplicación es la "precondición más débil" para que S termine de modo que R sea cierto. Un ejemplo es la siguiente definición de la sentencia de asignación:

$wp(x := E, R)\ =\ R_E^x$

De esta operación resulta un predicado que es una copia de R pero con el valor E asignado a la variable x.

Un ejemplo de un cálculo válido de un wp para una asignación de variables enteras x e y es:

$wp(x := y - 5, x > 10)\ =\ (y - 5 > 10)\ =\ (y > 15)$

Esto significa que para que la "postcondición" x > 10 sea cierta tras la asignación, la "precondición" y > 15 debe ser cierta antes de la asignación. Esto también es la "precondición más débil", en tanto en cuanto es la restricción "más débil" que hay aplicar al valor de y para que x > 10 sea cierto tras la asignación.

Dijkstra también definió construcciones de este tipo para las estructuras alternativa (if) y repetitiva (do) así como un operador de composición (;) utilizando wp. Las construcciones alternativa y repetitiva usan comandos guardados para influir en la ejecución. A causa de las reglas impuestas por él en la definición de wp, ambas construcciones permiten ejecuciones no-deterministas si los guardianes de los comandos no son disjuntos.

A diferencia de otros formalismos semánticos, la semántica de transformación de predicados no fue fruto de la investigación realizada en centros de computación. Más bien fue creada con la intención de proveer a los programadores una metodología de desarrollo de programas "correctamente construidos" basada en un "estilo matemático".

Aunque es el más común y más comentado por su relevancia en la programación secuencial, la "precondición más débil" no es el único transformador de predicados existente. Por ejemplo, Leslie Lamport ha propuesto win y sin como transformadores de predicados a utilizar en la programación concurrente.

Referencias

• Edsger Dijkstra, "Guarded commands, nondeterminacy and formal derivation of programs". Communications of the ACM, 18(8):453–457, August 1975. [1]
• Leslie Lamport, "win and sin: Predicate Transformers for Concurrency". ACM Transactions on Programming Languages and Systems, 12(3), July 1990. [2]
• Ralph-Johan Back and Joakim von Wright, Refinement Calculus: A Systematic Introduction, 1st edition, 1998. ISBN 0-387-98417-8.
• Edsger W. Dijkstra. A Discipline of Programming (A systematic introduction with examples). ISBN 0-613-92411-8.