heap_implem.mlw 4.24 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5

module Implementation

use import int.Int
use import int.ComputerDivision
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
6
(*use import map.Map*)
7

MARCHE Claude's avatar
MARCHE Claude committed
8 9
use import heap_model.Model
use import bag_of_integers.Bag_integers
10
use import elements.Elements
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
11
use import heap.Heap
MARCHE Claude's avatar
MARCHE Claude committed
12 13 14

lemma Is_heap_min:
  forall a:map, n :int. n > 0 ->
15
    is_heap_array a 0 n -> a[0] = min_bag (model (a, n))
MARCHE Claude's avatar
MARCHE Claude committed
16

17
use import ref.Ref
18
use map.Const
MARCHE Claude's avatar
MARCHE Claude committed
19 20

(* implementation of heaps *)
21 22
let create () : ref logic_heap
  ensures { is_heap !result /\ model !result = empty_bag }
23
  = let x = (Const.const 0, 0) in ref x
MARCHE Claude's avatar
MARCHE Claude committed
24 25 26

exception Break

27 28 29 30
let insert (this : ref logic_heap) (e : int) : unit
  requires { is_heap !this }
  ensures { is_heap !this /\ model !this = add e (model (old !this)) }
= let (a, n) = !this in
MARCHE Claude's avatar
MARCHE Claude committed
31 32 33 34 35 36 37 38 39
  let arr = ref a in
  let i = ref n in
  try
  while (!i > 0) do
    invariant {
      0 <= !i <= n /\
      (!i = n ->
         is_heap_array !arr 0 n  /\
         model (!arr, n) = model (a, n)) /\
40
      (!i < n ->
MARCHE Claude's avatar
MARCHE Claude committed
41
         is_heap_array !arr 0 (n + 1) /\
42
         !arr[!i] > e /\
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
43
         model (!arr, n+1) = add !arr[!i] (model (a, n)))
MARCHE Claude's avatar
MARCHE Claude committed
44 45 46 47 48
    }
    variant { !i }
    let parent = div (!i - 1) 2 in
    let p = A.get !arr parent in
    if (e >= p) then raise Break;
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
49
    arr := !arr[!i<-p];
MARCHE Claude's avatar
MARCHE Claude committed
50
    i := parent
MARCHE Claude's avatar
MARCHE Claude committed
51 52 53
  done
  with Break -> ()
  end;
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
54
  arr := !arr[!i<-e];
MARCHE Claude's avatar
MARCHE Claude committed
55
  this := (!arr, n + 1);
MARCHE Claude's avatar
MARCHE Claude committed
56
  assert { 0 < !i < n -> is_heap !this };
57
  assert { !i < n -> model !this = add e (model (a,n)) }
MARCHE Claude's avatar
MARCHE Claude committed
58

59 60 61 62 63 64
let extractMin (this : ref logic_heap) : int
requires { model !this <> empty_bag /\ is_heap !this }
ensures { is_heap !this /\
  result = min_bag (model (old !this)) /\
  model (old !this) = add result (model !this) }
= let (a, n) = !this in
MARCHE Claude's avatar
MARCHE Claude committed
65
  assert {n > 0};
66
  let min = a[0] in
MARCHE Claude's avatar
MARCHE Claude committed
67
  let n' = n-1 in
68 69 70 71
  let last = a[n'] in
  assert { n' > 0 -> nb_occ last (diff (model (a,n))
                        (singleton min)) > 0 } ;
  let arr = ref a in
MARCHE Claude's avatar
MARCHE Claude committed
72 73 74 75
  let i = ref 0 in
  try
    while ( !i < n') do
      invariant {
76 77
        0 <= !i /\
        (n' > 0 -> !i < n') /\
MARCHE Claude's avatar
MARCHE Claude committed
78
        is_heap_array !arr 0 n' /\
79 80 81 82 83 84 85
        (!i = 0 -> !arr = a) /\
        (n' > 0 ->
          elements !arr 0 n' =
            add !arr[!i] (diff (diff (model (a,n))
                 (singleton last))
               (singleton min))) /\
        (!i > 0 -> !arr[parent !i] < last) }
MARCHE Claude's avatar
MARCHE Claude committed
86 87 88 89 90 91
      variant {n' - !i}
      let left = 2 * !i + 1 in
      let right = 2 * !i + 2 in
      if (left >= n') then raise Break;
      let smaller = ref left in
      if right < n' then
92
        if !arr[left] > !arr[right]
MARCHE Claude's avatar
MARCHE Claude committed
93
          then smaller := right;
94 95
      if last <= !arr[!smaller] then raise Break;
      arr := !arr[!i <- !arr[!smaller]];
MARCHE Claude's avatar
MARCHE Claude committed
96 97
      i := !smaller
    done;
98 99
    assert { n' = 0 }
  with Break -> ()
MARCHE Claude's avatar
MARCHE Claude committed
100
  end;
101
  if !i < n' then
MARCHE Claude's avatar
MARCHE Claude committed
102
    begin
103
      arr := !arr[!i <- last];
104
      assert { !i > 0 -> is_heap_array !arr 0 n' };
MARCHE Claude's avatar
MARCHE Claude committed
105
      assert { is_heap_array !arr 0 n' };
106 107
      assert { n' > 0 -> elements !arr 0 n' =
                  (diff (model (a,n)) (singleton min)) }
MARCHE Claude's avatar
MARCHE Claude committed
108 109 110 111
    end;
  this := (!arr, n');
  min

112 113
(*

114 115 116 117
let extractMin0 (this : ref logic_heap) : int
requires { model !this <> empty_bag }
ensures  { model !this = diff (model (old !this)) (singleton result) }
= let (a, n) = !this in
118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162
  assert {n > 0};
  let min = a[0] in
  let n' = n-1 in
  let last = a[n'] in
  assert { n' > 0 -> nb_occ last (diff (model (a,n))
                        (singleton min)) > 0 } ;
  let arr = ref a in
  let i = ref 0 in
  try
    while ( !i < n') do
      invariant {
        0 <= !i /\
        (n' > 0 -> !i < n') /\
        (!i = 0 -> !arr = a) /\
        (n' > 0 ->
          elements !arr 0 n' =
            add !arr[!i] (diff (diff (model (a,n))
                 (singleton last))
               (singleton min))) /\
        (!i > 0 -> !arr[parent !i] < last) }
      variant {n' - !i}
      let left = 2 * !i + 1 in
      let right = 2 * !i + 2 in
      if (left >= n') then raise Break;
      let smaller = ref left in
      if right < n' then
        if !arr[left] > !arr[right]
          then smaller := right;
      if last <= !arr[!smaller] then raise Break;
      arr := !arr[!i <- !arr[!smaller]];
      i := !smaller
    done;
    assert { n' = 0 }
  with Break -> ()
  end;
  if !i < n' then
    begin
      arr := !arr[!i <- last];
      assert { n' > 0 -> elements !arr 0 n' =
                  (diff (model (a,n)) (singleton min)) }
    end;
  this := (!arr, n');
  min
*)

MARCHE Claude's avatar
MARCHE Claude committed
163
end