A METHOD FOR THE DEVELOPMENT OF TOTALLY CORRECT SHARED-STATE PARALLEL PROGRAMS

A syntax-directed formal system for the development of totally correct programs with respect to an (unfair) shared-state parallel programming language is proposed. The programming language is basically a while-language extended with parallel- and await-constructs. The system is called LSP (Logic of Specified Programs) and can be seen of as an extension of Jones' rely/guarantee method. His method is strengthened in two respects: Specifications are extended with a wait-condition to allow for the development of programs whose correctness depends upon synchronisation. The wait-condition is supposed to characterise the states in which the implementation may become blocked. The implementation is not allowed to become blocked inside the body of an await-statement. Auxiliary variables are introduced to increase expressiveness. They are either used as a specification tool to eliminate undesirable implementations or as a verification tool to prove that a certain program satisfies a particular specification. Although it is possible to define history variables in LSP, the auxiliary variables may be of any type, and it is up to the user to define the auxiliary structure he prefers. Moreover, the auxiliary structure is only a part of the logic. This means that auxiliary variables do not have to be implemented as if they were ordinary programming variables.