In addition, one must establish the relationships between the object classes constituting the system and delineate the facilities the system offers to the user. Such facilities are usually derived from a requirements document and may be formally specified in terms of abstract operations on the system.
In this section we will look at the means we have available to express the properties of our object model, and we will study how we may employ abstract specifications of system operations to arrive at the integration of user actions and the object model underlying a system in a seamless way. The approach sketched may be characterized as event-centered.
In contrast, objects (in the more general sense) usually hide object and non-object data members, and instead provide a method interface. Moreover, object-oriented modeling focuses on behavioral properties, whereas semantic modeling has been more concerned with (non-behavioral) data types and (in the presence of inheritance) data subtypes.
Relations, as may be expressed in the entity-relationship model, can partly be expressed directly in terms of the mechanisms supported by object-oriented languages. For instance, the is-a relation corresponds closely (although not completely) with the inheritance relation. See slide 3-challenges. Both the has-a and uses relation is usually implemented by including (a pointer to) an object as a data member. Another important relation is the is-like relation, which may exist between objects that are neither related by the inheritance relation nor by the subtype relation, but yet have a similar interface and hence may be regarded as being of analogous types. The is-like relation may be enforced by parametrized types that require the presence of particular methods, such as a compare operator in the case of a generic list supporting a sort method.
Z
Change and invariance
Verification
In the following, an outline of
the specification language Z will be given.
More importantly, the specification
of a simple library system will be discussed,
illustrating how we may specify
user actions in an abstract way.
(The use of the Z specification language
is in this respect only of subsidiary
importance.)
In the subsequent section, we will look
at the realization of the library
employing an abstract system of objects
and events corresponding to the user
actions, which reflects the characterization
given in the formal specification.
The specification language Z is based on classical
(two-valued) logic and set theory.
It has been used in a number of industrial projects,
itself is a compound schema
that results from the logical conjunction of the schema
state and its primed version 
,
which denotes state after applying op.
Both schema inclusion and schema conjunction are
examples of the powerful schema calculus supported by Z,
which enables the user to specify complex systems
in Z.
Moreover, schemas may be decorated to
specify the effects of an operation.
Invariance may be specified
as in 
, which expresses that the
state before applying the operation
is the same as the state (denoted by 
)
after applying the operation.
Since schemas are specified in a logical manner,
both pre- and post-conditions are implicitly
specified by the constraints included in the schema.
Hence, to verify that an operation op is legal
for a state it is merely required to verify
that the conditions specified for state hold,
and that, together with the pre-conditions
(which are implicitly specified by the schema for op),
they imply the logical formula characterizing op.
See slide 10-model.
.
The operations Incr and Decr are specified
by defining the
state following the operation by,
respectively, 
and
.
Both operations require the declaration
to indicate that the
state specified by Counter will
be modified.
In addition, the operation Decr requires
as a pre-condition that 
,
needed to prevent the
violation of the invariant, which
would happen whenever n became less
than zero.
Z
which acts,
by convention, as an input parameter.
Similarly, the integer variable
declared for the operation value
acts, again by convention, as an output
parameter.
Since Z allows the inclusion of
other schemas in the declaration part
of a schema, we may easily mimic
inheritance as illustrated
in the specification of
, which is a Counter
with a maximum given by
an integer constant Max.
Similarly, we may specify the operations
for the 
by including
the corresponding operations
specified for the Counter, adding conditions
if required.
From a schema we may easily extract the pre-conditions for an operation by removing from the conditions the parts involving a primed variable. Clearly, the post-condition is then characterized by the conditions thus eliminated.
For example, the pre-condition of the
operation is 
, whereas
the post-condition is 
which corresponds to the implementation requirement
that the new value of the Counter
is the old value plus the value of the
argument 
.
In a similar way, the pre-condition
for applying the 
operation
is 
.
Note, however, that this pre-condition
is stronger than the original
pre-condition 
, hence to conform
with the rules for refinement
we must specify what happens when
as well.
This is left as an exercise for the reader.
Clearly, although Z lacks a notion
of objects or classes, it may conveniently
be employed to specify the behavior
of an object.
In
In contrast to Eiffel, which offers only
a semi-formal way in which to specify the behavior
of object classes, Z allows for
a precise formal specification of
the requirements a system must meet.
To have the specification reflect
the object structure of the system
more closely, one of the extensions
of Z mentioned above may be used.
An example of using (plain) Z
to specify the functionality
of a library system is given below.
The specification of a library
and a person 
,
the function 
is defined by extending borrowed
with the association between 
and 
,
which is expressed as
the mapping 
.
As a pre-condition for Borrow, we have that borrowed
must not be defined for 
, otherwise
some person would already have borrowed
the book 
.
The Return action may be considered
as the reverse of the Borrow action.
Its pre-condition states that borrowed
must be defined for 
and the result of the operation
is that the association between
and 
is removed from
.
Finally, the operation Has
allows us to query what books are in
the possession of a person 
.
The specification of Has employs
the mathematical features of Z
in a nice way.
The output, which is stored in
the output parameter 
,
consists of all the books related
to the person 
.
The set of books related to 
is obtained
by taking the relational image of the inversion
of borrowed for the singleton set
consisting of 
, that is,
each book x
for which
an association 
is in borrowed
is included in the set 
.
Again, it is not the notation that is important
here, but the fact that the specification defines
all top-level user interactions.
p = new person(); b = new book(); p = b->borrower; s = p->books; tf = b->inlibrary(); b->borrow(p); p->allocate(b); p->deallocate(b); b->_return(p);
For
class book {
public:
person* borrower;
book() {}
void borrow( person* p ) { borrower = p; }
void _return( person* p ) { borrower = 0; }
bool inlibrary() { return !borrower; }
};
class person {
public:
person() { books = new set(); }
void allocate( book* b ) { books->insert(b); }
void deallocate( book* b ) { books->remove(b); }
set* books;
};
book* Stroustrup = new book();example
book* ChandyMisra = new book(); book* Smalltalk80 = new book(); person* Hans = new person(); person* Cees = new person(); Stroustrup->borrow(Hans); Hans->allocate(Stroustrup); ChandyMisra->borrow(Cees); Cees->allocate(ChandyMisra); Smalltalk80->borrow(Cees); Cees->allocate(Smalltalk80);
Note that lending a book involves both the invocation of and . This could easily be simplified by extending the function and with the statements and respectively. However, I would rather take the opportunity to illustrate the use of events, providing a generic solution to the interaction problem noted.
class Event {
public:
virtual void operator()() = 0;
};
class Borrow : public Event {
public:
Borrow( person* _p, book* _b ) { _b = b; _p = p; }
void operator()() {
require( _b && _p ); _b and _p exist
_b->borrow(p);
_p->allocate(b);
}
private:
person* _p; book* _b;
};
The Borrow event class provides a controlled
way in which to effect the borrowing of a book.
In a similar way, a Return event class may be defined.
Events are primarily used
as intermediate between the user (interface)
and the objects comprising the library system.
For the application at hand, using events
may seem to be somewhat of an overkill.
However,
events not only give a precise characterization of
the interactions involved but, equally importantly,
allow for extending the repertoire
of interactions without disrupting
the structure of the application
simply by introducing additional event types.
class Return : public Event {
public:
Return( person* _p, book* _b ) { _b = b; _p = p; }
void operator()() {
require( _b && _p );
_b->_return(p);
_p->deallocate(b);
}
private:
person* _p; book* _b;
};
[4]
-
[up]
[top] -
[I]
[II]
[III]
[IV] -
[1]
[2]
[3]
[4]
[5]
[6]
[7]
[8]
[9]
[10]
[11]
[12] -
[A]
[R]
|
Hush Online Technology
hush@cs.vu.nl
12/29/99 |
|
|