Re: "Assert"? "Assume"? (was: next "big" language?? (disagree))

[imc@ecs.ox.ac.uk (Ian Collier)]

In article <4r07k8$9mf@seram.dcs.glasgow.ac.uk>, bunkenba@dcs.gla.ac.uk (Alexander Bunkenburg) wrote:
>claird@Starbase.NeoSoft.COM (Cameron Laird) writes:
>Assert(x) and Fact(x) seem to be the "assertion" and "guards" of "the"
>refinement calculus a la Back, Morris, and Morgan.

>They are written
>{x} ; E
>x -> E
>where E is the program following the assertion or guard.
>Nigel Ward in his thesis about a functional refinement calculus
>calls "assertion" "assumptions".  He writes them
>x >- E
>where E is the expression for which x is asserted.

Well, as long as we are talking formal computing science, I have also seen
such constructions.  I believe the following versions were used by Hoare,
though I'm slightly uncertain on that.  I borrowed the assumption in my
thesis.  They are written:

     _|_
  {p}           assertion - the same as [p,true]

     T
  {p}           assumption - the same as [true,p].

The first of these causes the program to abort when p is false.  The second
is "magic" - it is not possible ever for p to be false at that point in the
program.

The guarded command p -> SKIP as mentioned above has identical semantics
to the assumption, but you never see it by itself except in some formal
proofs.

Ian Collier - imc@comlab.ox.ac.uk - WWW Home Page:
http://www.comlab.ox.ac.uk/oucl/users/ian.collier/index.html