From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 107f24,a964c15062937091,start X-Google-Attributes: gid107f24,public X-Google-Thread: f891f,9d58048b8113c00f X-Google-Attributes: gidf891f,public X-Google-Thread: 1014db,9d58048b8113c00f X-Google-Attributes: gid1014db,public X-Google-Thread: 103376,2e71cf22768a124d X-Google-Attributes: gid103376,public X-Google-Thread: 101deb,b20bb06b63f6e65 X-Google-Attributes: gid101deb,public From: bunkenba@dcs.gla.ac.uk (Alexander Bunkenburg) Subject: Re: "Assert"? "Assume"? (was: next "big" language?? (disagree)) Date: 1996/06/28 Message-ID: <4r07k8$9mf@seram.dcs.glasgow.ac.uk>#1/1 X-Deja-AN: 162539543 references: <4ql1fv$5ss@goanna.cs.rmit.EDU.AU> <4qsbm7$r1s@Starbase.NeoSoft.COM> organization: Department of Computing Science, University of Glasgow, Scotland newsgroups: comp.lang.c,comp.lang.misc,comp.lang.pl1,comp.lang.ada,comp.lang.functional Date: 1996-06-28T00:00:00+00:00 List-Id: claird@Starbase.NeoSoft.COM (Cameron Laird) writes: > In article <4ql1fv$5ss@goanna.cs.rmit.EDU.AU>, > Dale Stanbrough 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