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: 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: imc@ecs.ox.ac.uk (Ian Collier) Subject: Re: "Assert"? "Assume"? (was: next "big" language?? (disagree)) Date: 1996/06/28 Message-ID: <8635.imc@comlab.ox.ac.uk>#1/1 X-Deja-AN: 162558076 references: <4ql1fv$5ss@goanna.cs.rmit.EDU.AU> <4qsbm7$r1s@Starbase.NeoSoft.COM> <4r07k8$9mf@seram.dcs.glasgow.ac.uk> organization: Oxford University Computing Laboratory x-local-date: Friday, 28th June 1996 at 1:34pm BST newsgroups: comp.lang.c,comp.lang.misc,comp.lang.pl1,comp.lang.ada Date: 1996-06-28T00:00:00+00:00 List-Id: 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