Le 03/07/2018 à 11:44, Julia Lawall a écrit :
The "cores" type has to be abstract, since "cores'invariant" has to hold for
any of its inhabitants. (Otherwise, the proof context would be trivially
inconsistent, in the general case.) As a consequence, "current" cannot have a
concrete definition.
Nonetheless, none of the information is missing. Indeed, "current" is a total
function, and "cores'invariant" fully specifies it.
I see that it has the type of a function, but I'm not sure how to actually
extract the value that is found in that field at the moment.
"current foo" is exactly the value found in the "current" field of the
"foo" value.
Since you did not provide a testcase, let me propose one:
type t = { bar : int } invariant { bar > 0 }
let f () ensures { bar result <> 2 } = { bar = 1 }
Here Why3 requires you to prove three theorems:
1. non-emptyness of t: exists bar, bar > 0
2. safety of f: 1 > 0
3. soundness of f: forall result, bar result = 1 -> bar result <> 2
Notice how the last theorem is provable whether "bar" is an unfoldable
definition or not.
Best regards,
Guillaume
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
