X400-Received: by mta hedera.stl.stc.co.uk in /PRMD=STC Plc/ADMD=GOLD 400/C=GB/;
               Relayed; Thu, 27 Jun 1991 14:07:48 +0100
X400-Received: by /PRMD=stc plc/ADMD=gold 400/C=GB/; converted (ia5); Relayed;
               Thu, 27 Jun 1991 14:12:31 +0100
X400-Received: by /PRMD=icl/ADMD=gold 400/C=GB/; Relayed;
               Thu, 27 Jun 1991 13:56:23 +0100
Date: Thu, 27 Jun 1991 13:56:23 +0100
X400-Originator: R.B.Jones@gb.gold-400.icl.icl.win0103
X400-Mts-Identifier: [/PRMD=icl/ADMD=gold 400/C=GB/;win0103 0000010300000623]
Original-Encoded-Information-Types: ia5, undefined
X400-Content-Type: P2-1984 (2)
Content-Identifier: 623
From: win0103!R.B.Jones@net.eu.relay
Message-Id: <"623*/I=RB/S=Jones/OU=win0103/O=icl/PRMD=icl/ADMD=gold 400/C=GB/"@MHS>
To: info-hol@edu.uidaho.cs.ted
Subject: A response to "select" (on use of the choice function)
Sender: win0103!R.B.Jones@net.eu.relay


------------------------------ Start of body part 1

(this is a bit late since its been languishing at ucdavis)


------------------------------ Start of body part 2

Use of Choice function for writing loose specifications

The "new_specification" facility was introduced into HOL to support loose
specifications precisely because the choice function is not a satisfactory
substitute for a loose specification.  If you want to say that "f" is an
arbitrary function whose results have property "P" then use the property
"!x. P(f x)" in a call to new specification.

Given that the "new_specification" facility is available it should not be
necessary to use the choice function unless you really want the axiom of
choice, which is fairly unlikely for applications in computing.

However, this still won't enable you to prove some putative implementation "g"
to be correct, since there will be no relation between f and g which is
expressible let alone provable in the object language. (in the meta-language
you can say something like that every model of g is a model of f).

I personally regard this as being a deficiency in what is commonly held to
be a specification, and this view is reflected in most of the work which
is undertaken at ICL (Secure Systems).
The position we normally adopt is that a "specification"
is a property of systems, and an implementation is a system having that
property (or perhaps a widget which can be interpreted as such a system).

If this approach is adopted then the specification of a function the results
of which all have property P is:

"spec_f fun = !x. P(fun x)"

(which in this case can be entered by definition since the definition of this
loose specification is not itself loose)

It is now possible to express the claim that a function "g" satisfies this
specification.  This is simply "|-? spec_f g".  In most cases where this is
true it will also be provable.

Roger Jones (International Computers Limited)

------------------------------ End of body part 2