Re: [CZT-Devel] Z Std extension - schema tagging

[Leo F. <leo...@ne...>]

Hi Mark,

Yes, that's a good idea - and is similar to what ProB/Z does. But it has some shortcomings,
mostly when you have complex state (e.g., using the schema calculus) or promotion...
In the end, I've added those syntactic tags....

PS:
sorry for the delay, I am on holiday :-)

best,
Leo

________________________________________
From: bm....@gm... [bm....@gm...] On Behalf Of Mark Utting [ma...@cs...]
Sent: 10 December 2011 03:19
To: Leo Freitas
Cc: czt...@li...
Subject: Re: [CZT-Devel] Z Std extension - schema tagging

Leo,

Another option might be to specify these things *within* Z.
Then you wouldn't need to extend the language or parser
and other tools wouldn't barf on your extended input.

Eg.  look for a schema with a special name, and use it
fields to specify the structure of the state machine:

\begin{schema}{MachineDefinition}
state:  BirthdayBook
init: InitBirthday
% all other names / fields are public operations
add: RobustAddBirthday
find: RobustFindBirthday
remind: RobustRemind
\end{schema}


???

Cheers
Mark


On 22 August 2011 23:09, Leo Freitas <leo...@ne...<mailto:leo...@ne...>> wrote:
Hi,

I am integrating the Z VCG into the CZT Eclipse plugin. Whilst doing that for refinement (and compact version of precondition) proofs,
I came across the need to know what schema is to be considered as the "State" (+ retrieve, init, concrete, etc).
In other tools, this can be made explicit by the user, yet each time the tool is run. I was thinking about some persistent version using
specific keywords/tags near SchBox AxPara (e.g., "\begin{schema}{S}"). What do you think?

I've implemented this already within the ZEves Z parser and thought to put it into the Z one (haven't committed either).
The "keywords" are treated by the scanner/parser outside of boxes. An example would be something like

======================================================
\begin{zsection}
  \SECTION zstate\_toolkit \parents standard\_toolkit
\end{zsection}

Synonymns for when only (abstract/concrete) state is present?
%%Zword \zstate zstate
%%Zword \zstinit zstinit

%%Zword \zastate zastate
%%Zword \zastinit zastinit
%%Zword \zcstate zcstate
%%Zword \zcstinit zcstinit
%%Zword \zretrieve zretrieve
======================================================
\begin{zsection}
  \SECTION zstatev1 \parents zstate\_toolkit
\end{zsection}

\zstate
\begin{schema}{S}
  x: \nat
\where
  bar > x
\end{schema}

\zstinit
\begin{schema}{SInit}
  S~'
\where
  x' = 0
\end{schema}

======================================================
\begin{zsection}
  \SECTION zstatev2 \parents zstate\_toolkit
\end{zsection}

\zastate
\begin{schema}{AState}
  x: \power \nat
\where
 x \neq \emptyset
\end{schema}

\zastinit
\begin{schema}{ASInit}
  AState~'
\where
  x' = \{ 0 \}
\end{schema}

\zcstate
\begin{schema}{CState}
 y: \seq \nat
\where
  y \neq \langle \rangle
\end{schema}

\zcstinit
\begin{schema}{CStInit}
  CState~'
\where
 y' = \langle 0 \rangle
\end{schema}

\zretrieve
\begin{schema}{Retr}
  AState \\
  CState
\where
  \ran~y = x
\end{schema}

======================================================

If there are no objections, I will keep it to the Z parser. Only if you import zstate_toolkit as a parent
would it "work". So, like fuzz_toolkit and named theorems, I see this as a CZT Z extension....

I've extended the printer and typechecker as well to cope with the new markup and to ensure
there are no duplication (e.g., duplicated state tags).

Comments  / thoughts?

Best,
Leo
------------------------------------------------------------------------------
uberSVN's rich system and user administration capabilities and model
configuration take the hassle out of deploying and managing Subversion and
the tools developers use with it. Learn more about uberSVN and get a free
download at:  http://p.sf.net/sfu/wandisco-dev2dev
_______________________________________________
CZT-Devel mailing list
CZT...@li...<mailto:CZT...@li...>
https://lists.sourceforge.net/lists/listinfo/czt-devel