Ver el código de «Semántica de transformación de predicados»

La '''semántica de transformación de predicados''' es una extensión de [[Lógica de Hoare|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 [[Programación imperativa|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 ''[[aserción (programación)|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''') <math>wp(S, R)</math>. 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:

:<math> wp(x := E, R)\ =\ R_E^x </math>

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:

:<math> wp(x := y - 5, x > 10)\ =\ (y - 5 > 10)\ =\ (y > 15) </math>

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 ''[[guardián (programación)|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. [http://doi.acm.org/10.1145/360933.360975]
* [[Leslie Lamport]], "''win'' and ''sin'': Predicate Transformers for Concurrency". ''[[Association for Computing Machinery|ACM]] Transactions on Programming Languages and Systems'', 12(3), July 1990. [http://research.microsoft.com/users/lamport/pubs/pubs.html#lamport-win]
* [[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.

{{Control de autoridades}}
[[Categoría:Programación imperativa]]
[[Categoría:Métodos formales]]
[[Categoría:Edsger Dijkstra]]