Abstracting Interference in Postconditions
Diego Machado Dias, Leo Freitas, Cliff B. Jones · 2014
Specification of concurrent processes in rely-guarantee may require a postcondition of a process to account for changes made by the environment on the shared state. This leads to complicate postconditions, and distracts the designer from specifying the changes the process should make on the program state. We found that, when used in postconditions, the notion of possible values shifts the designer's perspective from a global view of the parallelism to a local view of it. This enhances the separation of concerns between the rely and the postcondition and may reduce the gap between a sequential and a concurrent version of the same process. In view of this finding, this document is concerned with a preliminary investigation of a semantics for possible values, and the consequence on the proof obligations.