The denotational semantics intends to view the program behaviour from a more abstract aspect. Two programs are hard to compare, if we take into account all the smaller steps of program execution. Rather than evaluating a program from a given state step by step, the denotational semantics renders a denotation to the program, which is a partial function from states to states. We consider two programs equal if their denotations coincide. More formally,
The question is whether we are able to give a more direct way to compute the denotations of program than the operational approach. Before giving the denotations of programs, we should give the denotations of arithmetic- and Boolean expressions, but this is straightforward, so we ignore this task. We turn directly to defining the denotations of programs. The denotation of a program C is the partial function , where is the subset of on which is defined. In what follows, we may use the more convenient notation rather than . Moreover, to make our notation more illustrative, we write , if , and , if .
Remark 17. We remark that in the above definition the composition of relations is used in a manner somewhat different from the treatment of some of the textbooks. If A, B and C are arbitrary sets and is a relation over , and is a relation over , then in a large number of the textbooks the composition is denoted by . To facilitate readability, however, we distinguish the notation of the composition reflecting a different order of the components: we use instead of , as detailed in the Appendix.
In Definition 16 the least fixpoint of an operator is determined. By the Kanster-Tarski theorem it exists provided is continuous.
Let us calculate the denotational semantics of the program of Example 13. As before, let C denote the whole program, denote the loop and denote the body of the loop.
where are the approximations of according to Theorem 142. Let us calculate the values of :
Continuing in this way we obtain that
So far we have defined two different approaches to the meanings of programs. The question arises naturally how these approaches are connected. We state and prove the following theorem about the relation of the two approaches.
() Assume , that is, . The proof goes by induction on the length of the reduction sequence.
If , the statement trivially holds.
Assume , then we can distinguish several subcases.
: then we have for some , and . Moreover, the reduction sequences and are strictly shorter than n. By induction hypothesis, and . By Definition 16, this implies .
: assume . Hence, . This involves, by induction hypothesis, . The case for is treated similarly, and, by Definition 16, we obtain the result.
: assume . Then . By induction hypothesis we obtain . Let . Then , which is again in . Definition 16 gives the result.
() The proof goes by induction on the complexity of C. If C is skip, or an assignment, then the result is immediate.
: assume . Then, by Definition 16, we have and for some . By the induction hypothesis, and . This gives , which was to be proved.
: let , assume . Then , thus . Otherwise and . By Definition 12, the result follows.
: let , assume . Then , where
Let us consider the , , .
By Theorem 142, . We prove by induction on n that .
We should observe that if we use the notation of the previous chapter we can reformulate the appearance of as
Additionally, we prove another handy characterization of the denotational semantics of the while loop.
Proof. Let and , where . We prove that
which, by Lemma 143, gives the result. To this end, we prove by induction on n that
where and are the usual approximations of and , respectively. For the statement is trivial. Assume for some , and the equation holds for k. Then
By this, the proof is complete.