Difference between revisions of "Auto-Completion Design"
From Event-B
Jump to navigationJump to searchimported>Laurent |
imported>Laurent m (→Witness Labels) |
||
| Line 21: | Line 21: | ||
==== Witness Labels ==== | ==== Witness Labels ==== | ||
| − | * | + | * Disappearing parameters (of abstract event) |
| − | * Variables (abstract) | + | * Primed Disappearing Variables (of abstract machine) that are non-deterministically assigned in abstract event |
==== Witness Predicates ==== | ==== Witness Predicates ==== | ||
Revision as of 09:52, 10 March 2009
Contents
Proposed names depending on edit context
In Context Models
Axioms and Theorems
- Sets (all)
- Constants (all)
In Machine Models
Invariants, Theorems and Variants
- Sets (all)
- Constants (all)
- Variables (all)
Guards and Actions
- Sets (all)
- Constants (all)
- Variables (all)
- Parameters (of local event)
Witness Labels
- Disappearing parameters (of abstract event)
- Primed Disappearing Variables (of abstract machine) that are non-deterministically assigned in abstract event
Witness Predicates
- Parameters (of abstract event and local event)
- Variables (all)
- Sets (all)
- Constants (all)
