1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
|
(* Quelques preuves sur des programmes simples,
* juste histoire d'avoir un petit bench.
*)
Require Correctness.
Require Omega.
Global Variable x : Z ref.
Global Variable y : Z ref.
Global Variable z : Z ref.
Global Variable i : Z ref.
Global Variable j : Z ref.
Global Variable n : Z ref.
Global Variable m : Z ref.
Variable r : Z.
Variable N : Z.
Global Variable t : array N of Z.
(**********************************************************************)
Require Exchange.
Require ArrayPermut.
Correctness swap
fun (N:Z)(t:array N of Z)(i,j:Z) ->
{ `0 <= i < N` /\ `0 <= j < N` }
(let v = t[i] in
begin
t[i] := t[j];
t[j] := v
end)
{ (exchange t t@ i j) }.
Proof.
Auto with datatypes.
Save.
Correctness downheap
let rec downheap (N:Z)(t:array N of Z) : unit { variant `0` } =
(swap N t 0 0) { True }
.
(**********************************************************************)
Global Variable x : Z ref.
Debug on.
Correctness assign0 (x := 0) { `x=0` }.
Save.
(**********************************************************************)
Global Variable i : Z ref.
Debug on.
Correctness assign1 { `0 <= i` } (i := !i + 1) { `0 < i` }.
Omega.
Save.
(**********************************************************************)
Global Variable i : Z ref.
Debug on.
Correctness if0 { `0 <= i` } (if !i>0 then i:=!i-1 else tt) { `0 <= i` }.
Omega.
Save.
(**********************************************************************)
Global Variable i : Z ref.
Debug on.
Correctness assert0 { `0 <= i` } begin assert { `i=2` }; i:=!i-1 end { `i=1` }.
(**********************************************************************)
Correctness echange
{ `0 <= i < N` /\ `0 <= j < N` }
begin
label B;
x := t[!i]; t[!i] := t[!j]; t[!j] := !x;
assert { #t[i] = #t@B[j] /\ #t[j] = #t@B[i] }
end.
Proof.
Auto with datatypes.
Save.
(**********************************************************************)
(*
* while x <= y do x := x+1 done { y < x }
*)
Correctness incrementation
while !x < !y do
{ invariant True variant `(Zs y)-x` }
x := !x + 1
done
{ `y < x` }.
Proof.
Exact (Zwf_well_founded `0`).
Unfold Zwf. Omega.
Exact I.
Save.
(************************************************************************)
Correctness pivot1
begin
while (Z_lt_ge_dec !i r) do
{ invariant True variant (Zminus (Zs r) i) } i := (Zs !i)
done;
while (Z_lt_ge_dec r !j) do
{ invariant True variant (Zminus (Zs j) r) } j := (Zpred !j)
done
end
{ `j <= r` /\ `r <= i` }.
Proof.
Exact (Zwf_well_founded `0`).
Unfold Zwf. Omega.
Exact I.
Exact (Zwf_well_founded `0`).
Unfold Zwf. Unfold Zpred. Omega.
Exact I.
Omega.
Save.
|
