-- Johannes Kanig (2014-02-12)
>
>
>> your example. There is a catch, however. Internally, Why3 keeps a
>> single formula for a precondition, not a list of formulas. That is,
>> "requires { true }" is the same as no "requires" at all. I can imagine
>> that you wouldn't want to see a subgoal "true" in your example if f2
>> didn't have preconditions, which means that you want to distinguish
>> the two cases. Is that right?
>
> I'm not sure, in any case it never came up up to now. So I would say do as
> you wish!
In our translation to Why3, we use "requires { true }" when there is no
explicit precondition on the Ada subprogram, but we do not end with a subgoal
of "true" in that case, so it must be discarded by the WP.
--
Yannick Moy, Senior Software Engineer, AdaCore
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
