[Why3-club] "if formula then" in expressions?
alan.schmitt at polytechnique.org
Wed Nov 7 09:36:12 CET 2012
Jean-Christophe Filliâtre <Jean-Christophe.Filliatre at lri.fr> writes:
>> 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. Generally speaking, any logical term or formula is
> accepted in a program, following one of the key idea of Hoare's logic.
> The question of being executable or not is orthogonal. In the (still
> under development) extraction to OCaml, pieces of WhyML programs that
> are not executable (uninterpreted symbols, inductive predicates, etc.)
> are turned into program place holders to be filled by the user.
OK, it makes sense.
It may be useful to make this explicit by adding formulas to expressions
in the manual.
More information about the Why3-club