Learn how easy it is to sync an existing GitHub or Google Code repo to a SourceForge project! See Demo
Close
From: Mark Utting <marku@cs...>  20050725 05:18:55

Petra Malik wrote: >the z2jml tool is not yet implemented but Mark tries to find a student >to work on this (as far as I know). > > An initial version was done by a student in 2003, but was not robust or complete enough to be useful. I don't have any prospective students who are currently interested in this, so we would welcome proposals from anyone interested in doing it. It would be an interesting project. One goal would be to take a Z spec (state, init, operations etc.) and generate a Java skeleton of its implementation, with JML model variables for the Z state variables and JML preconditions and postconditions wrapped around each method. This would give good documentation of the Java class, but might also make it possible to do JML runtime checking (after manually writing the Java implementations of the methods) to check that the specs and code agree. Mark 
From: Leo Freitas <leo@cs...>  20050712 10:33:34

Hi folks, I've seen in a CZT paper about a z2jml translator. In the repository I couldn't find such tool (i.e. CZT_HOME/translators). Is it available elsewhere? If not implemented, is there any plan for this implementation? Thanks, Leo 
From: Petra Malik <petra@cs...>  20050725 02:27:22

Hi Leo, the z2jml tool is not yet implemented but Mark tries to find a student to work on this (as far as I know). Petra Leo Freitas wrote: > Hi folks, > > I've seen in a CZT paper about a z2jml translator. In the repository I > couldn't find such tool (i.e. CZT_HOME/translators). > Is it available elsewhere? If not implemented, is there any plan for > this implementation? > > Thanks, > Leo 
From: Mark Utting <marku@cs...>  20050725 05:18:55

Petra Malik wrote: >the z2jml tool is not yet implemented but Mark tries to find a student >to work on this (as far as I know). > > An initial version was done by a student in 2003, but was not robust or complete enough to be useful. I don't have any prospective students who are currently interested in this, so we would welcome proposals from anyone interested in doing it. It would be an interesting project. One goal would be to take a Z spec (state, init, operations etc.) and generate a Java skeleton of its implementation, with JML model variables for the Z state variables and JML preconditions and postconditions wrapped around each method. This would give good documentation of the Java class, but might also make it possible to do JML runtime checking (after manually writing the Java implementations of the methods) to check that the specs and code agree. Mark 
From: Leo Freitas <leo@cs...>  20050725 07:48:48

Hello folks, > An initial version was done by a student in 2003, but was not robust > or complete enough to be useful. > > I don't have any prospective students who are currently interested in > this, so we would welcome proposals from anyone interested in doing it. > > It would be an interesting project. One goal would be to take a Z > spec (state, init, operations etc.) and generate a Java skeleton of > its implementation, with JML model variables for the Z state variables > and JML preconditions and postconditions wrapped around each method. > This would give good documentation of the Java class, but might also > make it possible to do JML runtime checking (after manually writing > the Java implementations of the methods) to check that the specs and > code agree. I am interested on this as well. In the model checking algorithm, I've used Z and its refinement calculus to go from the very abstract Z spec down to the code and I wanted to encode the invariants, pre/post etc... in JML! I was wondering however, how can you explicitly encode the precondition of a schema? Do you calculate (simplify the expression) or assume that the schema must give it somewhat separately? Is there a copy of this somewhere in the CVS? As I am looking at some strategy for this kind of translation now, I could have a look and see if I could make any further contribution :) > Mark thanks Mark, Leo 
From: Mark Utting <marku@cs...>  20050725 21:37:53

