🚀 go-pugleaf

   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