A Formal Reference for SCOOP - Empirical Software Engineering and Verification - page 89

formalization of the operational behavior of SCOOP, specified by a structural opera-
tional semantics. The main contributions of the paper are:

- A formal specification of SCOOP that treats all important language elements.
- Clarification and correction of the informal specification in [25].

This work does not provide a formal completeness and soundness proof with respect
to an axiomatic semantics. Sec. 6 discusses this possibility as part of future work. This
work focuses on a formal reference for a concurrent programming language. We argue
that this formal reference reflects and corrects the informal description by following a
systematic approach.
This article is a condensed version of our technical report [24] on the same subject.
This paper is structured as follows. The remainder of this introduction gives a brief
overview of the main ideas of the SCOOP model to provide a basic intuition for the main
part of the paper. Sec. 2 gives an overview of related work. Sec. 3 gives an overview
of the considered language. The two following chapters contain the main parts of the
formalization: Sec. 4 describes the state formalization and Sec. 5 the formalization of
computations. Sec. 6 concludes and discusses future applications of the formalization.

1.1 An Informal Overview of SCOOP

The starting idea of SCOOP is that every object is associated for its lifetime with a
processor, called its handler .A processor is an autonomous thread of control capable
of executing actions (features) on objects. A processor can be a hardware CPU, but
it can also be implemented in software, for example as a process or as a thread; any
mechanism that can execute instructions sequentially is suitable as a processor.
A reference variable belonging to a processor (for example, a field of an object han-
dled by that processor) can point to an object with the same handler, or to an object on
another processor. In the second case the reference is said to be separate . The semantics
of a call x . f depends on this distinction: if x is not separate (as always in sequential pro-
gramming), the call is synchronous; if x is separate, meaning that it points to an object
handled by a different processor, that processor will execute the call asynchronously.
This possibility of asynchronous calls is the main source of concurrent execution.
The producer-consumer problem serves as a simple illustration of these ideas. A root
class defines the entities producer and consumer . The keyword separate specifies that
these entities may be handled by a processor different from the current one. A creation
instruction on a separate entity such as producer and consumer will create an object on
another processor; by default the instruction also creates that processor.

producer : separate PRODUCER
−− The producer.

consumer : separate CONSUMER
−−

The consumer.