State space: In this book, the state space is regarded as being built up as a Cartesian product, and the states is the points.

Predicate is the formal expression of condition. Each predicate is assumed to be defined in each point of the state space. Given a point, the value of a predicate is either “True” or “False”. Therefore, the predicate characterize the set of all points where the predicate is true. Two predicates P = Q , when they characterize the same set of states.

T is the predicate that is true in all points of the state space. F is the predicate that is false in all points of the state space.


Deterministic machines: the happening that will take place upon activation of the mechanism is fully determined by its initial state.

Nondeterministic machines: activation in a given initial state will give rise to one out of a class of possible happenings, the initial state only fixing the class as a whole.

Post-condition: In computer programming, a post-condition is a condition or predicate that must always be true just after the execution of some section of code or after an operation in a formal specification. via wiki

Weakest pre-condition corresponding to that post-condition: 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. If the system is denoted by S and the desired post-condition by R, then we denote the corresponding weakest pre-condition by wp(S, R)

A predicate transformer: For a fixed mechanism S such a rule, which is fed with the post-condition R and delivers the corresponding weakest pre-condition wp(S, R), is called “a predicate transformer”.

Sufficient pre-condition: P is a sufficient pre-condition, denoted as P => wp(S, R), requires that wherever P is true, wp(S, R) is true as well.


A Discipline of Programming