Is there an example that uses a while loop to iterate over the elements of
a list? I tried:
while (not(!rdy = Nil))
do
variant { !rdy }
match !rdy with
Nil -> ()
| Cons t ts ->
rdy := ts;
end;
done
but at the call site of the function that contains this code, it complains
that:
warning: this expression may diverge, which is not stated in the
specification
Can I just ignore the warning?
I would like the whyml code to look like what one would most naturally
write in an imperative language, so I didn't want to wriet a recursive
function.
thanks,
julia
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
