Relations
The most basic UTP theory is the alphabetised predicate calculus, which has no alphabet restrictions or healthiness conditions. The theory of relations is slightly more specialised, since a relation's alphabet may consist of only:
- undecorated variables, modelling an observation of the program at the start of its execution; and
- primed variables, modelling an observation of the program at a later stage of its execution.
Some common language constructs can be defined in the theory of relations as follows:
- The skip statement, which does not alter the program state in any way, is modelled as the relational identity:
- The assignment of value to a variable is modelled as setting to and keeping all other variables (denoted by ) constant:
- The sequential composition of two programs is just relational composition of intermediate state:
- Non-deterministic choice between programs is their greatest lower bound:
- Conditional choice between programs is written using infix notation:
- A semantics for recursion is given by the least fixed point of a monotonic predicate transformer :
Read more about this topic: Unifying Theories Of Programming
Famous quotes containing the word relations:
“Happy will that house be in which the relations are formed from character; after the highest, and not after the lowest order; the house in which character marries, and not confusion and a miscellany of unavowable motives.”
—Ralph Waldo Emerson (1803–1882)
“Society does not consist of individuals but expresses the sum of interrelations, the relations within which these individuals stand.”
—Karl Marx (1818–1883)
“Consciousness, we shall find, is reducible to relations between objects, and objects we shall find to be reducible to relations between different states of consciousness; and neither point of view is more nearly ultimate than the other.”
—T.S. (Thomas Stearns)