[Why3-club] "if formula then" in expressions?

Alan Schmitt alan.schmitt at polytechnique.org
Wed Nov 7 09:30:39 CET 2012


Guillaume Melquiond <guillaume.melquiond at inria.fr> writes:

> Le mercredi 07 novembre 2012 à 08:49 +0100, Alan Schmitt a écrit :
>> Hello,
>> 
>> Why3 accepts program expressions of the form "if formula then ...". This
>> does not seem to make sense as such a program could not be executed. Is
>> this a bug or am I missing something?
>
> This is not a bug. Possibly, the thing you are missing is that "x < y"
> is a formula. (Sure, decidable formulas are just a tiny part of all the
> formulas, so I understand how troubling such if-then-else expressions
> might be.)

Well, according to Figures 7.3 and 7.7 of the manual, it's both a
formula and an expression (since '<' is an "infix-op"). What I have
trouble understanding is the mismatch between Figure 7.7 (where an "if"
can only take an expression as conditional argument) and the
implementation.

Related questions are: what is the type of the expression (not formula)
"x = y"? And what is the expected type of "expr" in the expression "if
expr then ..."?

Thanks,

Alan



More information about the Why3-club mailing list