[CZT-Devel] Animating Z Formal Specification

[Urmas R. <ur...@ho...>]

Hello, Petra, Leo.

I want to attach Formal Z specifications to the existing error localization and repair C++  project.
The error diagnosis requre reference model, that will generate referene outputs, what are used in diagnosis during comparison them with actual outputs.
This is basic idea of error diagnosis.

I want to make Formal Specifications written in Z to generate reference outputs. Using that the PhD will be much more full and i will have knowlege of formal specifications also.

The specifications i will create manually and will assume that they are generated somewhere somehow, i don't care how.
This requires just make the next steps:

1. Create specification.
2. Animate specification from c++ code using system c++ command.
3. Provide valid inputs (the format of inputs can be parameters that are sert at the moment of animation or data can be readed from file)
4. Recieve outputs.
5. Store outputs in valid format.
6. Continue diagnosis and repair using generated outputs.

The only one paragraph i have a problem - how to animate the specification.
I need to generate outputs from inputs using linux script, i will paste script to c++. I hope that CZT have this possibility, or i can use just parts of CZT that will animate the specification. Maybe it is possibly in specification write variables values to file?
I think its a good idea.

So for example if i have specification like
 ┌AddAB
 a?, b?, c!: ℕ
 |
 c! = a?+b?
 └

and input file with values
1 2
3 4
1 4
4 6
45 1

this will generate me
3
7
5
10
46

Thats all i need. The format of specification can be defined later.

ProZ - i need just to animate the specification prefably in ISO standart. So ZLive seems suitable. 

Urmas.

