Designing a semantic model for a wide-spectrum language with concurrency

Colvin, Robert J., Hayes, Ian J. and Meinicke, Larissa A. (2017) Designing a semantic model for a wide-spectrum language with concurrency. Formal Aspects of Computing, 1-23. doi:10.1007/s00165-017-0416-4


Author Colvin, Robert J.
Hayes, Ian J.
Meinicke, Larissa A.
Title Designing a semantic model for a wide-spectrum language with concurrency
Journal name Formal Aspects of Computing   Check publisher's open access policy
ISSN 1433-299X
0934-5043
Publication date 2017-02-27
Sub-type Article (original research)
DOI 10.1007/s00165-017-0416-4
Open Access Status Not yet assessed
Start page 1
End page 23
Total pages 23
Place of publication London, United Kingdom
Publisher Springer U K
Collection year 2018
Language eng
Formatted abstract
A wide-spectrum language integrates specification constructs into a programming language in a manner that treats a specification command just like any other command. The primary contribution of this paper is a semantic model for a wide-spectrum language that supports concurrency and a refinement calculus. A distinguishing feature of the language is that steps of the environment are modelled explicitly, alongside steps of the program. From these two types of steps a rich set of specification commands can be constructed, based on operators for nondeterministic choice, and sequential and parallel composition. We also introduce a novel operator, weak conjunction, which is used extensively to conjoin separate aspects of specifications, allowing us to take a separation-of-concerns approach to subsequent reasoning. We provide a denotational semantics for the language based on traces, which may be terminating, aborting, infeasible, or infinite. To demonstrate the generality and unifying strength of the language, we use it to express a range of concepts from the concurrency literature, including: a refinement theory for rely/guarantee reasoning; an abstract specification of local variables in a concurrent context; specification of an abstract, linearisable data structure; a partial encoding of temporal logic; and defining the relationships between notions of nonblocking programs. The novelty of the paper is that these diverse concepts build on the same theory. In particular, the rely concept from Jones’ rely/guarantee framework, and a stronger demand concept that restricts the environment, are reused across the different domains to express assumptions about the environment. The language and model form an instance of an abstract concurrent program algebra, and this facilitates reasoning about properties of the model at a high level of abstraction.
Keyword Concurrency
Program algebra
Refinement calculus
Rely-guarantee
Wide-spectrum language
Q-Index Code C1
Q-Index Status Provisional Code
Institutional Status UQ

Document type: Journal Article
Sub-type: Article (original research)
Collections: HERDC Pre-Audit
School of Information Technology and Electrical Engineering Publications
 
Versions
Version Filter Type
Citation counts: Scopus Citation Count Cited 0 times in Scopus Article
Google Scholar Search Google Scholar
Created: Tue, 14 Mar 2017, 00:24:17 EST by System User on behalf of Learning and Research Services (UQ Library)