[Why3-club] types with invariants

Guillaume Melquiond guillaume.melquiond at inria.fr
Wed Jul 4 07:35:40 CEST 2018


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


More information about the Why3-club mailing list