OCaml Program
Checking:
Static
Dynamic
Hybrid
 
let min (x:int) y = if x <=y then x else y let not x = if x then false else true let null (xs : int list) = match xs with [] -> true | (h::t) -> false let rec sorted (xs:int list) = match xs with | [] -> true | x::m -> match m with | [] -> true | y::n -> x <= y && sorted m (* let rec for_all (p : int -> bool) (xs : int list) = match xs with [] -> true | a::l -> p a && for_all p l let le_all2 x xs = for_all (fun y -> x <= y) xs Cannot use this predicate at the moment most likely because SMT solver cannot find the existentially quantified function. Partial evaluation may help, but it may be heavy. *) let rec le_all x (xs : int list) = match xs with | [] -> true | a::l -> x <= a && le_all x l contract get_min = {xs | not (null xs)} -> {x | le_all x xs} let rec get_min (xs: int list) = match xs with | [] -> failwith "Empty" | (x::l) -> begin match l with | [] -> x | h :: t -> min x (get_min l) end let rec rm_min m xs = match xs with | [] -> [] | h :: t -> if h = m then t else h :: rm_min m t contract selectionsort = {xs | true} -> {ys | sorted ys} let rec selectionsort xs = match xs with | [] -> [] | h::l -> let m = get_min xs in m :: (selectionsort (rm_min m xs))