Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

loops.mlw 614 Bytes
Newer Older
1
module M
2

3 4
use int.Int
use ref.Ref
5

6 7
(** 1. A loop increasing [i] up to 10. *)

Andrei Paskevich's avatar
Andrei Paskevich committed
8
val i : ref int
9

10
let loop1 (_u:unit) requires { !i <= 10 } ensures { !i = 10 }
11
= while !i < 10 do
12
    invariant { !i <= 10 } variant { 10 - !i }
13 14 15 16 17 18
    i := !i + 1
  done


(** 2. The same loop, followed by a function call. *)

Andrei Paskevich's avatar
Andrei Paskevich committed
19
val x: ref int
20

21
let negate (_u:unit) ensures { !x = - (old !x) } = x := - !x
22

23
let loop2 (_u:unit) requires { !x <= 10 }
24
= begin
25
    while !x < 10 do invariant { !x <= 10 } variant { 10 - !x }
26 27
      x := !x + 1
    done;
28
    assert { !x = 10 };
29
    if !x > 0 then (negate ());
30
    assert { !x = -10 }
31 32
  end

33
end