From: David Shepherd <des@com.inmos>
Message-Id: <16345.9106210936@frogland.inmos.co.uk>
Subject: Re: select
To: sandy@com.tis (Sandy Murphy)
Date: Fri, 21 Jun 91 10:36:25 BST
Cc: info-hol@edu.uidaho.cs.ted (info-hol mailing list)
In-Reply-To: <9106202358.AA25006@TIS.COM>; from "Sandy Murphy" at Jun 20, 91 7:58 pm
Sender: des@com.inmos.inmos-c

Sandy Murphy has said:
> Many math algorithms have a statement in them that denotes a choice to
> be made.  Something like: take any item X with the property P.  The
> specific item is not important, just the fact that it has property P.
> Using the @ function works fine in specifying such an algorithm, and you
> can go on to prove useful theorems about the algorithm.
>
> I believe that it is not possible to show that the function f correctly
> implements the @ function, given the usual meaning of "correctly
> implements".  (@x.Px) denotes some particular but unspecified x.  The
> usual meaning of "correctly implements" is that every state change in
> the implementation must be an allowed state change in the algorithm
> (this is an over simplification, but OK for now).  There is no way to
> show that the state change made by f is the same as the one made by @ --
> no way to show that f chooses the same x as @.

this is a simple misunderstanding about @ which mosy of us probably make
at first ... @x.P(x) is has a fixed value (given P) and it really an
implementation orientated object (i.e. the spec says use any x such that
.. so here's one that fits).

> I have concluded that @ is the wrong thing to use in specifying an
> algorithm, where your goal is to prove an implementation.

perhaps the problem is that your trying to specify the algorithm as a
function where, due to the choice of X, it is a relation at that level?

e.g. suppose your algorithm takes a value x and adds an odd number to
it. then the specification could be

ALG_SPEC x x' = ? y. IS_ODD y /\ (x' = x+y)

then a valid implmentation would be

f x = x + (@y.IS_ODD y)

and you could prove

! x. ALG_SPEC x (f x)


--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk or des@inmos.com    tel: 0454-616616 x 529
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
                "pugh,  pugh,  barney mcgrew, cuthbert,  dibble,  grubb !"