[Why3-club] syntactic sugar
moy at adacore.com
Mon Sep 24 12:24:22 CEST 2012
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. To
see that, replace your call to "M.make n n 0" by a call to "M.make n
(n+1) 0". You'll see in why3ide that the goal "square_board result" has
been replaced by "n = n+1". So inlining of the postcondition of M.make
and of the predicate allows Why3 to reduce the original postcondition to
"n=n" which it discards as trivially true.
> Am I using "predicate" in a wrong way?
No, that's fine.
Yannick Moy, Senior Software Engineer, AdaCore
More information about the Why3-club