function check condition [id] [message]
arg CBool condition ; arg ErrorID id ; arg Str message
So, at last, it's the same as:
if pliant_debugging_level>=2 and not condition
error id message
For an introduction to Design by Contract, please read Todd article.
basically, 'require' defines a set of conditions that must all be true when the function enters, end 'ensure' defines a set of conditions that should all be true when the function leaves. If one of the conditions introduced by 'require' is false, it means that the function has been improperly used, so the calling program is buggy. If one of the conditions introduced by 'ensure' is false, it means that the function implementation is buggy (does not match the specifications).
function foo x y -> z
arg Int x y z
z := x+y
Pliant DbC implemention is in dbc.pli