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:
“When any one of our relations was found to be a person of a very bad character, a troublesome guest, or one we desired to get rid of, upon his leaving my house I ever took care to lend him a riding-coat, or a pair of boots, or sometimes a horse of small value, and I always had the satisfaction of finding he never came back to return them.”
—Oliver Goldsmith (1728–1774)
“I know all those people. I have friendly, social, and criminal relations with the whole lot of them.”
—Mark Twain [Samuel Langhorne Clemens] (1835–1910)
“Our relations to each other are oblique and casual.”
—Ralph Waldo Emerson (1803–1882)