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

[bunkenba@dcs.gla.ac.uk (Alexander Bunkenburg)]

claird@Starbase.NeoSoft.COM (Cameron Laird) writes:

> In article <4ql1fv$5ss@goanna.cs.rmit.EDU.AU>,
> Dale Stanbrough  <dale@goanna.cs.rmit.EDU.AU> wrote:
> 			.
> 			.
> 			.
> >Obviously if there are two concepts, then we should have two names. For
> >example (in Ada) we could stick with
> >
> >	pragma Assert(x);
> >
> >for the traditional "please check this really is the case" assertion
> >and introduce
> >
> >	pragma Fact(x);
> >
> >(or some other name) for the "this really is true, trust me, and make
> >appropriate optimisations" type assertion. Can anyone think of a better
> >name (pragma Declare(x) is not available in Ada) than "Fact"?
> >
> >Dale

Assert(x) and Fact(x) seem to be the "assertion" and "guards" of "the"
refinement calculus a la Back, Morris, and Morgan. E.g. Carroll Morgan:
"Programming from Specifications", 1994, Prentice Hall. 

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.

	Alex