[Why3-club] syntactic sugar

Alan Schmitt alan.schmitt at polytechnique.org
Mon Sep 24 13:51:58 CEST 2012


Yannick Moy <moy at adacore.com> writes:

> On 09/24/2012 11:57 AM, Alan Schmitt wrote:
>
>> When I generate the proof obligation, I only have to prove the
>> precondition of M.make (its first two arguments are greater than 0) and
>> the first postcondition of mk_board. For some reason, I don't have to
>> show that "square_board result" holds.
>
> Why3 is able to realize that "square_board result" is always true.

I did not know Why3 was this smart. Thanks!

Alan



More information about the Why3-club mailing list