Existence Property Pattern
Existence Property Pattern
Intent
To describe a portion of a system's execution that contains
an instance of certain events or states. Also known as Eventually.
Example Mappings
Examples and Known Uses
The classic example of existence is specifying termination, e.g.,
on all executions do we eventually reach a terminal state.
Relationships
This pattern is the dual of the Absence pattern. In fact, in
many specification formalisms negation and explicit queries for
existence will be used to formulate an instance of the Absence
pattern.
We may wish to specify that a state/event occur at most some bounded number
of times. The Bounded Existence pattern
handles that case.
If one wishes to require the existence of a state characterized
by multiple propositions
or multiple events one can do this by defining P appropriately.
One common use is to fill the role of P in the above mappings
with disjunctions of propositions or event symbols. For other
parameterizations of patterns
consult the pattern notes.
This is an Occurrence pattern.