mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
26 lines
340 B
Plaintext
26 lines
340 B
Plaintext
module While3
|
|
|
|
use int.Int
|
|
use ref.Ref
|
|
|
|
let b [@infer] [@bddinfer] (_:int) : int
|
|
ensures { result = 0 }
|
|
=
|
|
let i = ref 0 in
|
|
let j = ref 0 in
|
|
j := 0;
|
|
i := 1;
|
|
while !i < 10 do
|
|
variant { 10 - !i }
|
|
i := !i + 1;
|
|
j := !j + 2;
|
|
done;
|
|
while !i > 1 do
|
|
variant { !i }
|
|
i := !i - 1;
|
|
j := !j - 2;
|
|
done;
|
|
!j
|
|
|
|
end
|