jg@cl.cam.ac.uk (Jim Grundy) (12/20/90)
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 jg@cl.cam.ac.uk (Jim Grundy) (12/20/90)
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