OCaml Program
Checking:
Static
Dynamic
Hybrid
 
let fst v = match v with | (x,y) -> x let snd v = match v with | (x,y) -> y let rec sorted (xs:int list) = match xs with | [] -> true | x::m -> match m with | [] -> true | y::n -> x <= y && sorted m contract len = {xs | true} -> {n | n >= 0} let rec len (xs : int list) = match xs with | [] -> 0 | (h::t) -> 1 + len t axiom a0 : forall x:int. forall l:int list. sorted(x::l) -> sorted l contract merge = {xs | sorted xs} -> {ys | sorted ys} -> {zs | sorted zs} (* contract merge = {xs | true} -> {ys | true} -> {zs | len zs = len xs + len ys} *) let rec merge (xs:int list) (ys: int list) = match xs with | [] -> begin match ys with | [] -> [] | (y::l) -> ys end | (x::m) -> begin match ys with | [] -> xs | (y::l) -> if x <= y then x :: (merge m ys) else y :: (merge xs l) end contract split = {xs | true} -> k:({p | true}, {q | true}) -> ({ys | true}, {zs | len ys + len zs = len (fst k) + len (snd k) + len xs}) let rec split (xs: int list) (pair: int list * int list) = match xs with | [] -> pair | (x::l) -> begin match l with | [] -> begin match pair with | (xs, ys) -> ((x::xs), ys) end | (y::zs) -> begin match pair with | (xs, ys) -> split zs ((x::xs),(y::ys)) end end contract mergesort = {xs| true} -> {ys | sorted ys} let rec mergesort (xs: int list) = match xs with | [] -> [] | x::l -> begin match l with | [] -> [x] | y::m -> begin match split xs (([]:int list),([]:int list)) with | (vs, ws) -> merge (mergesort vs) (mergesort ws) end end (* let rec print_list xs = match xs with | [] -> print_string "]" | (x::l) -> print_int x; print_string ";"; print_list l let t1 = mergesort [5;1;8;2;3] let _ = print_list t1 *)