A simple example of amortization
A simple example of amortization
Auteurs: Jean-Christophe Filliâtre
Catégories: Algorithms
Outils: Why3
see also the index (by topic, by tool, by reference, by year)
A simple example of amortization.
From Chris Okasaki's "Purely Functional Data Structures" Chapter 5 -- Fundamentals of Amortization
This is an abstraction where
- we do not implement the operations and we do not model the contents of the queue (irrelevant here);
- we assume that push is O(1) (contrary to Okasaki's code, which has an internal invariant |f|>=|r|).
use int.Int use list.ListRich
Global clock. Function tick
is unused below but one must imagine
that it would be called at each function call and each loop iteration.
val ghost ref clock: int val ghost tick () : unit writes { clock } ensures { clock = old clock + 1 }
Queue abstraction.
type elt = int type queue = abstract { ghost size: int; ghost credits: int; } invariant { size >= 0 } invariant { 0 <= credits <= size } val empty () : (q: queue) ensures { q.size = 0 } ensures { q.credits = 0 } val push (_: elt) (q: queue) : (r: queue) writes { clock } ensures { r.size = q.size + 1 } ensures { clock = old clock + 1 } ensures { r.credits = q.credits + 1 } val pop (q: queue) : (_: elt, r: queue) requires { q.size > 0 } writes { clock } ensures { r.size = q.size - 1 } ensures { r.credits <= q.credits } ensures { clock = old clock + 1 + r.credits - q.credits }
Test client: Let us show that if we insert n values in a queue, then remove all of them, the total cost is O(n).
let client (n: int) : unit requires { n >= 0 } ensures { clock <= old clock + 2*n } = let ref q = empty () in for k = 0 to n-1 do invariant { q.size = q.credits = k } invariant { clock = old clock + k } q <- push 42 q done; for k = 0 to n-1 do invariant { q.size = n-k } invariant { clock = old clock + q.credits + k } let _, r = pop q in q <- r done
download ZIP archive
Why3 Proof Results for Project "amortization"
Theory "amortization.Top": fully verified
Obligations | CVC4 1.7 | |
VC for queue | 0.03 | |
VC for client | --- | |
split_vc | ||
loop invariant init | 0.02 | |
loop invariant init | 0.03 | |
loop invariant preservation | 0.03 | |
loop invariant preservation | 0.03 | |
loop invariant init | 0.03 | |
loop invariant init | 0.03 | |
precondition | 0.03 | |
loop invariant preservation | 0.03 | |
loop invariant preservation | 0.04 | |
postcondition | 0.04 | |
postcondition | 0.02 | |
out of loop bounds | 0.03 |