Specifications

Syntax

<specification> ::= <assumes>? <requires>? <ensures>?

Semantics

• They are only used by the compiler when the verification is turned on.
• They do not affect the result of compilation.