A Comparison of Z and VDM with B/AMN

cited from
http://www.b-core.com/ZVdmB.html

• • • -

We are frequently asked to compare the AbstractMachine Notation (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.

e.g. 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. e.g.

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.