> From: leo...@ne...
> To: ur...@ho...
> CC: czt...@li...
> Date: Wed, 12 Oct 2011 16:29:20 +0100
> Subject: Re: [CZT-Devel] installing CZT
> 
> Urmas,
> 
> I still don't quite understand what you are trying to animate (e.g., where does your Z spec will come from?),
> but the general guideline is that it needs to be concrete enough, and bounded / finite. So "\nat" wouldn't work
> well, unless you have fixed values / equations for the variables, like in your example.
> 
> So far as I understand it, ZLive's strength is in that it is fully Z-ISO compatible, which means it will process mostly
> all Z specs (that are concrete enough) quite naturally. Another strength is that it has a rule-based mechanism where
> you can influence the way the rewriting / animation engine works, and that is quite a strength, given it would be
> in the direction of semi-automated theorem proving. (Now I am guessing), a weakness might perhaps be in the
> reasoning power the tool will have in the presence of complex invariants / predicates. But then it will depend on
> the nature of your model.
> 
> Another tool that might be suitable for animation is ProZ, although it is not within CZT toolset. The strengths of ProZ
> is that it can handle pretty complicated invariants, has integration with sat solvers, state-space graphical visualisation etc
> (E.g., it is based in Prolog). The weakeness is that it's just a prototype: although it covers a lot of (Spivey / old) Z, it doesn't
> handle the schema calculus as naturally (e.g., it is a tool developed originally for the B method and CSP). Having said
> that, it works well for certain kind of Z specs, and I use it when I want to know more about intricate aspects of a model that
> I don't understand well (yet).
> 
> However, without knowing better what do you want to achieve, it is a bit difficult to see what would be most suitable :-)
> By the way, you mentioned this was part of your PhD, could you send us (or me) the PhD proposal / topic, for instance?
> 
> Hope this helps....
> 
> Best,
> Leo
> 
> On 12 Oct 2011, at 08:11, Urmas Repinski wrote:
> 
> Hello,
> 
> 
> I have one more question at the moment if its possible.
> 
> Is there any tutorial how to animate the specification using CZT?
> For example i have simple specification like
> 
> ┌AddAB
>       a?, b?, c!: ℕ
>      |
>        c! = a?+b?
> └
> 
> 
> 
> I would like to get output 3 if i provide inputs 1 and 2.
> 
> is it possible to animate the specification using command line?
> Is it possible to store outputs in output file and read inputs from input file?
> Can this operations be defined in specification or i have to provide inputs as parameters?
> 
> Urmas.
> 
> ________________________________
> From: ur...@ho...<mailto:ur...@ho...>
> To: czt...@li...<mailto:czt...@li...>
> Date: Tue, 11 Oct 2011 10:51:28 +0200
> Subject: [CZT-Devel] installing CZT
> 
> Hello,
> 
> I had recently downloaded the last fixes, and now the installation comes through.
> [INFO] Reactor Summary:
> [INFO]
> [INFO] Community Z Tools ................................. SUCCESS [1.479s]
> [INFO] CZT Util .......................................... SUCCESS [5.354s]
> [INFO] CZT Jaxb .......................................... SUCCESS [17.602s]
> [INFO] CZT ZML ........................................... SUCCESS [2.448s]
> [INFO] CZT GnAST ......................................... SUCCESS [2.387s]
> [INFO] CZT GnAST Maven Plugin ............................ SUCCESS [2.791s]
> [INFO] CZT Corejava ...................................... SUCCESS [3:22.958s]
> [INFO] CZT SpecReader .................................... SUCCESS [4.513s]
> [INFO] CZT Session ....................................... SUCCESS [3.272s]
> [INFO] CZT Java Cup ...................................... SUCCESS [4.908s]
> [INFO] CZT Parser Source ................................. SUCCESS [1.528s]
> [INFO] CZT Cup Maven Plugin .............................. SUCCESS [1.329s]
> [INFO] CZT Parser ........................................ SUCCESS [1:29.434s]
> [INFO] CZT Z Pattern Parser .............................. SUCCESS [20.646s]
> [INFO] CZT Typechecker ................................... SUCCESS [25.878s]
> [INFO] CZT Rules ......................................... SUCCESS [29.582s]
> [INFO] CZT ZLive ......................................... SUCCESS [22.648s]
> [INFO] CZT Gaffe ......................................... SUCCESS [11.563s]
> [INFO] CZT Gaffe2 ........................................ SUCCESS [4.354s]
> [INFO] CZT jEdit plugins ................................. SUCCESS [0.332s]
> [INFO] CZT ZLive jEdit Plugin ............................ SUCCESS [1.365s]
> [INFO] CZT Object Z Parser ............................... SUCCESS [27.113s]
> [INFO] CZT Object-Z Typechecker .......................... SUCCESS [19.771s]
> [INFO] CZT Z/Eves (proofs) Parser ........................ SUCCESS [1:30.195s]
> [INFO] CZT Z/Eves (proofs) Typechecker ................... SUCCESS [44.580s]
> [INFO] CZT Z VCG ......................................... SUCCESS [21.737s]
> [INFO] CZT ZSideKick jEdit Plugin ........................ SUCCESS [6.955s]
> [INFO] CZT Z Palette jEdit Plugin ........................ SUCCESS [1.407s]
> [INFO] CZT Z/Eves Integration ............................ SUCCESS [44.098s]
> [INFO] CZT Z/Eves jEdit Plugin ........................... SUCCESS [2.165s]
> [INFO] CZT Circus Parser ................................. SUCCESS [1:02.805s]
> [INFO] CZT Object Z Pattern Parser ....................... SUCCESS [32.151s]
> [INFO] CZT Circus Typechecker ............................ SUCCESS [16.917s]
> [INFO] CZT User Interface ................................ SUCCESS [30.234s]
> [INFO] CZT Z to B translator ............................. SUCCESS [9.747s]
> [INFO] ------------------------------------------------------------------------
> [INFO] BUILD SUCCESS
> [INFO] ------------------------------------------------------------------------
> [INFO] Total time: 14:27.724s
> [INFO] Finished at: Tue Oct 11 11:44:46 EEST 2011
> [INFO] Final Memory: 47M/769M
> [INFO] ------------------------------------------------------------------------
> 
> So i have jar files generated in lib folder, will try to attach them with c++ command line.
> 
> If somebody has any corresponding experience how to execute CZT from c++ then please let me know to make things simpler.
> 
> Thank You,
> Urmas.
> 
> ------------------------------------------------------------------------------ All the data continuously generated in your IT infrastructure contains a definitive record of customers, application performance, security threats, fraudulent activity and more. Splunk takes this data and makes sense of it. Business sense. IT sense. Common sense. http://p.sf.net/sfu/splunk-d2d-oct
> _______________________________________________ CZT-Devel mailing list CZT...@li...<mailto:CZT...@li...> https://lists.sourceforge.net/lists/listinfo/czt-devel
> <ATT00001..txt><ATT00002..txt>
>