[Why3-club] constants

Julia Lawall julia.lawall at lip6.fr
Wed Mar 20 11:49:48 CET 2019



On Wed, 20 Mar 2019, Jean-Christophe Filliatre wrote:

> Dear Julia,
>
> With a goal as simple as
>
>   let constant realtime = 0
>   let constant timeshare = 1
>   goal G: realtime <> timeshare
>
> I get an SMT input file (e.g. for CVC4) which is
>
>   (assert
>   ;; G
>    ;; File "test.mlw", line 3, characters 5-6
>     (not (not (= 0 1))))
>
> and (obviously) proved with no difficulty. I get the same SMT input file
> with a program VC such as
>
>   let f () ensures { realtime <> timeshare } = ()
>
> for instance. So I guess you are referring to a more complex situation.
> Could you please tell us in which situation you have trouble knowing
> that realtime and timeshare have different values?

OK, I think it woud be hard to cut down my code to something
understandable that would show the problem.  I was hoping that constants
would be just inlined away, like for a #define in C.  But perhaps there
are good reasons for not doing that.

thanks,
julia


>
> Best regards,
> --
> Jean-Christophe
>
> On 3/19/19 10:36 PM, Julia Lawall wrote:
> > I have some definitions:
> >
> > let constant realtime = 0
> > let constant timeshare = 1
> >
> > However, subsequently why3 seems to have trouble proving things involving
> > these values, particularly things that involve knowing that realtime and
> > timeshare don't have the same value.  Inlining the values makes the proofs
> > work out, but is not great for readability.  In the end, I put
> >
> > 0(*realtime*)
> > 1(*timeshare*)
> >
> > at all the usage sites.  Is there a way to cause uses of realtime and
> > timeshare to behave exactly like uses of 0 and 1?
> >
> > thanks,
> > julia
> > _______________________________________________
> > Why3-club mailing list
> > Why3-club at lists.gforge.inria.fr
> > https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> >
> _______________________________________________
> 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