OCaml Program
Checking:
Static
Dynamic
Hybrid
 
let not x = if x then false else true let null (xs:int list) = match xs with [] -> true | (h::t) -> false let null2 (xs:(int list) list) = match xs with [] -> true | (h::t) -> false let imply x y = if x then y else true contract head = {xs | not (null2 xs)} -> {r | true} let head (xs : (int list) list) = match xs with | [] -> failwith "head" | (h::t) -> h contract tail = {xs | not (null2 xs)} -> {r | true} let tail (xs : (int list) list) = match xs with | [] -> failwith "tail" | (h::t) -> t contract risers = {xs | true} -> {r | imply (not (null xs)) (not (null2 r))} let rec risers (xs:int list) : (int list) list = match xs with | [] -> [] | (x::l) -> match l with | [] -> [[x]] | (y::etc) -> let ss = risers (y :: etc) in if x <= y then (x :: (head ss)) :: (tail ss) else [x] :: ss