ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity
Files
master
why3/examples_in_progress/maximal_rectangle.mlw
MARCHE Claude 72a423af11 move examples in progress outside the examples directory
2023-03-08 12:26:34 +00:00

504 lines
14 KiB
Plaintext
Raw Permalink Blame History

(* Grands rectangles - Concours d'Informatique X-ENS PC 2014 *)
(* Partie I *)
module Search_in_array
use int.Int
use ref.Ref
use array.Array
(* use int.MinMax*)
(* Qeustion 1 *)
let nombreZeroDroite i tab n
requires { 1 <= i <= n < tab.length }
requires { forall k. i <= k <= n -> tab[k] = 1 \/ tab[k] = 0 }
ensures { i <= result <= n + 1 }
ensures { forall k. i <= k < result -> tab[k] = 0 }
ensures { result <= n -> tab[result] = 1 }
=
let j = ref i in
while !j <= n && tab[!j] = 0 do
variant { n - !j }
invariant { i <= !j <= n + 1}
invariant { forall k. i <= k < !j -> tab[k] = 0 }
j := !j + 1;
done;
!j
(* Question 2 *)
let nombreZeroMaximum tab n =
requires { 1 <= n < tab.length }
requires { forall k. 1 <= k <= n -> tab[k] = 1 \/ tab[k] = 0 }
ensures { let (p,q) = result in
(1 <= p <= q <= n + 1) /\
(forall k. p <= k < q -> tab[k] = 0) }
ensures { let (p,q) = result in
forall i j.
(1 <= i <= j <= n + 1) ->
(forall k. i <= k < j -> tab[k] = 0) ->
j - i <= q - p }
let p = ref 1 in
let q = ref 1 in
let i = ref 1 in
while !i <= n do
variant { n - !i }
invariant { 1 <= !i <= n + 1 }
invariant { 1 <= !p <= !q <= !i }
invariant { forall k. !p <= k < !q -> tab[k]= 0 }
(*invariant { 2 <= !i -> !q <= n -> tab[!q] = 1 }*)
invariant { forall a b.
(1 <= a <= b <= !i) ->
(forall k. a <= k < b -> tab[k] = 0) ->
b - a <= !q - !p }
invariant { 1 < !i <= n -> (tab[!i] = 1 \/ tab[!i-1] = 1) }
let next = nombreZeroDroite !i tab n in
begin
if next - !i > !q - !p then begin p:= !i; q := next end;
i:= if !i = next then !i + 1 else next;
end
done;
(!p, !q)
(*
(* Question 1 *)
let nombreZeroDroite i tab n
requires { 1 <= i <= n }
requires { n = tab.length - 1 }
requires { forall k. i <= k <= n -> tab[k] = 1 \/ tab[k] = 0 }
ensures { 0 <= result <= n - i + 1 }
ensures { forall k. 0 <= k < result -> tab[i + k] = 0 }
ensures { let j = i + result in j <= n -> tab[j] = 1 }
=
let j = ref i in
while !j <= n && tab[!j] = 0 do
variant { n - !j }
invariant { 0 <= !j - i <= n - i + 1}
invariant { forall k. 0 <= k < (!j - i) -> tab[i + k] = 0 }
j := !j + 1;
done;
!j - i
let test_0 () =
let tab = make 14 0 in
tab[0]<- (-1);
tab[1] <- 0; tab[2] <- 0;
tab[3] <- 1; tab[4] <- 1;
tab[5] <- 0; tab[6] <- 0; tab[7] <- 0;
tab[8] <- 1;
tab[9] <- 0; tab[10] <- 0; tab[11] <- 0;
tab[12] <- 1; tab[13] <- 1;
let n1 = nombreZeroDroite 4 tab 13 in
assert { n1 = 0 };
let n2 = nombreZeroDroite 6 tab 13 in
assert { n2 = 2 }
(* Question 2 *)
(*TODO*)
let nombreZeroMaximum tab n =
requires { 1 <= n /\ n = tab.length - 1}
requires { forall k. 1 <= k <= n -> tab[k] = 1 \/ tab[k] = 0 }
ensures { exists i.
(1 <= i <= n) /\
(0 <= result <= n - i + 1) /\
(forall k. 0 <= k < result -> tab[i + k] = 0) /\
(i + result <= n -> tab[i + result] = 1) }
ensures { forall j ofs.
(1 <= j <= n) ->
(0 <= ofs <= n - j + 1) ->
(forall k. 0 <= k < ofs -> tab[j + k] = 0) ->
ofs <= result }
let max = ref (nombreZeroDroite 1 tab n) in
let ghost max_i = ref 1 in
let i = ref (if !max = 0 then 2 else !max + 1) in
while !i <= n do
variant { n - !i }
invariant { 1 <= !i <= n + 1}
invariant { 1 <= !max_i < !i }
invariant {0 <= !max < !i - !max_i + 1 }
invariant {forall k. 0 <= k < !max -> tab[!max_i + k]= 0 }
invariant {!max_i + !max <= n -> tab[!max_i + !max] = 1 }
invariant { forall j ofs.
1 <= j <= !i ->
(0 <= ofs <= !i - j + 1) ->
(forall k. 0 <= k < ofs -> tab[j + k] = 0) ->
ofs <= !max }
let ofs_i = nombreZeroDroite !i tab n in
begin
if ofs_i > !max then begin max := ofs_i; max_i := !i end;
if ofs_i = 0 then i := !i + 1 else i:= !i + ofs_i;
end
done;
!max
*)
end
(* Partie II. De la 1D vers la 2D *)
(* Partie III. Algorithme optimisé *)
(*Questions 7 - 12 *)
(*
let rec calculeL_aux i histo l =
let j = ref i in
while !j > 1 && histo.(!j-1) >= histo.(i) do
j := calculeL_aux (!j-1) histo l
done;
l.(i) <- !j; !j
let calculeL histo =
let l = Array.make (Array.length histo) 0 in
let i = ref (Array.length histo - 1) in
while !i > 0 do
let j = calculeL_aux !i histo l in
if j < !i then i := j else i := !i - 1
done;
l
let rec calculeR_aux i histo r =
let j = ref i in
while !j < Array.length histo - 1 && histo.(!j+1) >= histo.(i) do
j := calculeR_aux (!j+1) histo r
done;
r.(i) <- !j; !j
let calculeR histo =
let r = Array.make (Array.length histo) 0 in
let i = ref 1 in
while !i < Array.length histo do
let j = calculeR_aux !i histo r in
if j > !i then i := j else i := !i + 1
done; r
let calculeLR histo = (calculeL histo, calculeR histo)
let plusGrandRectangleHistogramme lx histo =
let l, r = calculeLR histo in
let cx = ref 0 in
let ly = ref 0 in
let cy = ref 0 in
let s = ref 0 in
for i = 1 to Array.length histo - 1 do
let s' = (r.(i) - (l.(i) - 1)) * histo.(i) in
if s' > !s then
begin
cx := l.(i);
cy := r.(i);
ly := lx - (histo.(i) - 1);
s := s';
end
done;
((lx, !cx), (!ly, !cy), !s)
let res col =
let lx, cx, ly, cy, s = ref 0, ref 0, ref 0,ref 0, ref 0 in
for i = 1 to Array.length col - 1 do
let (lx', cx'), (ly', cy'), s' = plusGrandRectangleHistogramme i col.(i) in
if s' > !s then
begin
lx := i;
cx := cx';
ly := ly';
cy := cy';
s := s';
end
done;
(!lx, !cx), (!ly, !cy), !s
let histo = [|-1;3;1;2;4;2;2;0;1|]
let col =
[|
[|-1 |];
[|-1; 1; 1; 0; 0; 1; 1; 1; 0 |];
[|-1; 2; 2; 1; 1; 0; 2; 2; 0 |];
[|-1; 0; 3; 2; 2; 1; 3; 3; 0 |];
[|-1; 1; 0; 3; 3; 2; 4; 4; 0 |];
[|-1; 2; 1; 0; 0; 3; 5; 5; 0 |];
[|-1; 3; 2; 0; 1; 4; 6; 6; 0 |];
[|-1; 4; 0; 0; 0; 5; 0; 7; 0 |];
[|-1; 5; 1; 0; 0; 6; 1; 8; 0;|]
|]
let _ = plusGrandRectangleHistogramme 4 histo
let _ = res col *)
(************************************************)
(*
module Recherche_bidimensionnelle
use int.Int
use ref.Ref
use array.Array
let rec calculeL_aux i histo l
requires {l.length = histo.length}
requires {0 <= i < histo.length }
ensures {0 <= result <= i}
ensures {forall k. result <= k <= i -> histo[k] >= histo[i]}
ensures {result > 0 -> histo[result-1] < histo[i]}
ensures {result = l[i]}
variant { i }
=
let j = ref i in
while !j > 0 && histo[!j-1] >= histo[i] do
variant {!j}
invariant {forall k. !j <= k <= i -> histo[k] >= histo[i]}
invariant {0 <= !j <= i }
j := calculeL_aux (!j-1) histo l
done;
l[i] <- !j; !j
let calculeL i histo l
requires {l.length = histo.length}
requires {0 <= i < histo.length }
ensures {forall k. result <= k <= i -> histo[k] >= histo[i]}
ensures {result > 0 -> histo[result-1] < histo[i]}
ensures {0 <= result <= i}
ensures {result = l[i]}
= calculeL_aux i histo l
let rec calculeR_aux i histo r
requires {r.length = histo.length}
requires {0 <= i < histo.length }
ensures {i <= result < histo.length}
ensures {forall k. i <= k <= result -> histo[k] >= histo[i]}
ensures {result < histo.length - 1 -> histo[result+1] < histo[i]}
ensures {result = r[i]}
variant { histo.length - i }
=
let j = ref i in
while !j < histo.length - 1 && histo[!j+1] >= histo[i] do
variant {histo.length - !j}
invariant {forall k. i <= k <= !j -> histo[k] >= histo[i]}
invariant {i <= !j < histo.length }
j := calculeR_aux (!j+1) histo r
done;
r[i] <- !j; !j
let calculeR i histo r
requires {r.length = histo.length}
requires {0 <= i < histo.length }
ensures {forall k. i <= k <= result -> histo[k] >= histo[i]}
ensures {result < histo.length -1 -> histo[result+1] < histo[i]}
ensures {i <= result < histo.length}
ensures {result = r[i]}
= calculeR_aux i histo r
let calculeLR i histo l r
requires {r.length = histo.length}
requires {l.length = histo.length}
requires {0 <= i < histo.length }
ensures {
let (li, ri) = result in forall k. li <= k <= ri -> histo[i] <= histo[k]}
= (calculeL i histo l, calculeR i histo r)
predicate is_li (i j: int) (histo : array int) =
0 <= j <= i < histo.length /\
(forall k. j <= k <= i -> histo[k] >= histo[i]) /\
(j > 0 -> histo[j-1] < histo[i])
let test () =
let histo = make 8 0 in
let l = make 8 0 in
histo[0] <- 3; histo[1] <- 1; histo[2] <- 2; histo[3] <- 4;
histo[4] <- 2; histo[5] <- 2; histo[6] <- 0; histo[7] <- 1;
let l0 = calculeL 0 histo l in
assert {l0 = 0 /\ is_li 0 0 histo};
let l1 = calculeL 1 histo l in
assert {l1 = 0 /\ is_li 1 0 histo};
let l2 = calculeL 2 histo l in
assert {histo[1] < histo[2]};
assert {not is_li 2 1 histo};
assert {l2 = 2 /\ is_li 2 2 histo};
let l3 = calculeL 3 histo l in
assert {l3 = 3 /\ is_li 3 3 histo};
let l4 = calculeL 4 histo l in
assert {l4 = 2 /\ is_li 4 2 histo};
let l5 = calculeL 5 histo l in
assert {l5 = 2 /\ is_li 5 2 histo};
let l6 = calculeL 6 histo l in
assert {l6 = 0 /\ is_li 6 0 histo};
let l7 = calculeL 7 histo l in
assert {l7 = 7 /\ is_li 7 7 histo};
assert {not is_li 7 6 histo};
assert {not is_li 7 5 histo};
assert {not is_li 7 2 histo};
end *)
(*
let rec calcule i k
requires {0 < k}
requires {l.length > 0}
requires {l.length = histo.length}
requires {0 <= i < histo.length}
ensures {0 <= result <= i }
variant { k }
=
let li = (aux i i (k-1)) in
l[i] <- li;
li
with aux i j k
requires { l.length > 0 }
requires {0 < k}
requires { l.length = histo.length }
requires { 0 <= i < histo.length }
requires { 0 <= j < histo.length }
requires { 0 <= j <= i}
ensures { 0 <= result <= j}
variant {k}
=
if j = 0
then 0
else
if histo[j-1] < histo[i]
then j
else aux i (calcule (j-1) (k-1)) (k-1)
*)
(* ((ri < histo.length -1 -> histo[ri+1] < histo[i]) /\ *)
(* li > 0 -> histo[li-1] < histo[i]) /\
(i <= ri < histo.length) /\
(0 <= li <= i)} *)
(*(* Partie II. De la 1D vers la 2D *)
module recherche_bidimen
use int.Int
use ref.Ref
use array.Array
predicate is_li (i j: int) (histo : array int) =
0 <= j <= i < histo.length /\
(forall k. j <= k <= i -> histo[k] >= histo[i]) /\
(j > 0 -> histo[j-1] < histo[i])
let rec f i j histo l =
requires {l.length = histo.length}
requires {forall k. j <= k <= i -> histo[k] >= histo[i]}
requires {0 <= j <= i < histo.length }
ensures {is_li i result histo}
ensures {result = l[i]}
variant {j}
let li =
if j = 0 then 0
else if histo[j-1] < histo[i] then j
else f i (f (j-1) (j-1) histo l) histo l
in l[i] <- li; li
let calculeL i histo l =
requires {0 <= i < histo.length}
requires {l.length = histo.length}
ensures {is_li i result histo}
ensures {result = l[i]}
f i i histo l
let test () =
let histo = make 8 0 in
let l = make 8 0 in
histo[0] <- 3; histo[1] <- 1; histo[2] <- 2; histo[3] <- 4;
histo[4] <- 2; histo[5] <- 2; histo[6] <- 0; histo[7] <- 1;
let l0 = calculeL 0 histo l in
assert {l0 = 0 /\ is_li 0 0 histo};
let l1 = calculeL 1 histo l in
assert {l1 = 0 /\ is_li 1 0 histo};
let l2 = calculeL 2 histo l in
assert {histo[1] < histo[2]};
assert {not is_li 2 1 histo};
assert {l2 = 2 /\ is_li 2 2 histo};
let l3 = calculeL 3 histo l in
assert {l3 = 3 /\ is_li 3 3 histo};
let l4 = calculeL 4 histo l in
assert {l4 = 2 /\ is_li 4 2 histo};
let l5 = calculeL 5 histo l in
assert {l5 = 2 /\ is_li 5 2 histo};
let l6 = calculeL 6 histo l in
assert {l6 = 0 /\ is_li 6 0 histo};
let l7 = calculeL 7 histo l in
assert {l7 = 7 /\ is_li 7 7 histo};
assert {not is_li 7 6 histo};
assert {not is_li 7 5 histo};
assert {not is_li 7 2 histo};
end
module Histo_loop
use int.Int
use int.Lex2
use ref.Ref
use array.Array
predicate is_li (i j: int) (histo : array int) =
0 <= j <= i < histo.length /\
(forall k. j <= k <= i -> histo[k] >= histo[i]) /\
(j > 0 -> histo[j-1] < histo[i])
let rec calculeL_aux i histo l
requires {l.length = histo.length}
requires {0 <= i < histo.length }
ensures {is_li i result histo}
ensures {result = l[i]}
variant { i }
=
let j = ref i in
while !j > 0 && histo[!j-1] >= histo[i] do
variant {!j}
invariant {forall k. !j <= k <= i -> histo[k] >= histo[i]}
invariant {0 <= !j <= i }
j := calculeL_aux (!j-1) histo l
done;
l[i] <- !j; !j
let calculeL i histo l
requires {l.length = histo.length}
requires {0 <= i < histo.length }
ensures {is_li i result histo}
ensures {result = l[i]}
= calculeL_aux i histo l
let test () =
let histo = make 8 0 in
let l = make 8 0 in
histo[0] <- 3; histo[1] <- 1; histo[2] <- 2; histo[3] <- 4;
histo[4] <- 2; histo[5] <- 2; histo[6] <- 0; histo[7] <- 1;
let l0 = calculeL 0 histo l in
assert {l0 = 0 /\ is_li 0 0 histo};
let l1 = calculeL 1 histo l in
assert {l1 = 0 /\ is_li 1 0 histo};
let l2 = calculeL 2 histo l in
assert {histo[1] < histo[2]};
assert {not is_li 2 1 histo};
assert {l2 = 2 /\ is_li 2 2 histo};
let l3 = calculeL 3 histo l in
assert {l3 = 3 /\ is_li 3 3 histo};
let l4 = calculeL 4 histo l in
assert {l4 = 2 /\ is_li 4 2 histo};
let l5 = calculeL 5 histo l in
assert {l5 = 2 /\ is_li 5 2 histo};
let l6 = calculeL 6 histo l in
assert {l6 = 0 /\ is_li 6 0 histo};
let l7 = calculeL 7 histo l in
assert {l7 = 7 /\ is_li 7 7 histo};
assert {not is_li 7 6 histo};
assert {not is_li 7 5 histo};
assert {not is_li 7 2 histo};
end*)
Reference in New Issue View Git Blame Copy Permalink