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:

    “So soon did we, wayfarers, begin to learn that man’s life is rounded with the same few facts, the same simple relations everywhere, and it is vain to travel to find it new.”
    —Henry David Thoreau (1817–1862)

    “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)

    “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)