[Why3-club] types with invariants

Julia Lawall julia.lawall at lip6.fr
Tue Jul 3 11:44:30 CEST 2018



On Tue, 3 Jul 2018, Guillaume Melquiond wrote:

> 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 -> ...

Parameter current: cores -> array (list thread).

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

In our case, the invariant does provide information about all of the
fields, so perhaps it could be used to get access to the fields in some
way, although I don't see how at the memont.  But I guess that in general
the invariant might only concern some of the fields, if there is no extra
information to specify about them.

> 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 founf in that field at the moment.

thanks,
julia


More information about the Why3-club mailing list