Predicate calculus. Program semantics of guarded commands. Postconditions
and specifications. Weakest preconditions. Weakest liberal preconditions. Loop
invariants. Termination and non-termination. Partial and total functions. Non-
determinacy. Standard techniques in program derivation. Examples of program
derivation.​