Hi Margarita, sorry for the late answer
Le 20/04/2020 à 17:58, margarita.capretto a écrit :
Dear colleagues,
My name is Margarita Capretto and I am doing research with prof. Cesar
Sanchez
at the IMDEA Software Institute. We are using Why3 (and in particular
WhyML) for deductive software verification.
Thanks for letting us know. I remind for everybody that if anybody has a
project using Why3, and say at least a public Web page about it, we can
add a link to your project on the main Why3 page.
We have some problems trying to prove/generating counterexample for
some simple code in WhyML using CVC4 (version 1.7) and Z3 (version
4.8.6) and we'd appreciate if someone can help us understand why this
happen.
Here is a simplified example that illustrates the issue:
let function mult3 (t: uint64) : uint64 =
requires { in_bounds (3*t) }
ensures { result = 3*t }
3*t
predicate post_mult3 (n: uint64) (result: uint64) =
result = mult3 n
let f_pred_mult3 (n: uint64) : uint64 =
requires { in_bounds (3*n) }
ensures { post_mult3 n result }
3*n
The VC for the function f_pred_mult3 can be proven by Z3. However,
CVC4 runs out of time while trying to prove it but then can prove it
when it tries to get a counterexample.
This is a rare situation that others already met. When calling CVC4 for
counterexamples, then Why3 produces a different SMT file. That is
intended, so it may occasionally happen that the VC is proved when
trying to find a counterexample.
Anyway, as soon as Z3 proves your VC you should be satisfied
If we don't define any
predicate and we simply write
ensures {result = mult3 n} (see f_mult3)
or if we don't use function mult3 (see f and f_pred), then CVC4 can
prove the VC without any problem.
Adding an extra predicate adds a very small amount of input for the
prover and sometimes it is enough to turn proved VCs into unproved ones.
Regarding predicates, there have been a discussion in the past, and a
good advice, if you are sure that your predicates should be always
expended, to add the attribute [@inline:trivial] to the definition of
the predicate
predicate post_mult3 [@inline:trivial] (n: uint64) (result: uint64) =
result = mult3 n
In the attached file there are more
examples where the argument is passed in a record or the result is
returned in a list. In some of this cases, Z3 is not able to prove nor
generate counterexamples for the VCs (see f_record_list_pred and
f_list_pred) and CVC4 has the same problem as above. Seems like some
problems can be avoided if we do not use predicates, why is that?
I hope the inline:trivial technique above could help
Is
there an easy way to see the input to CVC4 and Z3 generated by Why3?
Just hit the 'e' key (bound to the Tools/Edit entry of the menu) to see
the file. You may need to configure the "Default editor" in the
preferences, the default 'editor' being usually a CLI-only editor. USe
"emacs" or "vim" for example.
Hope this helps,
- Claude
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
