[Top] | [Contents] | [Index] | [ ? ] |
\result
\old
and \pre
\not_assigned
\not_modified
\only_accessed
\only_assigned
\only_called
\only_captured
\fresh
\reach
\duration
\space
\working_space
\nonnullelements
\typeof
\elemtype
\type
\lockset
\max
\is_initialized
\invariant_for
\lblneg
and \lblpos