Diagnostics · semantic
semantic[empty-guarantee]
A GUARANTEE block with no ENSURE clauses.
Remove the block, or add a guarantee. An empty PROHIBITION block is allowed.
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 {
}
PROHIBITION {
FORBID grant WHEN Request.count > cap [SOURCE:over_cap]
}
}rejected semantic[empty-guarantee] at 18:3 GUARANTEE block of Claim has no ENSURE clauses
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()
}
PROHIBITION {
FORBID grant WHEN Request.count > cap [SOURCE:over_cap]
}
}accepted
See also: the specification.