Design by contract: require / ensure / assert
require checks a precondition, ensure a postcondition, and assert is the same primitive used standalone โ all three lower to one contract_check host call, enforced identically whether interpreted, run here via WASM (no rustc at all), or compiled natively. The last line deliberately violates a precondition so you can see enforcement fire.
PatLang source
# Design-by-contract demo in the Stage 1 self-hosted language.
# `require` checks a precondition, `ensure` a postcondition (checked wherever
# it's written โ usually right before the value it names is returned), and
# `assert` is the same primitive used standalone. All three lower to the
# same contract_check(func, kind, text, ok) host call, so enforcement is
# identical whether interpreted, run via run_ir (no rustc), or compiled
# natively. The last line deliberately violates a precondition, to show
# what enforcement actually looks like.
make a function called safe_divide takes a, b returns r
require b != 0
let r = a / b
ensure (r * b) == a
return r
end
make a function called clamp takes x, lo, hi returns r
require lo <= hi
if x < lo then
let r = lo
else
if x > hi then
let r = hi
else
let r = x
end
end
ensure (r >= lo) and (r <= hi)
return r
end
make a function called factorial takes n returns r
require n >= 0
if n < 2 then
let r = 1
else
let r = n * factorial(n - 1)
end
ensure r >= 1
return r
end
print("safe_divide(10, 2) = " + safe_divide(10, 2))
print("clamp(15, 0, 10) = " + clamp(15, 0, 10))
print("clamp(-5, 0, 10) = " + clamp(-5, 0, 10))
print("factorial(6) = " + factorial(6))
assert (1 + 1) == 2
print("standalone assert passed")
print("--- now deliberately violating a precondition ---")
print("safe_divide(1, 0) = " + safe_divide(1, 0))
print("(unreachable: the line above aborts the program)")
(not run yet)
Native run on the build machine:
safe_divide(10, 2) = 5 clamp(15, 0, 10) = 10 clamp(-5, 0, 10) = 0 factorial(6) = 720 standalone assert passed --- now deliberately violating a precondition --- IR runtime error: contract violation: precondition failed in safe_divide(): (Var(b) != Num(0))