An attempt to reason about shared-state concurrency in the style of VDM

The paper presents an attempt to develop a totally correct shared-state parallel program in the style of VDM. Programs are specified by tuples of five assertions (P,R, W, G, E). The pre-condition P, the rely-condition R and the wait-condition Wdescribe assumptions about he environment, while the guar-condition G and the eft-condition E characterise commitments to the implementation. The pre-, rely- and guar-conditions are closely related to the similarly named conditions in Jones' rely/guarantee m thod, while the elf-condition corresponds towhat Jones calls the post-condition. The wait-condition is supposed to characterise the set of states in which it is safe for the implementation to be blocked; in other words, the set of states in which the implementation, when it becomes blocked, eventually will be released by the environment. The implementation is ot allowed to be blocked uring the execution of an atomic statement. Auxiliary variables are introduced to increase the expressiveness. They are used both as a specification tool; to characterise a program that has not yet been implemented, and as a verification tool; to show that a given algorithm satisfies a specific property. However, although it is possible to define history-variables in this approach, 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.