Theories
The semantic foundation of the UTP is the first-order predicate calculus, augmented with fixed point constructs from second-order logic. Following the tradition of Eric Hehner, programs are predicates in the UTP, and there is no distinction between programs and specifications at the semantic level. In the words of Hoare:
A computer program is identified with the strongest predicate describing every relevant observation that can be made of the behaviour of a computer executing that program.
In UTP parlance, a theory is a model of a particular programming paradigm. A UTP theory is composed of three ingredients:
- an alphabet, which is a set of variable names denoting the attributes of the paradigm that can be observed by an external entity;
- a signature, which is the set of programming language constructs intrinsic to the paradigm; and
- a collection of healthiness conditions, which define the space of programs that fit within the paradigm. These healthiness conditions are typically expressed as monotonic idempotent predicate transformers.
Program refinement is an important concept in the UTP. A program is refined by if and only if every observation that can be made of is also an observation of . The definition of refinement is common across UTP theories:
where denotes the universal closure of all variables in the alphabet.
Read more about this topic: Unifying Theories Of Programming
Famous quotes containing the word theories:
“Generalisation is necessary to the advancement of knowledge; but particularly is indispensable to the creations of the imagination. In proportion as men know more and think more they look less at individuals and more at classes. They therefore make better theories and worse poems.”
—Thomas Babington Macaulay (1800–1859)
“The two most far-reaching critical theories at the beginning of the latest phase of industrial society were those of Marx and Freud. Marx showed the moving powers and the conflicts in the social-historical process. Freud aimed at the critical uncovering of the inner conflicts. Both worked for the liberation of man, even though Marx’s concept was more comprehensive and less time-bound than Freud’s.”
—Erich Fromm (1900–1980)
“In the course of a life devoted less to living than to reading, I have verified many times that literary intentions and theories are nothing more than stimuli and that the final work usually ignores or even contradicts them.”
—Jorge Luis Borges (1899–1986)