[Why3-club] syntactic sugar

Yannick Moy 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 mailing list