[Why3-club] loops and "Exit" exception

Johannes Kanig kanig at adacore.com
Mon Mar 14 15:05:03 CET 2011


Hi Why3-Club,

While investigating how to migrate from Why2 to Why3, I came across the
case of loops. Similarly to Why2, while loops in Why3 are internally
represented by an infinite loop that raises an exception when the
looping condition is false:

while C do
  Body;
done

becomes

try
  loop (* infinite loop *)
    if not C then raise Exit;
    Body
  done
with Exit -> ()

In our current usage of Why2, we take advantage of this mechanism to
model the Ada construct

  exit when C;

which exits the loop whenever C is true, and can be written anywhere in
the loop. In Why2, we can model this as

if C then raise Exit

where "Exit" is the aforementioned exception.

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. I understand why
the Why3 team has hidden the exception, and our usage of it is a bit of
a hack, even though it should be correct. I consider this not a very
clean solution.

* 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?

* Expose the internal infinite loop statement to the user. This would
allow us to do the described construction ourselves, avoiding two
different exceptions:
  try
    loop
       if C then raise Ada_Exit
    done
  with Ada_Exit -> ()

 As in Ada, the simplest form of a loop is precisely an infinite loop,
this would be the easiest way to model Ada loops for us.

Thinking of it, the solution that "hijacks" the internal Why exception
is only correct when we do not allow exiting of an outer loop, something
which is possible in Ada using so-called named loops. So the other two
solutions are definitely superior.

Which solution (or maybe another one) does the Why team recommend?

P.S.: I put the hi-lite list in CC, which might be interested.

-- 
Johannes Kanig <kanig at adacore.com>



More information about the Why3-club mailing list