<- 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




 
Weakest Precondition
The condition that characterizes the set of all initial states, such that activation will certainly result in a properly terminating happening leaving the system in a final state satisfying a given post-condition, is called "the weakest pre-condition corresponding to that post-condition". (We call it "weakest", because the weaker a condition, the more states satisfy it and we aim here at characterizing all possible starting states that are certain to lead to a desired final state.) If the system (machine, mechanism) is denoted by "S" and the desired post-condition by "R", then we denote the corresponding weakest pre-condition by wp(S,R). [Source: A discipline of programming, Edsger Wybe Dijkstra] [Edsger Wybe Dijkstra and Carol S. Scholten, Predicate Calculus and Program Semantics, Text and Monographs in Computer Science, Springer-Verlag, 1990]
 

 

<- People Behind Informatics


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