OCaml Program
Checking:
Static
Dynamic
Hybrid
 
contract h1 = {y | y > 0} -> {r | true} let h1 (y:int) = true let k1 n = let f1 (x:int) (g:int -> bool) = g (x + 1) in if n > 0 then f1 n h1 else true let intro1 = k1 (Random.int 1) contract h2 = {y | true} -> {r | y > 0} let h2 (y:int) = true let k2 n = let f2 x g = g (x + 1) in if n >= 0 then f2 n h2 else true let intro2 = k2 (Random.int 1) contract h3 = {z | true} -> {y | y > z} -> {r | true} let h3 (z: int) (y:int) = true let k3 n = let f3 (x:int) g = g (x+1) in if n >= 0 then f3 n (h3 n) else true let intro3 = k3 (Random.int 1) let g x y = x let twice f x y = f (f x) y let neg x y = let z = x 1 in 0 - z contract t1 = {n | n >=0} -> {z | z >=0} let t1 n = twice neg (g n) 1