[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