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

Jean-Christophe Filliâtre Jean-Christophe.Filliatre at lri.fr
Wed Nov 7 09:29:38 CET 2012

> 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.


More information about the Why3-club mailing list