<- People Behind Informatics


All 0-9 A B C D E F G H I J K L M N O P Q R S T U V W XY Z




 
Predicate Transformers
Predicate transformer semantics is a way to use verification technology to define programming languages. Each statement in a language is characterized by the way it transforms preconditions to postconditions. Dijkstra and his followers have even advocated the direct use of predicate transformers, such as the weakest precondition transformer (wp), in program development; the argument is that such predicate transformers aid calculational proofs. The semantics of a repetitive construct can be defined in terms of a recurrence relation between predicates, whereas the semantic definition of general recursion requires a recurrence relation between predicate transformers. For a fixed mechanism S such a rule, which is fed with the predicate R denoting the post-condition and delivers a predicate wp(S,R) denoting the corresponding weakest precondition, is called "a predicate transformer". When we ask for the definition of the semantics of the mechanism S, what we really ask for is its corresponding predicate transformer. [Sources: A discipline of programming, Edsger Wybe Dijkstra; http://www.cs.iastate.edu/~leavens/ComS641-Hesselink.html]
 

 

<- People Behind Informatics


Home  |  Top  |  Search  |  Gallery  | Glossary  | Sitemap  |  Making Of  |  Help