[Why3-club] special "ignoring" construct for VC creation

Johannes Kanig kanig at adacore.com
Fri Nov 18 17:24:40 CET 2011

On 11/14/2011 05:46 PM, Yannick Moy wrote:
>   ___ignore(<Why code for checking absence of runtime errors in an expression>)

It just occurred to me that these ignored code blocks often contain if
expressions, or short-circuit operators, as they are translations of Ada
boolean expressions, which will often contain "and then" or "or else".
So this puts an additional burden on the WP calculus because it has to
generate VCs for all those possible paths.

> I wondered if this is a problem others face, and if there could be a way to have
> a special "ignore" construct in Why, so that VCs never contain in their context
> the hypotheses for such ignored blocks.

So such a special ignore construct would be useful for us in two ways,
it would act as a "cut" and reduce the number of paths in a function,
and reduce the context to consider for each VC.

What do you think?

Johannes Kanig <kanig at adacore.com>

More information about the Why3-club mailing list