Diagnostics · unsupported
unsupported[ensure-form]
An ENSURE that is not exactly ENSURE action() WHEN condition [SOURCE:id].
ENSURE keeps its empty parentheses, takes no arguments, and needs both a condition and a source tag.
Example
compileSourceCONTRACT Claim {
ENFORCEMENT_MODE: enforced
CONTEXT {
ENTITIES Request {
count: int
region: string
ready: bool
ratio: float
}
CONSTANTS {
zero: int == 0 [SOURCE:POLICY]
cap: int == 25 [SOURCE:POLICY]
}
}
TRIGGER {
grant()
}
GUARANTEE {
ENSURE grant WHEN Request.ready == true [SOURCE:must_be_ready]
}
PROHIBITION {
FORBID grant WHEN Request.count > cap [SOURCE:over_cap]
}
}rejected unsupported[ensure-form] at 19:5 GUARANTEE supports ENSURE action() WHEN predicate [SOURCE:id] only
Fix
compileSourceCONTRACT Claim {
ENFORCEMENT_MODE: enforced
CONTEXT {
ENTITIES Request {
count: int
region: string
ready: bool
ratio: float
}
CONSTANTS {
zero: int == 0 [SOURCE:POLICY]
cap: int == 25 [SOURCE:POLICY]
}
}
TRIGGER {
grant()
}
GUARANTEE {
ENSURE grant() WHEN Request.ready == true [SOURCE:must_be_ready]
}
PROHIBITION {
FORBID grant WHEN Request.count > cap [SOURCE:over_cap]
}
}accepted
See also: the specification.