Information Technology Reference
In-Depth Information
Regarding semantics, an Alloy model defines valid states for a given system
- interpretations [16] - that contain mappings of signatures and relation names
to sets of object values . Object values may be single objects for sets and pairs of
objects for relations. We consider the semantics of an object model in Alloy as
the set of all valid interpretations satisfying all modeled invariants. Each of these
interpretations consists of all valid assignments of values to signatures and the
relation names. All modeled invariants - implicit or explicit [16] - are satisfied.
Invariants are implicit when they constrain the model but are not declared in
facts, such as implicit constraints from extends .
For programs, states are formalized as heaps of object values, mapping class
names to sets of objects and field names to pairs of object values (references). If
an object in a heap contains a field storing a null value, no pair of values exists
with that object as the first member. The semantics of a program is given by the
set of sequences of heaps resulting from all possible execution traces - depending
on the possible program inputs.
It would be straightforward to consider all heaps from every execution trace;
however, this approach does not truly reflect the real intentions of consistency
checking, since some heaps may be acceptably invalid at some well-defined points
of the program. We adopt a specification methodology by Barnett et al. [25],
in which every object is added a special validity field .Ifthisfieldhasatrue
value, the invariants over its state should hold, and consistency checking is only
performed when all objects are valid. This field can only be modified through the
use of two special statements, unpack and pack . The command unpack obj
sets the field to false, while pack obj does the opposite.
Our semantic consistency regards solely valid heaps (which we call heaps of
interest ). A program is in semantic consistency with a model if, and only if, it
is in syntactic consistency, and, for every valid heap from its execution, there is
a corresponding interpretation from the semantics of the model.
3.3 Examples of Synchronizers
For each applied Alloy law, two synchronizers are defined. In this paper we show
two synchronizers associated with Law 1: introduce and remove subclass. We
define synchronizers in a notation for refinement tactics , based on the Angel
language [26]. Angel constructs are appropriate for describing law applications,
with the needed arguments. Tactics may be a simple law applications, with the
law name with arguments. A law application may have two possible outcomes:
if all provisos are satisfied, then program is transformed. Otherwise, the appli-
cation of the law fails. For instance, law newSuperclass ( U, X,→
) applies Law
A( new superclass ) to the program, with three arguments: the superclass ( U ),
the subclass ( X ) and the application direction (
: from L-R). A special atomic
tactic, skip , always succeeds, leaving the program unchanged.
In order to sequentially composing two tactics, the t 1 ; t 2 construct can be
used. Similarly, tactics combined in alternation have the form ( t 1 |t 2 ). First, t 1 is
 
Search WWH ::




Custom Search