A concurrent wide-spectrum language combines a concurrent programming language with specification constructs. Colvin et al. provide a unified framework for defining the semantics of such languages. The semantics is trace-based and captures program and environment behavior.

The authors first introduce the trace model. For this model, program combinators, like sequential and parallel composition and iteration, are presented. A weak conjunction is introduced that synchronizes on non-aborting steps and aborts if one of the conjuncts aborts. Building on primitives and the combinators, the authors present a wide-spectrum language and discuss how rely and guarantee constructs as well as temporal logic specifications can be represented.

The rather theoretical focus of the paper is on the semantics framework. It is well written, and precise definitions are provided, well explained, and illustrated by helpful examples. Other current approaches are discussed and compared. Although no in-depth knowledge of the field is required, the reader should feel comfortable with formal notation.