OCaml Program
Checking:
Static
Dynamic
Hybrid
 
contract len = {xs | true} -> {n | n >= 0} let rec len (xs: int list) = match xs with [] -> 0 | (h::t) -> 1 + len t contract append = {xs | true} -> {ys | true} -> {rs | len xs + len ys = len rs} let rec append (xs: int list) (ys: int list) = match xs with | [] -> ys | x::l -> x :: append l ys