Up to this point, the semantics of the commands is determined by the relation between precondition and postcondition. This point of view is too restricted for the treatment of concurrent programs and reactive systems. The usual example is that of an operating system which is supposed to perform useful tasks without ever reaching a postcondition.

For this purpose, the semantics of commands must be extended by consideration of conditions at certain moments during execution. We do not want to be forced to consider all intermediate states or to formalize sequences of intermediate states. We have chosen the following level of abstraction. To every procedure name h, a predicate z.h is associated. The temporal semantic properties of a command q depend on the values of z.h.x for the procedure calls, say of procedure h in state x, induced by execution of command q. The main properties are ‘always’ and ‘eventually’, which are distinguished by the question whether z.h.x should hold for all induced calls or for at least one induced call. The concept of ‘always’ is related to stability and safety. The concept of ‘eventually’ is related to progress and liveness.

In this chapter, we regard nontermination of simple commands as malfunctioning and nontermination of procedures as potentially useful infinite behaviour. We therefore use wp for the interpretation of simple commands and wlp for procedure calls.