[Why3-club] types with invariants

Julia Lawall julia.lawall at lip6.fr
Tue Jul 3 10:44:29 CEST 2018


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?

thanks,
julia


More information about the Why3-club mailing list