Unifying Theories of Programming - Relations

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 one walks, one is brought into touch first of all with the essential relations between one’s physical powers and the character of the country; one is compelled to see it as its natives do. Then every man one meets is an individual. One is no longer regarded by the whole population as an unapproachable and uninteresting animal to be cheated and robbed.
    Aleister Crowley (1875–1947)

    The interest in life does not lie in what people do, nor even in their relations to each other, but largely in the power to communicate with a third party, antagonistic, enigmatic, yet perhaps persuadable, which one may call life in general.
    Virginia Woolf (1882–1941)

    The land is the appointed remedy for whatever is false and fantastic in our culture. The continent we inhabit is to be physic and food for our mind, as well as our body. The land, with its tranquilizing, sanative influences, is to repair the errors of a scholastic and traditional education, and bring us to just relations with men and things.
    Ralph Waldo Emerson (1803–1882)