[Why3-club] constants

Jean-Christophe Filliatre Jean-Christophe.Filliatre at lri.fr
Wed Mar 20 11:42:49 CET 2019


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?

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
> 


More information about the Why3-club mailing list