Leo Freitas wrote: >Hello folks, > > > >>An initial version was done by a student in 2003, but was not robust >>or complete enough to be useful. >> >>I don't have any prospective students who are currently interested in >>this, so we would welcome proposals from anyone interested in doing it. >> >>It would be an interesting project. One goal would be to take a Z >>spec (state, init, operations etc.) and generate a Java skeleton of >>its implementation, with JML model variables for the Z state variables >>and JML preconditions and postconditions wrapped around each method. >>This would give good documentation of the Java class, but might also >>make it possible to do JML runtime checking (after manually writing >>the Java implementations of the methods) to check that the specs and >>code agree. >> >> > >I am interested on this as well. In the model checking algorithm, I've >used Z and its refinement calculus to go from the very abstract Z spec >down to the code >and I wanted to encode the invariants, pre/post etc... in JML! >I was wondering however, how can you explicitly encode the precondition >of a schema? Do you calculate (simplify the expression) or assume that >the schema must give it somewhat separately? > > The z2b translator does this too (splits a schema into pre/post). >Is there a copy of this somewhere in the CVS? As I am looking at some >strategy for this kind of translation now, I could have a look and see >if I could make any further contribution :) > > See translators/z2b/src/net/sourceforge/czt/z2b/Z2B.java Here is the relevant method: /** Split a complex postcondition predicate into pre/post lists. This currently uses a very simplistic algorithm. It splits post into conjuncts and puts all conjuncts that do not involve primed or output variables into 'pre', and all remaining conjuncts into 'post'. This is not always correct, since some conjuncts that involve primes/outputs may add implicit constraints on inputs. TODO: improve the algorithm further. */ protected void splitPrePost(Pred pred, List pre, List post) { if (pred instanceof AndPred) { AndPred and = (AndPred) pred; splitPrePost(and.getLeftPred(), pre, post); splitPrePost(and.getRightPred(), pre, post); } else { if (freevarChecker_.containsPrimesOrOutputs(pred)) post.add(pred); else pre.add(pred); } Very simple/simplistic! And it works for the majority of cases :) But it returns a precondition that is TOO weak when there is a precondition implicit within a postcondition. For example, the schema [x,x' : \seq \nat  x' = tail ~ x] has the implicit precondition x \neq \{\}, but the above algorithm will just return an empty list (= true) for the precondition. For the moment, I am viewing this as a restriction on the input specification  users must be careful to make such implicit preconditions explicit (eg. by adding the x \neq \{\}) before using the z2b translator. Perhaps eventually it would be nice to have a separate `precondition analyser' tool that generates proof obligations like \pre S \implies explicitPre(S) for each operation schema S (where explicitPre(S) is the above algorithm). We could perhaps also incorporate domain analysis into an analysis tool like this (domain analysis checks that the meaning of the schema does not depend upon the value of a function outside its precondition. See the Z/EVES documentation for details.) Suggestions and improvements welcome. Mark 
From: Leo Freitas <leo@cs...>  20050726 08:03:56

Hello folks, >The z2b translator does this too (splits a schema into pre/post). > > That is great! I'll look at this.... >>Is there a copy of this somewhere in the CVS? As I am looking at some >>strategy for this kind of translation now, I could have a look and see >>if I could make any further contribution :) >> >e translators/z2b/src/net/sourceforge/czt/z2b/Z2B.java >Here is the relevant method: > > /** Split a complex postcondition predicate into pre/post lists. > This currently uses a very simplistic algorithm. > It splits post into conjuncts and puts all conjuncts that > do not involve primed or output variables into 'pre', and > all remaining conjuncts into 'post'. This is not always > correct, since some conjuncts that involve primes/outputs > may add implicit constraints on inputs. > > TODO: improve the algorithm further. > */ > protected void splitPrePost(Pred pred, List pre, List post) > { > if (pred instanceof AndPred) { > AndPred and = (AndPred) pred; > splitPrePost(and.getLeftPred(), pre, post); > splitPrePost(and.getRightPred(), pre, post); > } > else { > if (freevarChecker_.containsPrimesOrOutputs(pred)) > post.add(pred); > else > pre.add(pred); > } > >Very simple/simplistic! >And it works for the majority of cases :) >But it returns a precondition that is TOO weak when there is >a precondition implicit within a postcondition. For example, >the schema [x,x' : \seq \nat  x' = tail ~ x] has the implicit >precondition x \neq \{\}, but the above algorithm will just >return an empty list (= true) for the precondition. > >For the moment, I am viewing this as a restriction on the input >specification  users must be careful to make such implicit preconditions >explicit (eg. by adding the x \neq \{\}) before using the z2b translator. > > Ok, I see. This restricted version is okay. In the model checker I impose similar restrictions such as include schema components with their maximal types exactly to allow me to do a simpler unfolding. What about schema unfolding? Would this be a requirement for complete precondition derivation? >Perhaps eventually it would be nice to have a separate >`precondition analyser' tool that generates proof obligations like > > \pre S \implies explicitPre(S) > >for each operation schema S (where explicitPre(S) is the above algorithm). > > Hum... That sound very nice. Anyway, how could we improve "explicitPre(S)" so that this conjecture is to be more like a theorem? >We could perhaps also incorporate domain analysis into an analysis tool >like this (domain analysis checks that the meaning of the schema does >not depend upon the value of a function outside its precondition. See >the Z/EVES documentation for details.) > > Hum... I am also very used with Z/Eves domain checks. In fact, in the mean time, we could even export the proof obligations (or domain checks) to Z/Eves. I mean, Z/Eves accepts either XML or LaTeX (even though not very standarised). We could transform the CZT AST to Z/Eves LaTeX/XML , ask the prover to reduce the formula, and try collecting the results. I am very familiar with Z/Eves, once I get my (last chapter) thesis sorted I will have a quick look at these topcis. >Suggestions and improvements welcome. >Mark > > Leo 