[Why3-club] types with invariants

Guillaume Melquiond guillaume.melquiond at inria.fr
Tue Jul 3 11:15:53 CEST 2018


Le 03/07/2018 à 10:44, Julia Lawall a écrit :
> It seems that as soon as we put an invariant on a type, like:
> 
> type cores =
>      { cid : array int;
>        cload : array int;
>        current : array state;
>        ready : matrix state; (* allow multiple ready states *)
>        blocked : array state }
> invariant { valid_cores_pred cid cload current blocked ready }
> 
> then in coq it is no longer possible to access the fields of the
> structure.  Ie, eg current is no longer a definition that can be unfolded
> to access a field, but is rather a parameter that nothing is known about.
> Is this intentional?  Is the way around it to define some getter-like
> functions?

It is intentional. Moreover, "current" is already a getter, so you don't 
need to define additional ones. Given your definition above, you should 
obtain a Coq script that looks as follows:

Axiom cores: Type.
Axiom current: cores -> ...
Axiom cores'invariant:
   forall self, valid_cores_pred ... (current self) ...

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.

Best regards,

Guillaume


More information about the Why3-club mailing list