Wiki Agenda Contact Version française

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

download ZIP archive

Why3 Proof Results for Project "amortization"

Theory "amortization.Top": fully verified

ObligationsCVC4 1.7
VC for queue0.03
VC for client---
split_vc
loop invariant init0.02
loop invariant init0.03
loop invariant preservation0.03
loop invariant preservation0.03
loop invariant init0.03
loop invariant init0.03
precondition0.03
loop invariant preservation0.03
loop invariant preservation0.04
postcondition0.04
postcondition0.02
out of loop bounds0.03