[Why3-club] Several remarks and questions on Why3

David MENTRE dmentre at linux-france.org
Thu Aug 18 10:04:49 CEST 2016


Hello David,

Le 07/06/2016 à 13:41, David Hauzar a écrit :
> Why3 counterexamples are currently used mainly internally by the SPARK
> tool, but we should indeed put at least some basic documentation to Why3
> manual...
> 
> To produce a counterexample, terms (e.g., WhyML variables) must be
> explicitly marked using the label "model". See attached Why theory
> cvc4-models.why and WhyML program cvc4-models.mlw for several examples.
> 
> The best way how to see Why3 counterexamples is to use Why3IDE. If
> counterexamples are enabled (File -> Preferences -> General -> get
> counter-example) and a counterexample is generated for a selected goal,
> a goal annotated with the counterexample (in comments) is displayed in a
> tab Counter-example.
> 
> For more information about counterexamples, see this paper
> (https://hal.inria.fr/hal-01314885).

Thanks to the information you provided, I could play with counter
example generation with Why3 (0.87.0) and Z3 (4.4.1).

I still have two questions:

 1. In function k in attached WhyML file, there are two "returns"
clause. Two counter examples are generated (for line 26) but for the
second one the counter example is on "s.x" variable while I expected it
on "s.y". Indeed, in function k2 when I add a "model_vc" annotation,
then the right counter example is generated on s.y. Would it be a bug?

 2. In my test file, counter example are correctly generated. However,
in my real life example, no counter example is generated. It appears
that in this latter case Z3 is killed by why3-cpulimit while in the
former test case Z3 returns an output by itself before the time limit.

In attached example:
"""
<0.196102>Call_provers: command is:
/home/student/.opam/4.02.3/lib/why3/why3-cpulimit
            10 1000 -s z3 -smt2 sat.random_seed=42 nlsat.randomize=false
            smt.random_seed=42
            /tmp/why_d5a4ee_counter_example_test-T-WP_parameter_k2.smt2
<0.206458>Call_provers: exited with status 0
<0.206500>Call_provers: prover output:
sat
((s3 0)
 (s_vc_constant1 0))
(:reason-unknown )
why3cpulimit time : 0.000000 s

<0.206535>Call_provers: model:
<0.206546>Call_provers: File
/home/student/.opam/4.02.3/share/why3/theories/int.why:
Line 17:
s.y = 0File counter_example_test.mlw:
Line 31:
s.y = 0
counter_example_test.mlw Counter_example WP_parameter k2 : Unknown (0.00s)
Counter-example model:File
/home/student/.opam/4.02.3/share/why3/theories/int.why:
Line 17:
s.y = 0File counter_example_test.mlw:
Line 31:
s.y = 0
<0.206575>
"""

In my real life example:
"""
<1.130494>Call_provers: command is:
/home/student/.opam/4.02.3/lib/why3/why3-cpulimit
            1 1000 -s z3 -smt2 sat.random_seed=42 nlsat.randomize=false
            smt.random_seed=42

/tmp/why_729348_carriagemnlinemncontrol-T-WP_parameter_carriage_line_control_cycle.smt2
<2.130358>Call_provers: killed by signal 24
<2.130383>Call_provers: prover output:
why3cpulimit time : 0.990000 s

<2.130417>Call_provers: model:
<2.130424>Call_provers:
carriage-line-control.mlw Carriage_Line_Control WP_parameter
carriage_line_control_cycle : Timeout (0.99s)
"""

Do you know a way to generate a counter-example when time limit is
reached? By playing with Z3 options (e.g. using option -T)? Would it be
the same with CVC4? How do you handle the case in SPARK?

Best regards,
david

-------------- next part --------------
module Counter_example

  use import int.Int

  type s_t = {
    x : int;
    y : int;
  }

  let f (x "model" : int) : int
  ensures { result > 0 }
  = x+x

  let g1 (x : int) : int
  ensures { result = x + x }
  = x+x

  let g2 (x "model" : int) : int
  ensures { result > 0 }
  = g1 x

  let h (x "model" : int) : int
  returns { r -> r > 0 }
  = g1 x

  let k (s "model" : s_t) : s_t
  returns { r -> r.x > 0 }
  returns { r -> r.y > 0 } (* FIXME: why counter example is s.x = 0? *)
  = { x = g1 s.x; y = g1 s.y }

  let k2 (s "model" : s_t) : s_t
  returns { r -> r.x > 0 }
  returns { r -> "model_vc" r.y > 0 }
  = { x = g1 s.x; y = g1 s.y }

end

(*
$ why3 prove -C why3.config -P z3 --get-ce -a split_goal_wp counter_example_test.mlw
counter_example_test.mlw Counter_example WP_parameter f : Unknown (0.00s)
Counter-example model:File counter_example_test.mlw:
Line 10:
x = 0
counter_example_test.mlw Counter_example WP_parameter g1 : Valid (0.00s)
counter_example_test.mlw Counter_example WP_parameter g2 : Unknown (0.00s)
Counter-example model:File counter_example_test.mlw:
Line 18:
x = 0
counter_example_test.mlw Counter_example WP_parameter h : Unknown (0.01s)
Counter-example model:File counter_example_test.mlw:
Line 22:
x = 0
counter_example_test.mlw Counter_example WP_parameter k : Unknown (0.00s)
Counter-example model:File counter_example_test.mlw:
Line 26:
s.x = 0
counter_example_test.mlw Counter_example WP_parameter k : Unknown (0.00s)
Counter-example model:File counter_example_test.mlw:
Line 26:
s.x = 0
counter_example_test.mlw Counter_example WP_parameter k2 : Unknown (0.00s)
Counter-example model:File counter_example_test.mlw:
Line 31:
s.x = 0
counter_example_test.mlw Counter_example WP_parameter k2 : Unknown (0.00s)
Counter-example model:File /home/student/.opam/4.02.3/share/why3/theories/int.why:
Line 17:
s.y = 0File counter_example_test.mlw:
Line 31:
s.y = 0
*)


More information about the Why3-club mailing list