[Why3-club] how to prove a type is inhabited?

Raphael Rieu-Helft raphael.rieu-helft at lri.fr
Thu Feb 21 15:51:03 CET 2019


Hello,

Use the keyword `by`:

type t = { x = array int } invariant { length x > 0 /\ x[0] > 0 } by { x 
= Array.make 1 1 }

Raphaƫl

On 21/02/2019 15:47, Alan Schmitt wrote:
> Hello,
>
> I have this very simple specification that creates a type and states an
> invariant for it.
>
> module Test
>
> use int.Int
> use array.Array
>
> type t = { x : array int }
> invariant { length x > 0 /\ x[0] > 0 }
>
> end
>
> When I load this in why3, I'm asked to check that the type is inhabited.
> Is there a way to provide a witness, as why3 is unable to guess it?
>
> Thanks,
>
> Alan
>
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20190221/3d50f8bb/attachment.html>


More information about the Why3-club mailing list