Proving assertions about parallel programs

摘要

A simple but general parallel programming language is considered. The semantics of programs is defined in a concise and natural way using relations. “Verification conditions” derived from the semantic definitions enable Floyd's method of proving correctness to be applied to the parallel programs. Proofs of properties of programs using the verification conditions are claimed to be more systematic versions of the informal arguments normally used to check parallel programs. A program simulating an elementary airline reservation system is given, and several properties of the program are demonstrated using the technique.