NASA NTRS · 19910018471
Derivation of sequential, real-time, process-control programs
Abstract
The use of weakest-precondition predicate transformers 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 exists during program transitions.
Keep this discovery
Explore connections, maps & timelines
Marzullo, Keith, Schneider, Fred B., Budhiraja, Navin. 1991-07-01. Derivation of sequential, real-time, process-control programs. https://ntrs.nasa.gov/citations/19910018471
Cite the original work for its findings. Save a collection to share your selection of sources.