the underlying logic: it is thus a pure expression, totally defined, terminating and without side effect. version 1: version 2: Provided that E is well defined, we just apply the so-called one-point rule on version 1. Then The first version avoids a potential duplication of x in R, whereas the second version is simpler when there is at most a single occurrence of x in R. The first version also reveals a deep duality between weakest-precondition and strongest-postcondition (see below). An example of a valid calculation of wp (using version 2) for assignments with integer valued variable x is: This means that in order for the postcondition x > 10 to be true after the assignment, the precondition x > 15 must be true before the assignment. This is also the "weakest precondition", in that it is the "weakest" restriction on the value of x which makes x > 10 true after the assignment. Sequence For example, Conditional As example: While loop Partial Correctness Ignoring termination for a moment, we can define the rule for the weakest liberal precondition, denoted wlp, using a predicate INV, called the loop invariant, typically supplied by the programmer: Total Correctness To show total correctness, we also have to show that the loop terminates. For this we define a well-founded relation on the state space denoted as (wfs, <) and define a variant function vf , such that we have: Informally, in the above conjunction of three formulas: the first one means that the variant must be part of the well-founded relation before entering the loop; the second one means that the body of the loop (i.e. statement S) must preserve the invariant and reduce the variant; the last one means that the loop postcondition R must be established when the loop finishes. However, the conjunction of those three is not a necessary condition. Exactly, we have Non-deterministic guarded commands Actually, Dijkstra's Guarded Command Language (GCL) is an extension of the simple imperative language given until here with non-deterministic statements. Indeed, GCL aims to be a formal notation to define algorithms. Non-deterministic statements represent choices left to the actual implementation (in an effective programming language): properties proved on non-deterministic statements are ensured for all possible choices of implementation. In other words, weakest-preconditions of non-deterministic statements ensure that there exists a terminating execution (e.g. there exists an implementation), and, that the final state of all terminating