Counter
Z
- Counter \defs [ n : \nat | n ≥ 0 ]
- Counter::Incr \defs [ ∆Counter, v? : \nat | n′ = n + v? ]
- Counter::Decr \defs [ ∆Counter | n > 0; n′ = n − 1 ]
- Counter::Value \defs [ ΞCounter; v! : \nat | v! = n ]
Bounded counter
- Counter \defs [ n : \nat | n ≥ 0 ]
- Counter::Incr \defs [ ∆Counter, v? : \nat | n′ = n + v? ]
- Counter::Decr \defs [ ∆Counter | n > 0; n′ = n − 1 ]
- Counter::Value \defs [ ΞCounter; v! : \nat | v! = n ]
slide: An alternative specification of the Counter
An alternative specification of the
Counter is given in slide [z-ctr-2].
To emphasize that we may regard
the Counter as an object, the operations
have been prefixed by Counter in a
C++-like manner.
This is only a syntactic device, however,
carrying no formal meaning.
In addition, both the operations
Incr and Decr declare
an integer variable
v? which acts,
by convention, as an input parameter.
Similarly, the integer variable
v! 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
v!, which is a Counter
with a maximum given by
an integer constant Max.
Similarly, we may specify the operations
for the
Bounded::Counter 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
Bounded::Counter
operation is
v? ≥ 0, whereas
the post-condition is
n′ = n + v?
which corresponds to the implementation requirement
that the new value of the Counter
is the old value plus the value of the
argument
n′ = n + v?.
In a similar way, the pre-condition
for applying the
Bounded::Incr operation
is
n + v? ≤ Max.
Note, however, that this pre-condition
is stronger than the original
pre-condition
n + v? ≤ Max, hence to conform
with the rules for refinement
we must specify what happens when
n + v? > Max 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 [Stepney], a number of studies are collected which propose
extending Z with a formal notion of classes and inheritance.
The reader interested in these extensions is invited in particular
to study Object-Z, OOZE and Z++.
As an historical aside, we may note that Z has been of significant
influence in the development of Eiffel (see Meyer, 1992b).
Although the two approaches are quite divergent,
they obviously still share a common interest in correctness.
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
Imagine that you must develop
a program to manage a library,
that is keep a record of the books
that have been borrowed.
State
Library
books : Book
borrowed : Book Person
borrowed books
slide: The specification of a library
Before developing a detailed object
model,
you may well reflect on
what user services the library must
provide.
These services include the borrowing
of a book, returning a book and asking
whether a person has borrowed any books,
and if so which books.
These operations are specified
by the schemas Borrow, Return
and Has in slide [z-lib-2].
Operations
Borrow
Library; b? : Book; p? : Person
b? borrowed
b? books
borrowed' = borrowed { b? p? }
Return
Library; b? : Book; p? : Person
b? borrowed
borrowed' = borrowed { b? p? }
Has
Library; p? : Person; bks : Book
bks! = borrowed ^-1 { p? }
slide: The library operations
Don't be frightened of the mathematical notation
in which these operations are specified.
The notation is only of secondary importance
and will be explained as we go along.
Since we are only interested in the abstract
relations between people and books, we may
assume Book and Person to be primitive types.
The specification given in slide [z-lib-1]
specifies an abstract state,
which is actually a partial function
delivering the person that borrowed
the book if the function is defined for
the book.
The function is partial to allow for the situation where
a book has not been borrowed,
but still lies on the shelves.
The invariant of the library system
states that the domain of
the function borrowed must be a subset
of the books available in the library.
Given the specification of the state, and some
mathematical intuition,
the specification of the operations
is quite straightforward.
When a Borrow action occurs, which
has as input a book
Borrow
Library; b? : Book; p? : Person
b? borrowed
b? books
borrowed' = borrowed { b? p? }
Return
Library; b? : Book; p? : Person
b? borrowed
borrowed' = borrowed { b? p? }
Has
Library; p? : Person; bks : Book
bks! = borrowed ^-1 { p? }
and a person
p?,
the function
p?
is defined by extending borrowed
with the association between
b? and
p?,
which is expressed as
the mapping
p?.
As a pre-condition for Borrow, we have that borrowed
must not be defined for
b?, otherwise
some person would already have borrowed
the book
b?.
The Return action may be considered
as the reverse of the Borrow action.
Its pre-condition states that borrowed
must be defined for
b?
and the result of the operation
is that the association between
b? and
b? is removed from
borrowed ′.
Finally, the operation Has
allows us to query what books are in
the possession of a person
borrowed ′.
The specification of Has employs
the mathematical features of Z
in a nice way.
The output, which is stored in
the output parameter
bks!,
consists of all the books related
to the person
bks!.
The set of books related to
p? is obtained
by taking the relational image of the inversion
of borrowed for the singleton set
consisting of
p?, that is,
each book x
for which
an association
p? is in borrowed
is included in the set
bks!.
Again, it is not the notation that is important
here, but the fact that the specification defines
all top-level user interactions.