heap_implem.mlw 4.27 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 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39

use import module ref.Ref

(* implementation of heaps *)
let create () : ref logic_heap =
  { true }
    let x = (A.const 0, 0) in ref x
  { is_heap !result /\
    model !result = empty_bag }

exception Break

let insert (this : ref logic_heap) (e : int) : unit  =
{ is_heap !this }
  let (a, n) = !this in
  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 };
MARCHE Claude's avatar
MARCHE Claude committed
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
{ is_heap !this /\
    model !this = add e (model (old !this)) }

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

MARCHE Claude's avatar
MARCHE Claude committed
114 115 116 117 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 163 164
(*

let extractMin0 (this : ref logic_heap) : int =
{ model !this <> empty_bag }
  let (a, n) = !this in
  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
{ model !this = diff (model (old !this)) (singleton result) }
*)

MARCHE Claude's avatar
MARCHE Claude committed
165 166 167 168
end

(*
Local Variables:
169
compile-command: "why3ide -I . heap_implem.mlw"
MARCHE Claude's avatar
MARCHE Claude committed
170 171
End:
*)