[Why3-club] constants

Julia Lawall julia.lawall at lip6.fr
Wed Mar 20 12:05:57 CET 2019



On Wed, 20 Mar 2019, Mario Pereira wrote:

> Hi,
>
> Would it help if you attach a postcondition to your constants definition?
>
>    let constant realtime = 0
>      ensures { result = 0 }
>    let constant timeshare = 1
>      ensures { result = 1 }

I'll try that.  Thanks!

julia

>
> Best regards
> --
> Mário
>
> Le 20/03/19 à 10:49, Julia Lawall a écrit :
> >
> > 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
> >>
> > _______________________________________________
> > 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