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

[Mark U. <ma...@cs...>]

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...> 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...
> https://lists.sourceforge.net/lists/listinfo/czt-devel
>