Predicate transformer semantics is an extension of Floyd-Hoare Logic invented by Dijkstra and extended and refined by other researchers. It was first introduced in Dijkstra's paper "Guarded commands, nondeterminacy and formal derivation of programs". It is a method for defining the semantics of an imperative programming language by assigning to each command in the language a corresponding predicate transformer.

PropertyValue
dbpprop:abstract
  • Predicate transformer semantics is an extension of Floyd-Hoare Logic invented by Dijkstra and extended and refined by other researchers. It was first introduced in Dijkstra's paper "Guarded commands, nondeterminacy and formal derivation of programs". It is a method for defining the semantics of an imperative programming language by assigning to each command in the language a corresponding predicate transformer. A predicate transformer is a total function mapping between two predicates on the state space of a program. The canonical predicate transformer of sequential imperative programming is the so-called "weakest precondition" <math>wp(S, R)</math>. Here S denotes a list of commands and R denotes a predicate on the space, called the "postcondition". The result of applying this function gives the "weakest pre-condition" for S terminating with R true. An example is the following definition of the assignment statement: <math> wp\ =\ R_E^x </math> This gives a predicate that is a copy of R with the value of x replaced by E. An example of a valid calculation of wp for assignments with integer valued variables x and y is: <math> wp\ =\ (y - 5 > 10)\ =\ (y > 15) </math> This means that in order for the "post-condition" x > 10 to be true after the assignment, the "pre-condition" y > 15 must be true before the assignment. This is also the "weakest pre-condition", in that it is the "weakest" restriction on the value of y which makes x > 10 true after the assignment. Dijkstra also defined alternative (if) and repetitive (do) constructs as well as a composition operator using wp. The alternative and repetitive constructs used guarded commands to influence execution. Because of the rules he imposed on the definition of wp, both constructs allow for non-deterministic execution if the guards in the commands are non disjoint. Unlike many other semantic formalisms, predicate transformer semantics was not designed as an investigation into foundations of computation. Rather, it is intended to provide programmers with a methodology to develop their programs as "correct by construction" in a "calculational style". This style was advocated by Dijkstra and others, and also developed further in a higher order logic setting by R. -J. Back in the Refinement Calculus. Although the most common and most widely discussed because of their relevance to sequential programming, "weakest pre-conditions" are not the only predicate transformers. For example, Leslie Lamport has suggested win and sin as predicate transformers for concurrent programming.
  • Der wp-Kalkül ist ein Kalkül in der Informatik zur Verifikation eines imperativen Programmcodes. Die Abkürzung wp steht für weakest precondition, auf deutsch schwächste Vorbedingung. Die Überprüfung der Korrektheit geschieht durch Rückwärtsanalyse des Programmcodes. Ausgehend von der Nachbedingung wird geprüft, ob diese durch die Vorbedingung und den Programmcode garantiert wird. Alternativ kann auch der Hoare-Kalkül benutzt werden, bei dem im Gegensatz zum wp-Kalkül eine Vorwärtsanalyse stattfindet.
  • 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) <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\ =\ 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\ =\ (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 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.
  • 述語変換意味論（じゅつごへんかんいみろん、Predicate Transformer Semantics）は、エドガー・ダイクストラによるホーア論理の拡張であり、その後も他の研究者が改良を加えたものである。最初に登場したのはダイクストラの論文 "Guarded commands, nondeterminacy and formal derivation of programs" であった。
dbpprop:hasPhotoCollection
rdf:type
rdfs:comment
  • Predicate transformer semantics is an extension of Floyd-Hoare Logic invented by Dijkstra and extended and refined by other researchers. It was first introduced in Dijkstra's paper "Guarded commands, nondeterminacy and formal derivation of programs". It is a method for defining the semantics of an imperative programming language by assigning to each command in the language a corresponding predicate transformer.
  • Der wp-Kalkül ist ein Kalkül in der Informatik zur Verifikation eines imperativen Programmcodes. Die Abkürzung wp steht für weakest precondition, auf deutsch schwächste Vorbedingung. Die Überprüfung der Korrektheit geschieht durch Rückwärtsanalyse des Programmcodes. Ausgehend von der Nachbedingung wird geprüft, ob diese durch die Vorbedingung und den Programmcode garantiert wird.
  • 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").
  • 述語変換意味論（じゅつごへんかんいみろん、Predicate Transformer Semantics）は、エドガー・ダイクストラによるホーア論理の拡張であり、その後も他の研究者が改良を加えたものである。最初に登場したのはダイクストラの論文 "Guarded commands, nondeterminacy and formal derivation of programs" であった。
rdfs:label
  • Predicate transformer semantics
  • Wp-Kalkül
  • Semántica de transformación de predicados
  • 述語変換意味論
owl:sameAs
skos:subject
foaf:page
is dbpprop:redirect of
is owl:sameAs of