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.