[Why3-club] loops and "Exit" exception [K211-002]

Johannes Kanig kanig at adacore.com
Tue Mar 15 09:24:54 CET 2011


On 03/15/2011 09:04 AM, Jean-Christophe Filliâtre wrote:
>> * Model the exit statement with another exception, as follows:
> This should work fine.

>> * Expose the internal infinite loop statement to the user.
> 
> We could do that. I'm not enclined to introduce yet another keyword, but
> we may consider the syntax
> 
>     do invariant {fmla} variant {term} expr done
> 
> for infinite loops. Would that be ok?

Yes of course this would be OK. We will first experiment with the other
option (while loops + exceptions), as you and Yannick say that this
works fine.

-- 
Johannes Kanig <kanig at adacore.com>



More information about the Why3-club mailing list