91 lines
2.7 KiB
Plaintext
91 lines
2.7 KiB
Plaintext
type heap is map(nat, heap_element) ;
|
|
|
|
function is_empty (const h : heap) : bool is
|
|
block {skip} with size(h) = 0n
|
|
|
|
function get_top (const h : heap) : heap_element is
|
|
block {skip} with get_force(1n, h)
|
|
|
|
function pop_switch (const h : heap) : heap is
|
|
block {
|
|
const result : heap_element = get_top (h) ;
|
|
const s : nat = size(h) ;
|
|
const last : heap_element = get_force(s, h) ;
|
|
remove 1n from map h ;
|
|
h[1n] := last ;
|
|
} with h
|
|
|
|
function pop_ (const h : heap) : nat is
|
|
begin
|
|
const result : heap_element = get_top (h) ;
|
|
const s : nat = size(h) ;
|
|
var current : heap_element := get_force(s, h) ;
|
|
const i : nat = 1n ;
|
|
const left : nat = 2n * i ;
|
|
const right : nat = left + 1n ;
|
|
remove 1n from map h ;
|
|
h[1n] := current ;
|
|
var largest : nat := i ;
|
|
if (left <= s and heap_element_lt(get_force(s , h) , get_force(left , h))) then
|
|
largest := left
|
|
else if (right <= s and heap_element_lt(get_force(s , h) , get_force(right , h))) then
|
|
largest := right
|
|
else skip
|
|
end with largest
|
|
|
|
function insert (const h : heap ; const e : heap_element) : heap is
|
|
begin
|
|
var i : nat := size(h) + 1n ;
|
|
h[i] := e ;
|
|
var largest : nat := i ;
|
|
var parent : nat := 0n ;
|
|
while (largest =/= i) block {
|
|
parent := i / 2n ;
|
|
largest := i ;
|
|
if (parent >= 1n) then block {
|
|
if (heap_element_lt(get_force(parent , h) , get_force(i , h))) then block {
|
|
largest := parent ;
|
|
const tmp : heap_element = get_force(i , h) ;
|
|
h[i] := get_force(parent , h) ;
|
|
h[parent] := tmp ;
|
|
} else skip
|
|
} else skip
|
|
}
|
|
end with h
|
|
|
|
function pop (const h : heap) : (heap * heap_element * nat) is
|
|
begin
|
|
const result : heap_element = get_top (h) ;
|
|
var s : nat := size(h) ;
|
|
const last : heap_element = get_force(s, h) ;
|
|
remove s from map h ;
|
|
h[1n] := last ;
|
|
s := size(h) ;
|
|
var i : nat := 0n ;
|
|
var largest : nat := 1n ;
|
|
var left : nat := 0n ;
|
|
var right : nat := 0n ;
|
|
var c : nat := 0n ;
|
|
while (largest =/= i) block {
|
|
c := c + 1n ;
|
|
i := largest ;
|
|
left := 2n * i ;
|
|
right := left + 1n ;
|
|
if (left <= s) then begin
|
|
if (heap_element_lt(get_force(left , h) , get_force(i , h))) then begin
|
|
largest := left ;
|
|
const tmp : heap_element = get_force(i , h) ;
|
|
h[i] := get_force(left , h) ;
|
|
h[left] := tmp ;
|
|
end else skip ;
|
|
end else if (right <= s) then begin
|
|
if (heap_element_lt(get_force(right , h) , get_force(i , h))) then begin
|
|
largest := right ;
|
|
const tmp : heap_element = get_force(i , h) ;
|
|
h[i] := get_force(right , h) ;
|
|
h[left] := tmp ;
|
|
end else skip ;
|
|
end else skip ;
|
|
}
|
|
end with (h , result , c)
|