Hello Guillaume,
Le 19/08/2016 à 14:48, Guillaume Melquiond a écrit :
> Don't bother, it should be easy enough to fix (assuming my
> interpretation is correct).
[ ~20 minutes later: ]
> And the patch is now on the bugfix/v0.87 branch.
Thanks!
>> > Is there a work-around?
> In the meantime, using your own boolean type rather than the standard
> one should do the trick.
I failed to do it despite several attempts, see attached execute_test.mlw:
"""
$ why3 -C why3.config execute execute_test.mlw Execute_test.test
Execution of Execute_test.test ():
type: bool
Execution error: Cannot execute expression
match ((b1,
b2)) with
| DFalse, DTrue -> (DTrue)
| _, _ -> (DFalse)
end
"""
It is also apparently not possible to overwrite default 'bool' type.
For now, I removed the match constructions in my code. Much less
readable but it works. :-( Fortunately, thanks to Why3, I found a bug in
the rewritten code because all my properties where not replayed. :-)
I also tried OCaml code generation as another workaround. It works but
it is much more cumbersome to use.
Regarding the output of execute, it would be nicer if records could be
printed with their source code format.
I.e., instead of:
"""
type: (output_t, internal_state_t)
result:
((mk_output_t true false false true true),
(mk_internal_state_t false false (mk_counter_t 1 1 false)))
"""
have:
"""
result:
({ x1 = true; x2 = false; x3 = false; x4 = true; x5 = true }, [...])
"""
It would be more readable.
Another nice feature would be a step-by-step execution of the WhyML
code, to see intermediate computations in the program, like in a debugger.
Last step would be to combine counter-example generation and execution,
the produced counter-example being fed to 'why3 execute'. I know I know,
Why3 is open-source and I should just provide a patch. :-)
Thank you for the quick feedback!
Best regards,
david
module Execute_test
type bool_t = DTrue | DFalse (* work-around for execute bug in Why3 0.87.0 *)
function bool_t_of_bool (b : bool) : bool_t
= match b with True -> DTrue | False -> DFalse end
function bool_of_bool_t (b : bool_t) : bool
= match b with DTrue -> True | DFalse -> False end
let f (cmd_previous cmd_current : bool) : bool
= let b1, b2 = (bool_t_of_bool cmd_previous, bool_t_of_bool cmd_current) in
let r = match b1, b2 with
| DFalse, DTrue -> DTrue
| _, _ -> DFalse
end in
bool_of_bool_t r
let test ()
= f False True
end
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/mailman/listinfo/why3-club
