Formal specifications were first used in the description of program-
ming languages because of the central role that languages and their
compilers play in causing a machine to perform the computations required
by a programmer. In a relatively short time, specification notations
have found their place in industry and are used for the description of a
wide variety of software and hardware systems. A formal method - like
VDM - must offer a mathematically-based specification language. On this
language rests the other key element of the formal method: the ability
to reason about a specification. Proofs can be empioyed in reasoning
about the potential behaviour of a system and in the process of showing
that the design satisfies the specification. The existence of a formal
specification is a prerequisite for the use of proofs; but this
prerequisite is not in itself sufficient. Both proofs and programs are
large formal texts. Would-be proofs may therefore contain errors in the
same way as code. During the difficult but inevitable process of
revising specifications and devel- opments, ensuring consistency is a
major challenge. It is therefore evident that another requirement - for
the successful use of proof techniques in the development of systems
from formal descriptions - is the availability of software tools which
support the manipu- lation of large bodies of formulae and help the user
in the design of the proofs themselves.