From owner-qed Wed Dec 14 12:46:34 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id MAA03359 for qed-out; Wed, 14 Dec 1994 12:44:49 -0600
Received: from thialfi.cs.cornell.edu (THIALFI.CS.CORNELL.EDU [128.84.254.220]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id MAA03354 for ; Wed, 14 Dec 1994 12:44:44 -0600
Received: from CLOYD.CS.CORNELL.EDU by thialfi.cs.cornell.edu (5.67/I-1.99G)
id AA05693; Wed, 14 Dec 94 13:44:41 -0500
Received: from HERA.CS.CORNELL.EDU by cloyd.cs.cornell.edu (5.67/I-1.99F)
id AA13210; Wed, 14 Dec 94 13:44:46 -0500
Message-Id: <9412141844.AA15783@hera.cs.cornell.edu>
Received: by hera.cs.cornell.edu (5.67/N-0.13aa)
id AA15783; Wed, 14 Dec 94 13:44:39 -0500
To: qed@mcs.anl.gov
Cc: yodaiken@sphinx.nmt.edu, des@inmos.co.uk
Subject: Re: Hardware verification
Date: Wed, 14 Dec 1994 13:44:39 -0500
From: Paul Jackson
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
A few years ago I was studying the spec. that Geoff Barrett wrote in the
Z specification language for the T800 Transputer floating-point microcode
(see below for references).
I came across several errors, that may be what Kahan was referring to in
his remarks. One of the errors can probably be counted as a typo and
probably would have been caught by a basic Z syntax-checker. Others were
logical errors; the spec. stated a `theorem' that was false and
part of the spec. was inconsistent. For those interested in
the technical details, I describe below the errors that I noticed.
I talked to Geoff Barrett in 1990 or '91 about this, and I seem to
remember him saying that subsequent to the spec being submitted for
publication, the errors were noticed and corrected.
At any rate, the fact that there were errors at all I think indicates the
importance of having mechanical type-checking / theorem-proving support
to back up formal specifications; all these errors would have been caught
very quickly if the spec. had been mechanically checked. Then again,
maybe all that was needed was some independent careful human appraisal of
the spec.
I'd be curious to hear from anyone who is up on the current status of
proof tools for Z. I know that at ICL in the UK, R.B.Jones has been
working on such tools. Could they be used today to flush out the errors
I mention below?
Paul.
**********************
The Z Spec was published in:
Geoff Barrett, "Formal Methods Applied to a Floating-Point
Number System".
IEEE Transactions on Software Engineering,
Vol 15, No. 5, May 1989, p611-621.
A slightly earlier version of this paper was:
Geoff Barrett, "Formal Methods Applied to a Floating-Point
Number System".
Technical Monograph PRG-58. Jan 1987
Oxford University Computing Laboratory.
The errors I was able to find last night, going back to look at the
paper, include the following (referring to the IEEE version). All these
errors pertain just to the specification of rounding. I've tried to make
the comments intellible, even if you don't have the paper at hand.
The paper introduces a set of real numbers `ApproxValues', that are
intended to be exactly all the real numbers that can be denoted by a
floating-point bit-vector in some given format. Initially, the
set is introduced abstractly; all that is required is that it
satisfy certain constraints. Only later is the connection made to some
floating-point format.
The paper also introduces two real numbers `MinValue' and `MaxValue' that
delimit the ApproxValues set, and introduces a subset of
ApproxValues U {MinValue,MaxValue}
that are called `PreferredValues'. These are the values one rounds to
in the `round to nearest' mode when one has to make a choice about
rounding to one of two distinct equidistant values that can actually be
represented.
1. p614. Left column, top: the paper notes a `theorem' that when rounding
towards +infinity, and MinValue is not in ApproxValues, the rounded value
cannot be MinValue. In light of the IEEE spec. this is a sensible claim
to want to make (though I thought that the Z spec should have been clear
from the start about whether MinValue was considered to be in
ApproxValues or not). However, I could not see how this is a consequence
of the definition of what it is to `round towards +infinity' given in the
`Above' schema on p613. (`Schemas' in Z are the basic units that many
definitions come in; they declare types of variables and specify
constraints on those variables.) Indeed, it seems that the spec is
non-deterministic; when rounding up a value below MinValue, it allows
both MinValue and the most negative element of ApproxValues as legitimate
rounded values.
2. p613, centre. The `Round_Signature' schema specifies the consistency
of the PreferredValues set. It says that given any two real numbers v1,
v2 in the set,
ApproxValues U {MinValue,MaxValue}
such that v1 > v2,
there is a element p in PreferredValues such that v1 >= p >= v2.
At the foot of p614, the FP_Round1 schema introduces definitions for
ApproxValues, PreferredValues, MinValue and MaxValue that are based on a
given floating-point format. Unfortunately, the consistency constraint
mentioned above on PreferredValues isn't satisfied by these definitions.
In particular, if v1 is MaxValue and v2 is the greatest element of
ApproxValues (neither of which are in PreferredValues), there is no
suitable p.
3. p615, top. In the Exception_Spec signature, a (') (prime) suffix is
omitted from a variable `value'. This would have been caught by a
simple Z syntax checker, because `value' without a prime suffix is not
declared anywhere in the context of this signature.