Notes on Proof Outline Logic

Abstract

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.