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.
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. 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. 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? Is
there an easy way to see the input to CVC4 and Z3 generated by Why3?
Thank you advance.
Best regards,
Margaritamodule Counterexample
use int.Int
use mach.int.UInt64
use list.ListRich
type storage = {
x : uint64;
}
invariant { 3*x <= max_uint64 }
by {
x = 10
}
let function mult3 (t: uint64) : uint64 =
requires { in_bounds (3*t) }
ensures { result = 3*t }
3*t
(* ------- Simple cases --------- *)
predicate post (n: uint64) (result: uint64) =
result = 3*n
(*Proved by Z3 and CVC4*)
let f (n: uint64) : uint64 =
requires { in_bounds (3*n) }
ensures { result = 3*n }
3*n
(*Proved by Z3 and CVC4*)
let f_pred (n: uint64) : uint64 =
requires { in_bounds (3*n) }
ensures { post n result }
3*n
predicate post_mult3 (n: uint64) (result: uint64) =
result = mult3 n
(*Proved by Z3 and CVC4*)
let f_mult3 (n: uint64) : uint64 =
requires { in_bounds (3*n) }
ensures { result = mult3 n }
3*n
(*CVC4 runs out of time while trying to prove this case but then can prove it when it tries to get a counterexample.
Z3 proves it.*)
let f_pred_mult3 (n: uint64) : uint64 =
requires { in_bounds (3*n) }
ensures { post_mult3 n result }
3*n
(* ------- Argument in a Record --------- *)
predicate post_record (s: storage) (result: uint64) =
result = 3*s.x
(*Proved by Z3 and CVC4*)
let f_record (s: storage) : uint64 =
ensures { result = 3*s.x }
3*s.x
(*CVC4 runs out of time while trying to prove this case but then can prove it when it tries to get a counterexample.
Z3 proves it.*)
let f_record_pred (s: storage) : uint64 =
ensures { post_record s result }
3*s.x
predicate post_record_mult3 (s: storage) (result: uint64) =
result = mult3 s.x
(*CVC4 runs out of time while trying to prove this case but then can prove it when it tries to get a counterexample.
Z3 proves it.*)
let f_record_mult3 (s: storage) : uint64 =
ensures { result = mult3 s.x }
3*s.x
(*CVC4 runs out of time while trying to prove this case but then can prove it when it tries to get a counterexample.
Z3 proves it.*)
let f_record_pred_mult3 (s: storage) : uint64 =
ensures { post_record s result }
3*s.x
(* ------- Result in a List --------- *)
predicate post_list (n: uint64) (result: list uint64) =
result = Cons (mult3 n) Nil
(*Proved by Z3 and CVC4*)
let f_list (n: uint64) : list uint64 =
requires { in_bounds (3*n) }
ensures { result = Cons (mult3 n) Nil }
Cons (3*n) Nil
(*CVC4 runs out of time while trying to prove this case but then can prove it when it tries to get a counterexample.
Z3 run out of time both when trying to prove it and when generating a counterexample.*)
let f_list_pred (n: uint64) : list uint64 =
requires { in_bounds (3*n) }
ensures { post_list n result }
Cons (3*n) Nil
(* ------- Argument in a Record and Result in a List --------- *)
predicate post_list_record (s: storage) (result : list uint64) =
result = Cons (mult3 s.x) Nil
(*CVC4 runs out of time both when trying to prove it and generating a counterexample.
Z3 proves it.*)
let f_record_list (s: storage) : list uint64 =
ensures { result = Cons (mult3 s.x) Nil }
Cons (3*s.x) Nil
(*CVC4 runs out of time while trying to prove this case but then can prove it when it tries to get a counterexample.
Z3 runs out of time when trying to prove it and runs out of memory when generating a counterexample.*)
let f_record_list_pred (s: storage) : list uint64 =
ensures { post_list_record s result }
Cons (3*s.x) Nil
end
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
