Derivation of Sequential, Real-Time, Process-Control Programs

The use of weakest-precondition predicate tranformers in the derivation of sequential, process-control software is discussed. Only one extension to Dijkstra's calculus for deriving ordinary sequential programs was found to be necessary: function-valued auxiliary variables. These auxiliary variables are needed for reasoning about states of a physical process that exist during program transitions