public interface StateUpdate extends QntPred
Process state update is a list of assignment pairs representing how state updates took place sequentially. For complex compositional operators, such as external choice and parallel composition, there are semantic functions that define how the state merge occurs, which is much like what happens in the UTP.
These classes shall never be instantiated by the user manually. They are produced by Circus tools as they go along performing the varied state update forms the language allows.
It is a Z quantified predicate extended to contain a list of assignment pairs. Essentially, a tool, say a typechecker, collects the assignment pairs representing a particular branch of the AST. This can be built backwards as it traverses the AST during typechecking. After that, another tool, say an animator or model checker, can apply necessary transformations needed to the assignment pairs list so that the merge of information reflect the denotational semantics of a particular construct. The resulting predicate representing the whole state update is then feed into the actual structure of a QntPred, where the SchText is the state components (and invariant), and the predicate is the calculated state merge. (!)
It is part of a ProcessSignature. It is also be part of a StateUpdateAnn.
| Modifier and Type | Method and Description |
|---|---|
ListTerm<AssignmentPairs> |
getAssignmentPairs()
Returns the AssignmentPairs elements.
|
getPred, getSchText, getZSchText, setPred, setSchTextListTerm<AssignmentPairs> getAssignmentPairs()
Returns the AssignmentPairs elements.
To add or remove elements, use the methods provided by the List interface (that's why there is no need for a setter method).
Copyright © 2003–2016 Community Z Tools Project. All rights reserved.