>From vigna@c700-1.sm.dsi.unimi.it Wed Sep 29 13:12:30 CDT 1993 Article: 8351 of comp.theory Path: cs.utexas.edu!uwm.edu!spool.mu.edu!nigel.msen.com!caen!batcomputer!ghost.dsi.unimi.it!ghost.dsi.unimi.it!not-for-mail From: vigna@c700-1.sm.dsi.unimi.it (sebastiano vigna) Newsgroups: comp.theory Subject: Is UNITY consistent? Date: 26 Sep 1993 10:12:13 +0100 Organization: Computer Science Dep. - Milan University Lines: 22 Distribution: inet Message-ID: <283mdd$a9t@c700-1.sm.dsi.unimi.it> NNTP-Posting-Host: c700-1.sm.dsi.unimi.it Status: O There is a persistent rumour hanging around that the logic of UNITY is not sound. I have found two "references" to this "fact" which are of completely different nature (a paper by Kok et al. which shows that under a specific non standard semantics the logic of UNITY can't characterize all state transformations---who cares, and a paper by Sanders which states that an incorrect understanding of the rules, i.e. viewing them as relations rather than inference rules, mixed up with the substitution axiom leads to contradiction---who cares, again). I have again heard this rumor, this time supported by some kind of "simple example" shown at a conference. Of course, the person couldn't reproduce the example or give a reference. If anyone has a reference of any kind, I would be immensely grateful. seba >From beverly@cs.caltech.edu Wed Sep 29 13:13:11 CDT 1993 Article: 8363 of comp.theory Path: cs.utexas.edu!math.ohio-state.edu!howland.reston.ans.net!pipex!uunet!elroy.jpl.nasa.gov!nntp-server.caltech.edu!beverly From: beverly@cs.caltech.edu (Beverly A. Sanders) Newsgroups: comp.theory Subject: Re: Is UNITY consistent? Date: 28 Sep 1993 17:16:26 GMT Organization: California Institute of Technology Lines: 30 Distribution: inet Message-ID: <289rhaINN40a@gap.caltech.edu> References: <283mdd$a9t@c700-1.sm.dsi.unimi.it> NNTP-Posting-Host: fides.cs.caltech.edu Status: ORS Perhaps someone heard my talk at the IFIP Working conference on Programming Concepts and Methods, Sea of Gallilee, Israel, April, 1990. The example is given in my paper, Eliminating the Substitution Axiom from UNITY logic" Formal Aspects of Computing, 3(2) 189-285, 1991. Jan van de Snepscheut gave a similar example at a different conference somewhere about the same time. Although there were some problems in Chandy and Misra's book, they can be easily fixed. One way is given in my paper. (In my version, all proofs can be reduced to proofs in linear temporal logic, thus soundness follows from the soundess of temporal logic.) The consequences of the problems were that some of the proofs of the metatheorems given in the book are not correct, although the theorems themselves hold, and some people published completeness results about UNITY which were incorrect (claimed it was not complete, when in fact it is "relatively complete in the sense of Cook") since they did not properly account for the substitution axiom. As a practical matter, one can use UNITY for proving programs exactly as described in the book. Beverly Sanders Institut fuer Computersysteme Swiss Federal Institute of Technology (ETH Zurich) CH-8092 Zurich, Switzerland sanders@inf.ethz.ch >From jan@cs.caltech.edu Wed Sep 29 21:09:33 CDT 1993 Article: 8372 of comp.theory Path: cs.utexas.edu!swrinde!elroy.jpl.nasa.gov!nntp-server.caltech.edu!jan From: jan@cs.caltech.edu (Jan van de Snepscheut) Newsgroups: comp.theory Subject: Re: Is UNITY consistent? Date: 30 Sep 1993 00:03:22 GMT Organization: California Institute of Technology Lines: 94 Distribution: inet Message-ID: <28d7oaINN8pg@gap.caltech.edu> References: <283mdd$a9t@c700-1.sm.dsi.unimi.it> <289rhaINN40a@gap.caltech.edu> NNTP-Posting-Host: triton.cs.caltech.edu Status: ORS Hi, here is an example that shows that Unity logic is inconsistent. (This is a bit long; I don't know how to make it short and yet point out what the problem is (sorry).) declare p,q: boolean initially p=true /\ q=false assign p:= not q I will compute p unless q in two ways and get different values. In order to do so, one has to understand the Hoare triple of an assignment statement, especially how to reduce a predicate to a boolean scalar. (A predicate is a boolean function of the variables in the program, a scalar is a boolean value, not a function of the variables.) The problems have to do with this reduction. I take it that the Hoare triple {P} S {Q} is a boolean scalar, namely the one given by (forall x:: P ==> wp(S,Q)) where wp is Dijkstra's weakest precondition, and x is the list of all program variables. First, following the definition. p unless q = { definition of unless } (forall s: s in F:: {p /\ not q} s {p \/ q}) = { program conatins only one statement } {p /\ not q} p:= not q {p \/ q} = { definition of Hoare triple } (forall p,q:: (p /\ not q) ==> wp(p:= not q, p \/ q)) = { wp of an assignment statement is substitution } (forall p,q:: (p /\ not q) ==> (not q \/ q)) = { predicate calculus } (forall p,q:: (p /\ not q) ==> true) = { predicate calculus } (forall p,q:: true) = { predicate calculus } true Next, prove that q=false is an invariant (I'll skip that part), use the substitution rule on p unless q , and compute p unless false instead. p unless false = { definition of unless } (forall s: s in F:: {p /\ not false} s {p \/ false}) = { predicate calculus } (forall s: s in F:: {p} s {p}) = { program conatins only one statement } {p} p:= not q {p} = { definition of Hoare triple } (forall p,q:: p ==> wp(p:= not q, p)) = { wp of an assignment statement is substitution } (forall p,q:: p ==> not q) = { predicate calculus } (forall p,q:: not p \/ not q) = { predicate calculus } false The latter step produces false because for p=true,q=true the term not p \/ not q reduces to false, and therefore the universal quantification reduces to false. The problem with "understanding" the contradiction is that the state p=true,q=true does not occur during program execution. This example was given to me by Jan Eppo Jonker in the winter or early spring of 1988, who was at that time s student in a Unity class that I was teaching. I have mentioned this example to various people and at various places, including the Mathematics of Program Construction conference in June 1989. At that time, many people seemed to be aware of the problem of reachability of states. The first calculation of p unless q is entirely independent of the initial values of the variables. The calculation of p unless false is independent of initial values also. However, the fact that q=false is an invariant _does_ depend on initial values and this is where reachability of states enters the picture. One can construct variations of the Unity logic but, unless the meaning of a Hoare triple is redefined, the problem will not disappear. And if one defines the universal quantification that is implied by the Hoare triple to be a quantification over reachable states instead of a quantification over all states, then the definition of the Hoare triple itself becomes very messy and you cannot even answer such question like is {p} p:= not q {q} true? without knowing more about the execution of the program in which this statement is embedded, thereby giving up all hope for a compositional semantics. --Jan van de Snepscheut >From jrrao@watson.ibm.com Thu Sep 30 16:57:30 CDT 1993 Article: 8376 of comp.theory Newsgroups: comp.theory Path: cs.utexas.edu!uunet!newsgate.watson.ibm.com!hawnews.watson.ibm.com!jrrao From: jrrao@watson.ibm.com (J.R.Rao) Subject: Re: Is UNITY consistent? Sender: news@hawnews.watson.ibm.com (NNTP News Poster) Message-ID: Date: Thu, 30 Sep 1993 15:28:41 GMT Distribution: inet Disclaimer: This posting represents the poster's views, not necessarily those of IBM. References: <283mdd$a9t@c700-1.sm.dsi.unimi.it> <289rhaINN40a@gap.caltech.edu> <28d7oaINN8pg@gap.caltech.edu> Nntp-Posting-Host: monkey.watson.ibm.com Organization: IBM T.J. Watson Research Center Lines: 85 Status: ORS Jan van de Snepscheut has presented an example which illustrates the problem of using the substitution rule with the definitions of UNITY operators unless, ensures and leads-to as given in the UNITY book [CM88]. As Jan has mentioned this problem has been known since late 1987 to early 1988. The key role played by the substitution rule (see the second example in Jan's posting) has lead to several proposals to fix the problem. I summarize and give references for some of them below. 0. In [Misra 90], J. Misra suggests that the definition of the UNITY operators be weakened from strict equivalences to implication. For instance, if one can prove wp.s.(p or q)> then one is allowed to infer p unless q. But one cannot do the reverse, as the substitution rule may have been used to infer p unless q. 1. In [Sanders 90], Beverly Sanders suggests that the problematic substitution axiom be dropped. She redefines UNITY operators using the concept of the strongest invariant. The strongest invariant (which allows one to capture the notion of reachable states), is introduced in the hypothesis to prove UNITY properties. For instance, is SI is the strongest invariant of a UNITY program then p unless q would be defined as wp.s.(p or q)> 2. In [Knapp 90], Edgar Knapp redefines the square brackets operator (introduced in [DS90]). The square brackets are meant to capture universal quantification over the state space of the program. Knapp redefines them to mean universal quantification over the reachable state space of the program. 3. Jan van de Snepscheut has written an article on this as well. I request him to provide a reference for the same. 4. The approach that I have taken to this problem in my work on UNITY (and in my thesis [Rao 1992]) is to drop initial conditions from UNITY programs. This has the effect of of removing the problem in Jan's example. Dropping initial conditions is not problematic as one can introduce statements in the assign section that establish the required initial conditions. Then one does not need to change the definitions of the UNITY operators or drop the substitution axiom. While this may not be feasible in some situations, I found it to be more than adequate for my meta-theoretic studies of UNITY. 5. There is closely related work in [Cohen 92] and [Pachl 90]. I hope you find this to be helpful. -J R Rao ------------------------------------------------------------------ [CM88] K. Mani Chandy and Jayadev Misra, Parallel Program Design - A Foundation, 1988. [DS90] E. W. Dijkstra and C. S. Scholten, Predicate Calculus and Program Semantics, 1990. [Cohen 92] Ernie Cohen, Modular Progress Proofs of Asynchronous Programs, Phd thesis, Department of Computer Sciences, The University of Texas at Austin, Austin, Texas 1992. [Knapp 90] Edgar Knapp, Soundness and Relative Completeness of UNITY, In his Phd thesis, Refinement as a basis of Concurrent Program Design, The University of Texas at Austin, Austin, Texas, 1992. [Misra 90] Jayadev Misra, Soundness of the Substitution Axiom, Notes on UNITY 14-90, Department of Computer Sciences, The University of Texas at Austin, Austin, Texas 78712, 1990. [Pachl 90] Jan Pachl, Three Definitions of leads-to for UNITY, Notes on UNITY, 23-90, Department of Computer Sciences, The University of Texas at Austin, Austin 1990. [Rao 92] J. R. Rao, Building on the UNITY experience: Compositionality, Fairness and Probability in Parallelism, Department of Computer Sciences, The University of Texas at Austin, Austin, 1992. [Sanders 90] Beverly Sanders, Eliminating the Substitution Axiom from UNITY, Technical Report 128, Departement Informatik fur Computersysteme, Eidgenossische Technische Hochschule, Switzerland, 1990.