OCaml Program
Checking:
Static
Dynamic
Hybrid
 
let imply x y = if x then y else true let rec sorted (xs:int list) = match xs with | [] -> true | x::m -> match m with | [] -> true | y::n -> x <= y && sorted m axiom a0 : forall x:int. forall l:int list. sorted(x::l) -> sorted l let rec append (xs: int list) (ys: int list) = match xs with | [] -> ys | x::l -> x :: append l ys let rec le_all p (xs : int list) = match xs with | [] -> true | a::l -> a <= p && le_all p l let rec gt_all p (xs : int list) = match xs with | [] -> true | a::l -> a > p && gt_all p l contract partition = {p| true} -> {ys| true} -> ({u | le_all p u}, {v | gt_all p v}) let rec partition (pivot: int) (ys: int list) : (int list * int list) = match ys with | [] -> ([], []) | h::t -> begin match partition pivot t with | (l,r) -> if h <= pivot then (h::l,r) else (l, h::r) end let same_bag xs ys = true axiom a1: forall p:int. forall xs,ys: int list. same_bag xs ys -> gt_all p xs -> gt_all p ys axiom a2: forall p:int. forall xs,ys: int list. same_bag xs ys -> le_all p xs -> le_all p ys axiom a3: forall p:int. forall xs,ys: int list. sorted xs -> sorted ys -> le_all p xs -> gt_all p ys -> sorted (append xs (p::ys)) contract quicksort = {xs | true} -> {ys | sorted ys && same_bag xs ys} let rec quicksort (xs : int list) = match xs with | [] -> [] | pivot::rest -> begin match rest with | [] -> [pivot] | y::m -> begin match partition pivot rest with | (l,r) -> append (quicksort l) (pivot :: quicksort r) end end