Information Technology Reference
In-Depth Information
local
produced item
:
INTEGER
do
produced item
:=
new item
buffer
.
put
(
produced item
)
end
The asynchronous nature of separate calls such as
buffer
.
put
(
x
) implies a distinction
between the notion of
feature call
and
feature application
. In sequential programming,
executing a call means executing the corresponding feature immediately. With asyn-
chronous calls, the client processor logs the call with the supplier processor (feature
call) and moves on. Only at some later time will the supplier processor actually execute
the body (feature application).
The main part of the paper defines formally the implementation that gives rise to the
behavior outlined above. It also introduces advanced concepts and additional language
elements, which cannot be covered in a brief overview, and shows how these give rise
to a complexity which can only be dealt with satisfactorily with a formal specification.
2
Related Work
The discussion is divided into work on SCOOP and work on other languages.
2.1
Approaches for SCOOP
In his dissertation, Nienaltowski [25] worked out the details of an implementation of
SCOOP as suggested by Meyer [21], and provided a prototype implementation. The
language semantics is described informally only, with the exception of the type system
which is defined using an inference system. The informal description and the prototype
contain various ambiguities and omissions, which we are able to clarify.
Torshizi et al. [33] have defined and implemented JSCOOP, a version of the SCOOP
model for the Java language. Only the most important language elements are consid-
ered, and no attempt at formalization is made. In contrast, our specification and imple-
mentation [31] on top of Eiffel considers all language elements. We believe that our
specification could help to extend JSCOOP to a full treatment of the language concepts.
Brooke, Paige and Jacob [5] have used CSP [13] to give a semantics to SCOOP as
described by Meyer [21]. Their initial hope was to use tools for analyzing CSP speci-
fications, such as FDR, to automatically check for deadlock in SCOOP programs, but
found the size of the specification prohibitive. A benefit of their approach is that CSP
provides the machinery needed to express concurrency and synchronization, leading to
a relatively concise model. Our goal is to provide formal descriptions close to an actual
implementation, and therefore prefer to design an own operational semantics, rather
than going through the indirection of another process algebra.
Structural operational semantics, introduced by Plotkin [29], is a flavor of operational
semantics that has been used with great success to define various concurrent systems.
Our specification uses this style of semantics as well. To model SCOOP we also make
Search WWH ::
Custom Search