Fifty years of Hoare's Logic
Krzysztof R. Apt, Ernst-Ruediger Olderog
TL;DR
This paper reviews the development and impact of Hoare's logic over the past fifty years, highlighting its evolution and significance in formal verification.
Contribution
It provides a comprehensive historical overview of Hoare's logic, emphasizing its foundational role and developments in program verification.
Findings
Hoare's logic has significantly influenced formal methods.
The logic has evolved to address modern programming challenges.
Historical insights into its development and applications.
Abstract
We present a history of Hoare's logic.
Click any figure to enlarge with its caption.
Figure 1
Figure 2
Figure 3Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Computability, Logic, AI Algorithms · Advanced Malware Detection Techniques
Fifty Years of Hoare’s Logic
Krzysztof R. Apt
CWI, Amsterdam, The Netherlands
MIMUW, University of Warsaw, Warsaw, Poland
Ernst-Rüdiger Olderog
University of Oldenburg, Oldenburg, Germany
Abstract
We present a history of Hoare’s logic.
Contents
-
9.3 Advanced topics in the verification of object-oriented programs
-
10.1 Weakest precondition semantics and systematic program development
1 Introduction
Hoare’s logic is a formalism allowing us to reason about program correctness. It was introduced fifty years ago in the seminal article [Hoa69] of Tony Hoare that focused on a small class of while programs, and was soon extended by him in [Hoa71a] to programs allowing local variables and recursive procedures. This approach became the most influential method of verifying programs, mainly because its syntax-oriented style made it possible to extend it to almost any type of programs. Also, thanks to parallel developments in program semantics, this approach leans itself naturally to a rigorous analysis based on the methods of mathematical logic. Since then, several books appeared that discuss Hoare’s logic, or at least have a chapter on it: [dB80, LS87, TZ88, Fra92, Win93, AFPdS11, Ben12], to name a few.
More than thirty years ago two surveys of Hoare’s logic appeared, [Apt81], concerned with deterministic programs, and [Apt84], concerned with nondeterministic programs. At the beginning of the nineties an extensive survey [Cou90] was published that also included an account of verification of parallel programs and a discussion of other approaches to program verification.
A systematic exposition of Hoare’s logics for deterministic, nondeterministic and parallel programs appeared in our book [AO91]. The last edition of it, [AdBO09], written jointly with F.S. de Boer, extended the presentation to recursive procedures and object-oriented programs. In this paper we occasionally rely on the material presented in this book, notably to structure the presentation.
Given that the literature on the subject is really vast, we would like to clarify the scope of this survey. Our objective is to trace the main developments in Hoare’s logic that originated with the original article [Hoa69] and resulted in proof systems dealing with several classes of programs. To realize this natural research programme various difficulties, notably concerning the logical status of the proposed proof systems, had to be resolved. We clarify here these and other complications and explain how they were addressed.
In particular, we discuss the problem of completeness, the issues concerning local variables, parameter mechanisms, and auxiliary rules. We also discuss various alternatives to Hoare’s logic that were proposed in the literature. Given the scope of this exposition we discuss only briefly (in the final section) the use of automated reasoning in the context of Hoare’s logic. This important sequel to the research reported here deserves a separate survey.
According to Google Scholar, the original article [Hoa69] has been cited more than 7000 times. This forced us to make some selection in the presented material. Some omissions, such as the treatment of the nowadays less often used goto statement or coroutines, were dictated by our effort to trace and explain the developments that withstood the test of time.
Further, we do not introduce any program semantics. Consequently, we do not prove any soundness or completeness results. Instead, we focus on a systematic account of the established results combined with an explanation of the reasons why some concepts were introduced, and on a discussion of some, occasionally subtle, ways Hoare’s logic differs from customary logics.
We begin the exposition by discussing in the next section the contributions to program verification by Alan Turing and Robert Floyd that preceded those of Hoare. Then, in Section 3, we discuss Hoare’s initial contributions that focused on the while programs and programs with recursive procedures, though we extend the exposition by an account of program termination. Next, we discuss in Section 4 the soundness and completeness of the discussed proof systems. An essential difference between Hoare’s logic and first-order logic has to do with the features specific to programming languages, such as subscripted variables, local variables, and parameter mechanisms. We discuss these matters in Section 5. This provides a natural starting point for an account of verification of programs with arbitrary procedures, notably procedures that allow procedures as parameters. This forms the subject of Section 6.
In Section 7 we discuss verification of nondeterministic programs, the corresponding issue of fairness, and verification of probabilistic programs. Then, in Section 8 we focus on the verification of parallel and distributed programs. Next, in Section 9, we provide an account of verification of object-oriented programs. In the final two sections, 10 and 11, we shed light on alternative approaches to program verification, discuss briefly the use of automated verification in relation to Hoare’s logic, and attempt to explain and assess the impact of Hoare’s logic.
2 Precursors
2.1 Turing
The concern about correctness of computer programs is as old as computers themselves. Tracing the history of program verification is not the focus of this survey, so we only discuss here two key contributions preceding those of Tony Hoare. Readers interested in the early history of this subject are referred to the paper [Jon03] by C.B. Jones.
In 1949, Alan Turing gave a presentation entitled “Checking a Large Routine” at a conference in Cambridge U.K. at the occasion of the launching of the computer EDSAC (Electronic Delay Storage Automatic Calculator), published as [Tur49]. F.L. Morris and C.B. Jones recovered [MJ84] the original typescript of Turing’s presentation and made it available for a wider audience, thereby correcting several typing errors.
Turing started by asking
“How can one check a routine in the sense of making sure that it is right?”
and proposed that
“… the programmer should make a number of definite assertions which can be checked individually, and from which the correctness of the whole programme easily follows.”
Turing demonstrated his ideas for a flowchart program with nested loops computing the factorial of a given natural number , where multiplication is achieved by repeated addition; see Figure 1. Note that the effect of a command in the flowchart is represented by an equation like , where the primed variable denotes the value of the variable after the execution of the command. Today, this notation is still in use in logical representations of computation steps like in the specification language Z (see, e.g., [Spi92]) and bounded model checking.
Turing referred already to assertions. In the example he presented them in the form of a table referring to the numbers of the locations storing the variables , see Figure 2. From today’s viewpoint these assertions are admittedly very specific and difficult to read.
Turing was not only concerned with delivering correct values, but also with termination. He wrote
“Finally the checker has to verify that the process comes to an end. Here again he should be assisted by the programmer giving a further definite assertion to be verified. This may take the form of a quantity which is asserted to decrease continually and vanish when the machine stops.”
This refers already to the concept of a termination function. Turing stated a global termination function for the example program, i.e., an integer expression yielding a non-negative value that decreases with every step of the program.
Summarizing, Turing introduced the notions of assertions and termination functions, but did not state loop invariants and local termination functions for the two loops of the program. Still, as we show in the Appendix, his approach can be represented within the framework of Hoare’s logic.
2.2 Floyd
Robert Floyd was the first to propose a fully formal method for proving the correctness of flowchart programs known as inductive assertions method in [Flo67]. (Floyd actually mentions that his work is “based on ideas of Perlis and Gorn, and may have made their earliest appearance in an unpublished paper by Gorn.”) Here the assertions are logical formulas in terms of the variables appearing in the flowcharts. The begin of the flowchart is annotated with an assertion stating the assumptions under which the flowchart is supposed to work. The end of the flowchart is annotated with an assertion specifying the desired result. To verify that these input-output annotations are correct, each loop of the flowchart needs to be annotated at some selected point with an assertion that should hold whenever the control reaches this point. The assertion should thus be an invariant at this selected point. Floyd states rules how to verify this by completing the flowchart so that there is at least one assertion between any two subsequent statements. The rules explain how to modify a given assertion when passing a test statement and when passing an assignment statement. When two assertions are adjacent to the same arc then the logical implication has to hold in the direction of the arc.
In Figure 3 we show Turing’s example as a flowchart with annotations according to Floyd’s method. At the begin of the flowchart the annotation states the assumption of the computation, at the end the annotation specifies the desired result that should hold whenever the computation reaches . To verify that this annotation is correct, in every loop a point needs to be selected and annotated with an invariant. In this example, we select the bullet points and annotate them with the assertions
[TABLE]
and
[TABLE]
While the inductive assertions method is a natural approach to program verification, it is limited to programs that can be represented as flowcharts. This obvious deficiency was overcome by Hoare by proposing an approach that is applicable to programs written in the customary textual form.
3 Hoare’s Contributions
3.1 Reasoning about while programs
To reason about programs Hoare introduced in [Hoa69] a new notation
[TABLE]
with the interpretation
“If the assertion is true before initiation of a program , then the assertion will be true on its completion.”
Nowadays one rather writes
[TABLE]
so that additional assertions can be freely inserted in the program text, by putting the brackets around them. Such a possibility will turn out to be especially important when reasoning about parallel programs. In what follows we shall use the latter notation. In this context is referred to as a precondition and as a postcondition.
Subsequently Hoare introduced an axiom to reason about the assignment statement and the proof rules to reason about the program composition and the while statement. He also introduced two consequence rules, now combined into one, that allow one to strengthen the precondition and to weaken the postcondition. He then used these axioms and rules to establish correctness of the following simple program, let us call it DIV, that finds “the quotient and a remainder obtained on dividing by ”:
[TABLE]
All variables are assumed to range over the nonnegative integers.
In what follows we review these steps. We view assertions as formulas in some first-order language and assume from the reader some rudimentary knowledge of basic concepts of logic. The assignment axiom has the form:
ASSIGNMENT
[TABLE]
where is a variable, is an expression, and is the result of substituting for all free occurrences of in .
The already mentioned consequence rule has the following form:
CONSEQUENCE
[TABLE]
Here it is assumed that the mentioned implications can be established in some further unspecified proof system exclusively concerned with the assertions. (Hoare just referred to as ‘logical implication’.)
The final two rules were:
COMPOSITION
[TABLE]
and
WHILE
[TABLE]
Nowadays one refers to the assertion that satisfies the premise of this rule as a loop invariant.
Hoare’s correctness proof of the DIV program is presented in Figure 4. (Hoare wrote the postcondition of the conclusion of the WHILE rule as \neg B\mbox{\ \wedge\ }P and this is how it is recorded in Figure 4.) It yields the desired conclusion that is the quotient and the remainder resulting from dividing by . The crucial step in this proof is line 10 that clarifies the role played by the assertion . This line establishes that is a loop invariant of the considered while statement and its discovery is essential for the proof to succeed.
As pointed out in [JR10] the assignment axiom was originally proposed in [Kin69], the PhD thesis of J. King. From [Flo67] one can distill a more complex assignment axiom
ASSIGNMENT I
[TABLE]
that reasons “forward” starting from the precondition .
The striking simplicity of the ASSIGNMENT axiom reveals a close relation between the assignment statement and the substitution operation. This is achieved, in contrast to Floyd’s approach, by reasoning ‘backwards’, so starting from the postcondition . The adoption of this axiom by Hoare probably influenced a couple of years later Edsger W. Dijkstra to propose the weakest precondition semantics that adopted this reasoning ‘backward’ to all program statements. We shall discuss this alternative approach to program verification in Section 10. From the mathematical point of view, Hoare’s proof rules and axioms form an unusual mix: the assignment axiom adopts ‘backward’ reasoning, while the proof rules embrace ‘forward’ reasoning, in the sense that they maintain the view that a program is a transformation of a precondition to a postcondition.
Historically, Hoare’s approach was preceded by P. Naur’s paper [Nau66] in which a simple Algol 60 program that finds the greatest element in an array of numbers was verified using ‘snapshots’, which are in fact assertions. However, Naur’s reasoning is not backed up by any proof rules. His paper closes with this remark: “Similar concepts have been developed independently by Robert W. Floyd (unpublished paper, communicated privately).” that clearly refers to Floyd’s paper discussed in the previous subsection.
Hoare’s paper turned out to be the beginning of a far reaching change in reasoning about programs, resulting from moving from flowcharts to programs expressed in the customary textual form. This opened the way to reasoning about programs that cannot be readily expressed as flowcharts, for example, recursive procedures or programs with variable declarations. Also it made it possible to adopt a syntax-directed reasoning about programs by using their structure as guidance in organizing the proof.
A related, implicit, feature of the proof system proposed by Hoare is that it encourages program development by allowing one to first specify the desired preconditions and postconditions of a program component and subsequently to look for a program fragment for which the corresponding correctness statement can be established. Hoare took a lead in this novel view of program correctness by publishing in [Hoa71b] a correctness proof of the FIND program, the purpose of which is to find the th largest element of an array by rearranging its elements so that upon termination
[TABLE]
The program is very subtle —it uses a triply nested while loop— and as a result its correctness proof is highly nontrivial. The proof is not carried out in the proof system of [Hoa69] but from the way it is written it is clear that it can be done so. In fact, Hoare refers in a number of places to invariants that he defines as formulas that remain true throughout the execution of the program independently of the values of the program variables.
A similar in style contribution is [Hoa72b], in which a correctness proof was given of a program encoding the sieve of Eratosthenes. The difference was that the program was developed together with its correctness proof and presented using non-recursive procedures and classes, drawing on the contemporary works of E.W. Dijkstra on structured programming and O.J. Dahl on the object-oriented programming language SIMULA 67, which appeared as chapters in [DDH72]. These two contributions of Hoare, [Hoa71b] and [Hoa72b], showed that his original logic could be seen not only as a tool to verify programs but also as a guide to design correct programs. These ideas were further developed by Dijkstra, notably in his book [Dij76a].
3.2 Reasoning about recursive procedures
Let us continue with another milestone in the history of Hoare’s logic. Foley and Hoare established correctness of the program Quicksort [FH71], originally proposed by Hoare in [Hoa61]. Foley and Hoare stated:
“The purpose of the program Quicksort is to sort the elements to of an array into ascending order, while leaving untouched those below and above .”
The main difficulty was that Quicksort uses recursion. (Actually it was the first non-trivial example of a successful use of recursion in imperative programming.) This required appropriate proof rules that were introduced by Hoare in [Hoa71a].
In what follows, given a program we denote by the set of variables that are subject to change in it. In general, this set depends on the initial state of the program, but one can define syntactically a superset of it that takes care correctly of local variables and multiple procedure declarations. In what follows we mean by this syntactically defined superset.
Further, we use to denote the declaration of a procedure with the body and two disjoint lists of distinct formal parameters: is the list of all global variables of which are subject to change by , i.e., , and is the list of all other global variables of (read-only variables). (Hoare actually used a slightly different notation that is now obsolete.)
Legal procedure calls are of the form , where
- •
is a list of distinct variables of the same length as that are substituted for ,
- •
is a list of expressions not containing any variable of , of the same length as , that are substituted for .
The following proof rule dealt with a ‘generic’ procedure call :
RECURSION
[TABLE]
where the procedure is declared by .
(Hoare actually included the procedure declaration as an additional premise of the rule.) What is the intuition behind this rule? Hoare states in [Hoa71a] that it permits
“the use of the desired conclusion as a hypothesis in the proof of the body itself.”
More specifically, the symbol in the premise denotes the provability relation. So this rule is actually a metarule. According to [FH71] the premise of this rule
“permits to be assumed as a hypothesis in the proof of .”
This proof is supposed to be carried out using the remaining axioms and proof rules. The conclusion of the rule then coincides with this hypothesis.
To transfer a result established by the recursion rule to any other procedure call with actual parameters, say the lists and , the following substitution rule was introduced:
SUBSTITUTION
[TABLE]
where the following holds for the substitutions applied to and :
- •
is a list of free variables of or that do not occur in or , but which occur in or ,
- •
is a list of fresh variables of the same length as that are substituted for . So the variables in do not appear globally in the procedure body , are not free in or , and do not occur in or ,
- •
and are such that the call is legal.
So the substitution of the formal parameters by the actual ones is carried out together with an appropriate renaming of the ‘potentially conflicting’ variables in and .
Hoare noted that the above two rules are not sufficient to reason about recursive procedures. To have a more powerful proof method, he introduced the following rule, where stands for the set of free variables in an assertion and similarly with . Further, for a list of variables, denotes the set of all variables occurring in . Similarly, denotes the set of all variables occurring in the lists and .
ADAPTATION
[TABLE]
where is a list of variables with .
The precondition of the conclusion of this rule looks complicated. What does it express? Hoare explained in [Hoa71a]:
“If is the desired result of executing a procedure call, , and is already given, what is the weakest precondition such that is universally valid? It turns out that this precondition is \exists\,\mathbf{z}\;(P\land\forall\mathbf{a}\;(Q\mbox{>\rightarrow>}R)).”
We shall discuss this rule further in Subsection 5.1.
To deal with the declarations of local variables Hoare introduced the following rule:
DECLARATION
[TABLE]
where and does not appear in unless the variables and are the same.
Additionally, a proof rule, originally proposed in [Lau71], to reason about the conditional if-then statement was used. We present here instead a more common rule that deals with the if-then-else statement:
CONDITIONAL
[TABLE]
The correctness proof of Quicksort by Foley and Hoare in [FH71] was carried out using the above proof rules, originally presented in [Hoa71a]. The authors formulated two correctness criteria that should hold upon termination of Quicksort:
- •
Sorted: the output array should be sorted within the given bounds and .
- •
Perm: the output array should be a permutation of the original input array within the given bounds and but untouched outside these bounds.
The proof established these properties simultaneously, using appropriate assertions. In [AdBO09] a detailed modular correctness proof of Quicksort was given. Modular means here that the property Perm was proved first and next, based on this result, the property Sorted.
3.3 Reasoning about termination
So far we did not discuss within Hoare’s logic the subject of program termination. Nowadays, one talks of partial correctness, which refers to the conditional statement ‘if the program terminates starting from a given precondition, then it satisfies the desired postcondition’ and this is precisely what Hoare’s proof system allows one to accomplish. A more demanding property is total correctness, which stipulates that all program computations starting from a given precondition terminate and satisfy the desired postcondition. To formalize these notions we need to refer to the program semantics. We shall discuss it in the next section.
All approaches to proving program termination within Hoare’s logic formalize Floyd’s [Flo67] observation that
“Proofs of termination are dealt with by showing that each step of a program decreases some entity which cannot decrease indefinitely.”
The challenge is to incorporate such a reasoning into Hoare’s framework in a simple way. The first extension of Hoare’s proof system to total correctness was proposed in [MP74], but the proposed strengthening of the WHILE rule was somewhat elaborate. In [Har79] the appropriate rule took a simpler form:
WHILE I
[TABLE]
where is an assertion with a free variable that does not appear in and ranges over natural numbers.
Still, a disadvantage of this rule is that it requires to find a parameterized loop invariant such that the value of decreases exactly by 1 with each loop iteration. Such a precise information is not needed to establish termination and sometimes is difficult to come up with.
Additionally, it is often inconvenient to reason about partial correctness and termination at the same time. These concerns were addressed in the following proof rule introduced in [OG76a] that adds two new premises to the original WHILE rule:
WHILE II
[TABLE]
where is an integer expression, called a termination function (sometimes called a bound function or a variant), and is an integer variable that does not appear in or .
This proof rule corresponds to Dijkstra’s modification of his weakest precondition semantics proposed in [Dij76b] and reproduced as [Dij82]. Returning to the DIV program from Subsection 3.1 note that it does not terminate when . To prove its termination one needs to assume that initially and use a stronger loop invariant, namely . The termination function is particularly simple here: it is just . The relevant claims,
[TABLE]
and
[TABLE]
are straightforward to prove.
Hoare did discuss program termination in the already discussed [Hoa71b], where he showed termination of the FIND program. Since this property is not captured by his proof system from [Hoa69], he used informal arguments. According to the above terminology, he established total correctness of the program FIND. Hoare noticed that the termination proof required new invariants in addition to those needed for proving partial correctness. However, he did not introduce the concept of a termination function with a corresponding proof rule for total correctness of while programs.
To deal with the total correctness of the recursive procedures the following analogue of the WHILE I rule was proposed independently in [Cla76] and [Sok77]:
RECURSION I
[TABLE]
given the procedure declaration , and where is an assertion with a free variable that does not appear in and ranges over natural numbers.
This rule shares with the WHILE I rule the same disadvantage concerning the parameterized assertion . This matter was addressed in [AdBO09], where the following analogue of the WHILE II rule was used for recursive procedures:
RECURSION II
[TABLE]
given the procedure declaration , where is a termination function, is an integer variable that does not occur in and and is treated in the proofs as a constant.
The last restriction means that in the proof in the first premise no proof rules are apply quantification or substitutions to the variable . Examples of such rules are introduced in Subsection 5.1. We shall discuss the need for such a restriction in Subsection 6.1.
In the presentation of the correctness of the recursive procedure Quicksort in [FH71] only few remarks were spent on termination. In [AdBO09] termination of this program was proved using an extension of the RECURSION II rule to procedures with the call-by-value parameter mechanism.
4 Soundness and Completeness Matters
4.1 Preliminaries
In mathematical logic a standard way to judge the adequacy of a proof system is by means of the soundness and completeness concepts. It is then legitimate to address these matters for the proof systems introduced in the previous section. This requires some care since the CONSEQUENCE rule also uses implications between assertions as premises, the WHILE II rule refers to integer variables and expressions, whereas the RECURSION rules refer in their premises to the provability relation. For these considerations one needs to define some semantics with respect to which the introduced axioms and proof rules can be assessed.
To proceed in a systematic way we need to recall some basic notions from mathematical logic. Assume a first-order language . An interpretation for consists of
- •
a non-empty domain ,
- •
an assignment to each -ary function symbol in of an -ary function over ,
- •
an assignment to each -ary predicate symbol of an -ary relation over .
Given an interpretation , a state is a function from the set of variables to the domain . The definition of disregards our assumption that all variables are typed. However, it is easy to amend it by replacing the domain by the set of typed domains and by stipulating that each variable ranges over the domain associated with its type.
The next step is to define, given an interpretation and a state , the value of an expression and when satisfies a formula of , written as . We omit both definitions. We then say that a formula is true (or valid) in , written as , if for all states we have .
The consecutive step is to define semantics of the underlying programming concepts. This can be done in a number of ways. The common denominator of all approaches is the above concept of a state. Assume that all function and predicate symbols of the considered programming languages belong to the assumed first-order language. (In fact, this assumption is already implicit in the way assertions are formed in the ASSIGNMENT axiom and the WHILE rule.) However, some adjustments are needed to deal with more complex expressions that are customary in programming languages. In particular, we need to extend the domain of the states to array variables. We stipulate that to such variables a state assigns a function from the domain of the array to the range type. Using such a function we can then assign values to expressions that use array variables. As the complexity of the considered programming language grows, its expressions become more involved and the concept of the state gets more complex. At this stage we limit ourselves to the notion of a state that assigns values to all simple variables (i.e, variables of a simple type) and array variables.
The final step is to define semantics of the programs. Several approaches were proposed in the literature. Their discussion and comparison is beyond the scope of this paper. For the sake of the subsequent discussion we assume a semantics of the programs that allows us to define computations of each considered program, which are identified here with the sequences of states that can be generated by it.
In Hoare’s logic the types of the variables in the considered programs, for instance in the program DIV studied in Figure 4, are usually omitted and one simply assumes that all variables are typed and that the considered programs are correctly typed.
4.2 Soundness
Let us return now to assertions and programs. Suppose that all assertions are formulas in a given first-order language and that all considered programs use function and predicate symbols of . Each interpretation for then determines the set of states and thus allows us for each program to define the set of its computations over . This in turn allows us to introduce the following notions.
Let be an interpretation. We say that the correctness formula is true in in the sense of partial correctness if the following holds:
every terminating computation of over that starts
in a state that satisfies ends in a state that satisfies .
Further, we say that the correctness formula is true in in the sense of total correctness if the following holds:
every computation of over that starts in a state that
satisfies terminates and ends in a state that satisfies .
Denote now by the original proof system of Hoare presented in Subsection 3.1 and by the proof system obtained from by replacing the WHILE rule by the WHILE II rule. The following two results capture the crucial properties of these proof systems.
Soundness Theorem 1 Consider a proof of the correctness formula in the proof system that can use in the applications of the CONSEQUENCE rule assertions from a set . Consider an interpretation in which all assertions from are true. Then is true in in the sense of partial correctness.
This property of the proof system is called soundness in the sense of partial correctness. It was first established in [HL74] w.r.t. the relational semantics in which programs were represented as binary relations on the sets of states. Returning to the original proof of [Hoa69] presented in Figure 4, the appropriate set of the assertions consists of the formulas listed in lines 1 and 6. Since they are true in the standard interpretation of Peano arithmetic, we conclude by the above theorem that the established correctness formula listed in line 12 of Figure 4 is true in in the sense of partial correctness.
The following counterpart of of the above theorem justifies the reasoning about termination. It is, however, important to read it in conjunction with the qualifications that follow.
Soundness Theorem 2 Consider a proof of the correctness formula in the proof system that can use in the applications of the CONSEQUENCE rule assertions from a set . Consider an interpretation in which all assertions from are true. Then is true in in the sense of total correctness.
This property of the proof system is called soundness in the sense of total correctness. The first proof was given in [Har79] and referred to the proof system in which instead of the WHILE II rule the WHILE I rule was used. In this rule the assertion refers to a free variable that ranges over natural numbers. To guarantee the correct interpretation of such assertions one needs to ensure that in each state such a variable is interpreted as a variable of type ‘natural number’. In [Har79] this is achieved by considering assertion languages that extend the language of Peano arithmetics and by limiting one’s attention to arithmetic interpretations. These are interpretations that extend the standard model for arithmetic.
In the case of the WHILE II rule similar considerations are needed to ensure the correct interpretation of the integer expression and the integer variable . The corresponding result was given in [AO91] and reproduced in the subsequent two editions of the book. As in [AO91] all variables are assumed to be typed, and are correctly interpreted and the need for the arithmetic interpretations disappears.
4.3 Completeness
The completeness of the and proof systems aims at establishing some form of converse of the Soundness Theorems. It is a subtle matter and requires a careful analysis. Let us start with the proof system . It is incomplete for an obvious reason. Consider for instance the correctness formula . By the ASSIGNMENT axiom we get . To conclude the proof we need to establish the obvious implication and apply the CONSEQUENCE rule. However, we have no proof rules and axioms that allow us to derive this implication.
A way out is to augment by a proof system allowing us to prove all true implications between the assertions. Unfortunately, in general such proof systems do not exist. This is a consequence of two results in mathematical logic. The first one states that the set of theorems in a proof system with recursive sets of axioms and finitary rules is recursively enumerable. The second one is Tarski’s undefinability theorem of 1936, see [Tar36]. It implies that the set of formulas of Peano arithmetic that are true in the standard model of arithmetic is not arithmetically definable, so in particular not recursively enumerable. This means that completeness of the proof system cannot be established even if we add to it a proof system concerned with the assertions.
A natural solution is to try to establish completeness relative to the set of true assertions, that is to use the set of true assertions as an ‘oracle’ that can be freely consulted in the correctness proof. However, even then a problem arises because the assertion language can fail to be sufficiently expressive. Namely [Wan78] exhibited a true correctness formula that cannot be proved because the necessary intermediate assertions cannot be expressed in the considered assertion language. Simpler examples of such assertion languages were provided in [BT82a].
A solution to these complications was proposed by S.A. Cook in [Coo78]. To explain it we need to introduce some additional notions. We call a set of states definable in an interpretation iff for some formula we have .
Next, we assign to each program its meaning relative to , defined by
[TABLE]
At this moment the set \mbox{{\cal M}_{I}[![{S}]!]}(\sigma) has at most one element, which will not be anymore the case when nondeterministic or parallel programs are considered.
Then given an assertion and a program we define
[TABLE]
So is the set of states that can be reached by executing over starting in a state satisfying ; ‘’ stands for the strongest postcondition.
We then say that the language is expressive relative to an interpretation and a class of programs if for every assertion and program the set of states is definable. Finally, given a first-order language , a proof system for a class of programs is called complete in the sense of Cook if for every interpretation such that is expressive relative to and the following holds:
every correctness formula true in in the sense of partial
correctness can be proved in assuming all true formulas in .
In other words, completeness in the sense of Cook is a restricted form of relative completeness mentioned above, in which we limit ourselves to the class of interpretations w.r.t. which the underlying language is expressive. The following result is a special case of a theorem established in [Coo78].
Completeness Theorem The proof system for partial correctness of the while programs is complete in the sense of Cook.
The main difficulty in the proof, that proceeds by induction on the program structure, consists in finding the loop invariants. A simpler argument was provided in [Cla79], where a dual definition of expressiveness was used. Instead of the strongest postcondition it relied on the so-called weakest liberal precondition, which, given an interpretation , assertion and a program , is defined by
[TABLE]
So is the set of states from which all terminating computations of over end in a state satisfying . The qualification ‘liberal’ refers to the fact that termination is not guaranteed. The assumption that the set of states is definable makes it possible to find a very simple loop invariant. Namely, assuming that \{{P}\}\ {\mbox{\mbox{{\bf while}\ }{B}\ \mbox{{\bf do}\ }{S}\ \mbox{{\bf od}}}}\ \{{Q}\} is true in an interpretation such that is expressive relative to it in this revised sense, it turns out that a loop invariant is simply an assertion defining wlp_{I}(\mbox{\mbox{{\bf while}\ }{B}\ \mbox{{\bf do}\ }{S}\ \mbox{{\bf od}}},Q). Additionally, both and are true in , which allows one to establish \{{P}\}\ {\mbox{\mbox{{\bf while}\ }{B}\ \mbox{{\bf do}\ }{S}\ \mbox{{\bf od}}}}\ \{{Q}\} by the WHILE and CONSEQUENCE rules.
The above completeness result led to a number of works that tried to clarify it in a logical setting. In particular, J.A. Bergstra and J.V. Tucker noticed in [BT82b] that expressiveness is not a necessary condition for a Hoare’s logic to be complete. Indeed, if one takes as the assertion language the language of Peano arithmetic, then there exist interpretations for which it is not expressive, while all correctness formulas that are true in in the sense of partial correctness can be proved in the proof system .
We should also mention here a proposal put forward in [BG87] by A. Blass and Y. Gurevich. They suggested to use a different assertion language than first-order logic (or its multi-sorted variants dealing with subscripted variables or typed variables). The proposed assertion language is a fragment of the second-order logic, called existential fixed-point logic (EFL). EFL extends a fragment of first-order logic, in which negation is applied only to atomic formulas and the universal quantifier is absent, by a fixed-point operator. The authors showed that EFL is sufficient for proving relative completeness of the proof system without any expressiveness assumption. The reason is that both the strongest postconditions and the weakest liberal preconditions of the while programs (also in presence of recursive parameterless procedures) are definable in EFL.
Different insights on the relative completeness can be obtained by just limiting the assertion language to propositions. The resulting propositional fragment of Hoare’s logic of while programs (PHL) can then be studied in a purely algebraic way, by means of an equational reasoning. D. Kozen showed in [Koz00] that an extension of Kleene’s algebra of regular expressions with tests (KAT) subsumes PHL. In this setting the program is represented by the expression and the correctness formula by the equation , where is the complementation operator of KAT. After this translation the proof rules of the proof system become theorems of KAT. Further, after defining validity of implications between conjunctions of expressions using a relational semantics, a counterpart of the completeness result can be established for PHL. This shows that reasoning within propositional Hoare’s logic can be represented by purely equational reasoning. This work was followed by [KT01], where it was clarified how the notion of completeness in the sense of Cook can be captured by adding the weakest liberal precondition to the assertion language and an appropriate axiomatization of it to the axioms of KAT.
An even more general analysis of soundness and relative completeness of the proof system was presented in [AMMO09] within the framework of category theory, using a simple theory of pre-ordered sets. Such a general approach allowed the authors to derive new sound and relatively complete Hoare’s logics for the runtime analysis and for verification of linear dynamical systems.
Consider now the proof system for total correctness of while programs. To establish its completeness in the appropriate sense we encounter the same complications as in the case of , but additionally we have to deal with the problem of definability of the termination functions used in the WHILE II rule. In [Har79] completeness was established for the assertion languages that extend the language of Peano arithmetic and for arithmetic interpretations defined in the previous subsection, but the paper considered the WHILE I rule in which the termination functions are absent. To be able to express in the assertion language the parameterized loop invariants the definition of an arithmetic interpretation stipulates that there is a formula in the assertion language that, when interpreted, encodes finite sequences of the domain elements by one element.
In [AO91] and the subsequent two editions of the book relative completeness of was established. To this end, it was assumed that the underlying assertion language is expressive, which meant that for every while loop there exists an integer expression such that whenever terminates when started in a state , then the value is the number of loop iterations. In the adopted setup the assumption that all variables are typed automatically ensures that the considered interpretations included the standard model of Peano arithmetic and that is a natural number.
5 Fine-tuning the Approach
The matters discussed until now gloss over certain issues that have to do with the adjustments of the preconditions and postconditions, various uses of variables, and procedure parameters. In this section we discuss closely these matters, as they reveal some differences between customary logics and Hoare’s logic and show the subtleties of reasoning about various uses of variables in the context of programs.
5.1 Adaptation rules
In Hoare’s logic we see two types of rules. First, for each programming construct there is at least one axiom or rule dealing with its correctness. Together, they make possible a syntax-directed reasoning about program correctness. Second, there are proof rules where the same program is considered in the premise and the conclusion. These rules allow us to adapt an already established correctness formula about to another proof context. Most prominent is the CONSEQUENCE rule that allows us to strengthen the precondition to a precondition with P\mbox{>\rightarrow>}P_{1} and to weaken the postcondition to a postcondition with Q_{1}\mbox{>\rightarrow>}Q, thus arriving at the conclusion . Another one is Hoare’s ADAPTATION rule dealing with procedure calls. Hoare stated in [Hoa71a] that in the absence of recursion, i.e., in his proof system for while programs, his ADAPTATION rule is a derived rule. So the power of this rule is only noticeable in the context of recursion.
Other rules can be conceived that are concerned with the same program in the premise and conclusion. For example, the following rules were introduced in [Har79] and [AdBO09]. Here and elsewhere we denote the set of variables of a program by .
INVARIANCE
[TABLE]
where \mathit{free}(P)\cap change(S)=\mbox{\emptyset}.
-INTRODUCTION
[TABLE]
where .
SUBSTITUTION I
[TABLE]
where (\{\mathbf{z}\}\cap var(S))\cup(var(\mathbf{t})\cap change(S))=\mbox{\emptyset}.
We shall return to these rules shortly. But first, following [Old83b], let us discuss the ADAPTATION rule in the more general setting of programs. We say that a program is based on a finite set of variables if holds. Now we can recast Hoare’s ADAPTATION rule as follows:
ADAPTATION I
[TABLE]
where and are lists of variables, is based on , and .
Following Hoare, the precondition in the conclusion of this rule intends to express the weakest precondition such that holds (in the sense of partial correctness), assuming that is the desired result of executing and is already established. This intention can be phrased as follows: find the weakest assertion such that holds for all programs based on that satisfy . In [Old83b] this precondition was calculated as follows:
[TABLE]
where is a list of fresh variables of the same length as with and .
Comparing with the precondition used in the conclusion of the ADAPTATION I rule shows that the implication
[TABLE]
holds but the converse is false. Thus Hoare’s precondition is sound but is stronger than necessary. This suggests the following variant of the rule:
ADAPTATION II
[TABLE]
where is based on and is the precondition calculated above.
To show the weakness of the Hoare’s ADAPTATION I rule in the context of recursive procedures, consider the following example essentially taken from [Old83b]. Let be the standard interpretation of integers and consider the procedure declaration
[TABLE]
where is an integer variable. Then the procedure call satisfies the following correctness formula
[TABLE]
where is a fresh variable . It expresses the fact that the procedure call leaves the variable unchanged. For the postcondition the ADAPTATION I rule (or, equivalently, the original ADAPTATION rule) permits us to conclude only
[TABLE]
whereas the weakest liberal precondition is expressed by the formula . This precondition is correctly calculated by the ADAPTATION II rule, which yields
[TABLE]
To compare the power of different adaptation rules in a systematic way, S. de Gouw and J. Rot [dGR16] used the following notion due to [Kle99]. A set of proof rules for a class of programs is called adaptation complete if for all assertions and finite sets of variables
- •
whenever for all programs based on the truth of implies the truth of in the sense of partial correctness,
- •
then for all program based on there is a derivation of from using only rules of , written as \mbox{{{P}}\ {S}\ {{Q}}}\vdash_{\mathcal{R}}\mbox{{{P^{\prime}}}\ {S}\ {{Q^{\prime}}}}.
By the result of [Old83b], the set is adaptation complete. Further, enjoys two properties, as noted in [dGR16]:
Other adaptation rules, like -INTRODUCTION and slightly weakened versions of the INVARIANCE and SUBSTITUTION I rules are derivable from . 2. 2.
Any derivation in can be replaced by a single application of each of the two rules in .
What about Hoare’s adaptation rule? Let . From the above example it follows that this set is not adaptation complete. Nevertheless, enjoys property 1, but not property 2 of .
The paper [Old83b] also investigated three other adaptation rules proposed in the literature. An adaptation rule introduced in [GL80] turned out to be sound but not adaptation complete when grouped together with the CONSEQUENCE rule. In turn an adaptation rule for the programming language Euclid given in [LGH*+*78] is not even sound, while an adaptation rule introduced in [CO81] is both sound and adaptation complete when grouped together with the CONSEQUENCE rule.
5.2 Subscripted and local variables
Subscripted variables In both [Hoa71b] and [FH71] programs with arrays were studied. To reason about assignments to the subscripted variables the ASSIGNMENT axiom was used, implicitly assuming that the definition of substitution to subscripted variables is obvious. This is indeed the case when the array subscripts are simple expressions, for example a constant or a simple variable, which was indeed the case for both programs analyzed there. However, in the case of more complex subscripts difficulties may arise, as the following example discussed in [dB80] shows. In the case of an assignment to a simple variable any correctness formula , where is a constant is true. However, the correctness formula
[TABLE]
is false. Indeed, given the precondition the execution of the assignment amounts to executing the assignment after which the expression evaluates to 2 and not 1. This suggests that the ASSIGNMENT axiom cannot be used for arbitrary subscripted variables.
This complication was clarified and solved in a systematic way in [dB80], by extending the definition of substitution to an arbitrary subscripted variable. The crucial step in the inductive definition of the substitution deals with the case when and , for which one defines
[TABLE]
So in the if case one checks whether after performing the substitution on the subscripts and are aliases —and substitutes in that case by — while in the else case one applies the substitution inductively to the subscript of .
J.W. de Bakker showed that with this extended definition of substitution the ASSIGNMENT axiom remains sound for subscripted variables. Different axioms for assignment to subscripted variables were given in [HW73, Gri78, Apt81]. In the first two references in the corresponding axiom an array is treated as a partial function and an assignment to a subscripted variable is interpreted as a change in the whole function.
Local variables Consider now the case of local variables. They can be viewed as a counterpart of bound variables in logical formulas. However, the situation is more complicated because of the dynamic character of variables in programming languages and the presence of procedures.
We discussed already completeness in the sense of Cook of the proof system given in [Coo78]. Cook actually considered an extension of the proof system by axioms and proof rules for a small programming language that allows variable declarations and nonrecursive procedures and proved its completeness in the above sense. However, the semantics of the block statement made the corresponding completeness result invalid. It is useful to discuss this matter more closely.
Local variables were already dealt with in the DECLARATION rule mentioned in Subsection 3.2. In [Coo78] a different rule was used in which the substitution was applied to the assertions and not to the programs, namely:
BLOCK
[TABLE]
where .
More precisely, a slightly adjusted version of this rule was used so that one could reason about variable declarations in the context of non-recursive procedures. But even without this adjustment a possible problem arises. Consider the program
[TABLE]
In many programming languages it would yield an error because the right-hand side of the second assignment refers to a value of the uninstantiated variable . However, according to the semantics proposed in [Coo78] such assignments were allowed. Local variables were modelled using a stack in which the last used value was kept on the stack and implicitly assigned to the next local variable. As a result the correctness formula
[TABLE]
was true according to the semantics though there is no way to prove it.
[Coo81] provided a corrigendum in which two possible fixes were suggested. One was to modify the semantics so that the proposed proof system is still complete. This can be achieved by assigning to each newly declared variable a register that has not been used before and modifying the notion of a state accordingly.
Another one was to require all newly declared variables to be initialized to some fixed value, say . This option was first used in [Gor75], where a variant of the BLOCK rule was used in which the initialization was modelled on the proof-theoretic level by the conjunct added to the precondition of the premise. To correct the proof of the relative completeness result given in [Coo78], one should then use an initialization of the local variables, both in the semantics and in the proof theory, so use the variant of the BLOCK rule given in [Gor75].
Yet another option is to require all newly declared variables to be explicitly initialized to some arbitrary expression. This approach was taken in [AdBO09], where the following more general version of the corresponding rule was used that allowed a declaration of a list of new variables:
BLOCK I
[TABLE]
where \mbox{{{\mathbf{x}}}}\cap free(Q)=\mbox{\emptyset}.
Here , where is a list of different variables and a corresponding list of expressions, is a parallel assignment, introduced in [Dij75] and further discussed in Section 10.
It is natural to postulate in this rule that the variables listed in do not appear in the expressions from . However, this is a syntactic condition concerning the program formation that is not needed to reason about partial correctness. Further, as we shall soon see, putting no restrictions on and turns out to be useful for modelling parameter passing in a subtle situation when some formal parameters happen to coincide with the global variables that are used in actual parameters.
The observant reader will notice that in the discussed rules substitution is used differently. In the DECLARATION rule the substitution is applied to the programs, in the BLOCK rule it is applied to the assertions, while —interestingly— in the BLOCK I rule it is not used at all. The resulting proof systems yield different results when applied to programs that use procedures. To illustrate the problem consider the parameterless procedure declared by , the program
[TABLE]
and the correctness formula
[TABLE]
To reason about the procedure call we add to the proof system the following degenerated version of the RECURSION rule:
COPY
[TABLE]
assuming the declaration of a parameterless non-recursive procedure .
In our case it allows us to derive from . This in turn allows us to derive
[TABLE]
Now, applying the DECLARATION rule we get (1).
However, using the BLOCK rule we get a different conclusion. Namely, we first establish
[TABLE]
from which
[TABLE]
follows.
Finally, if we use the BLOCK I rule, and therefore consider a slightly modified program
[TABLE]
we get
[TABLE]
These differences have to do with the way local variables are interpreted in the presence of procedures. According to the static scope policy the procedures should be evaluated in the environment in which they were declared, while according to the dynamic scope policy they should be evaluated in the environment in which they were called. So according to the static scope, which is adopted in most imperative languages, we should conclude (1) and not (2) or (3).
We conclude that the proof systems studied in [Coo78] and [Gor75] dealt with dynamic scope and not static scope. The same is in principle the case for [AdBO09], but one requires there that the local variables are first renamed so that they differ from global variables. The effect is that then static and dynamic scopes coincide. In the above example one thus considers the statement
[TABLE]
instead of . Then we get , as desired.
5.3 Parameter mechanisms and procedure calls
The call-by-name parameter mechanism was originally proposed in Algol 60. It was used in [Hoa71a] and [Coo78] and adopted in all subsequently discussed papers on procedures, unless stated otherwise. It boils down to a simultaneous substitution of the actual parameters for the formal ones, so naturally it was modelled in the SUBSTITUTION rule by a straightforward substitution.
However, a most commonly used parameter mechanism is call-by-value. According to its semantics the actual parameters are evaluated first and subsequently their values assigned to the formal parameters. Some other parameter mechanisms were occasionally used. For example, the programming language Pascal (see [JW75]) also allows the call-by-variable mechanism (also called call-by-reference), which is a mixture of call-by-name and call-by-value. The actual parameter has to be a variable. In case it is a subscripted variable, its index is evaluated first and the resulting subscripted variable is substituted for the formal parameter.
In [AdB77] it was proposed to model these two parameter mechanisms of Pascal by means of an appropriate syntactic transformation of the procedure body, that was called ‘syntactic application’. In what follows we use in the procedure declaration the qualification to indicate call-by-value and to indicate call-by-variable. Given a procedure declaration , so with called by value and called by variable, the call , where is an expression and a, possibly subscripted, variable, was modelled by the syntactic application defined by
[TABLE]
where is a simple variable and do not appear in or .
This leads to the following generalization of the COPY rule from the previous subsection:
CALL-BY-VALUE/CALL-BY-VARIABLE
[TABLE]
where the non-recursive procedure is declared by .
In [AdBO09] this approach to call-by-value was simplified by noting that no variable renaming is needed to model it. The resulting rule, that needs to be used in conjunction with the BLOCK I rule, became:
CALL-BY-VALUE
[TABLE]
where the non-recursive procedure is declared by .
To see how this rule correctly handles a subtle situation when a formal parameter coincides with a global variable used in an actual parameter, consider a procedure declared by
[TABLE]
Using the BLOCK I rule we can then establish the correctness formula
[TABLE]
from which
[TABLE]
follows by the CALL-BY-VALUE rule. This agrees with the semantics of the call-by-value parameter mechanism. (The stronger postcondition, can be established using the axioms and proof rules introduced in the next section.) So the assignment refers on the left-hand side to the formal parameter and on the right-hand side to the actual parameter that contains the global variable .
In [Apt81] it was suggested that other parameter mechanisms can also be modelled by means of an appropriate syntactic application, and subsequently reasoned about within Hoare’s logic. An example is the call-by-result parameter mechanism of Algol W, a precursor of Pascal (see [WH66]). According to it the actual parameter is either a simple or a subscripted variable. Upon termination of the call the value of the formal parameter is assigned to the actual parameter. In the case the actual parameter is a subscripted variable, its index is evaluated first. This parameter mechanism is used in conjunction with the call-by-value.
We shall return to this subject in the next section when discussing completeness of the counterparts of such rules for recursive procedures.
6 Reasoning about Arbitrary Procedures
6.1 Completeness results for recursive procedures
The relative completeness result established in [Coo78] dealt with the language considered in [Hoa71a] and Subsection 3.2, except that recursion was disallowed. To ensure soundness in the sense of partial correctness Cook stipulated that for the procedure calls no variable in different from formal parameters occurs globally in the procedure body.
Cook’s work was extended to the language in which recursive procedures were allowed in the Master Thesis of G.A. Gorelick, written under the supervision of Cook. The details are only available as a technical report [Gor75]. We present the essentials for the case of a single recursive procedure , in line with the presentation in Subsection 3.2.
The conceptual contribution of Gorelick is the introduction of most general formulas. He wrote:
“The completeness result for recursive programs is then obtained by exhibiting, for each recursive procedure , a “most general formula” such that , and for all true formulas about .”
Given a procedure declaration , a most general formula for the procedure is a correctness formula
[TABLE]
where is the list of variables that appear in the formal parameters and or have a global occurrence in , and is a list a fresh variables (not occurring in , or ), of the same length as that serves to freeze the initial values of the variables in before they are changed by . The formula is taken to express the strongest postcondition introduced in Subsection 4.3. Since the variables in and may appear in as free variables, describes the relationship between the initial values of represented by and the final values of computed by the procedure body and represented by itself.
The crucial properties of most general formulas are captured by the following lemmas due to [Gor75].
Lemma G1 If is true in in the sense of partial correctness then it can be derived from and the set of all true formulas in using “suitable adaptation rules”.
Lemma G2 For each procedure call the most general formula can be derived from the set of all true formulas in using Lemma G1 and the RECURSION rule.
The proof of Lemma G1 is based on the following axiom and adaptation rules, proposed in [Gor75] for the case where is a procedure call :
INVARIANCE
[TABLE]
where \mathit{free}(P)\cap var(S)=\mbox{\emptyset}.
CONJUNCTION
[TABLE]
VARIABLE SUBSTITUTION
[TABLE]
where
- •
\{\mathbf{z}\}\cap var(S)=\mbox{\emptyset},
- •
if for any component of the list , var(t_{i})\cap var(S)\neq\mbox{\emptyset}, then the corresponding component of the list satisfies .
Using Lemmas G1 and G2, Gorelick established the following result. (The result was actually established for a system of recursive procedures, so the RECURSION rule was appropriately generalized.)
Completeness Theorem For programs with recursive procedures as defined in Subsection 3.2, the proof system extended by the RECURSION and SUBSTITUTION rules of Subsection 3.2 and the above axiom and adaptation rules is complete in the sense of Cook.
Both [Coo78] and [Gor75] followed [Hoa71a] and used the call-by-name parameter mechanism. The restrictions imposed on the actual parameters of ‘legal’ procedure calls were partly lifted in [CO81]. Analogous research was carried out in [dB80] for the case of the call-by-value and call-by-variable parameter mechanisms in the presence of recursive procedures. To this end, the CALL-BY-VALUE/CALL-BY-VARIABLE rule from the previous section was modified to the following rule:
RECURSION III
[TABLE]
where the procedure is declared by and , i\in\mbox{{{1,\mbox{},n}}}, are the procedure calls that appear in and .
In [dB80] soundness and relative completeness for a corresponding proof system was proved. However, the proof was established only for the special case of a single recursive procedure, given the combinatorial explosion of the cases concerned with the relation between the actual and formal parameters. The main ideas of this proof were discussed in [Apt81].
Proof systems for recursive procedures with the call-by-value parameter mechanism were studied in a couple of other publications. In [vO99] a sound and relatively complete proof system was introduced for a programming language with local and global variables and mutually recursive procedures with the call-by-value mechanism, that allows for both static and dynamic scope. The proofs were not provided but it was mentioned that they were certified in the Isabelle theorem prover. In this work each assertion was identified with its meaning represented as a function from states to Boolean values. This approach simplifies the soundness and relative completeness proofs by avoiding various complications concerned with possible variable clashes (in particular, it obviates the use of the SUBSTITUTION rules), but makes it cumbersome to verify specific programs and deviates from the syntactic approach pursued in the literature on Hoare’s logic.
Further, in [AdBOdG12] soundness and relative completeness of the proof system introduced in [AdBO09] was established. The recursive procedures with the call-by-value parameter mechanism were dealt with by an appropriate modification of the CALL-BY-VALUE rule from the previous section.
However, in all these works on the call-by-value and call-by-variable parameter mechanisms correctness of each procedure call had to be dealt with separately. This is an obvious drawback, since the resulting correctness proofs are then not linear in the length of the program. It would be preferable if could establish a desired property for a ‘generic call’ just once, from which the needed properties of all specific calls would follow by some form of a substitution rule. In [AdBO09] it was observed that this can be achieved for the calls in which no actual parameter contains a global variable. Recently, K.R. Apt and F.S. de Boer introduced in [AdB19] a sound and relatively complete proof system that provides a satisfactory solution to this problem, without any restriction. They used a generalization of the following recursion rule to a system of mutually recursive procedures:
RECURSION IV
[TABLE]
where the procedure is declared by and \mbox{{{\mathbf{x}}}}\cap free(Q)=\mbox{\emptyset}.
It was combined with the following rule:
PROCEDURE CALL
[TABLE]
where the side conditions are the same as in the previous rule.
The resulting proof system uses the BLOCK I rule from the previous section, so it is appropriate for the dynamic scope. However, the authors pointed out that for a natural class of programs in which the global variables that occur in procedure bodies differ from the local variables, static and dynamic scopes coincide. Such a class of programs was first considered in [CO81].
So far we discussed partial correctness of programs with recursive procedures. In [Apt81] it was stated without a proof that a proof system corresponding to the one used in [Gor75] is sound in the sense of total correctness. In this system the INVARIANCE axiom was dropped (it is not sound for total correctness), the procedures had no parameters and the RECURSION rule was replaced by the RECURSION I rule. However, it was discovered in [AdB90a] that this claim is false. The problem has to do with the fact that the counter variable can be subject to quantifier elimination in the -INTRODUCTION rule, and to substitution in the SUBSTITUTION rule.
For example, given the procedure declaration of an obviously nonterminating procedure one can establish the premises and \mbox{{{P(n)}}\ {\mathbf{call}>p}\ {{\mathbf{true}}}}\vdash\mbox{{{P(n+1)}}\ {S}\ {{\mathbf{true}}}} of the above rule for and conclude by the RECURSION I and CONSEQUENCES rules.
The solution proposed in [AdB90a] was to stipulate that the counter variables are treated as constants in the -INTRODUCTION and SUBSTITUTION rules. This allowed the authors to prove both soundness and relative completeness of the resulting proof system for total correctness of recursive procedures without parameters w.r.t. the arithmetic interpretations introduced in Subsection 4.2. The above remarks explain why we added in the RECURSION II rule a qualification concerning the counter variable .
6.2 Clarke’s incompleteness result
Programming languages like Algol 60 [NBB*+*63] and Pascal [JW75] contain procedure mechanisms that are considerably more complex than what we discussed so far. In his seminal paper [Cla79], E.M. Clarke identified a combination of features for which it is impossible to obtain a Hoare-like proof system that is sound and relatively complete (in the sense of Cook). By a Hoare-like proof system we mean a set of syntax-directed proof rules for correctness formulas about programs in the programming language under consideration such that the application of each proof rule is decidable. Moreover, the proof system allows one to prove correctness formulas concerning programs from a given programming language.
Clarke proved this incompleteness result for a block-structured programming language which includes the following features that are present in Algol 60 and Pascal:
procedure names as parameters of procedure calls, 2. 2.
recursion, 3. 3.
static scope, 4. 4.
global variables in procedure bodies, 5. 5.
nested procedure declarations.
Clarke’s incompleteness result is based on the following two lemmas for Hoare-like proof systems and programming languages .
Lemma A If is sound and relatively complete for , then the divergence problem for is decidable for finite interpretations .
Lemma B If has a rich procedure concept including features 1–5, then its divergence problem is undecidable for all finite interpretations with at least two domain elements.
An interpretation is called finite if its domain is finite. A program in diverges for if never terminates when started with any input values from for its variables. The divergence problem for a programming language for an interpretation is the problem of deciding whether an arbitrary program of diverges.
The proof of Lemma A rests on the following general observations. A program of diverges for if and only if the correctness formula is true in in the sense of partial correctness. Since is sound and relatively complete, the latter is true if and only if is provable in , when all assertions in the proofs are interpreted in . Thus all diverging programs in can be recursively enumerated by enumerating all proofs in , thereby deciding in the assertions used in the applications of the CONSEQUENCE rule, which is possible because is finite. Trivially, also all non-diverging programs in can be recursively enumerated: simply start each program for all of its finitely many inputs from and enumerate it in case it halts for one of these inputs. Decidability of the set of all diverging programs follows since both the set and its complement are recursively enumerable.
For the proof of Lemma B, Clarke shows that queue machines (or Post machines), which have an undecidable halting problem, see, e.g., [Man74], can be simulated by programs from . A queue machine manipulates a queue and finitely many registers. A machine program is a finite sequence of labelled instructions of three types:
- •
enqueue that adds the value of register to the rear of the queue,
- •
dequeue that removes the front entry from the queue and puts into register , and
- •
if x=y then go to that branches to the instruction labelled with if the values of the registers and agree.
Clarke [Cla79] described his simulation idea of a queue machine with a program in as follows:
“The queue is represented by successive activations of a recursive procedure with the queue entries being maintained as values of the variable which is local to . Thus an addition to the rear of the queue may be accomplished by having call itself recursively. Deletions from the front of the queue are more complicated. also contains a local procedure which is passed as a parameter during the recursive call which takes place when an entry is added to the rear of the queue. In deleting an entry from the front of the queue, this parameter is used to return control to previous activations of and inspect the values of local to those activations. The first entry in the queue will be indicated by marking (e.g. negating) the appropriate copy of .”
From this description it is clear that the simulation program exploits the features 1, 2 and 5. Feature 4 is also needed since a global variable program_counter is used in the body of the procedure . Feature 3 (static scope) concerns the semantics of procedures and is needed to achieve the correct back pointers for the procedure in the runtime stack generated by the successive activations of the procedure .
Note that the procedure has a formal parameter that is instantiated with procedures, which in turn have no formal procedure parameters on their own. Here the concept of mode depth is helpful. The mode depth of a procedure is defined inductively. A procedure that may not take identifiers of procedures as parameters has mode depth 1. For any , a procedure that may take identifiers of procedures of mode depth has mode depth . Thus for Clarke’s simulation, procedures of mode depth suffice. This restriction is also obeyed in Pascal [JW75]. Procedures of an arbitrary finite mode depth, corresponding to arbitrary higher types, as in Algol 68 [vWMP*+*75], or even with self-application, i.e., with procedure calls of the form , as possible in Algol 60 [NBB*+*63], are not needed.
6.3 Clarke’s language
Clarke also claimed that each language obtained from by disallowing self-application and the feature of the above list has a sound and relatively complete Hoare-like proof system [Cla79]. However, he proved this only for the case of in which dynamic scope replaces static scope. The completeness argument rests on the fact that each program in has a finite range, where the range of is the set of different procedure calls that can be invoked in the computations of . He claimed that a similar proof system could be obtained for in which global variables are disallowed. His argument was that programs of can be transformed into schematically equivalent ones in , where nested procedure declarations are disallowed. Such programs have a sound and relatively complete Hoare-like proof system.
H. Langmaack and E.R. Olderog [LO80] discovered that this argument is wrong. They considered the formal execution trees of programs and showed that programs in may have trees with context-free path languages whereas programs in can generate only trees with regular path languages. Therefore they posed the challenge of developing a sound and relatively complete Hoare-like proof system for .
As a first step, Langmaack proved in [Lan82] that for all Algol-like programs in the divergence problem is decidable for finite interpretations. This is a necessary condition for the existence of a sound and relatively complete Hoare-like proof system according to Lemma A. Moreover, due to a theorem by R.J. Lipton [Lip77], this decidability result is also sufficient for the existence of a sound and relatively complete ‘Hoare logic’ for Algol-like programs in . However, Lipton’s notion of a ‘Hoare logic’ is rather weak: it means that the set of correctness formulas that are true in the sense of partial correctness is recursively enumerable relative to the underlying interpretation. Lipton’s theorem does not yield any usable, syntax-oriented proof rules.
First concrete axiomatizations for programs appeared independently in papers by Olderog [Old84] and W. Damm and B. Josko [DJ83]. The former studied the case of Pascal-like programs, i.e. with mode depth . The key idea is the use of second-order relation variables in the assertion language to stand for the behaviour of uninterpreted, symbolic procedures in a new SEPARATION rule. In order to determine what a procedure call of a procedure with an actual procedure parameter does, this rule first determines separately what does and what does with a symbolic procedure instead of represented by a formula and then composes both results using substitution. Applications of the SEPARATION rule have the effect of a systematic transformation of an initially non-regular formal execution tree into a regular tree at the cost of introducing higher-order tree combinators. The resulting regularity enables a suitably complete Hoare-like proof system.
The paper [DJ83] handled the more general case of Algol-like programs with arbitrary finite modes by using higher-order predicate variables and unevaluated substitutions to such variables. Common to both papers is that they deviated from the standard notion of relative completeness in that they used a higher-oder assertion language and an appropriate notion of expressiveness.
The status of the language was finally clarified in 1989 in an over 90 pages long paper by S.M. German, E.M. Clarke and J.Y. Halpern [GCH89] in which a Hoare-like proof system for was provided that is sound and relatively complete in the (original) sense of Cook. The completeness proof heavily relies on an appropriate arithmetic encoding of procedure declarations so that the assertion language remains first-order.
6.4 The characterization problem
Exploring the border between relative completeness and incompleteness (in the sense of Cook) of Hoare’s logics has been the focus of considerable research in the 1980s. Clarke called it the “Characterization Problem for Hoare Logics” in his survey article [Cla85]. The key question is what is meant by a ‘Hoare logic’. Several researchers proved results for a weak interpretation where a Hoare logic is just the set of correctness formulas that are true in the sense of partial correctness. Here the problem is for which classes of programs , assertions , and underlying interpretations this set is recursively enumerable or even decidable.
We cited already Lipton’s result [Lip77]. Since its proof was only sketched, Langmaack provided in [Lan79] a rigorous proof for the setting of Algol-like programs . Both Lipton and Langmaack restrict themselves to quantifier-free assertions . Clarke, German and Halpern established [CGH83] an “effective axiomatization of Hoare logics” extending Lipton’s result to first-order formulas . However, these results do not yield any usable, syntax-directed proof rules that are in the spirit of Hoare-like proof systems that appeared since the publication of [Hoa69]. Therefore Clarke stated in [Cla85]:
“Certainly the most important research problem is to develop a version of the characterization theorem that provides some insight as to when a syntax-directed proof system can be obtained.”
Two such characterization theorems were established in [Old81] and [Old83a]. The first paper studied a language of Algol-like programs with the features 1, 2, 4 and 5 of [Cla79] (see Subsection 6.2). Feature 3 (static scope) was not fixed but left as a parameter in the form of a copy rule. Such a rule defines how during program execution a procedure call is replaced by a copy of the procedure body. In the copy certain occurrences of local variables and procedures in the procedure body are renamed to avoid name clashes. By varying the copy rule, different program semantics varying from dynamic to static scope were defined. The COPY rule from Subsection 5.2 is a trivial example of such a rule in which no renaming takes place.
Parameterized by a given copy rule , a Hoare-like proof system for the partial correctness of Algol-like programs was introduced. A program was called -bounded if applications of the copy rule do not lead to programs with “procedural reference chains” of arbitrary length. A program has a finite -index if the relation of “substitutional equivalence” induces only finitely many equivalence classes in the set of reachable procedure calls. Due to this equivalence, the condition of finite -index is more liberal than the conditions of finite recursive cycle and finite range used by Gorelick [Gor75] and Clarke [Cla79], respectively, in their completeness proofs. The following result holds.
Theorem Suppose the assertion language is expressive relative to the considered interpretation and the copy rule . Then the following are equivalent for Algol-like programs and assertions :
can be proved in the proof system assuming all true formulas in . 2. 2.
has a finite -index and is true in in the sense of partial correctness. 3. 3.
is -bounded and is true in in the sense of partial correctness.
As corollaries to this theorem various completeness results were obtained in [Old81]. For the naive copy rule , which models “dynamic scoping”, the proof system is sound and relatively complete for the full set because all programs in are -bounded. This corresponds to Clarke’s language . For the Algol 60 copy rule , which models “static scoping”, the proof system is sound and relatively complete for the following sublanguages of because all programs in these sublanguages are -bounded:
- •
– all programs without procedure nesting, corresponding to Clarke’s language ,
- •
– all programs with parameterless procedures only,
- •
– all programs without procedures as parameters, corresponding to Clarke’s language ,
- •
– all programs in which formally recursive procedures are disallowed to have procedure identifiers as formal parameters, a superset of Clarke’s language ,
- •
– all programs without global formal procedure parameters.
The paper [Old83a] studied a set of programs with Pascal-like procedures , i.e., with mode-depth . Here a sublanguage is called admissible if it is closed under certain program transformations that leave the procedure structure invariant. In particular, these transformations allow for the introduction of global variables. A tree is regular if the set of paths in is a regular language in the Chomsky hierarchy or, equivalently, if has only finitely many different patterns of subtrees. The formal call tree of a program describes in which order the procedures of are called, where a branching appears when from one procedure several immediate successors can be called. The following theorem refers to a particular Hoare-like proof system that was introduced in [Old83a].
Theorem For every admissible language the following are equivalent:
There exists a sound and relatively complete Hoare logic for in the sense of Lipton. 2. 2.
The divergence problem for is decidable for finite interpretations. 3. 3.
All programs in have regular formal call trees. 4. 4.
The Hoare-like proof system is sound and relatively complete for .
Since contains programs with a non-regular formal call tree, the theorem implies that there is no sound and relatively complete Hoare logic for itself, a fact that follows from Clarke’s incompleteness result. Note that this theorem does not contradict the results obtained for because a sublanguage without global variables is not admissible.
7 Nondeterministic and Probabilistic Programs
7.1 Reasoning about nondeterminism
In the context of programming languages nondeterminism stands for the phenomenon that a program can yield more than one answer. In the sixties and early seventies a couple of simple programming constructs were proposed that introduced nondeterminism. In particular, in [Lau71] the nondeterministic statement was considered with the meaning: execute either or , and the following proof rule:
OR
[TABLE]
But the undoubtedly most successful and elegant proposal is the language of guarded commands introduced by E.W. Dijkstra in [Dij75] and in the book form in [Dij76a]. Dijkstra’s original motivation for introducing this language was to simplify programs by delaying some arbitrary choices to the implementation level and to restore symmetry that is not present in the if-then-else statement. This led to a specific proposal for nondeterminism.
For the sake of what follows it is sufficient to consider two crucial statements of Dijkstra’s language:
- •
the alternative command
[TABLE]
- •
repetitive command
[TABLE]
where each is a Boolean expression, called a guard, and each is a program statement. The symbol represents a nondeterministic choice.
The alternative command is executed by selecting a guard that evaluates to true and executing the associated statement . If more than one guard evaluates to true any of the corresponding statements may be executed next. If all guards evaluate to false, the execution of the alternative command results in a failure. The repetitive command is executed in a similar way, with two differences. First, after termination of a selected statement the repetitive command is executed again. Second, if all guards evaluate to false, the execution of the repetitive command simply terminates. So it is a natural generalization of the while statement.
As an illustration of the use of the alternative command consider the customary program for computing the maximum of two numbers using the conditional statement:
[TABLE]
A solution using the alternative command is symmetric in the variables and and also involves nondeterminism:
[TABLE]
As an illustration of the use of the repetitive command consider the customary while program for computing the greatest common divisor (gcd) of two natural numbers, initially stored in the variables and :
[TABLE]
Using the repetitive command the same algorithm can be written as
[TABLE]
Both programs terminate with the gcd stored in the variables and but the second program is more readable and, unlike the first one, is symmetric in the variables and .
To reason about the guarded command language Dijkstra introduced in [Dij75] the weakest precondition calculus that we briefly discuss in Section 10. This approach allows one to reason about total correctness. It is easy to conceive Hoare-style proof rules that deal with partial correctness of the alternative and repetitive commands (they were proposed first in [dB80]). For total correctness some care has to be exercised to deal with the absence of failures, which is a new concept in this framework. The appropriate rule, introduced in [Apt84], takes the following form:
ALTERNATIVE COMMAND II
[TABLE]
To obtain a proof system for total correctness of guarded commands it suffices now to deal with the termination of the repetitive command. The following natural generalization of the WHILE II rule was used in [AdBO09]:
REPETITIVE COMMAND II
[TABLE]
where is a termination function and is an integer variable not occurring in or for i\in\mbox{{{\mbox{}}}}.
7.2 Reasoning about fairness
Fairness is a concept that arises in presence of any form of nondeterministic choice. Suppose that we repeatedly have some choice among a fixed set of alternatives, for instance of going left or going right. If we repeatedly select the alternative of ‘going left’, then we systematically ignore the other alternative. In such case we can argue that the adopted selection procedure is not fair with respect to the other alternative, ‘going right’. To exclude such unfair selection procedures we need to focus on infinite ‘runs’ of selections of alternatives and make precise when an alternative can be selected.
These matters can be discussed in a more precise way using the guarded commands language. Consider the following program, where is a fixed natural number:
[TABLE]
It does not always terminate, since we can repeatedly select the first guard. The resulting computation is considered unfair since from some moment on the second guard is always enabled (i.e., evaluates to true), but never selected. Once the second guard is selected when it is enabled, the program terminates. More formally, we say that the above program terminates under the fairness assumption, which stipulates that each guard that is from some moment on continuously enabled is infinitely often selected.
As another example consider the following program, where is a test with the expected meaning:
[TABLE]
Also this program does not always terminate. The only infinite computation repeatedly ignores the second guard. However, in contrast to the previous example, in this infinite computation at no moment the second guard becomes continuously enabled. So even under the fairness assumption this program does not terminate.
On the other hand in this infinite computation the second guard is infinitely often enabled. We say that this computation is strongly unfair. If the second guard is selected when it is enabled, the program terminates. In this case we say that the above program terminates under the strong fairness assumption, which stipulates that each guard that is infinitely often enabled is infinitely often selected. (To stress the difference the first notion of fairness is usually called weak fairness.)
Both forms of fair termination can be established by means of appropriate proof rules. In what follows we explain the transformational approach proposed in [AO81] and in a journal form in [AO83]. To prove termination of a repetitive command under the assumption of weak (or strong) fairness (with respect to a precondition ) one can transform it into a repetitive command the computations of which coincide with the weakly (or strongly) fair computations of . To this end, we need a random assignment that assigns nondeterministically to the variable an arbitrary natural number. To understand why this command naturally arises when considering fairness, note that under both assumptions of fairness the program
[TABLE]
mentioned in [Dij76a] is equivalent to
[TABLE]
In what follows we limit ourselves to the presentation of strong fairness and to explain the idea we focus on a repetitive command with just two guards:
[TABLE]
The transformed program uses two auxiliary variables and ranging over natural numbers and has the following form:
[TABLE]
Informally, each variable tracks the number of times the corresponding guard is enabled and the augmented guards prevent that an infinitely often enabled guard is never selected.
To reason about the strong fair termination of it is now equivalent to reason about the termination of the program . To this end, we only need an axiom dealing with the random assignment. Such an axiom was proposed in [Har79]:
RANDOM ASSIGNMENT
[TABLE]
where does not appear free in .
But this indirect approach can be avoided by absorbing the transformation into the proof of termination of the program . This way one obtains a proof rule for establishing termination under the strong fairness assumption that deals directly with the original program and is similar in shape to the REPETITIVE COMMAND II rule. We omit the details, though we should mention that to reason about fairness it is in general necessary that the termination function takes values from an arbitrary well-founded ordering and not just natural numbers (see [AO83], [APS84], and [AP86], where soundness and relative completeness of a proof system for total correctness of while programs augmented with random assignment was established.).
Different approaches to reason about fairness in the context of nondeterministic programs were independently proposed in [LPS81] and [GFMdR81], that appeared in a journal form as [GFMdR85]. In [APS84] the method presented here was extended to programs with nested nondeterminism. These approaches and proof rules were discussed in book form in [Fra86], where also additional versions of fairness were considered.
The transformational approach to fairness was originally developed in [AO81, AO83] for the Dijkstra’s guarded command language in which each repetitive command has a fixed finite number of alternatives. The transformations can be seen as implementing a general fair scheduler controlling finitely many processes. These transformations were extended in [OP10, HOP10] to deal with dynamic control, where processes can be created dynamically. Then the overall number of processes can be infinite, but at each step of an execution of the system the number of created processes is finite. J. Hoenicke and A. Podelski went in [HP15] one step further and extended the transformations to deal with fairness with an infinitary control, where the number of created processes can be infinite. Both dynamic and infinitary control were expressed by repetitive commands with infinitely many alternatives. However, these papers did not propose any proof rules derived from the new transformations.
7.3 Probabilistic programs
Probabilistic programs are sequential programs with the ability to draw values at random from probabilistic distributions. They have attracted large attention in the research community due to many applications, for example in security to describe randomized encryptions, in machine learning to describe distribution functions, and in randomized algorithms. They have typically just a few lines of code, but are hard to analyze, see, e.g., [KGJ*+*15]. Properties of interest for such programs include the expected runtime and almost sure termination.
Most formal modelling takes place in the setting of an extended Dijkstra’s guarded command language, called probabilistic guarded command language, abbreviated pGCL. Here, both nondeterministic choice and probabilistic choice are admitted. In particular, McIver and Morgan [MM05] carried out their research on probabilistic programs in this setting. They extended the notion of weakest precondition to weakest pre-expectations.
J. den Hartog and E.P. de Vink [dHdV02] introduced a Hoare-like proof system for partial correctness of probabilistic programs which are defined as (determininistic) while programs extended by the probabilistic choice between the statements and . This intention is that the statement is chosen with the probability and the statement with the probability . This necessitates the introduction of probabilistic predicates in the assertion language. In these predicates, the real-valued expression yields the probability that the normal predicate holds. For example, for an integer variable the correctness formula
[TABLE]
holds. The proof system of [dHdV02] contains several new rules that go beyond the ones concerning the while programs. In particular, for the probabilistic choice the following rule was proposed:
PROBABILISTIC CHOICE
[TABLE]
where the probabilistic choice operator is also applied to the probabilistic predicates and .
Den Hartog and de Vink established soundness of their proof system. They also proved relative completeness for the subset of loop-free probabilistic programs and a restricted set of predicates in the postcondition. The proof is based on calculating the weakest precondition.
Some other developments concerning verification of probabilistic programs are discussed in Subsection 10.7.
8 Parallel and Distributed Programs
By a concurrent program we mean a program that has a number of components, the execution of which proceeds in parallel. If the program components share some variables one usually refers to this framework as shared memory parallelism. Following [AdBO09], we refer to the corresponding programs as parallel programs. If the program components do not share variables but can communicate by messages, one usually calls these components processes and refers to the corresponding concurrent programs as distributed programs. A most commonly used approach relies on asynchronous message passing. However, within the framework of program verification, for reasons of simplicity, one rather focuses on synchronous message passing, which means that the processes need to synchronize their actions to make the communication possible. Again following [AdBO09], we mean by distributed programs the ones with synchronous message passing, within the context of a specific language proposal due to Hoare [Hoa78].
8.1 Reasoning about parallel programs
Verification of parallel programs calls for new insights. To discuss the matters let us first introduce the syntax. By
[TABLE]
we mean a parallel composition of sequential programs, S_{1},\mbox{\ldots},S_{n}, that may share variables.
The main complication in reasoning about parallel programs is the interference caused by the use of shared variables. For example, both
[TABLE]
and
[TABLE]
hold but
[TABLE]
does not since one possible computation consists of executing the assignments in the following order , which yields the final value 3.
The first limited approach to the verification of parallel programs was proposed by Hoare in [Hoa72c], where he dealt with parallel composition of disjoint program components. More formally, we say that the component programs S_{1},\mbox{\ldots},S_{n} of [S_{1}\|\mbox{\ldots}\|S_{n}] are disjoint if no variable subject to change in one component appears in another component. This led to the following proof rule:
DISJOINT PARALLELISM
[TABLE]
where \mathit{free}(P_{i},Q_{i})\cap change(S_{j})=\mbox{\emptyset} for .
As noticed by Hoare in [Hoa75], parallel and sequential compositions of program components coincide under the assumption of disjointness. This brought him to suggest the following rule:
SEQUENTIALIZATION
[TABLE]
(In [Hoa72c] and [Hoa75] actually only parallel composition of two components was studied). In 1975 this limited approach to program correctness was extended to arbitrary parallel programs. It was based on a novel idea of interference freedom, first introduced in the PhD thesis of S. Owicki [Owi75], and subsequently published in two papers by her and supervisor D. Gries, [OG76a] and [OG76b]. This approach became known as the Owicki-Gries method.
In what follows we explain the ideas behind this extension of Hoare’s logic. To deal with the problem of interference mentioned above, Owicki and Gries suggested to compose not the correctness statements about the component programs but their proofs, presented in an appropriate form. This form relies on the fact that the correctness proofs of the component programs are syntax-directed, that is they follow in some sense the program structure. As a result the proof can be recorded by retaining the used assertions in the program text. For example, the application of the WHILE rule can be retained in the text of the while statement by writing its conclusion as
[TABLE]
while the conclusion of the CONSEQUENCE rule can be written as
[TABLE]
which amounts to interpreting two consecutive assertions as an implication. The crucial point of such a proof representation, called a proof outline, is that each statement is preceded in it by at least one assertion. Subsequent assertions indicate implication between them.
Here is an example of a proof outline for the correctness proof of the DIV program that we considered in Subsection 3.1:
[TABLE]
In the Appendix we give another example of a proof outline by representing in such a form Turing’s proof discussed in Subsection 2.1. To understand the essence of the approach of Owicki and Gries let us return for a moment to the original Hoare’s proof system. It is sound in the following stronger sense, where, given a proof outline and a subprogram , we denote by the assertion that directly precedes . For a proof see, e.g., [AdBO09].
Strong Soundness Theorem Consider a proof outline that represents the proof of a correctness formula . Take a computation of that starts in a state that satisfies . Each time reaches a substatement of , the precondition is satisfied. Further, if terminates, its final state satisfies .
Armed with this knowledge let us return to parallel programs. Suppose that we established the correctness formulas , where i\in\mbox{{{\mbox{}}}} and S_{1},\mbox{\ldots},S_{n} are the component programs of the parallel program [S_{1}\|\mbox{\ldots}\|S_{n}]. Let be the corresponding proof outlines. We call them interference-free if for all assignments in [S_{1}\|\mbox{\ldots}\|S_{n}] and all assertions used in a proof outline of another component the correctness formula
[TABLE]
holds. Informally, the proof outlines are interference-free if the execution of each assignment statement in the state that satisfies its assertion does not invalidate the assertions used in the proof outlines of other components. Then the following proof rule allows us to reason about parallel programs:
PARALLELISM
[TABLE]
Owicki and Gries noted that to reason about parallel programs they needed auxiliary variables (occasionally called by other researchers ghost variables), so variables that neither influence the control flow nor the data flow of the program, but only record some additional information about the program execution. Formally, a set of simple variables is called a set of auxiliary variables of if each variable from occurs in only in assignments to the variables from . The appropriate proof rule allowing one to delete them is:
AUXILIARY VARIABLES
[TABLE]
where for some set of auxiliary variables of the program results from by deleting all assignments to the variables in , and no variable from appears free in .
In presence of shared variables it is sometimes useful to restrict the number of interference points. This can be done by allowing atomic sections (see [Lip75] and [Lam77]), which are statements of the form , where does not contain any loops or further atomic sections. The idea is that such a statement is executed without any interruption by another component of the parallel program. This suggests the following proof rule (see [Owi78]):
ATOMIC SECTION
[TABLE]
To allow for synchronization between the component programs, Owicki and Gries used a generalization of the atomic section statement, called an await statement , with the following meaning: if evaluates to true, the statement is executed as an atomic section. The corresponding proof rule is:
AWAIT
[TABLE]
The presence of synchronization statements leads to a possibility of a deadlock, an undesired situation in which some components of a parallel program did not terminate while the nonterminated components are all blocked. Owicki and Gries noted that interference-free outlines allow one to reason about absence of deadlock in a simple way. To this end, it suffices to identify the possible deadlock situations and to show for each of them that the corresponding conjunction of the assertions cannot be simultaneously satisfied.
This approach to verification was successfully applied in [OG76a] to establish correctness of non-trivial parallel programs, in particular two versions of the classical producer/consumer problem, a parallel version of the FIND program mentioned in Subsection 3.1, and an implementation of Dijkstra’s semaphores. In [OG76b] it was extended to parallel programs that use a more efficient synchronization construct called conditional regions introduced in [Hoa72a], and in [Owi78] to concurrent programs with shared data classes.
Termination Let us discuss now the issue of termination of parallel programs. Owicki and Gries proposed to establish it by using the WHILE II rule instead of the WHILE rule and by postulating that no component program increases the termination function of a while statement used in another component program. However, the authors of [AdBO90] noticed that the termination of parallel programs is subtler than it sounds and came up with an example of simple parallel program that does not terminate, even though its termination can be established using Owicki and Gries method.
The problem has to do with the fact that the assertions used in the proof of the second premise of the WHILE II rule, so \{{P\mbox{\ \wedge\ }B\mbox{\ \wedge\ }t=z}\}\ {S}\ \{{t<z}\}, are not tested for interference freedom. In [AdBO90] two ways of solving this problem are proposed. The first is to retain in the proof outlines the correctness proofs of both the first and second premise of this rule, so that all assertions used in these proofs are subjected to the interference freedom test. Another is by adding additional requirements to the definition of interference freedom that ensure that the used termination functions decrease along all syntactically possible paths through the program. The latter approach suffices to validate the termination proofs presented in [OG76a].
Finally, termination of parallel programs under the fairness assumption was dealt with in [OA88], where the Owicki-Gries method was combined with a transformational approach presented in Subsection 7.2.
Independently of the Owicki-Gries method of [OG76a], L. Lamport proposed in [Lam77] an essentially equivalent approach to verification of parallel programs. The difference was that, as in [Flo67], he considered programs presented as flowcharts, now one for each component program. As a result the interference-freedom test referred to the assertions attached to the flowchart nodes and translated into a requirement that these assertions are monotone, that is, that they are maintained by the actions of the other components. Lamport used this approach to establish correctness of a solution to the mutual exclusion problem. In the paper also program properties were considered that had not been hitherto addressed. We shall return to this matter in the last section of the paper.
The rely-guarantee approach A drawback of the Owicki-Gries method is that due to the test of interference freedom, verification of a parallel program S\equiv\mbox{[S_{1}|\mbox{}|S_{n}]} is possible only if all components S_{1},\mbox{\ldots},S_{n} of are explicitly given. Further, this method is not compositional, where ‘compositionality’ means that (partial) correctness of a parallel program is derived directly from the correctness of its components.
This prompted research on alternative formalisms for reasoning about parallel programs. A discussion of these approaches can be found in [dRdBH*+*01, pp. 479-484]. Here we limit ourselves to an account of one, perhaps most successful proposal, called the rely-guarantee approach. It was introduced in the PhD thesis of C.B. Jones, [Jon81], the essence of which appeared in [Jon83]. This approach provides a compositional way reasoning about concurrent programs by incorporating the interference-freedom test into the proof. This is achieved by using more informative correctness formulas.
We follow here the presentation given in the book by W.P. de Roever et al. [dRdBH*+*01]. In the rely-guarantee approach one assumes that a given program is executed in some environment and therefore uses an extended specification format
[TABLE]
where a correctness formula is extended by an interface specification of the environment consisting of a rely condition and a guarantee condition . In contrast to the assertions and in the correctness formula, and are predicates on transitions, i.e., they relate two states, the one before executing a transition and the one after it. As in Turing’s flowchart in Subsection 2.1, primed versions of variables are used to refer to the state after executing the transition. For example, expresses that the value of the variable decreases. The idea is that states assumptions that makes on the transitions of its environment and that states the guarantees that provides to the environment.
Informally, \langle R,G\rangle:\mbox{{{P}}\ {S}\ {{Q}}} expresses that the correctness formula is true in the sense of partial correctness if
- •
whenever at some moment during the computation of all past environmental transitions satisfy
- •
then all transitions of up to that moment satisfy .
For parallel composition of programs and the following proof rule is presented in [dRdBH*+*01]:
PARALLEL COMPOSITION
[TABLE]
In [dRdBH*+*01, p. 453] this rule is explained as follows:
- •
every transition of (which is characterized by ) and every transition of the common environment of and (characterized by ) is seen by with as an environment transition which has to satisfy ,
- •
every transition by or is a transition of , and therefore has to satisfy , and
- •
since the validity of \langle R_{i},G_{i}\rangle:\mbox{{{P_{i}}}\ {S_{i}}\ {{Q_{i}}}} implies is invariant under , the postcondition holds upon termination of ; since implies , , this implies that is invariant under after has terminated, too.
Note that the rule is compositional for the customary correctness formulas. The crux of applying it is to find suitable rely-guarantee conditions for which the implications in the premises hold. In [Jon83] and [dRdBH*+*01] this approach was illustrated by providing alternative correctness proofs of a solution to the mutual exclusion problem and of a parallel version of the FIND program considered in [OG76a]. In practice, this approach may be as difficult as proving interference freedom.
8.2 Reasoning about distributed programs
Hoare introduced an elegant approach to distributed programming based on synchronous communication [Hoa78]. In an intentional analogy to the title of Dijkstra’s seminal paper [Dij68] on parallel programs, this proposal was called Communicating Sequential Processes. In the paper Hoare introduced a simple programming language for distributed programming, called since then CSP, in which Dijkstra’s guarded command language was extended by allowing communication primitives for synchronous communication. This focus on synchronous, as opposed to asynchronous, communication had a huge impact on the theory of distributed programming and was also realized in the programming language Occam [INM84]. The idea is that synchronous communication is simpler to reason about as it obviates the discussion of message ordering and buffers and their management. Synchronous communication can be implemented by means of asynchronous one, by adding additional processes that simulate message buffers, so it can be viewed as an elegant abstraction.
In [AFdR80] a proof system was proposed to reason about a simple class of CSP programs. The crucial idea of this approach was an introduction of a cooperation test that corresponds to the interference test of the Owicki-Gries method.
To explain the matters we first clarify the relevant aspects of CSP. Each CSP program consists of a parallel composition of processes, written as
[TABLE]
Each is a label of a process and is its program. These processes share no variables. They communicate by means of synchronous communication that is achieved by means of two matching input/output commands, in short i/o commands. An i/o command has the form (an input command) or (an output command), where is a variable, and an expression. The i/o commands or match if , appears in the program for process , appears in the program for process , and the types of and coincide.
When the control in the programs for processes and is just in front of the mentioned i/o commands and they match, they can be executed jointly, with the effect that the value of is assigned to . So the effect of the joint execution of the commands or is that of an assignment .
In the CSP language, Dijkstra’s guarded commands are generalized by allowing i/o commands to appear in the guards. So the guards can now also be of the form , where is a Boolean expression and is an i/o command. If evaluates to true the i/o command of the generalized guard behaves the same way as the usual i/o command, though it fails if it addresses a process that terminated. If evaluates to false the generalized guard fails.
Further, Dijkstra’s do-od notation is replaced by using a star ’*’ and the ‘[’ and ‘]’ brackets, while the if-fi notation is replaced by the ‘[’ and ‘]’ brackets, that are also used to enclose the parallel composition.
As an example of a CSP program consider the following transmission problem, taken from [AdBO09], that is a simplified version of a similar problem discussed in [Hoa78]. We wish to transmit from the process to the process through a process a sequence of characters in such a way that process deletes from the sequence all blank characters. The following CSP program
[TABLE]
where
[TABLE]
is a solution to this problem.
Here the sequence of characters is initially stored in the array of characters in the process . The last element of the array is the special character ‘’, i.e., a[M-1]=\mbox{`*'}. The process has an array of characters serving as an intermediate store for processing the character sequence and the process has an array of characters to store the result of the filtering process. For coordinating its activities the process uses two integer variables and pointing to elements in the array .
The process can communicate with both other processes. It can receive characters from process until ‘’ has been received and it can transmit all nonblank characters to the process . The Boolean parts of the generalized guards of the process can both evaluate to true. In that case the next action can be either a communication between and or between and . Consequently this CSP program exhibits a nondeterministic behaviour.
The process terminates once it has sent all its characters to the process. The process terminates when it has received the character ‘’ and it has transmitted to all nonblank characters it has received. Finally, the process terminates once it has received from the character ‘’. Thus the parallel composition of these three processes terminates if sends as the last of its characters the ‘’.
The proof system proposed in [AFdR80] extends the one for the guarded commands language by the following axioms and proofs rules that deal with the communication. For simplicity we assume that all variables and expressions are of the same type.
INPUT
[TABLE]
OUTPUT
[TABLE]
GENERALIZED ALTERNATIVE COMMAND
[TABLE]
GENERALIZED REPETITIVE COMMAND
[TABLE]
The INPUT axiom may look strange since it allows us to conclude an arbitrary postcondition. However, the used assertions still have to pass the cooperation test. This test refers to the proof outlines which are defined as in the case of Owicki-Gries approach.
Suppose now that we established the proof outlines , where i\in\mbox{{{\mbox{}}}} and S_{1},\mbox{\ldots},S_{n} are respective programs of the processes {PR}_{1},\mbox{\ldots},{PR}_{n}. We say that these proof outlines cooperate if
- •
the assertions used in contain no variables subject to change in for ,
- •
\{{pre_{1}\mbox{\ \wedge\ }pre_{2}}\}\ {{PR}_{j}?x\,\|\,{PR}_{i}!t}\ \{{post_{1}\mbox{\ \wedge\ }post_{2}}\} holds whenever and
are taken respectively from the proof outlines and .
Intuitively, proof outlines cooperate if they help each other to validate the post conditions of the i/o commands present in these proofs. To establish cooperation the following axiom is needed.
COMMUNICATION
[TABLE]
provided and match.
This axiom simply states that, as mentioned before, the effect of the joint execution of a pair of matching i/o commands and is that of an assignment . Recall that in CSP, the processes composed by parallel composition do not share variables, so cannot occur in . This justifies the simple postcondition for the assignment .
Then the following proof rule allows one to draw conclusion about the parallel composition of processes:
CSP PARALLELISM
[TABLE]
To reason about the CSP programs, as in the case of the Owicki-Gries approach, the AUXILIARY VARIABLES rule is needed. The presented reasoning about deadlock freedom is analogous as in [OG76a], though the reasons for a deadlock can now be different. In particular, a process can be blocked forever if the control in its program is just before an i/o command that addresses a process that terminated. Using the proposed proof system some example CSP programs were proved correct in [AFdR80]. (In [Moi83] it was pointed out that one of the correctness proofs contained an error and a corrected version was presented.) The proof system was subsequently proved in [Apt83] to be sound and complete in the sense of Cook. Neither [AFdR80] nor [Apt83] considered termination.
Independently of [AFdR80] a very similar proof system to reason about CSP programs was proposed in [LG81], in which the satisfaction property corresponds to the cooperation test. However, the authors used a different semantics of the generalized repetitive commands than the one stipulated in [Hoa78] and taken care of in the proof system of [AFdR80]. On the other hand, in contrast to [AFdR80], program termination was considered. A number of different approaches to reason about communicating processes was proposed in the literature around that time. They are surveyed in [HdR86].
Subsequently, a simplified proof system for a fragment of CSP was proposed in [Apt86] and used to establish correctness of a solution to the so-called distributed termination problem. In this fragment a program for each process consists of a guarded commands program followed by a single generalized repetitive command. The i/o commands can appear only in the guards of this repetitive command and thus not as separate statements. An example of a CSP program written in this fragment is the above-mentioned solution to the transmission problem. This fragment was studied independently in [ABC87] and [Zöb88], where it was shown that each CSP program can be transformed into a program in this subset using some control variables.
The underlying idea of this approach is that such simpler CSP programs can be transformed into Dijkstra’s guarded commands language without introducing any additional variables. By absorbing this transformation into a proof rule one obtains a proof rule that uses a global invariant and deals directly with the considered CSP program. This way this approach dispenses with the cooperation test. Termination is naturally dealt with by following the approach used for the guarded commands language. This proof system was adopted in [AdBO09] and its two previous editions, where its soundness was shown to be a direct consequence of the correctness of the above-mentioned program transformation.
In [AFK88] it was explained that in the context of CSP programs fairness, a notion we discussed in Subsection 7.2, can have various interpretations. One of them states that every pair of matching i/o commands that is infinitely enabled is also infinitely often selected. In [GFK84] a proof rule for dealing with this form of fairness of the CSP programs was proposed.
The approach of [AFdR80] and [LG81] was presented only for CSP programs without nested parallelism. It was extended in [AdB90b] to CSP programs that allowed nested parallelism and also dynamic process creation, a feature not present in CSP. Subsequent work in this direction, [dB91], shifted emphasis to reasoning about objects, a subject that deserves a separate section.
Finally, let us mention that verification of parallel and distributed programs in the Hoare-like style was systematically presented in book form in [dRdBH*+*01].
9 Object-oriented Programs
Object-oriented programming, as exemplified by languages like C++ or Java, builds upon the notion of an object and concepts like inheritance and subtyping. The difficulty in reasoning about such programs is that their execution creates dynamic pointer structures that go beyond the static program structure that has been the backbone of the syntax-directed Hoare-style proof rules discussed so far.
9.1 Language characteristics
As object-oriented programming has been realized in many, often incompatible, ways, we clarify first the main characteristics of the objects here considered. These are:
- •
objects possess (and encapsulate) their own instance variables,
- •
objects interact via method calls,
- •
objects can be dynamically created.
Each object consists of a set of instance variables and a set of methods. In contrast to the formal parameters of procedures and the local variables of the block statements which only exist temporarily, the instance variables of an object exist permanently. The local state of an object is a mapping that assigns values to its instance variables. Each object represents its local state by a pointer to it. Encapsulation means that the instance variables of an object cannot be directly accessed from other objects; they can be accessed only by the method calls of the object.
A method call invokes a procedure which is executed by the called object. The execution of a method call thus involves a temporary transfer of control from the local state of the caller object to that of the called object (also referred to as callee). Upon termination of the method call the control returns to the local state of the caller. The method calls are the only way of transferring control from one object to another.
The account of verification of object-oriented programs that follows is based on [AdBO09, Chapter 6]. We distinguish two kinds of variables: the set of normal variables, the ones considered so far, and the set of instance variables, which are owned by objects.
We consider a set of methods, each defined by means of a declaration
[TABLE]
where the identifier denotes a method, is the list of formal parameters of type , and is the method body, which may include recursive calls of .
Methods are invoked by means of the parameterized method calls that are of the form
[TABLE]
where is an expression that denotes the called object and is the list of actual parameters of the method .
A program consists of a main statement and a set of method definitions. In programs we use a basic (i.e., not compound) type object that denotes an infinite set of objects. The constant null of type object represents the void reference, a special construct which does not have a local state. The normal variable self of type object stores at any moment the currently executing object. Inside a method body no assignments to the variable self are allowed, that is, this variable is read-only. Values of type object can only be tested for equality. Variables of type object are called object variables, and expressions of type object are called object expressions.
To illustrate the considered programs consider a recursive method used to find a zero in a linked list represented by objects. We represent such lists using the instance object variable that links the objects of the list, and the constant null that allows us to identify the last element of the list. We assume that each object stores a value kept in an instance integer variable . Additionally, we use the normal object variable to point to the first object in the list. Figure 5 shows an example of such a list representation.
The desired method is declared as follows.
[TABLE]
Then upon termination of the call the object variable points to the first object in the list that stores zero, if it exists, and otherwise it returns the void reference, represented by the constant null.
9.2 Reasoning about object-oriented programs
The methods in object-oriented programs use local updates to manipulate a global, dynamically changing pointer structure, the heap. Therefore the assertion language must be able to express properties of the heap. To this end, global expressions are introduced by extending the (local) expressions that may appear inside methods by navigation expressions of the form , where is an object expression and an instance variable. If denotes a certain object (for example self) and is an instance variable (for example next), then points to the corresponding object (in the example self.next). This way, one can navigate from object to object along the pointers in the heap. Assertions are then constructed from global Boolean expressions by allowing Boolean combinations and quantification over normal variables in .
As an example consider the assertion used in [AdBO09, pp. 226-227] to reason about the above method find:
[TABLE]
In addition to the instance object variables and and the instance integer variable used in the definition of find, one uses here the following normal variables: an array of type {\bf integer}\mbox{>\rightarrow>}\mbox{{\bf object}}, integer variables and , and the object variable self.
The assertion states that the array section stores a linked list of objects which starts with the object self, ends with the object , and all of its objects, except possibly the last one, are different from null and do not store in zero. Note the use of the navigation expressions and .
The desired behaviour of the above method find can then be specified by means of the following correctness formula:
[TABLE]
where the postcondition is defined in terms of the assertion :
[TABLE]
So the postcondition states that the returned object is null or stores zero and that for some array section the assertion holds.
To reason about such correctness formulas we need new axioms and proof rules.
Correctness of the customary assignment to normal variables is captured by the ASSIGNMENT axiom that for a given postcondition calculates the precondition by applying the substitution to . In object-oriented programs one can additionally use assignments to instance variables and use the dereferencing in the method calls. The latter calls for an extension of the assertion language with the corresponding expressions .
F.S. de Boer proposed in [dB99] the following textually identical axiom for such assignments:
ASSIGNMENT TO INSTANCE VARIABLES
[TABLE]
where is a (possibly subscripted) instance variable in .
So, as in the case of the assignment to subscripted variables, the solution relies on an extension of the definition of substitution, in this case to the instance variables.
As usual, the definition of the substitution proceeds by induction on the structure of . The difference appears at the level of expressions for which the definition of is more elaborate. If is of the form for an object expression , the substitution has to take care of possible aliases of . More precisely, if after applying the substitution inductively to , the result refers to the currently active object, i.e., if , then the outcome of the substitution is . Otherwise, is left untouched and the substitution is applied inductively to . This is expressed in the following definition:
[TABLE]
In case of only one (possibly recursive) method definition, the RECURSION rule for procedure calls can be adapted to method calls as follows, where we use the block statement discussed in Subsection 5.2:
RECURSION IV
[TABLE]
where the method is declared by .
So, as for recursive procedures we may use the desired conclusion as a hypothesis in the correctness proof of a block statement, where self and the list of formal parameters of the method are treated as local variables that are respectively initialised by the called object and the list of actual parameters and are accessed in the method body . A rule analogous to the RECURSION II rule is adopted to deal with total correctness.
To adjust correctness formulas that deal with generic method calls to specific objects and lists of actual parameters , we modify the SUBSTITUTION rule as follows, where we refer to the given set of method definitions:
INSTANTIATION
[TABLE]
where is a list of variables in which do not appear in and var(s,\mathbf{t})\cap change(D)=\mbox{\emptyset}.
In [AdBO09] these axioms and proof rules were used to establish total correctness of the above example program expressed by the correctness formula (4) and of an object-oriented program that inserts an element into a linked list.
9.3 Advanced topics in the verification of object-oriented programs
Various other aspects of object-oriented programming were studied from the correctness point of view. One of them is object creation. An object can be dynamically created by the assignment statement , where is an object variable and new is a keyword in the considered programming language. The execution of this statement creates a new object and assigns its identity to the variable . This new object comes with a default initialisation of all its instance variables. This can be modelled by some bookkeeping of the set of objects that are currently created, for example by maintaining a counter referring to an unbounded array. This allows one to reason about this assignment using a small program transformation. A drawback of this approach is that it refers to an explicit implementation.
An alternative is to use a substitution of for object variables and define its application to a limited class of assertions (we call them pure) that take into account that object variables can only be compared for equality or be dereferenced in the method calls , and in which one does not quantify over such object variables. This leads to the following axiom proposed in [dB99]:
OBJECT CREATION
[TABLE]
where is a simple (so not subscripted) object variable and is a pure assertion.
We omit the details of the definition of the substitution and only remark that one cannot simply replace in by the keyword new because it is not an expression of the assertion language. The details are given in [AdBO09, Chapter 6].
C. Pierik and F.S. de Boer showed in [PdB03] how the approach of [dB99] can be extended to deal with classes, inheritance and subtyping. The same authors introduced in [dBP03] a general methodology for obtaining relatively complete Hoare’s logics for object-oriented programs. A key issue is the extension of Gorelick’s most general formulas [Gor75] (see Subsection 6.1) to deal with the states of object-oriented programs.
As another contribution to this line of research on verification of object-oriented programs let us mention [ÁdBdRS05] in which a Hoare-like proof system for partial correctness and deadlock freedom was developed for a subset of Java. The considered subset comprised the object-oriented core of Java, as well as concurrency via thread classes, allowing for a multithreaded flow of control. The Java concurrency model includes synchronous message passing, dynamic thread creation, shared-variable concurrency via instance variables, and coordination via reentrant synchronization monitors. The verification method was formulated in terms of proof outlines that were tested both for interference freedom of shared-variable concurrency, as in [OG76a], and for cooperation of synchronous message passing, as in [AFdR80]. The authors established the soundness and relative completeness of their proof system. From an annotated program, a number of verification conditions were generated and discharged using the interactive theorem prover PVS [ORS92].
The verification of Java programs was also in the focus of tool-supported research projects around the year 2000. The LOOP project led by B. Jacobs considered sequential Java programs with specifications written in the Java Modeling Language (JML) [JP04]. JML was developed by a group led by G.T. Leavens [LCC*+*05]. It was inspired by the idea of Design-by-Contract introduced by B. Meyer in the context of the object-oriented programming language Eiffel [Mey97]. A contract is a specification in the form of assertions. The contract is agreed upon before an implementation is developed that should satisfy this contract. In its simplest form, a JML specification of a method comprises a precondition, one postcondition for normal termination and second one for exceptional termination, and a set of variables that may be changed. The LOOP compiler takes as input a Java program and a JML specification and outputs files in the syntax of the PVS theorem prover that describe the semantics of the program and proof obligations generated from the specification. These are then proven interactively using PVS.
For a subset of sequential Java programs, called NanoJava, a Hoare’s logic was proven sound and relatively complete w.r.t. an operational semantics of the programs in the interactive theorem prover Isabelle/HOL [vON02]. In this approach, as in the paper [vO99] cited in Subsection 6.1, a semantic view of assertions was taken, whereby an assertion is a function from states to Boolean values. No separate syntactic representation of assertion was introduced. Thus, subtleties like the right definition of syntactic substitutions were not considered.
For the object-oriented programming language Eiffel a sound and relatively complete Hoare’s logic was established in [NCMM09]. The emphasis was on the treatment of features in Eiffel that are not present in other object-oriented languages. These concern the details of the exception handling, so-called once routines, and multiple inheritance.
More recently B. Engelmann [EO16, Eng17] considered object-oriented programs in the context of dynamic typing. This means that variables do not have an a priori declared static type but may assume any value during the execution of the program. As an example consider the following method from [Eng17], where it is assumed that is a Boolean variable:
[TABLE]
If is true, the method call yields the numeric value , but if is false, it yields the string value . So the type of and is determined dynamically during runtime, and it is either numeric or string, with the operation + being either addition or string concatenation. Such dynamically typed programs are present in the list processing language LISP and in widespread programming languages like Python and JavaScript.
Engelmann developed in [Eng17] a Hoare-like proof system for a model language dyn of object-oriented programs with dynamic typing. He proved soundness and relative completeness of his system, thereby extending the arguments of [Coo78, Gor75] and [dBP03] to the object-oriented part.
10 Alternative Approaches
10.1 Weakest precondition semantics and systematic program development
Dijkstra suggested an alternative approach to program verification, called weakest precondition semantics [Dij75]. The idea is that given a program and a desired postcondition we would like to find the weakest precondition such that holds in the sense of total correctness. ‘Weakest’ means here that for any precondition such that holds in the sense of total correctness, the implication holds.
This approach differs from Hoare’s original approach by
- •
insisting on total correctness instead of on partial correctness,
- •
assuming that initially only the postcondition is given.
Additionally, Dijkstra insisted that the program should be developed together with its correctness proof. In [Dij75] he advanced this approach for his guarded command language that we briefly discussed in Subsection 7.1. Its notable feature was the use of programming constructs that support nondeterminism. Another interesting feature of the language was parallel assignment , where is a list of different variables and is a list of expressions of the same length. This construct is for example useful to swap the values of variables without additional variables:
[TABLE]
The weakest precondition is defined by induction on the structure of the program, with
- •
,
- •
,
as typical clauses.
The main problem is how to deal with loops. In [Dij75] the weakest precondition for guarded commands was defined as follows. Denote the alternative command \mbox{{\bf if}\ }B_{1}\mbox{>\rightarrow>}S_{1}\Box\mbox{\ldots}\Box B_{n}\mbox{>\rightarrow>}S_{n}\ \mbox{{\bf fi}} by , the repetitive command \mbox{{\bf do}\ }B_{1}\mbox{>\rightarrow>}S_{1}\Box\mbox{\ldots}\Box B_{n}\mbox{>\rightarrow>}S_{n}\ \mbox{{\bf od}} by and abbreviate to . Then
[TABLE]
where
[TABLE]
and for
[TABLE]
Intuitively, is the weakest precondition guaranteeing proper termination in a state satisfying , after at most guard selections.
Since is used as a subscript of , ‘\mbox{\exists}k:k\geq 0’ is here not a customary quantification but a shorthand for an infinite disjunction, with additionally the formulas defined by induction. In other words, so defined weakest precondition of a repetitive command is not an assertion in a first-order language. The same is the case for the weakest liberal preconditions mentioned in Subsection 4.3, that can be defined for while programs in an analogous way.
On the other hand, if one confines one’s attention to the language of Peano arithmetic, then the weakest (liberal) preconditions can be encoded as first-order formulas, see for example [Win93, Chapter 7]. However, the resulting formulas are not natural and using them to express loop invariants (recall from Subsection 4.3 that weakest liberal preconditions can be used in a simple way to express loop invariants) is an overkill. This underlies the difficulty of finding simple loop invariants, the problem we already mentioned in Subsection 3.1, and clarifies why finding them is an important problem in developing correct programs or in establishing their correctness.
These complications disappear if one identifies assertions with the sets of states that satisfy them and views the weakest precondition as a way of assigning inductively semantics to programs. The above clauses defining show then how a program can be viewed as a predicate transformer, a concept further discussed in Subsection 10.3. So the weakest precondition approach can be viewed both as an approach to program verification and as a way of defining program semantics.
The concept of weakest precondition was used a number of times in this survey, which shows how this notion permeated research on Hoare’s logic and program verification. The idea of using it to develop programs together with their correctness proofs was subsequently presented in book form in [Dij76a], where the weakest precondition semantics was extended to blocks and procedures. A systematic development of provably correct programs was further advanced by David Gries in his book [Gri81], notably by proposing a number of heuristics for finding loop invariants. Other books devoted to this subject are [Bac86, DF88, Kal90, BvW08]. Various aspects of the weakest precondition semantics were further discussed in book form in [DS90]. The problem of finding loop invariants became central in the subsequent study of program verification and development. [FMV14] surveyed various ways of constructing loop invariants, and provides their classification and analysis.
Another matter relevant for a systematic program development is termination. Both the WHILE II and RECURSION II rules provide only a kind of template for an actual termination proof, without explaining how the termination functions are to be found. Some sophisticated techniques were developed to establish termination. They go beyond the framework of Hoare’s logic or the weakest precondition semantics and rely on various methods developed in other areas, notably term rewriting systems. The authors of [CPR11] provided an accessible account of the recent developments. In particular, they explain a recent alternative approach to proving termination called disjunctive termination argument: only one of a disjunction of the termination functions needs to decrease, but this has to be the case after any number of iterations of the loop. It is argued that disjunctive termination arguments are easier to find than the classical termination argument dating back to Turing [Tur49] (see Subsection 2.1), where a single termination function has to decrease its values taken from a well-founded set with each iteration of the loop.
One difficulty of this approach for program verification is that it is not clear how to extend the weakest precondition semantics to deal with advanced programming constructs, for instance arbitrary procedures as considered in Section 6. In contrast, Hoare’s approach is more flexible. In particular, as we have seen in Subsection 5.1, the reasoning can be supported by various adaptation rules. This cannot be done in the framework of the weakest precondition semantics which requires computing a single assertion. On the other hand, as we saw in Subsection 7.3, the weakest precondition semantics turned out to be helpful for the verification of probabilistic programs.
10.2 Specifying in Hoare’s logic
Until now we used Hoare’s logic exclusively to reason about programs. But the formalism of correctness formulas can be also used to specify programs, though some care needs to be exercised. For example, the correctness formula does not properly specify that a still to be constructed program computes in the sum of and because also satisfies this correctness formula.
To overcome this problem, one specifies the set of variables that may access. Then every variable outside is known to keep its value during the computation of . These variables can be used to freeze values of the initial state to use them in the postcondition evaluated in the final state. For example, by postulating , the correctness formula
[TABLE]
specifies that computes in the sum of and while leaving and unchanged. This specification technique is also at the heart of the most general formulas introduced by Gorelick in his completeness proof for recursive procedures [Gor75] and discussed in Subsection 6.1.
In a similar vein the adaptation rules keep track of the set of the variables accessed by a program , sometimes refined into the variables that are changed and those that are only read by .
To support the specification of programs, variants of Hoare’s logic have been proposed that introduce distinguished variables that may never be accessed by programs. By different authors, these variables are called logical variables (in [vON02]), logical constants (in [Mor94], further discussed in the next subsection), specification-only variables, or auxiliary variables (in [Kle99]). The last name, however, is in conflict with the concept of auxiliary variable introduced by Owicki and Gries in the context of parallel programs [OG76a] and discussed in Subsection 8.1.
T. Kleymann developed in [Kle99] a variant of Hoare’s logic where such explicit logical variables appear in the assertions and a new consequence rule is proposed that takes care of these variables. As a result, he showed that this consequence rule is powerful enough to achieve adaptation completeness (a notion discussed in Subsection 5.1) without further adaptation rules.
We mentioned auxiliary variables first in the context of the Owicki-Gries method, when discussing verification of parallel programs in Subsection 8.1. The need for auxiliary variables in correctness proofs was already observed in [Cli73]. In [AdBO09] it was noted that the AUXILIARY VARIABLES rule is already needed to reason about disjoint parallel programs. Indeed, the correctness formula
[TABLE]
cannot be proved using the DISJOINT PARALLELISM rule and the rules of the proof system .
The most extensive analysis of these matters was provided in [dGR16] that clarified and extended initial results of [Kle98] and [Kle99]. The authors of [dGR16] showed that the AUXILIARY VARIABLES rule is a derived rule both in the proof system and in a proof system for parameterless recursive procedures, which means that it can be eliminated from any proof that uses it. In the case of disjoint parallel programs the authors showed that this rule can be replaced by the simpler -INTRODUCTION rule discussed in Subsection 5.1.
They also showed that for parallel programs with shared variables the AUXILIARY VARIABLES rule turns out to be essential. On the other hand, no other proof rules are needed. Indeed, Owicki proved in [Owi76] that the above presented proof system for parallel programs is complete in the sense of Cook.
10.3 Programming from specifications
R.-J. Back [Bac80] and C. Morgan [Mor94] extended Dijkstra’s approach to a methodology for “programming from specifications” by a rule-based step-by-step development of specifications into programs. To this end, they introduced a specification statement. In [Mor94] it takes the form , with the meaning
“If the initial state satisfies the precondition then change only the variables listed in so that the resulting final state satisfies the postcondition .”
While the variables that are changed by a specification are explicitly mentioned, namely , there is no information which variables are accessed, i.e., is not defined. Recall that various Hoare-style proof rules for programs have application conditions concerning . Also, Gorelicks’s most general formulas require fresh variables outside of to freeze their initial values. To overcome this weakness, Morgan considers what he calls logical constants (occasionally also called specification-only variables), that by definition appear only in assertions and are thus never changed by any program or specification. With a logical constant the initial values of a variable can be frozen. For example, specifies that should be increased. The amount of the increment is left unspecified.
The idea is that specifications and programs are handled on the same footing, so that programming operators like sequential composition or loops can be applied to specifications, as well. Constructs and in this extended syntax can be compared by a refinement relation: denotes that is refined by . Semantically, specifications and programs are considered as predicate transformers that transform given postconditions into the corresponding weakest preconditions. Refinement means that for all postconditions the implication
[TABLE]
holds, i.e., establishes the postcondition in at least all states where establishes . For example, . In this approach specifications are stepwise refined to programs by the applications of refinement rules, described in [Mor94].
Morgan [Mor94] also considers a number of advanced programming concepts like recursive procedures with parameters, modules with local declarations of variables and procedures, and data refinement.
Subtly different from Morgan’s specification statement is the generic command of J. Schwarz [Sch77]. It is written as , where is a precondition, a postcondition, and a set of variables. Semantically, a generic command denotes a certain state transformer. Assume an interpretation . A state transformer based on a finite set of variables is a binary relation on the set of states that has only read or write access to the states via the variables in the set . For each program its meaning is a state transformer based on .
Let be the set of all state transformers based on . State transformers are ordered by the set inclusion: means that produces less output than . The least element is the empty state transformer producing no output, corresponding to a program that never terminates. Now, the semantics relative to of a generic command is given by
[TABLE]
So given an interpretation , denotes the largest state transformer based on that satisfies in the sense of partial correctness. ‘Largest’ refers here to the ordering of state transformers by the set inclusion. In [Old83b] it was shown that for the formula of the ADAPTATION II rule, introduced in Subsection 5.1, expresses the weakest liberal precondition of the generic command w.r.t. a given postcondition . This connects generic commands via the weakest liberal preconditions to the ADAPTATION II rule.
Schwarz used generic commands for stating an alternative version of a RECURSION rule, but did not embark on program development. Morgan’s specification statement is similar to the generic command , except that the list does not record the variables that are only read, which are also covered by .
10.4 Algorithmic logic and dynamic logic
Hoare’s logic is geared towards establishing program correctness. However, from the point of view of mathematical logic it has a very rigid syntax: the correctness formulas cannot be negated or combined, for example by disjunction. As a result one cannot view Hoare’s logic as an extension or a modification of some existing logics, even though it crucially relies on first-order logic and its extensions, for example by allowing subscripted variables. In some alternative approaches one could view reasoning about programs as an extension of reasoning within existing logics. We discuss now briefly two most prominent examples.
Algorithmic logic was originally proposed in [Sal70] and presented in book form in [MS87]. It extends first-order language by expressions that can be interpreted as programs and constructs that allow one to mix formulas and programs. Interestingly, substitutions for a sequence of variables are viewed as atomic programs. This is equivalent to the aforementioned parallel assignment of Dijkstra, and also shows a close connection with the ASSIGNMENT axiom. Programs are built by allowing formulas as tests and using program composition, conditionals, and loops, all written in a compact notation. For example, is written as v. In turn, the construct corresponds to .
Expressions of the form , where is a program and a formula, correspond to the strongest postcondition introduced in Subsection 4.3. Further, it is shown how termination of the considered programs can be expressed as a formula that admits countable disjunction. This is analogous to the definition of given earlier.
The relation between Hoare’s logic and algorithmic logic becomes clear when one realizes that the correctness formula can be expressed as the implication . Consequently, rules used in Hoare’s logic can be readily reproduced as rules in algorithmic logic, in particular various forms of adaptation rules. This straightforward modelling, however, does not yield new insights concerning program verification.
Research on algorithmic logic focused mostly on such matters as studies of consistency and the infinitary completeness of selected theories, derivation of the normal forms of programs, and axiomatization of various data structures, rather than on (relatively) complete axiomatizations of fragments concerned with specific features of programming languages, a direction Hoare’s logic took.
Dynamic logic was originally proposed in [Pra76] and presented in book form in [Har79] and more extensively in [HKT00]. It is very similar to algorithmic logic introduced six years earlier, though it was developed independently. It enriches first-order logic by constructs reminiscent of modal logic. First, programs are defined starting from atomic actions and tests, using the sequential composition (;), nondeterministic composition () (absent in algorithmic logic), and iteration () that corresponds to Kleene’s star. In the dynamic logic syntax the statement can be expressed as .
Further, one admits formulas of the form , where is a program and is a formula, with the intended interpretation “every execution of the program from the current state leads to a state in which is true”. The formulas and programs are defined by simultaneous induction, allowing the usual Boolean connectives. A dual formula to is , defined by:
[TABLE]
So its intended interpretation is “some execution of the program from the current state leads to a state in which is true”. The and operators can thus be viewed as the counterparts of the and operators in propositional modal logic, but parameterized with a program .
Research on dynamic logic mainly focused on a study of various fragments or extensions, with the corresponding sound and complete axiomatizations, and the corresponding decidability and computational complexity results. In particular, dynamic logic was extended in [Har79] to deal with recursive procedures.
Typical axioms are:
[TABLE]
which corresponds to one of the mentioned clauses that define the weakest precondition, and
[TABLE]
that captures the idea that ∗ stands for the infinite iteration.
The relation between Hoare’s logic and dynamic logic is easily established by noticing that the correctness formula can be expressed as the implication . So models what is called the weakest liberal precondition introduced in Subsection 4.3. Consequently, as in the case of algorithmic logic, proof rules of the proof system of Subsection 3.1 can be translated into proof rules of dynamic logic. Moreover, these translated rules are derivable from the adopted axioms and proof rules of dynamic logic.
Further, thanks to the richer syntax, it is possible to express other program properties and discuss such properties like program equivalence. For example, the following formula states that the program is deterministic:
[TABLE]
Dynamic logic was generalized in a number of ways, for example to epistemic dynamic logic (see, e.g., [BR16]), to allow reasoning about modalities and change. Also it was extended to specify and reason about hybrid systems, i.e., systems where a discrete control interacts with a continuous dynamics [Pla08]. Further, the KeY system (discussed Section 11) is based on dynamic logic.
10.5 Temporal logic and model checking
Research on verification of parallel programs carried out in the seventies showed limitations of Hoare’s logic in reasoning about concurrent programs. We discussed three properties of such programs: partial correctness, termination, and absence of deadlock. However, in contrast to the sequential programs, concurrent programs are often supposed to operate repeatedly, in a cyclic fashion. For instance, a solution to the mutual exclusion problem deals with infinite executions of the program components operating in parallel. This calls for a study of properties (such as an eventual access) that cannot be expressed in Hoare’s logic.
To express such concepts and to systematically reason about them A. Pnueli proposed in [Pnu77] to use temporal logic. Using it one can express in a natural way various program properties that do not necessarily deal with the input/output behaviour of a program. In contrast to Hoare’s logic the reasoning about programs is not syntax-directed. Instead, one usually reasons about specific control points in a program and a relation between them.
For example, the following formula states that a process infinitely often enters its critical section CS:
[TABLE]
where is a formula that states that the control in the process is within CS.
In turn, to express the strong fairness assumption for the repetitive command
[TABLE]
we can use the following formula:
[TABLE]
where holds when the control in the considered program is just in front of .
Appropriate axioms and proof rules were then developed to reason about such formulas. Temporal logic, applied to concurrent programs, grew into an impressive research area, see in particular the books [MP91, MP95] of Z. Manna and A. Pnueli. This line of research should be viewed as complementary to Hoare’s logic, that is why we do not devote more space to it.
In that context a distinction, first advanced in [Lam77], is useful. A safety property states ‘nothing bad will happen’ during a program execution, while a liveness property states that eventually ‘something good will happen’ during a program execution. According to this distinction partial correctness, absence of errors, and deadlock freedom are safety properties. In contrast, program termination, fairness, eventual access, infinite access, etc. are liveness properties. In temporal logic these properties can be formulated by means of invariants that become formulas of the form , while liveness properties are formulas of the form . Hoare’s logic is a convenient vehicle to prove safety properties. Its modification to deal with termination is also quite natural. As we saw in Section 7.2 one can also investigate within this logic fairness of nondeterministic programs. In fact, even more advanced liveness properties, such as fairness of parallel programs and eventual access properties can be studied, as well (see [OA88]). However, the treatment becomes awkward, as one has to reason then about appropriately transformed programs. This is in contrast to temporal logic that allows one to reason about liveness properties in a simple way, without any need for program transformations.
Temporal logic led in turn to model checking. Independently, E.M. Clarke and A. Emerson [EC82], as well as J.P. Queille and J. Sifakis [QS81], discovered that the problem of checking whether a finite-state system satisfies (is a model of) a propositional temporal logic formula is decidable, providing efficient algorithms for it. This was the start of enormous research activities extending the scope of model checking so that even industrial-size problems could be tackled [CGH*+*93]. Interestingly, model checking is often used to debug a system because in case the system does not satisfy the temporal logic specification, model checkers can provide a counterexample that is helpful for understanding the mismatch between a system and its specification. In the recent years model checking has been extended to infinite-state systems, mostly by automatically constructing and refining abstractions of the system, a method known as counterexample-guided abstraction refinement, see [CGJ*+*03]. The state of the art of model checking is represented in the handbook [CHVB18].
Another approach based on temporal logic is Temporal Logic of Actions (TLA) introduced by L. Lamport in [Lam94]. It is a method of specifying and reasoning about concurrent systems in which systems and their properties are represented in the same temporal logic. A system is specified by a temporal formula representing a single loop that in each iteration nondeterministically chooses one action for execution. An action describes a basic step of the considered system and is specified by a predicate using normal and primed variables as we have seen it already in Turing’s example in Subsection 2.1. The standard form of a TLA specification is
[TABLE]
where is the initial predicate, is the next-state relation expressed as a disjunction of actions, is the list of all variables occurring in these actions, and is a temporal formula that specifies a liveness condition in terms of fairness assumptions. To allow for refinement of concurrent systems in the presence of different granularities of the basic steps, stuttering steps are considered. To hide parts of the state, quantification over variables is possible. The extension TLA+ comes with facilities to structure system specifications into modules, see [Lam02]. Properties of a subset of TLA+ specifications can be verified with the model checker TLC discussed in [Lam02].
10.6 Separation logic
This approach to program verification was originally developed as an extension of Hoare’s logic to reason locally about about pointer structures, see [ORY01, Rey02, OYR04, O’H19]. To cope with pointers, separation logic builds upon a semantic model, in which a state is a pair consisting of a store and a heap . A store is a mapping from variables to values (so a state in the sense of Subsection 4.2), which may be data values such as integers, or pointer values such as addresses. A heap is a finite partial mapping from addresses (or cells) to values, which again can be data or pointers. It is assumed that the addresses are integers, which in turn are values.
Several low-level statements for manipulating the heap were considered in [ORY01, O’H19]. Let stand for a variable and for an integer expression, which can denote an address in the heap. One can explicitly distinguish between an address and its contents: denotes the contents of the heap at address . Assignments affect only the store. Besides the normal assignments there are lookups , where is interpreted as an address in the heap and the contents of is assigned to the variable in the store. Mutations affect the heap. An update expresses that the contents of the address in the heap becomes value of the expression . Further, expresses that the address is newly allocated to the heap, and expresses that the address is deallocated from the heap.
Separation logic extends the usual assertion language of Hoare’s logic to specify properties of the heap: asserts that the heap is empty, asserts that the heap consists of one cell, with address and contents , and asserts that the heap consists of one cell, with address but unknown content. The main new operator in separation logic is the separation conjunction, written * and pronounced “and separately”. The assertion expresses that the heap can be split into two disjoint parts in which and hold, respectively. Using separation conjunction, one can specify larger parts of the heap. For instance, the assertion describes two separate cells with addresses and and contents 21 and 42, respectively. As abbreviation one uses to stand for and thus asserting that the heap consists of adjacent cells with addresses and contents , respectively. For example, the assertion concisely specifies a heap with a cyclic pointer structure, in which stands for and similarly with . It consists of two separate parts of the heap at the addresses and that contain 21 and 42, respectively, and a pointer to the other address.
For mutations and lookups the following axioms were stated in [Bro07, O’H19]:
ALLOCATION
[TABLE]
DE-ALLOCATION
[TABLE]
UPDATE
[TABLE]
LOOKUP
[TABLE]
where does not occur in or .
Separation conjunction enables the formulation of proof rules for local reasoning about components of parallel programs. Crucial is the following rule, which is essentially the INVARIANCE rule in a semantic setting of heaps:
FRAME
[TABLE]
where \mathit{free}(R)\cap change(S)=\mbox{\emptyset}.
In separation logic, this rule serves to extend a local specification involving only the variables and parts of the heap that is used by by adding assertions about variables and other parts of the heap not modified by . Thus the FRAME rule is considered as the key to local reasoning about the heap [Rey02].
Separation logic was originally used for the verification of sequential programs manipulationg pointer structures. Exploiting its ability to reason explicitly about the heap, the approach was later extended in [O’H07] to reason in a modular way about concurrent programs. The idea is that two threads that operate on disjoint parts of the heap do not interfere, and thus can be verified in isolation. This is captured by the following rule, which is the DISJOINT PARALELISM rule in a semantic setting with heaps:
CONCURRENCY
[TABLE]
where \mathit{free}(P_{1},Q_{1})\cap change(S_{2})=\mathit{free}(P_{2},Q_{2})\cap change(S_{1})=\mbox{\emptyset}.
In this rule, the separation conjunction in the precondition of the parallel composition is true if the heap can be partitioned into sub-heaps making the local preconditions of the components and true. The premises of the rule state that the components and establish local postconditions and , respectively, which in the conclusion are combined into the global postcondition .
A major issue was developing a coherent semantical model for this concurrent separation logic. This was solved by S. Brookes in [Bro07]. His semantics evaluates resource-sensitive partial correctness formulas of the form \Gamma\vdash\mbox{{{P}}\ {S}\ {{Q}}}, where is a resource context that specifies for each resource name occurring in the program a finite set of variables, a protection list, and a resource invariant, and a proof system allows one to reason about these formulas.
10.7 Relational Hoare logic
We conclude this overview of alternative approaches by discussing a line of research that began with the work of N. Benton, [Ben04]. In it Hoare’s logic was modified to verify correctness of various optimizing program transformations. This was achieved by proposing a proof system in which one reasons at the same time about a pair of programs the variables of which are related by some precondition and postcondition. To this end the customary correctness formulas were replaced by judgments concerning two while programs, and . These are statements of the form
[TABLE]
where and are relations on program states. Informally, such a judgment states that if initially the relation between the variables of the programs and holds, then after their independent executions the relation between their variables holds. (So a notation would have been more intuitive.) Typically both programs use the same variables, so to indicate from which program the variable is taken the indices and are used in and .
As an example consider the technique of invariant hoisting. The program
[TABLE]
can be optimized to
[TABLE]
The resulting programs compute the same values for the variables and . This can be expressed as the judgment
[TABLE]
with . So the first occurrence of expresses the information that prior to the programs executions the values of their variables are respectively equal, while the second occurrence states that the values of these variables are respectively equal after the executions of both programs.
In general, if we rename to by appending to each of its variables the index , and similarly with for which we use the index , then the judgment can be interpreted as the correctness formula .
The resulting logic was called Relational Hoare Logic (RHL), where the qualification ‘Relational’ referred to the fact that instead of assertions relations were used. An example rule is the following one dealing with the conditional statement:
[TABLE]
The premise of this rule states that in the context determined by the and relations, the statement can be replaced by . Thus the second branch of the conditional statement can be replaced by , and consequently this conditional statement can be simplified to .
Appropriate proof rules formulated in this framework made it possible to verify various known compiler optimization techniques, including the above example of invariant hoisting.
In [BGB09] this approach was extended to study equivalence of probabilistic programs. The considered programs extend while programs by allowing a standard feature of probabilistic programs, called random sampling, which is an assignment of the form , where is a probability distribution over the values of the type of . The semantics of such programs, as in [dHdV02], is then a mapping from the set of states to the set of distributions over the states.
The semantics of the judgments is defined in such a way that it respects the fact that in both considered programs the same probability distributions are used. In particular the judgment , where , is true.
The resulting logic was called probabilistic Relational Hoare Logic (pRHL). pRHL is not a simple extension of RHL because in presence of probabilities some rules of RHL become unsound. For example, the rule
[TABLE]
is sound in RHL (because the programs are deterministic) but not in pRHL.
This work was carried out in the context of CertiCrypt, a system built on top of the interactive theorem prover Coq (see Section 11), that makes it possible to provide machine-checked correctness proofs of cryptographic algorithms.
In [BKOB13] this framework was further generalized to allow for a probabilistic reasoning about differential privacy, a notion of privacy that guarantees that the behaviour of an algorithm taking values from a database hardly changes when the database is slightly modified. Differential privacy in particular provides a formal guarantee that information about specific participants in a database is not revealed by the algorithm. The resulting formalism is called approximate probabilistic Relational Hoare Logic (apRHL).
In apRHL, the judgments of [BGB09] were generalized to parameterized judgments concerning two probabilistic programs. The appropriate proof rules generalize those of [BGB09]. This framework was implemented in a system called CertiPriv built on top of Coq, which was in particular used to provide machine-checked proofs of soundness of the considered rules. This work was further pursued in [BGA*+*14], where differential privacy was dealt with by means of a transformation of a probabilistic program into a non-probabilistic one that simulates two executions of the original program. As a result, differential privacy of a single program could be established using the original proof system presented in Subsection 3.1.
11 Final Remarks: a Summary and an Assessment
Hoare’s logic had a huge impact on program verification, notably by allowing one to approach it in a systematic way, using the logical apparatus of formal proofs. Combining it with the research on program semantics made it possible to argue about the soundness and relative completeness of the underlying proof systems. The syntax-directed form of Hoare’s logic suggested a natural research agenda, which —as we have seen— allowed one to deal with several programming constructs and forms of program construction, including higher-order procedures, nondeterminism, concurrency, and object-orientation.
This survey aimed at providing a systematic exposition of these developments. Because of space considerations we had to omit an account of various Hoare-style proof rules for such concepts as program jumps ([CH72]), go-to statement ([dB80, Chapter 10], written by A. de Bruijn), or several forms of abrupt loop termination present in Java ([HJ00]).
In the seventies Hoare’s logic was used to define programming languages. In [Hoa72a] and [HW73] an axiomatic definition of the programming language Pascal was given. These papers provided proof rules for simple constructs such as the case statement and the repeat statement. However, the presentation was incomplete. For example, no account of reasoning about recursive procedures or pointers was given. This work was pursued in [LGH*+*78] where axioms and proof rules in Hoare’s logic for the programming language Euclid were presented.
From the current perspective one can see that such axiomatic presentations were not rigorous since no soundness proofs were provided to justify the introduced axioms and rules, notably the recursion rule. To see that such soundness proofs are not superfluous recall from Subsection 5.1 the observation of [Old83b] that the adaptation rule for Euclid is not sound. Also, termination was not dealt with in these papers and the reasoning about it can be another source of possible, subtle, errors (see for example the discussion at the end of Subsection 6.1). In fact, as we saw, reasoning about soundness within the framework of Hoare’s logic started only after these two papers were published.
But even if such soundness proofs were presented, given the size of the considered programming languages, there would be a non-trivial chance of errors. In fact, we mentioned a number of times that arguments about correctness of various proof rules in Hoare’s logic or about soundness or relative completeness of some specific proof systems have led to various, occasionally, pretty subtle errors.
A logical remedy is to use automated reasoning to argue about various Hoare’s logics. This brings us to computer aided verification, one of the important research directions that emerged in the eighties. Since 1990 it is a subject of an annual conference with the same name (abbreviated to CAV). In relation to Hoare’s logic this work naturally divides into two categories:
- •
mechanical verification by means of interactive theorem provers of properties of various Hoare logics, such as soundness and relative completeness proofs,
- •
computer aided verification of selected programs.
In what follows we refer to a number of systems that are the outcome of several years of research and associated ongoing implementations. Given that mechanical verification is not the subject of this survey, we do not discuss these systems in detail. In each system, to appropriately formalize the assertion-based reasoning about programs and reason about the corresponding proof systems, several important design decisions have to be taken concerning the choice of the underlying assertion language, proof representation, choice of proof tactics, form of the interaction with the user, etc. A separate survey on this subject would be a most welcome addition to this one.
An early contribution in the first category was [Sok87], where soundness of the original proof system of Hoare from [Hoa69] was established in LCF (that stands for Logic for Computable Functions), an early interactive automated theorem prover developed in the seventies, see, e.g, [GMW79].
Next, in [Kle98], [Nip02a] and [Nip02b] soundness and relative completeness of Hoare’s logics for partial and total correctness of while programs and programs with recursive procedures was established in the Lego and Isabelle/HOL interactive theorem provers, the latter system described initially in [NPW02]. In Subsection 6.1, we mentioned already that in [vO99] soundness and relative completeness of a proof system for a programming language with the mutually recursive procedures with the call-by-value mechanism was established in Isabelle. In all these works assertions are identified with sets of states that satisfy them.
Further, in [NN99] the semantics and proof system of [OG76a] for partial correctness of parallel programs, that we discussed in Subsection 8.1, was formalized in the Isabelle/HoL system. Subsequently the authors proved soundness of this proof system and verified a number of correctness proof examples. An analogous formalization was carried out in [Bal06] on the basis of dynamic logic in the KIV system, described in [BRS*+*00]. This approach combined symbolic execution of the operational semantics of the programs with induction.
The works in the second category concern specific programs. They rely on various systems and tools that support mechanical verification of programs based on Hoare’s logic or some of the alternative approaches discussed in the previous section. An early example is [Gor88], where a simple program verifier implemented in LISP is described. It consists of a generator of verification conditions and a theorem prover. It was used in particular to justify Hoare’s correctness proof given in Figure 4 in Subsection 3.1. The following more recent selective contributions underscore the importance of mechanical verification. Several other recent systems and tools for program verification are described in [PR18].
- •
In his paper [Hoa71b] concerned with the correctness of the FIND program, Hoare expressed the desire for computer support in “formulating the lemmas, and perhaps even checking the proofs.” Only much later, Filliâtre [Fil07] published a mechanized proof of FIND using the interactive theorem prover Coq and following Hoare’s proof from [Hoa71b] as closely as possible. He noticed that Hoare’s informal termination proof does not meet the requirements of a termination function in the sense that the additional invariants used by Hoare are not real invariants.
Coq is based on a formal language called the Calculus of Inductive Constructions that extends typed lambda calculus, see, e.g., [Chl13]. It was used to verify formally proofs of a number of famous mathematical results, including the Four Color theorem.
- •
In [CDE*+*16] a tool-supported correctness proofs of Quicksort and its variants were reported. The authors used the Hoare’s logic based verification tool Dafny [Lei10].
Dafny comprises (1) an imperative, class-based language for programs annotated with the features needed for verification (such as assertions, framing clauses expressing the objects that are allowed to be changed, ghost variables, i.e., auxiliary variables in the sense of Subsection 8.1, and termination functions) and (2) a verifier that translates annotated Dafny programs to an intermediate language input by the tool Boogie [BCD*+*05]. The latter is a fully-automatic deductive verification system that generates verification conditions which are then passed to an SMT (satisfiability modulo theories) solver, where the default SMT solver is Z3 [dMB08]. Boogie uses the weakest precondition semantics discussed in Subsection 10.1.
- •
TimSort is a standard sorting algorithm provided by several programming framework, including the Java standard library. While trying to verify it the authors of [dGdBB*+*19] discovered a bug. They formally specified a revised version and mechanically verified its correctness, including termination, in the KeY system.
KeY is an extensive software development system that supports in particular specification and formal verification of object-oriented software, see [ABB*+*16]. As mentioned earlier, it is based on dynamic logic. The KeY-Hoare tool (see [BH16]), built on top of the KeY system, allows one to reason about partial and total correctness of while programs in an extension of Hoare’s logic with explicit state updates.
In recent years research on Hoare’s logic visibly slowed down, probably due to the fact that through hundreds of publications it achieved its main goal of creating a comprehensive formal framework to reason about various classes of programs. On the other hand, its versatility results in new applications in various contexts. We provide here three recent examples.
The first, due to [AMO13], concerns reasoning about linear systems (for example linear differential equations) that are expressed graphically as block diagrams. The authors, building upon the framework of abstract Hoare’s logic developed in [AMMO09] mentioned in Subsection 4.3, provided a sound Hoare-like proof system that allowed them to reason about various examples of linear systems, including linear filters and the steam boiler problem, a classic example of a hybrid system.
The second one concerns reasoning about time complexity of the programs. In [HN18] three Hoare’s logics for reasoning about time bounds, including the original logic due to [Nie87], were formalized and shown to be sound and relatively complete.
The final one is an application to quantum programs, a research direction that originated with the work of M. Ying [Yin11]. For a recent overview of the developments on this subject, that successfully parallel the developments of the customary Hoare’s logic, see [Yin19]. A related approach of [Unr19] follows the line of research started with [Ben04] and [BGB09] and introduces quantum Relational Hoare Logic (qRHL) that allows one to reason about how the outputs of two quantum programs relate given a relation between their inputs.
One should also mention here recent work aimed at supporting teaching of Hoare’s logic. In [SS14] an account was given of a tool called HAHA (Hoare Advanced Homework Assistant) that was specifically designed to teach Hoare’s logic. The tool supports reasoning about while programs with integer variables and arrays.
Hoare’s logic is an example of an assertion-based method of program verification, in the sense that it relies on the use of assertions. This is also a common feature of the approaches to program verification discussed in the previous section. In this sense we can say that all these approaches are direct or less direct successors of Turing’s approach from [Tur49].
However, there are other theories of program verification, notably of parallel and distributed programs, that take a different approach. A prominent example is CCS (Calculus for Communicating Systems) of Robin Milner that focuses on reasoning about equivalence of abstract distributed programs [Mil80, Mil89]. It is at the origin of a number of related theories and led to the field of process algebra [BPS01]. A comparative survey of these approaches would form a natural complement to this one.
Acknowledgements
We would like to thank all three reviewers for exceptionally detailed and helpful referee reports that led us to improve and expand the presentation.
Appendix A Turing’s example
We present here in Figure 6 a proof outline for a while program corresponding to Turing’s example given in Figure 3 of Subsection 2.1. The program without the assertions was shown in [OW12]. The qualification is used to annotate the loop invariants and to annotate the termination functions. So this is a proof outline establishing total correctness of the program w.r.t. the precondition and postcondition . The assertions used for partial correctness are similar to the ones used in the correctness proof of [dB75] of a program corresponding to Turing’s example that uses both a while and a repeat statement.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[ABB + 16] W. Ahrendt, B. Beckert, R. Bubel, R. Hähnle, P. H. Schmitt, and M. Ulbrich, editors. Deductive Software Verification - The Ke Y Book - From Theory to Practice , volume 10001 of Lecture Notes in Computer Science . Springer, 2016.
- 2[ABC 87] K. R. Apt, L. Bougé, and P. Clermont. Two normal form theorems for CSP programs. Information Processing Letters , 26:165–171, 1987.
- 3[Ad B 77] K. R. Apt and J. W. de Bakker. Semantics and proof theory of pascal procedures. In A. Salomaa and M. Steinby, editors, Automata, Languages and Programming: Proceedings of the Fourth Colloquium , volume 52 of Lecture Notes in Computer Science , pages 30–44. Springer, 1977.
- 4[Ad B 90a] P. America and F. S. de Boer. Proving total correctness of recursive procedures. Information and Computation , 84(2):129–162, 1990.
- 5[Ad B 90b] P. America and F. S. de Boer. A proof system for process creation. In M. Broy, editor, Programming concepts and methods: Proceedings of the IFIP Working Group 2.2, 2.3 Working Conference on Programming Concepts and Methods , pages 303–332. North-Holland, 1990.
- 6[Ad B 19] K. R. Apt and F. de Boer. Reasoning about call-by-value: a missing result in the history of Hoare’s logic, 2019. Available from http://arxiv.org/abs/1909.06215 .
- 7[Ád Bd RS 05] E. Ábrahám, F. S. de Boer, W. P. de Roever, and M. Steffen. An assertion-based proof system for multithreaded java. Theor. Comput. Sci. , 331(2-3):251–290, 2005.
- 8[Ad BO 90] K. R. Apt, F. S. de Boer, and E.-R. Olderog. Proving termination of parallel programs. In W. H. J. Feijen, A. J. M. van Gasteren, D. Gries, and J. Misra, editors, Beauty is Our Business, A Birthday Salute to Edsger W. Dijkstra , pages 0–6, New York, 1990. Springer-Verlag.