[Why3-club] constants

Julia Lawall julia.lawall at lip6.fr
Tue Mar 19 22:36:34 CET 2019


I have some definitions:

let constant realtime = 0
let constant timeshare = 1

However, subsequently why3 seems to have trouble proving things involving
these values, particularly things that involve knowing that realtime and
timeshare don't have the same value.  Inlining the values makes the proofs
work out, but is not great for readability.  In the end, I put

0(*realtime*)
1(*timeshare*)

at all the usage sites.  Is there a way to cause uses of realtime and
timeshare to behave exactly like uses of 0 and 1?

thanks,
julia


More information about the Why3-club mailing list