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

Through compileSource
CONTRACT 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

Through compileSource
CONTRACT 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.