On Wed, 4 Jul 2018, Guillaume Melquiond wrote:
> 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.
Thanks for the example. I am travelling at the moment, but will try it as
soon as possible.
julia
>
> Best regards,
>
> Guillaume
> _______________________________________________
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
