Notes on PL 08 - Axiomatic Semantics
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:
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:
This partial correctness statement is valid. That is, it is indeed the case that if we have any store
Note that this is a partial correctness statement: if the pre-condition is true before
The following total correctness statement is true.
The following partial correctness statement is not valid. (Why not?)
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.,
Satisfaction and Validity
Now we would like to describe what we mean by “assertion
Having defined validity for individual assertions, we now turn to partial correctness statements. We say that a partial correctness statement
Finally, we can say that a partial correctness triple is valid (written