Notes on Proof Outline Logic
Schneider, Fred B.
Formulas of Proof Outline Logic are program texts annotated with assertions. Assertions may contain control predicates as well as terms whose values depend on previous states, making the assertion language rather expressive. The logic is complete for proving safety properties of concurrent programs. A deductive system for the logic is presented. Solutions to the mutual exclusion and readers/writers problems illustrate how the logic can be used as a tool for program development.
computer science; technical report
Previously Published As