## A simple example of amortization

A simple example of amortization

Authors: Jean-Christophe Filliâtre

Topics: Algorithms

Tools: 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