Denotational semantics

The denotational semantics (functional semantics) is to define in theoretical computer science one of several possibilities, a formal semantics for a formal language. The formal language is used here as a mathematical model for a real programming language. Thus, the operation of a computer program can be formally described.

Specifically, one can approximately at a given assignment for input variables to calculate the final result for a set of output variables with the denotational semantics. It also more general correctness proofs are possible.

In the denotational semantics of partial functions are used to map the state spaces on each other. A state here is an assignment of variables with actual values. The denotational semantics is defined inductively over the syntactic constructs of the formal language instruction. Depending on the desired program semantics, the partial functions are selected.

In addition to the denotational semantics, there is also the operational semantics and the axiomatic semantics to describe the semantics of formal languages ​​.

Definition of the semantic function

Let the set of all possible states. The effect that an instruction on a condition that an image is spoken formally

Which a state assigns a next state.

Denotes the semantic function and assigns each instruction to construct a meaning by causing a change in state of the program.

Next, the operation of the main control structure of a programming language is checked for a state.

• The significance of the empty statement:

• The semantics of an instruction sequence can be described as follows:

• For the effect of an assignment to a condition applies:

• For the two - sided alternative applies:

• The importance of repetition is defined recursively:

Fixed point of the while- semantics

The fixed point of the function which describes the semantics of the while loop will be explained below with reference to a simple example.

To determine the fixed point of this equation, one uses the Tarski's fixed point theorem. This theorem states that for an ordered set which contains a smallest element, and a strictly monotonic function which maps onto itself, a smallest fixed point exists.

Thus, the theorem can be applied, first an ordered set for the example must be defined.

Be the partial function of the while loop from the example. This represents a state consisting of the assignment for the same variables in a different state with the variable assignment. The variables and are integers.

Let now the set of all partial functions.

The partial order for two partial functions is defined as follows:

The partial mapping is less than / equal if and only if the domain of a subset of the domain of being. It must also be that when a state change caused by even function after mapping.

The smallest element of the set is nowhere defined function.

In order to use the theorem of Tarski, now missing a strictly monotonic function that maps to itself. For this purpose, a function is defined:

According to the above example applies to:

Furthermore, it should:

Now all the conditions of fixed-point theorem are satisfied, there exists a fixed point.

The fixed point is calculated by thresholding the function.

To close to the limit, you start to calculate function values ​​.

• Because the smallest element of the set is.

• Is by definition the function:

• Is given by:

• For can be formulated:

The limit is now:

For the fixed point must now apply that.

This can be transformed into:

Thus applies. The fixed point is found. The meaning of the while loop from the example results from the fixed point. The loop terminates when, and returns the tuple. If so, the loop does not terminate.

• Theoretical computer science