OCaml Program
Checking:
Static
Dynamic
Hybrid
 
contract inc = {x | x > 0} -> {y | y > x} let inc x = x + 1 let t1 = inc 2 let t2 = inc 0 contract plus = {x | x > 0} -> {y | y > 0} -> {r | r > 0} ;; let plus x y = x + y;; let t3 = plus 2 3 let t4 = plus 0 3 let t5 = plus 5 0 let t6 x = if x > 0 then x + 1 else x contract sum = {x | true} -> {y | x <= y} let rec sum n = if n <= 0 then 0 else n + sum (n - 1) contract mult = {x | true} -> {n | n >=0 } -> {y | n <= y} let rec mult x n = if x <= 1 then n else n + mult (x - 1) n let max3 max2 (x:int) y z = max2 (max2 x y) z let max (x:int) y = if x >= y then x else y contract m = {x | true} -> {y | true} -> {z | true} -> {v | max x v = v} let m (x:int) y z = max3 max x y z