Attribute Index
Comprehensive index of all IML attributes used in ImandraX.
Verification attributes
| Attribute | Description |
|---|---|
[@@by tactic] | Specify the proof tactic for any verification goal (verify, theorem, lemma) |
[@@upto n] | Bounded verification (verify only): check the property up to unrolling depth n, producing a bounded theorem with counterexample completeness |
[@@timeout n] | Set a timeout in seconds for a verification goal |
Termination attributes
| Attribute | Description |
|---|---|
[@@adm x, y, ...] | Prove termination via lexicographic ordering on the listed arguments |
[@@measure expr] | Provide an explicit ordinal-valued termination measure |
Rule class attributes
| Attribute | Description |
|---|---|
[@@rw] / [@@rewrite] | Install theorem as a rewrite rule (left-to-right term rewriting) |
[@@fc] / [@@forward-chaining] | Install as a forward-chaining rule (derive new facts from hypotheses) |
[@@elim] / [@@elimination] | Install as an elimination rule (destructor elimination in the waterfall) |
[@@gen] / [@@generalization] | Install as a generalization rule (constrain generalizations) |
[@@perm] / [@@permutative] | Restrict rewrite rule to fire only when result is lexicographically smaller |
Definition attributes
| Attribute | Description |
|---|---|
[@@opaque] | Declare a function without exposing its definition to the logic |
Import directives
| Directive | Description |
|---|---|
[@@@import "file.iml"] | Import all definitions from a file |
[@@@import Module, "file.iml"] | Import a file and bind to a module name |
Expression-level annotations
| Annotation | Description |
|---|---|
[@trigger] | Mark a term as the trigger for forward-chaining or generalization rules |
[@trigger rw] | Mark a hypothesis term as the pattern for rewrite rule matching |
Region decomposition attributes
| Attribute | Description |
|---|---|
[@@imandra_rule_spec] | Define a rule specification for region decomposition |