Abstracting Interference in PostconditionsrnDiego Dias, Leo Freitas and Cliff Jones

摘要

Specification of concurrent processes in rely-guarantee may require a postconditionrnof a process to account for changes made by the environment on the shared state. Thisrnleads to complicate postconditions, and distracts the designer from specifying thernchanges the process should make on the program state. We found that, when used inrnpostconditions, the notion of possible values shifts the designer's perspective from arnglobal view of the parallelism to a local view of it. This enhances the separation ofrnconcerns between the rely and the postcondition and may reduce the gap between arnsequential and a concurrent version of the same process. In view of this finding, thisrndocument is concerned with a preliminary investigation of a semantics for possiblernvalues, and the consequence on the proof obligations.