Browse by author
Lookup NU author(s): Diego Machado Dias, Dr Leo Freitas, Emeritus Professor Cliff JonesORCiD
This is the final published version of a report that has been published in its final definitive form by School of Computing Science, University of Newcastle upon Tyne, 2014.
For re-use rights please refer to the publisher's terms and conditions.
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.
Author(s): Dias D, Freitas L, Jones C
Publication type: Report
Publication status: Published
Series Title: School of Computing Science Technical Report Series
Year: 2014
Pages: 15
Print publication date: 01/03/2014
Source Publication Date: March 2014
Report Number: 1415
Institution: School of Computing Science, University of Newcastle upon Tyne
Place Published: Newcastle upon Tyne
URL: http://www.cs.ncl.ac.uk/publications/trs/papers/1415.pdf
