function check condition [id] [message]
  arg CBool condition ; arg ErrorID id ; arg Str message

Checks the condition are stops with error if it's false.
If the 'message' is not provided, an automatic message will be generated that contains the name of the module where the debug instruction stands, plus the line and column numbers at least.
If the 'id' is provided, then the 'message' must also be provided.
The condition is evaluated, and so checked only if the debugging level is at least 2.

So, at last, it's the same as:

if pliant_debugging_level>=2 and not condition
  error id message


Syntax:

require
  condition1
  [condition2]
  ...
ensure
  condition1
  [condition2]
  ...

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).

A sample:

function foo x y -> z
  arg Int x y z
  require
    x>=0
    y>=x
  ensure
    z>x
    z>y
  z := x+y

Pliant DbC implemention is in dbc.pli