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

Julia Lawall julia.lawall at lip6.fr
Thu Feb 21 16:46:04 CET 2019



On Thu, 21 Feb 2019, Raphael Rieu-Helft wrote:

>
> Hello,
>
> Use the keyword `by`:
>
> type t = { x = array int } invariant { length x > 0 /\ x[0] > 0 } by { x =
> Array.make 1 1 }

Is by useful for anything else?  Sometimes I know that a particular lemma
should be useful for proving something, and from the English meaning of
"by" it would be nice to be able to say by useful_lemma.  But that doesn't
work.

julia

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


More information about the Why3-club mailing list