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) . 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:
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:
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.
Datos:Q291929
Agosto 10, 2021
semántica, transformación, predicados, semántica, transformación, predicados, extensión, lógica, floyd, hoare, ideada, edsger, dijkstra, extendida, refinada, otros, investigadores, esta, extensión, presentada, dijkstra, artículos, titulados, guarded, commands,. La semantica de transformacion de predicados es una extension de Logica de Floyd Hoare ideada por Edsger Dijkstra y extendida y refinada por otros investigadores Esta extension fue presentada por Dijkstra en sus articulos titulados Guarded commands nondeterminacy and formal derivation of programs Comandos guardados no determinismo y derivacion formal de programas Consiste en un metodo para definir la semantica de un lenguaje de programacion imperativa mediante la asignacion a cada comando del correspondiente transformador de predicados Un transformador de predicados es una funcion total entre dos predicados del conjunto de estados de un programa El transformador de predicados canonico de la programacion imperativa secuencial es el conocido normalmente como weakest precondition precondicion mas debil w p S R displaystyle wp S R Aqui S denota una secuencia de comandos y R un predicada llamado postcondicion El resultado de su aplicacion es la precondicion mas debil para que S termine de modo que R sea cierto Un ejemplo es la siguiente definicion de la sentencia de asignacion w p x E R R E x displaystyle wp x E R R E x De esta operacion resulta un predicado que es una copia de R pero con el valor E asignado a la variable x Un ejemplo de un calculo valido de un wp para una asignacion de variables enteras x e y es w p x y 5 x gt 10 y 5 gt 10 y gt 15 displaystyle wp x y 5 x gt 10 y 5 gt 10 y gt 15 Esto significa que para que la postcondicion x gt 10 sea cierta tras la asignacion la precondicion y gt 15 debe ser cierta antes de la asignacion Esto tambien es la precondicion mas debil en tanto en cuanto es la restriccion mas debil que hay aplicar al valor de y para que x gt 10 sea cierto tras la asignacion Dijkstra tambien definio construcciones de este tipo para las estructuras alternativa if y repetitiva do asi como un operador de composicion utilizando wp Las construcciones alternativa y repetitiva usan comandos guardados para influir en la ejecucion A causa de las reglas impuestas por el en la definicion de wp ambas construcciones permiten ejecuciones no deterministas si los guardianes de los comandos no son disjuntos A diferencia de otros formalismos semanticos la semantica de transformacion de predicados no fue fruto de la investigacion realizada en centros de computacion Mas bien fue creada con la intencion de proveer a los programadores una metodologia de desarrollo de programas correctamente construidos basada en un estilo matematico Aunque es el mas comun y mas comentado por su relevancia en la programacion secuencial la precondicion mas debil no es el unico transformador de predicados existente Por ejemplo Leslie Lamport ha propuesto win y sin como transformadores de predicados a utilizar en la programacion concurrente Referencias EditarEdsger 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 Datos Q291929Obtenido de https es wikipedia org w index php title Semantica de transformacion de predicados amp oldid 123617774, wikipedia, wiki, leyendo, leer, libro, biblioteca,
