[Why3-club] loops and "Exit" exception

Jean-Christophe Filliâtre Jean-Christophe.Filliatre at lri.fr
Tue Mar 15 09:04:38 CET 2011

Hi Johannes,

> In Why3, this exception has an internal name "%Exit", which cannot be
> used by programs. This rules out the trick I just described.
> What do you think whould be the best way to translate such Ada loops to
> Why3? I see three possibilities, two of which would require
> modifications to Why3:
> * Render the internal exception accessible, as in Why2

As you said, this is indeed a bad solution and I would prefer avoiding it.

> * Model the exit statement with another exception, as follows:
>    exception Ada_Exit
>    try
>       while C do
>             if C then raise Ada_Exit
>       done
>    with Ada_Exit ->  ()
>    This is a clean solution and does not require any changes to Why3. The
> only problem I have with it is that now there are *two* exceptions and
> exception handling blocks around the loop. I don't know very well the
> behavior of Why3 in this case; do you think it could be a problem?

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?


More information about the Why3-club mailing list