Correctness of recursive parallel nondeterministic flow programs

摘要

This paper presents a method for proving the partial correctness of programs with the following features: strongly typed expressions with call-by-value semantics for variables; iteration; recursive procedures with call-by-name semantics; nondeterminism; parallel assignment; and good old fashioned go-to's. An operational semantics is given to a program by viewing it as a program scheme together with an appropriate interpretation in a given model. Program schemes are viewed as diagrams in an algebraic theory, and the given models are relational algebras of this theory. A simple programming language, REPNOD, that embodies exactly the features that are discussed theoretically is defined, and several simple REPNOD programs, as well as a sample correctness proof, are given. This approach seems to provide a particularly simple framework for many problems in concurrent programming.