-- 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