A Comparison of Z and VDM with B
We are frequently asked to compare the AbstractMachineNotation (AMN)
of the B-Method with Z and VDM. We have chosen the following points
of comparison:
Underlying Logic
Z and AMN are based in the same underlying set theory. VDM has
its own 3-valued logic, which allows treatment of undefinedness
not explicitly treated in Z or AMN.
In addition, the semantics of AMN is based on Abrial's Generalised
Substitution Language (GSL) and an associated calculus, an extension
of Dijkstra's guarded commands.
Syntax
The semi-graphical schema notation of Z is not used in AMN; it is
keyword-based as is VDM. Also like VDM, there are two definitions of
the notation, one in ASCII, the other in mathematical style.
Specification Style
AMN is based on a predicate-transformer style of specification, which
means that whereas in VDM you would write a pre and post condition, in
AMN you write the state change as a substitution; for example:
VDM:
insert(elem:TYPE) =
wr var:set(TYPE)
pre ~(elem : var)
post var = var` \/ {elem}
AMN:
insert(elem) =
PRE
elem:TYPE &
elem /: var
THEN
var := var \/ {elem}
END
The post condition in AMN looks like an assignment, giving the
specification a pseudo-programming look. In fact its semantics is as
a substitution on the state, and Abrial has proved that it is exactly
equivalent to the PRE/POST condition style of VDM.
In AMN, non-determinism is always explicit. For example:
VDM:
sort =
wr list:seq(TYPE)
pre true
post is_sorted(list) &
is_permutation(list,list`)
AMN:
sort =
ANY newlist WHERE
is_sorted(newlist) &
newlist : perm(rng(list))
THEN
list := newlist
END
You are not usually in any doubt as to when you are using
non-determinism in AMN.
Preconditions, Invariants and Proof Obligations
Z, VDM and AMN each have a different treatment of preconditions and
invariants. In Z, the precondition is not explicitly stated; it has to
be calculated from the delta schema definitions.
In VDM and AMN the preconditions are explicit. The redundant act of
explicitly stating a precondition allows consistency checking: is the
real precondition of the operation covered by the stated one?
Where AMN and VDM differ is in their treatment of the invariant. In
VDM it is assumed also to be an implicit part of every pre and post
condition. The effect of this that the only proof obligation you have
to discharge with respect to an operation is one of feasibility -
usually a large existentially quantified expression which is rather
intractable.
In AMN, the statement of the invariant is also redundant; its
presence or absence does not change the meaning of the operations; it
is not assumed to be part of the post condition of operations.
This means that operations have to be defined in such a way that they
preserve the invariant. Now, because of this redundancy, it becomes
necessary to prove that every operation preserves the invariant,
whereas in VDM it must be so by definition.
However, the nature of this (typically large) number of
additional proof obligations is very different from the feasibility
proofs. Most of them are small and universally quantified, and much
easier to discharge.
Notation Coverage
Z remains rather strictly a specification notation.
VDM and AMN are "wide-spectrum", in that they have
imperative programming constructs as part of the notation.
AMN has a small imperative language as a subset,
consisting of 6 constructs, and in which all
data-types are encapsulated in Abstract Machines.
This allows refinement down to code within the same
semantic framework.
Structuring Specifications and Implementations
AMN has much stronger structuring constructs than VDM, and very
different from the schema calculus of Z. AMN is object-based;
information hiding of various kinds is enforced, so that encapsulation
of state by operations is the order of the day. There is no proper
concept of inheritance or polymorphism, so it stops short of being
object-oriented.
Particularly strong is the B-Method's notion of layered development,
which allows a complex development to be decomposed in a rich variety
of ways using a small number of basic constructs. This makes the
refinement of industrial-scale systems practical.
Tool Support
B/AMN seems to have a considerable advantage at present in terms of
the tool support available. Commercial quality tools such as the
B-Toolkit exist in a unified framework for type-checking, animation,
proof-obligation generation, automatic and interactive proof, code
translators, document mark-up facilities and a comprehensive
development environment supported by method-sensitive configuration
manager.
|
