class Example { method M(n: int) { var i := 0; while (i < n) decreases n - i; { i := i + 1; } } } // ----------------------------------- class Fibonacci { function Fib(n: int): int decreases n; { if n < 2 then n else Fib(n-2) + Fib(n-1) } } // ----------------------------------- class Ackermann { function F(m: int, n: int): int decreases m, n; { if m <= 0 then n + 1 else if n <= 0 then F(m - 1, 1) else F(m - 1, F(m, n - 1)) } } // ----------------------------------- class List { var data: int; var next: List; ghost var ListNodes: set; function IsAcyclic(): bool reads *; decreases ListNodes; { this in ListNodes && (next != null ==> next.ListNodes <= ListNodes && this !in next.ListNodes && next.IsAcyclic()) } method Singleton(x: int) returns (list: List) ensures list != null && list.IsAcyclic(); { list := new List; list.data := x; list.next := null; list.ListNodes := {list}; } method Prepend(x: int, tail: List) returns (list: List) requires tail == null || tail.IsAcyclic(); ensures list != null && list.IsAcyclic(); { list := new List; list.data := x; list.next := tail; list.ListNodes := if tail == null then {list} else {list} + tail.ListNodes; } function Sum(): int requires IsAcyclic(); reads *; decreases ListNodes; { if next == null then data else data + next.Sum() } }