Derivation of Sequential, Real-Time, Process-Control Programs
CORNELL UNIV ITHACA NY DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
The use of weakest precondition predicate transformers in the derivation of sequential, process control software is discussed. Only one extension to Dijkstras 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 Programming and Software