Derivation of Sequential, Real-Time, Process-Control Programs
Marzullo, Keith; Schneider, Fred B.; Budhiraja, Navin
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.
computer science; technical report
Previously Published As