Issue No. 02 - March (1977 vol. 3)
L. Lamport , Massachusetts Computer Associates, Inc.
The inductive assertion method is generalized to permit formal, machine-verifiable proofs of correctness for multiprocess programs. Individual processes are represented by ordinary flowcharts, and no special synchronization mechanisms are assumed, so the method can be applied to a large class of multiprocess programs. A correctness proof can be designed together with the program by a hierarchical process of stepwise refinement, making the method practical for larger programs. The resulting proofs tend to be natural formalizations of the informal proofs that are now used.
synchronization, Assertions, concufrent programming, correctness, multiprocessing
L. Lamport, "Proving the Correctness of Multiprocess Programs," in IEEE Transactions on Software Engineering, vol. 3, no. , pp. 125-143, 1977.