A Method for the Development of Totally Correct Shared-State Parallel Programs

Abstract. 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 awaitconstructs. The system is called LSP (Logic of Speci ed Programs) and can be seen of as an extension of Jones' rely/guarantee method. His method is strengthened in two respects: { Speci cations 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 speci cation tool to eliminate undesirable implementations or as a veri cation tool to prove that a certain program satis es a ...

• Type: Conference
• Year: 1991
• Where: CONCUR
• Authors: Ketil Stølen
• Keywords: Auxiliary Variables, CONCUR 1991, Distributed And Parallel Computing, Programming Language, Speci Cation