[Why3-club] constants

Mario Pereira mariojppereira at gmail.com
Wed Mar 20 12:00:43 CET 2019


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 }

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


More information about the Why3-club mailing list