Path: utzoo!mnetor!tmsoft!torsqnt!news-server.csri.toronto.edu!clyde.concordia.ca!thunder.mcrcim.mcgill.edu!snorkelwacker.mit.edu!apple!usc!wuarchive!uunet!mcsun!ukc!warwick!cam-cl!news
From: jg@cl.cam.ac.uk (Jim Grundy)
Newsgroups: comp.specification
Subject: Re: A Mistake in "The Z Notation"?
Keywords: Z
Message-ID: <1990Dec20.124927.713@cl.cam.ac.uk>
Date: 20 Dec 90 12:49:27 GMT
References: <1990Dec20.121939.2539@cl.cam.ac.uk>
Sender: news@cl.cam.ac.uk (The news facility)
Reply-To: jg@cl.cam.ac.uk
Organization: Cambridge Hardware Verification Group
Lines: 13


 Forget the bit where I say

   I think I would rephrase the whole thing like this though:
     \begin{zed}
         \all Astate; Cstate; x? : X @
             \pre Aop \land Abs \implies
                 (\exists Astate'; Cstate'; y! : Y @ Aop \land Cop \land Abs')
     \end{zed}

 the rest stands though.

 Jim