tmp/tmp75g2sowd/{from.md → to.md}
RENAMED
|
@@ -0,0 +1,46 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
### Enumerations <a id="support.contract.enum">[[support.contract.enum]]</a>
|
| 2 |
+
|
| 3 |
+
*Recommended practice:* For all enumerations in
|
| 4 |
+
[[support.contract.enum]], if implementation-defined enumerators are
|
| 5 |
+
provided, they should have a minimum value of 1000.
|
| 6 |
+
|
| 7 |
+
The enumerators of `assertion_kind` correspond to the syntactic forms of
|
| 8 |
+
a contract assertion [[basic.contract.general]], with meanings listed in
|
| 9 |
+
Table [[tab:support.contract.enum.kind]].
|
| 10 |
+
|
| 11 |
+
**Table: Enum `assertion_kind`** <a id="support.contract.enum.kind">[support.contract.enum.kind]</a>
|
| 12 |
+
|
| 13 |
+
| Name | Meaning |
|
| 14 |
+
| -------- | ------------------------- |
|
| 15 |
+
| `pre` | A precondition assertion |
|
| 16 |
+
| `post` | A postcondition assertion |
|
| 17 |
+
| `assert` | An *assertion-statement* |
|
| 18 |
+
|
| 19 |
+
|
| 20 |
+
The enumerators of `evaluation_semantic` correspond to the evaluation
|
| 21 |
+
semantics with which a contract assertion may be evaluated
|
| 22 |
+
[[basic.contract.eval]], with meanings listed in Table
|
| 23 |
+
[[tab:support.contract.enum.semantic]].
|
| 24 |
+
|
| 25 |
+
**Table: Enum `evaluation_semantic`** <a id="support.contract.enum.semantic">[support.contract.enum.semantic]</a>
|
| 26 |
+
|
| 27 |
+
| Name | Meaning |
|
| 28 |
+
| --------------- | --------------------------------- |
|
| 29 |
+
| `ignore` | Ignore evaluation semantic |
|
| 30 |
+
| `observe` | Observe evaluation semantic |
|
| 31 |
+
| `enforce` | Enforce evaluation semantic |
|
| 32 |
+
| `quick_enforce` | Quick-enforce evaluation semantic |
|
| 33 |
+
|
| 34 |
+
|
| 35 |
+
The enumerators of `detection_mode` correspond to the manners in which a
|
| 36 |
+
contract violation can be identified [[basic.contract.eval]], with
|
| 37 |
+
meanings listed in Table~ [[tab:support.contract.enum.detection]].
|
| 38 |
+
|
| 39 |
+
**Table: Enum `detection_mode`** <a id="support.contract.enum.detection">[support.contract.enum.detection]</a>
|
| 40 |
+
|
| 41 |
+
| Name | Meaning |
|
| 42 |
+
| ---------------------- | ------------------------------------------------------------------------------------------------ |
|
| 43 |
+
| `predicate_false` | The predicate of the contract assertion evaluated to `false` or would have evaluated to `false`. |
|
| 44 |
+
| `evaluation_exception` | An uncaught exception occurred during evaluation of the contract assertion. |
|
| 45 |
+
|
| 46 |
+
|