OCaml Program
Checking:
Static
Dynamic
Hybrid
 
let rec sorted (xs:int list) = match xs with | [] -> true | x::m -> match m with | [] -> true | y::n -> x <= y && sorted m let rec mem (x:int) (l:int list) = match l with | [] -> false | (y::m) -> x=y || mem x m let rec permut (l1:int list) (l2:int list) = match l1 with | [] -> begin match l2 with | [] -> true | (y::n) -> false end | (x::m) -> begin match l2 with | [] -> false | (y::n) -> if x=y then permut m n else mem x n && mem y m end axiom a0 : forall x:int. forall l:int list. sorted (x::l) -> sorted l axiom a2 : forall l1, l2:int list. permut l1 l2 <-> (forall x:int. mem x l1 <-> mem x l2) axiom a3 : forall x:int. forall z,w:int list. permut z w -> permut(x::z) (x::w) axiom a4 : forall l1, l2 :int list. permut l1 l2 -> permut l2 l1 axiom a5 : forall l1, l2, l3 :int list. permut l1 l2 -> permut l2 l3 -> permut l1 l3 contract insert = {x | true} -> {y | sorted y} -> {r | sorted r && permut (x::y) r} let rec insert (item:int) (xs:int list) = match xs with | [] -> [item] | x::l -> if item <= x then item::x::l else x::(insert item l) contract insertion_sort = {xs | true} -> {r | sorted r && permut xs r} let rec insertion_sort xs = match xs with | [] -> [] | x::l -> insert x (insertion_sort l) let t2 = insertion_sort [3;6;1] let rec print_list xs = match xs with | [] -> print_string "]" | (x::l) -> print_int x; print_string ";"; print_list l let t1 = insert 5 [1;3;6] let t3 = print_list t1; print_list t2