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


   I'm wondering if there is not a tiny mistake in Mike Spivey's 
"The Z Notation".   I believe it occurs on page 140 in section 5.6 on
Data Refinement.
   Mike is describing the necessary conditions for a concrete state (Cstate)
to be a good refinement of an abstract state (Astate).   The second condition
he gives is this:

	If an abstract state and a concrete state are releated by $Abs$, and
	both the abstract and concrete operations are guarenteed to terminate,
	then ever possible state after the concrete operation must be related
	by $Abs'$ to a possible operation after the abstract operation.  In
	symbols:

	\begin{zed}
	    \all Astate; Cstate; Cstate'; x? : X; y? : Y @
	        \pre Aop \land Abs \land Cop \implies 
                    (\exists Astate' @ Abs' \and Aop)
	\end{zed}

   I think this prediciate is slightly off; should it read:

	\begin{zed}
	    \all Astate; Cstate; Cstate'; x? : X; y? : Y @
	        (\exists Astate' @ Aop) \land Abs \land Cop \implies 
                    (\exists Astate' @ Abs' \and Aop)
	\end{zed}

   The problem I think lies with "\pre Aop" as this is defined to be
"\exists Astate'; y! : Y @ Aop" having the y! locally quantified in there
is not what is wanted (is it?)

   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}

Soooo Am I right?, or do I need a brain transplant?

If I am right then there is probably a similar mistake in the second condition
in section 5.7


Jim