mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
20 lines
265 B
Plaintext
20 lines
265 B
Plaintext
module While6
|
|
|
|
use int.Int
|
|
use ref.Ref
|
|
|
|
exception Myexc int
|
|
|
|
let b [@infer] [@bddinfer] (_:int) : int
|
|
ensures { result = 102 }
|
|
=
|
|
let i = ref 0 in
|
|
i := 0;
|
|
while !i < 100 do
|
|
variant { 10 - !i }
|
|
i := !i + 6;
|
|
done;
|
|
!i
|
|
|
|
end
|