Re: A Mistake in "The Z Notation"?

Article View: comp.specification

Article #303

Back to comp.specification Previous Next

#303

From: Jim Grundy
Date: Thu, 20 Dec 1990 12:49

13 lines
910 bytes

 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

Technical Details

Message-ID: <1990Dec20.124927.713@cl.cam.ac.uk>

Path:

arc1-ca.pugleaf.net!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

References: <1990Dec20.121939.2539@cl.cam.ac.uk>

Show Full Headers

Complete Article Headers

Path: arc1-ca.pugleaf.net!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

Reply to Parent Message