Introduction to Axiomatic Semantics

Now we turn to the third and final main style of semantics, axiomatic semantics. The idea in axiomatic semantics is to define meaning in terms of logical specifications that programs satisfy. This is in contrast to operational models (which show how programs execute) and denotational models (which show what programs compute). This approach to reasoning about programs and expressing program semantics was originally proposed by Floyd and Hoare and was developed further by Dijkstra and Gries.

A common way to express program specifications is in terms of pre-conditions and post-conditions: с where c is a program, and and are formulas that describe properties of the program state, usually referred to as assertions. Such a triple is usually referred to as a partial correctness specification (or sometimes a “Hoare triple”) and has the following meaning: In other words, if we start with a store in which Pre holds and the execution of with respect to terminates and yields a store , then Post holds in store .

Pre-conditions and post-conditions can be regarded as interfaces or contracts between the program and its clients. They help users to understand what the program is supposed to yield without needing to understand how the program executes. Typically, programmers write them as comments for procedures and functions as documentation and to make it easier to maintain programs. Such specifications are especially useful for library functions for which the source code is often not available to the users. In this case, pre-conditions and post-conditions serve as contracts between the library developers and users of the library.

However, there is no guarantee that pre-conditions and post-conditions written informally in comments are correct: the comments describe the intent of the developer, but they do not give a guarantee of correctness. Axiomatic semantics addresses this problem. It shows how to rigorously describe partial correctness statements and how to establish correctness using formal reasoning.

Note that partial correctness specifications don’t ensure that the program will terminate--this is why they are called “partial”. In contrast, total correctness statements ensure that the program terminates whenever the precondition holds. Such statements are denoted using square brackets: с meaning: In general a pre-condition specifies what the program expects before execution and the post-conditions specifies what guarantees the program provides (if the program terminates). Here is a simple example: It says that if the store maps to and to before execution, then, if the program terminates, the final store will map baz to (i.e.,−2 times the initial value of bar). Note that is a logical variable that doesn’t occur in the program and is only used to express the initial value of bar. Such variables are sometimes called ghost variables.

This partial correctness statement is valid. That is, it is indeed the case that if we have any store such that , and then .

Note that this is a partial correctness statement: if the pre-condition is true before , and terminates then the post-condition holds after . There are some initial stores for which the program will not terminate.

The following total correctness statement is true. That is, if we start with a store that maps to and to a non-negative integer, then the execution of the command will terminate in a final store with .

The following partial correctness statement is not valid. (Why not?) In the rest of our discussion of axiomatic semantics we will focus almost exclusively on partial correctness assertions.

Assertions

Now we turn to the following issues:

  • What logic do we use for writing assertions? That is, what can we express in pre-conditions and post-condition?

  • What does it mean that an assertion is valid? What does it mean that a partial correctness statement is valid?

  • How can we prove that a partial correctness statement is valid?

What can we say in pre-conditions and post-conditions? In the examples so far, we have used program variables, equality, logical variables (e.g., ), and conjunction (). What we allow in pre-conditions and post-conditions directly influences the sorts of program properties we can describe using partial correctness statements. We will use the set of logical formulas including comparisons between arithmetic expressions, standard logical operators (and, or, implication, negation), as well as quantifiers (universal and existential). Assertions may also introduce logical variables that are different than the variables appearing in the program. Observe that the domain of boolean expressions is a subset of the domain of assertions. Notable additions over the syntax of boolean expression are quantifiers ( and ). For instance, one can express the fact that variable divides variable using existential quantification: .

Satisfaction and Validity

Now we would like to describe what we mean by “assertion holds in store . But to determine whether 𝑃 holds or not, we need more than just the store (which maps program variables to their values); we also need to know the values of the logical variables. We describe those values using an interpretation , and define the function , which is like the denotation of expressions extended to logical variables in the obvious way: Now we can express the satisfiability of assertions as a relation read as "P is satisfied in store under interpretation '', or ''store satisfies assertion under interpretation .'' We will write whenever doesn't hold. We can now say that an assertion is valid (written ) if it is valid in any store, under any interpretation: .

Having defined validity for individual assertions, we now turn to partial correctness statements. We say that a partial correctness statement is satisfied in store 𝜎 and interpretation , written , if: Note that this definition depends on the execution of in the initial store .

Finally, we can say that a partial correctness triple is valid (written ), if it is valid in any store and interpretation: