Re: [CZT-Devel] Re: z2jml translator

[Leo F. <le...@cs...>]

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