We provide a sound and relatively complete Hoare logic for reasoning about partial correctness of recursive procedures in presence of local variables and the call-by-value parameter mechanism and in which the correctness proofs support contracts and are linear in the length of the program. We argue that in spite of the fact that Hoare logics for recursive procedures were intensively studied, no such logic has been proposed in the literature.
1 Introduction
1.1 Background and Motivation
Hoare logic was originally introduced by C. A. R. Hoare [23]. It is the most widely used approach to program verification. Since the early 1970s, it has been successfully extended to several classes of programs, including parallel and object-oriented ones, see, e.g., the textbook [4]. The recent survey on Hoare logic [6] by K. R. Apt and E.-R. Olderog traces these historical developments. Also, formalization of Hoare logic in various interactive theorem provers, for example Coq (see, e.g., References [9, 31]), led to a computer aided verification of several programming languages.
One of the crucial features of Hoare logic is its syntax-oriented style. It makes it possible to formally justify annotations of programs at relevant places (for example at the entrance of each loop) with invariants. Such annotations crucially increase programmer’s confidence in the correctness of the program. In turn, intended behaviour of procedures can be described by means of pre- and postconditions, which simplifies program development and supports the crucial “Design by Contract” methodology [26] employed by many large-scale software artifacts. The basic idea of this methodology is that a pre- and postcondition together form a contract between the user (client) of a procedure and the procedure itself: If the user ensures that whenever the procedure is used (called) the precondition holds, then the procedure ensures the corresponding postcondition. In this manner, correct use of procedures does not require knowledge of the implementation details, which is of crucial importance in mastering both the complexity of software development and software verification. For example, one of the state-of-the-art theorem provers for the verification of Java programs, the KeY system [1], is based on the Java Modeling Language [7] that supports the specification of contracts for method definitions in Java. Instead of verifying the correctness of a procedure (or method) definition for each call separately, contracts are verified only once, which reduces the total verification effort (for example, in the verification of OpenJDK’s sort method for generic collections, see Reference [16]).
The developments that further motivate the subject of the present article passed through a number of crucial stages. Already in Reference [24] a proof system for recursive procedures with parameters was proposed by Hoare that was subsequently used in Reference [18], where Hoare and M. Foley establish the correctness of the Quicksort program. This research was furthered by S. A. Cook [11], who proposed a by-now-standard notion of relative completeness, since then called completeness in the sense of Cook, and established relative completeness of a proof system for non-recursive procedures. Cook’s result was extended by G. A. Gorelick [21], where a proof system for recursive procedures was introduced and proved to be sound and relatively complete. This line of research led to the seminal paper of E. M. Clarke [10], who exhibited a combination of five programming features, the presence of which makes it impossible to obtain a Hoare-like proof system that is sound and relatively complete.
However, often overlooked is that all these papers assumed the by now obsolete call-by-name parameter mechanism. Our claim is that no paper so far provided a sound and relatively complete Hoare-like proof system for a programming language with the following programming features:
•
a system of mutually recursive procedures with explicit parameter declarations,
correctness proofs are linear in the length of the programs.
Given the above research and the fact that in many programming languages call-by-value is the main parameter mechanism, this claim may sound surprising. Of course, there were several contributions to Hoare logic concerned with recursive procedures, but none of them provided a proof system that met the above criteria. The aim of this article is to provide such a Hoare-like proof system and thus establish a link between the practice and theory of software verification by a formal justification of the use of contracts in the verification of mainstream programming languages like Java.
1.2 Related Work
The origin of recursive procedures in the context of programming languages is studied in Reference [33].
The first sound and relatively complete proof system for programs with local variables and recursive procedures was provided in the thesis of Gorelick [21]. But that paper assumed the call-by-name parameter mechanism and, as explained in Reference [3, pp. 459–460], dynamic scope was assumed. The relative completeness result also assumed some restrictions on the actual parameters in the procedure calls that were partly lifted by R. Cartwright and D. C. Oppen [8]. However, the restriction that global variables do not occur in the actual parameters is still present there.
In Reference [14] and in more detail in Reference [15, Section 9.4], J. W. de Bakker proposed a proof system concerned with the recursive procedures with the call-by-value and call-by-variable (present in Pascal) parameter mechanisms in presence of static scope and its proof of soundness and relative completeness. However, the correctness of each procedure call had to be proved separately, that is, each procedure call requires a separate correctness proof of the corresponding procedure body. As a result correctness proofs are only quadratic in the length of the programs, even in the presence of just one recursive procedure. As already stated above, in practice, however, procedures (or methods in object-oriented languages) are specified by contracts that provide a generic specification for each procedure call and allow for correctness proofs that are linear in the length of the programs.
Further, the relative completeness was established only for the special case of a single recursive procedure with a single recursive call. For the case of two recursive calls a list of 14 cases was presented in Reference [15, Section 9.4] that should be considered, but without the corresponding proofs. The main ideas of this proof were discussed in Reference [3]. The case of a larger number of recursive calls and a system of mutually recursive procedures were not analyzed because of the complications resulting from an accumulation of cases generated by the use of several variable substitutions.
In previous work [4, 5] (both co-authored by F. S. de Boer), a proof system was proposed for the programming language here considered and shown to be sound and relatively complete. However, also here correctness of each procedure call has to be dealt with separately, even in the presence of just one recursive procedure. An attempt was made to circumvent this inefficiency by proposing a proof rule for the instantiation of contracts [4, pp. 159–160] by replacing the formal parameters in both the pre- and postcondition of the contract by the actual parameters. However, this requires, among others, that the variables appearing in the actual parameters cannot be changed by the execution of the call. This is rather restrictive in practice (see Example 4.3 of Section 4).
D. von Oheimb [34] discusses a sound and relatively complete proof system for a programming language with mutually recursive procedures and a call-by-value parameter mechanism. The proofs were certified in the Isabelle theorem prover instantiated with Church’s higher-order logic (Isabelle/HOL). The formalization of the proof system itself abstracts from the syntactical representation of assertions, as stated as follows in Reference [34]:
Central to any axiomatic semantics is the notion of assertions, which describe properties of the program state before and after executing commands. Semantically speaking, assertions are just predicates on the state. We adopt this abstract view (similarly to our semantic view of expressions) and thus avoid talking explicitly on a syntactic level about terms and substitution and their interpretation.
Usually, in Hoare logic the formal language of predicate logic is used to represent syntactically the semantic relations between the values of the program variables. One of the main challenges of designing a Hoare-like logic is then to formalize the semantics of programs declaratively in predicate logic, at an abstraction level that coincides with that of the programming language. The abstract view of assertions blurs the clear distinction between the declarative nature of assertions and the operational semantics of programs. For example, in Reference [34] the assertions used in the proof rules for block statements and recursive procedure calls assume operations that are used to define operationally the program semantics, but that are not part of the programming language itself. Further, in Reference [34] assertions assume a program-independent distinction between local and global variables. In our work, we use assertions in the formal language of predicate logic. As such, we make no program-independent distinction between local and global variables within the assertion language: There is only the syntactical notion of free and bound variable occurrences. Further, our work allows the assertion language to have as interpretation an arbitrary underlying structure, e.g., the integers and Booleans. Thus, we are limited in how to formalize proof rules for dealing with local variables and parameters. This leaves us with the only logical possibilities of either restricting variable occurrences, or by renaming variables, in assertions.
We conclude that the relative completeness result presented here is new. It is useful to discuss how we dealt with the complications encountered in the reported papers.
One of the notorious problems when dealing with the above programming features is that variables can occur in a program both as local and global. The way this double use of variables is dealt with has direct consequences on what is being formalized. Additionally, variables can be used as formal parameters and can occur in actual parameters. This multiple use of variables can lead to various subtle errors and was usually dealt with by imposing some restrictions on the actual parameters, notably that the variables of the actual parameters cannot be changed by the call. In our approach no such restrictions are present but these complications explain the seemingly excessive care we exercise when dealing with this matter.
In the relative completeness proofs of Cook [11], Gorelick [21], and De Bakker [15], the main difficulties had to do with the local variables, the use of which led to some variable renamings, and the clashes between various types of variables, for example formal parameters and global variables, that led to some syntactic restrictions.
In fact, the original paper of Cook [11] contains an error that was corrected in Reference [12]. It is useful to discuss it (it was actually pointed out by Apt) in some detail. In the semantics adopted in Reference [11] 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, we have that holds after
is executed. However, there is no way to prove it. In Gorelick’s thesis [21] this error does not arise, since all local variables are explicitly initialized to a given-in-advance value, both in the semantics and in the proof theory (by adjusting the precondition of the corresponding declaration rule).
However, this problem does arise in the framework of Cartwright and Oppen [8], where the authors write on p. 371:
As Apt (personal communication) has observed, this rule [for local variables] is incomplete because it does not allow one to deduce the values of new variables on block entry. There are several possible solutions to this technical problem but they are beyond the scope of this paper.
In our framework this problem cannot occur because of the explicit initialization of the local variables in the block statement. However, our initialization is more general than that of Gorelick. For example, in the statement the local variable is initialized to the value of the global variable . Consequently, according to our semantics, and also the semantics used in Reference [11], holds after execution of the statement
This cannot be proved in the proof system used in Reference [11]. However, we can prove it in our proof system (as shown in Example 4.2).
1.3 Summary of Our Approach
We prove relative completeness for our programming language that allows for dynamic scoping of local variables. However, for a natural syntactically defined subset of programs that avoid name clashes between global and local variables, static scoping of local variables is ensured. By the general nature of our completeness result (which holds for all programs), we also obtain relative completeness for this sub-language. This class of programs was first considered in Reference [8], where it is introduced on p. 372 in a somewhat informal way:
[...] we assume that our PASCAL subset [...] requires that the global variables accessed by a procedure be explicitly declared at the head of the procedure and that these variables be accessible at the point of every call.
Let us discuss now how we succeeded to circumvent the complications reported above. We achieved it by various design decisions concerning the syntax and semantics, which resulted in a simple proof system. Some of these decisions were already taken in the textbook [4] and used in Reference [5] (both co-authored by F. S. de Boer). More precisely, the block statement that declares local variables must include explicit expressions used for initialization. This, in conjunction with the parallel assignment, allows one to model procedure calls in a simple way, by inlining.
Crucially, the semantics of such block statements does not require any variable renaming. This leads to a simple semantics of the procedure calls, without any variable renaming either.
As a result, in contrast to all other works in the literature, our BLOCK rule dealing with local variables uses no substitution. In contrast, in Reference [24] the substitution is applied to the program, while in Reference [11] and Reference [21] it is applied to the assertions. Further, in contrast to Reference [15], our RECURSION rule does not involve any substitution in the procedure body. This allowed us to circumvent the troublesome combinatorial explosion of the cases encountered in the relative completeness proof of Reference [15].
However, the key improvement over previous work [4, 5], is that, here, the RECURSION rule formalizes reasoning about contracts and, crucially, the PROCEDURE CALL rule does not impose any restrictions on the actual parameters. The latter is in contrast to all works that dealt with the call-by-name parameter mechanism. Thanks to this improvement, in contrast to the above two works, in our proof system the correctness proofs support contracts and as such are linear in the length of the program.
1.4 Plan of the Paper
In the next section, we introduce a programming language that includes all the basic features of recursive call-by-value procedures and identify a natural subset of clash-free programs for which dynamic and static scope coincide. Next, in Section 3, we recall various aspects of semantics introduced in the textbook [4] and establish some properties that are used when reasoning about the considered proof system. Section 4 introduces and motivates the design of a proof system for reasoning about recursive calls by means of inlining (or body replacement) and show how we can do better by means of contracts. Section 5 discusses the complexity of proofs and a proof normalization procedure for obtaining linear proofs. In Section 6, we show that the proof system given in Section 4 is sound. In Section 7, we establish relative completeness of the proof system. In Section 8, we describe a formalization of the main semantic argument underlying the relative completeness result in the theorem prover Coq. Finally, in Section 9 we discuss future work and conclude the article.
2 Syntax
Throughout the article, we assume a fixed first-order language . Expressions are terms in the language , Boolean expressions are quantifier-free formulas of , while assertions are formulas of , which are considered equal up to alphabetic renaming of quantified variables.
We denote the set of all variables of by Var. For a sequence of distinct variables, we denote by its corresponding set. For a Boolean expression or a sequence of expressions, we denote the set of all variables occurring in or in by, respectively, and . The set of variables that occur free in an assertion is defined in a standard way and denoted by .
A (simultaneous) substitution of a list of expressions for a list of distinct variables of the same length is written as and the result of applying it to an expression or an assertion as . To ensure a uniform presentation, we allow the empty substitution in which the list of variables is empty.
We now move on and introduce the syntax of the programs. For simplicity in the considered programming language, we admit only simple variables (so no array or subscripted variables), all of the same type. Statements are defined by the following grammar:
where
•
denotes the “empty” statement,
•
is a parallel assignment, with a (possibly empty) list of distinct variables and a list of expressions of the same length as ; when is empty, we identify with the statement,
•
is a procedure name; each procedure is defined by a declaration of the form
where is a (possibly empty) list of distinct variables, called formal parameters of the procedure , and is a statement, called the body of the procedure ,
•
is a procedure call, with the actual parameters, which is a (possibly empty) list of expressions of the same length as the corresponding list of formal parameters,
•
is a Boolean expression,
•
is a block statement where is a (possibly empty) list of distinct local variables, all of which are explicitly initialized by means of the parallel assignment .
By a program, we mean a pair , where is a statement, called the main statement and is a set of procedure declarations such that each procedure (name) that appears in or has exactly one procedure declaration in . So we allow mutually recursive procedures but not nested procedures. We denote by the set of variables that occur in .
By a correctness formula, we mean a triple , where are assertions and is a statement, or a triple , where is a program. Of special interest in our approach will be the representation of contracts that specify by means of a precondition and postcondition the input/output behavior of a procedure. We represent them by the correctness formulas , where are the formal parameters of . Such a call is called a generic procedure call.2 Note that so defined contracts abstract from the implementation of the specified procedure.
The parallel assignment plays a crucial role in the way procedure calls are dealt with: the procedure call , where is declared by , is interpreted as the block statement , where models the parameter passing by value and the block statement ensures that the changes to the formal parameters are local. Such a replacement of a procedure call by an appropriately modified procedure body is called inlining or a copy rule.
In our setup inlining results in a dynamic scope of local variables so that each procedure call is evaluated in the environment in which it is called. The simplest example is the parameterless procedure declared by and the main statement . Here the inlining results in the program
that yields upon termination. However, if we renamed the occurrence of in the block statement to a fresh variable, say, , and thus used the statement , then inlining would result in the program
that yields upon termination. Thus renaming of local variables (e.g., also known as alpha conversion in the lambda calculus) affects the semantics. However, renaming of local variables upon inlining, to avoid clashes between global and local variables, gives rise to a static scope of local variables, which ensures that each procedure call is evaluated in the environment in which it is declared.
The above example shows that static scope can also be ensured when certain variable name clashes are avoided. This can be made precise as follows.
Definition 2.1 (Global Variables).
Given a program , we define the set of global variables as follows.
•
,
•
,
•
where ,
•
,
•
,
•
,
•
,
Finally, we define
•
, where .
To formally justify the circularity caused by the presence of recursive calls, we use a sequence of functions, where , defined as follows. For each of them, we reuse the above equalities as definitions, except for the case of the procedure calls for which we set
•
,
•
,
where . A simple proof by induction shows that for all
so for each procedure call
Denote the least such by We identify then with , where . Clearly, thus defined satisfies the original equalities.
It is important to note that in the statement the variables occurring in are global, and as such those variables appearing in are interpreted differently from the local ones that only exist in the context of the block statement (as formalized in Section 3). We view the variables from as the global variables of the procedure .
Definition 2.2 (Lexical Scope).
A variable appears in the (lexical) scope of a block statement , if appears in the list of local variables and contains a call of . A program is called clash-free if the following holds for every procedure declared in : no variable appears in the scope of a block statement that occurs in .
Clash-free programs by definition thus ensure static scoping of local variables. So a programmer in the considered programming language can ensure static scope by adhering to a simple syntactic convention. This syntactic approach to static scoping also avoids the need for a different semantics of the block statement and allows for an uniform proof theory.
In our considerations it will be important to refer to the set of variables that a given program may change (but not necessarily does change).
Definition 2.3 (Write Variables).
Given a program , we define the set of variables that may be changed by it as follows. Consider the following equalities:
•
,
•
,
•
,
where ,
•
,
•
,
•
,
•
.
The circularity of this definition can be resolved as above.
3 Semantics
In this section, we gather various basic facts concerning semantics of our programming language. We begin by a slightly adjusted presentation extracted from the textbook [4], followed by a collection of various properties that will be needed later.
As already mentioned, we assume for simplicity that all variables are of the same type, say, . Each realization of this type (called a domain) yields an interpretation that assigns a meaning to the function symbols and relation symbols of the language .
Throughout this article, we assume a fixed interpretation . By a state, we mean a function that maps each variable to an element of the domain of . We denote the set of states by .
An update of a state , where is a variable and an element of the domain of , is a state that coincides with on all variables except to which it assigns . A simultaneous update of a state , where is a list of (distinct) variables and is a list of domain elements of the same length, is defined analogously.
Given a state and an expression , we define the element of the domain of inductively in the standard way and for we put .
For a set of variables, we denote by the restriction of the state to the variables occurring in and write for two states and
if . We extend the definitions of an update and equality to, respectively, a set of states and sets of states in the expected way. So for a set of states
and for two sets of states and and a set of variables ,
The relation “assertion is true in the state ,” denoted by , is defined inductively in the standard way. The meaning of an assertion (with respect to the interpretation ), written as , is defined by We say that is valid, and write , if .
The meaning of a program is a function of which the small-step operational semantics is given in the textbook [4]. See Figure 1 for its big-step operational semantics. The operational definition of the assignment, sequential composition, choice and iteration constructs are standard. A procedure call is defined in terms of a corresponding block statement. The semantics of a block statement resets the local variables after the execution of the statement . Note that since are evaluated in the initial state, the variables appearing in also refer to their values in the initial state.
Fig. 1.
Fig. 1. Big-step operational semantics.
For a given state , states the fact that the program terminates when started in the initial state , yielding the final state . If does not terminate when started in , then is the empty set.
We extend the function to deal with sets of states by
Definition 3.1 (Syntactic Approximation).
Given and a statement , we define the th syntactic approximation of by induction on :
where denotes a diverging statement (e.g., ) and is the result of a simultaneous replacement in of each procedure call by
Furthermore, let stand for .
Lemma 3.2 (Basic Semantic Properties).
Skip For all states
Assignment For all states
Composition For all states
Block For all states and where ,
Inlining For
As a special case, we have for any procedure declared by ,
Approximation
Access and Change For all states and if then
Lemma 3.2 collects various basic properties of the big-step operational semantics (their proofs are standard, and therefore omitted). Note that the clauses for the basic constructs can also be interpreted independently as a Definition of a denotational semantics.
The Block item employs the earlier introduced extension of the update operation to a set of states and is a concise way of writing that for all states
It states that the execution of a block statement consists of the initialization of the local variables, followed by the execution of its body, and a subsequent reset of the local variables to their initial values. The Access and Change item formalizes the intuition that when executing a program only variables in can be modified. It can be equivalently stated as that implies
Combining the above Block and Inlining items, we obtain that the execution of a procedure call consists of the initialization of the formal parameters to the actual parameters, followed by the execution of the procedure body, and a subsequent reset of the formal parameters to their initial values. This is stated by following corollary.
Corollary 3.3.
Suppose that the procedure is declared by . For all states
where .
Proof.
By the appropriate items of Lemma 3.2, we successively have
□
Definition 3.4 (Semantics Correctness Formulas).
Given a program and a correctness formula , we write
if
We say then that is true in the sense of partial correctness.
The following lemma states a basic property of the semantics of correctness formulas.
Lemma 3.5.
Suppose that for all states
Then for all assertions and such that
Proof.
By the first assumption
(1)
By the second assumption , so for arbitrary states and such that we have iff . Hence for two sets of states and such that , we have
So the desired equivalence follows Equation (1) and the definition of .□
Following Reference [11], we now introduce the following crucial notions underlying the completeness proof.
Definition 3.7 (Strongest Postcondition).
Denote by the strongest postcondition of the program with respect to an assertion , defined by
So is the set of states that can be reached by executing starting in a state satisfying .
We say that a set of states is definable (in the given interpretation ) iff for some formula of we have . We say then that defines.
Definition 3.8 (Expressivity).
The language is expressive with respect to the given interpretation , if for for every assertion and program the set of states is definable.
Throughout this article, we assume that the language is expressive with respect to the given interpretation and identify with its defining formula.
Given a proof system for proving correctness formulas, we denote by
that can be proved by means of the proof system. We say that a proof system
•
is sound if for every correctness formula ,
•
is complete, if for every correctness formula ,
4 Proof System
Figure 2 includes the usual basic Hoare logic for assignment and the basic control structures of sequential composition, choice and iteration (since the set of declarations is empty for this sub-language, it is omitted). We use simultaneous substitution to generalize the standard assignment axiom. A skip statement is identified with an empty assignment, and thus we obtain as an instance of the (parallel) assignment axiom, the derived axiom . Hoare actually introduced two consequence rules, that soon after were combined into the rule listed here. The proof rule concerning the if-then-else statement was originally proposed by P. Lauer [25].
Fig. 2.
Fig. 2. The proof systems: Basic Hoare logic, , CBV (each includes all rules and axioms of the former).
We note here that by collapsing consecutive applications of the consequence rule into one, we can normalize any proof in our basic Hoare logic that consists of the consequence rule, the assignment axiom and the rules for the basic control structures of sequential composition, choice and iteration. Such a normalization gives rise to proofs that are linear in the size of the statement, measured by its number of constructs (assignments, sequential composition, choice and iteration). To be more precise, let denote the number of constructs of , inductively defined as follows.
Definition 4.1 (Size of a Statement).
We inductively define the number as follows:
•
,
•
,
•
,
•
,
•
,
It is easy to verify by induction of that if is provable then there exists a proof that consists of at most rule applications.
To prove a correctness formula about a recursive program , we extend the basic Hoare logic with the following proof strategy:
•
prove the correctness formula of the main statement with respect to assumptions about the procedure calls (thus abstracting from their implementation),
•
discharge these assumptions by proving from them correctness formulas referring to the interpretation of these procedure calls in terms of the corresponding block statements.
The above idea is formalized by the following recursion rule (also used in the textbook [4]):
where . The sign refers to the provability in the basic Hoare logic extended with the following rule for the block statement from the textbook [4, p. 158]:
BLOCK
where .
Note that in the above recursion rule is allowed here that and denote the same procedure identifier, for some . In this rule there are subsidiary proofs in the premises, where is the total number of procedure calls that appear in . Note that the statements used on the right-hand sides of the last provability signs are the corresponding effects of inlining applied to the procedure calls on the left-hand side of . In this proof rule each procedure calls requires a separate subsidiary correctness proof. This results in inefficient correctness proofs.
More precisely, assuming a program with procedure calls, each of the subsidiary proofs in the premises of the above recursion rule can be established in the number of steps linear in the length of . But is linear in the length of , as well, and as a result the bound on the length of the whole proof is quadratic in the length of . This bound remains quadratic even for programs with a single procedure, since remains then linear in the length of .
Can we do better? Yes we can, by proceeding through a couple of simple steps. First, we replace each procedure call such that , where are the formal parameters of , by the block statement . This gives rise to so-called pure programs that only contain generic procedure calls (as introduced in Section 2). For pure programs the last premises of the above recursion rule reduce to
The transformation of programs the into pure ones can be avoided as follows. Incorporating in the proof system the BLOCK rule the above premises can be reduced to
provided that for .
Further, the replacement of every non-generic procedure call in the considered program by its corresponding block statement that uses a generic call can be captured proof theoretically by means of the proof rule
This rule can be further simplified to a direct instantiation of the generic call using a BLOCK rule:
PROCEDURE CALL
where .
Finally, recall that is the number of different procedure calls that appear in . But for pure programs , where is the number of procedure declarations in (or if each procedure declared is also called).
However, we shall also need the so-called adaptation rules. The SUBSTITUTION rule from the textbook [4, p. 98] is used to deal with the occurrences in the assertions of local variables of block statements and the formal parameters of the procedure calls. Additionally, we have the rules INVARIANCE and -INTRODUCTION also used in Reference [21] (though the side conditions are slightly different).
Let refer to provability in the proof system that extends the basic Hoare logic with the above BLOCK, PROCEDURE CALL and adaptation rules. Provability depends on to extract global information about the program variables (see the side conditions in Figure 2). This notion of provability is used in the following recursion rule:
RECURSION
where and for .
We denote the resulting proof system by CBV (for call-by-value), and for provability in CBV, and for the proof system CBV consisting of all the axioms and rules except the RECURSION rule. So refers to provability in (under the assumptions in ).
Example 4.2.
Consider the block statement and suppose that . We want to prove that
(2)
The approach where we first prove the same pre- and postcondition for the inner statement
is not possible, since then we cannot apply the BLOCK rule, because can occur in . So we introduce a fresh variable and proceed as follows. Let . By the ASSIGNMENT axiom, we have
and
so by the COMPOSITION rule, we have
Now we can apply the BLOCK rule, since , which yields
Applying the SUBSTITUTION rule on the above with the substitution , we then get (2) by the CONSEQUENCE rule, since and are valid. The crux here is that is not changed, because it is a local variable, so we may substitute by .
We can now also prove the correctness formula
(3)
(as discussed in the related work section). By the argument of above, we obtain
and
Applying to the last correctness formula the INVARIANCE rule, we get
Now Equation (3) follows by the COMPOSITION and CONSEQUENCE rules.
Example 4.3.
To illustrate the use of the PROCEDURE CALL rule consider the following example. Let the set of declarations include only the procedure declaration
and consider the correctness formula
(4)
So the variable is here both a global variable that is changed in the procedure body and an actual parameter of the procedure call, a feature that is not allowed in existing Hoare logics for recursive procedures, e.g., Reference [21], as explained in the introduction.
To prove Equation (4), we introduce the assumption
and first show that
(5)
Applying the PROCEDURE CALL rule to the assumption, we get
Next, applying the SUBSTITUTION rule with the substitution we obtain
A trivial application of the CONSEQUENCE rule then completes the proof of Equation (5).
We next show that
(6)
First, we get by the ASSIGNMENT axiom
so by the CONSEQUENCE rule we get
From Equation (5) and Equation (6), we derive by the RECURSION rule the correctness formula (4).
The above example proofs illustrate some characteristic uses of the adaptation rules. Adaptation rules are always applicable, and thus may lead to an arbitrary and unbounded number of applications within a proof. In Section 5, we show that we still can normalize proofs so that for each proof there exists a linear one.
5 Proof Normalization
A proof
may consist of an arbitrary number of applications of the adaptation rules. However, we shall show in this section that we can normalize such a proof to obtain a proof that is still linear in the size of the statement , defined as in Definition 4.1 but with the additional clauses:
•
,
•
.
We divide the rules of into analytical rules and adaptation rules. Analytical rules are those rules that one applies by analyzing the structure of a specified statement: The premise or premises of analytical rules are correctness formulas of sub-statements of the statement of the conclusion. Thus the number of analytical rules one may apply in any correctness proof of a statement is bounded by the size of the statement. Adaptation can be applied on any statement, and have exactly one correctness formula as premise. So, given a derivation in the proof system , we have that between every two successive applications of analytical rules there is a (possibly empty) sequence of adaptation rule applications.
Thus to show that one can always construct a proof that is of linear size, it suffices to transform sequences (of arbitrary length) of applications of the adaptation rules to equivalent ones of a fixed size. This transformation process (formalized below by a rewrite system) is called proof normalization, and the resulting proof is normal if all its adaptation rules are brought into a certain equivalent final form.
Rewrite system. For a formal description of the process of normalizing correctness proofs we introduce the following alphabet to abbreviate sequences of adaptation rules:
•
denotes an application of the CONSEQUENCE rule,
•
denotes an application of the SUBSTITUTION rule,
•
denotes an application of the INVARIANCE rule, and
•
denotes an application of the -INTRODUCTION rule.
Sequences of adaptation rule applications are represented by the regular expression , where denotes choice, and is Kleene’s star with respect to concatenation. Two such sequences are equivalent if their application to any correctness formula yields the same correctness formula. We will introduce a rewrite system by means of which any sequence in can be reduced to a equivalent normal form represented by the regular expression
(7)
where the juxtaposition of expressions is concatenation, and is the usual notation of optional acceptance, i.e., for any regular expression and the empty string . The regular expression (7) describes the empty sequence or non-empty sequences that consist of at most one application of the INVARIANCE followed by at most one application of the SUBSTITUTION rule that in turn is followed by a single application of the CONSEQUENCE rule or a single application of the -INTRODUCTION rule possibly preceded or followed by a single application of the CONSEQUENCE rule. Examples of such expressions are , , , . For technical convenience, to avoid trivial applications of the CONSEQUENCE rule, we assume below some basic logical equivalences in the specification of the correctness formulas.
First, we observe that any consecutive applications of the same rule can be collapsed into a single such rule application. This observation is formalized by the rewrite rules , for any .
For the CONSEQUENCE rule, we have that two consecutive applications
can be collapsed into
For the SUBSTITUTION rule, we have that two consecutive applications
can be collapsed into
where denotes the substitution with domain consisting of the variables of and those variables of that are not among such that
•
if does not appear in ,
•
if and denote the same variable,
•
if does not appear in .
The side-conditions are easily checked to still hold.
For the -INTRODUCTION rule, we have that two consecutive applications
can be collapsed into
where the side-conditions are easily checked to still hold. (Note that and are identical.)
Finally, assuming associativity of conjunction, for the INVARIANCE rule we have that two consecutive applications
can be collapsed into
where the side-conditions are easily checked to still hold.
The following rewrite rules allow to move the INVARIANCE rule applications to the front.
•
: A proof pattern
consisting of an application of the CONSEQUENCE rule followed by one of the INVARIANCE rule, can be transformed into a reverse pattern
•
: A proof pattern
consisting of an application the SUBSTITUTION rule followed by one of the INVARIANCE rule, can be transformed into a reverse pattern
where is a sequence of fresh variables of the same length as . In the SUBSTITUTION rule, we apply the (simultaneous) substitution . Note that equals ( do not appear free in ) and equals .
•
: By the rewrite rule (shown below) it suffices to show that a proof pattern
consisting of an application of the -INTRODUCTION rule followed by one application of the INVARIANCE rule, can be transformed into a pattern :
where, as above, is a sequence of fresh variables of the same length as , and in the application of the SUBSTITUTION rule we apply the substitution . Note that in the application of the -INTRODUCTION rule we assume the logical equivalence between and , which holds, because does not appear in .
The following rules allow to reverse an application of the CONSEQUENCE rule, or an application of the -INTRODUCTION rule, d by an application of the SUBSTITUTION rule.
•
: A proof pattern
consisting of an application of the CONSEQUENCE rule followed by one of the SUBSTITUTION rule, can be transformed into a reverse pattern
•
: A proof pattern
consisting of an application of the -INTRODUCTION rule followed by one of the SUBSTITUTION rule, can be transformed in the reverse pattern
where we note that we may assume that and are disjoint (note that we can simply remove the overlapping variables from the substitution ) and and are disjoint (by an alphabetic conversion of the existentially quantified variables ), and thus is logically equivalent to .
The mutual dependencies between consecutive applications of the CONSEQUENCE and the -INTRODUCTION rules do not allow a simple reversal of the ordering as above. This is because, on the one hand, the CONSEQUENCE rule may enable an application of the -INTRODUCTION rule by generating a postcondition that does not contain free occurrences of the quantified variable. However, the -INTRODUCTION may enable an application of the CONSEQUENCE rule by weakening the precondition. However, these dependencies can be unravelled by the following rewrite rule.
•
: A proof pattern
can be transformed into a pattern (assuming without loss of generality that and are disjoint)
Note that indeed we can existentially quantify both the variables and in this single application of the SUBSTITUTION rule, because the above pattern ensures that the variables of do not appear free in and that the variables do not appear free in . But validity of implies that we may assume without loss of generality that also does not contain free occurrences of . Further, note that validity of implies that of .
We thus obtain a rewrite system (see Reference [32]), in which the objects are sequences of adaptation rule applications, and rewrite rules are applicable anywhere in such sequences. It is straightforward to check that no rewrite rule is applicable if and only if the sequence is in normal form, as defined by the above regular expression (7). To show that any sequence in can be reduced to a equivalent normal form it thus suffices to show that the rewrite system terminates.
Termination. We show that our rewrite system terminates (see Reference [32, Chapter 6]) by associating with each sequence in an element of a well-founded ordering that (strictly) decreases with each application of a rewrite rule. Relevant parameters to consider are
•
the number of occurrences of , , and ,
•
for each occurrence of the number of preceding occurrences of , and ,
•
for each occurrence of the number of preceding occurrences of and .
However, the rules and increases the number of occurrences of and , and as such these rules will in general lead to an increase of the above second and third parameters. Therefore, we single out the two parameters that record for each occurrence of the number of preceding occurrences of and the number of occurrences of itself. To ensure each application of a rewrite rule causes an overall decrease, we use pairs of natural numbers, ordered lexicographically, that is, if , or and , and associate with each sequence in a pair such that sums up
•
the number of occurrences of ,
•
for each occurrence of the number of preceding occurrences of ,
and sums up
•
the number of occurrences of , an ,
•
for each occurrence of the number of preceding occurrences of and ,
•
for each occurrence of the number of preceding occurrences of and .
It is straightforward to check that with each application of a rewrite rule the above measure indeed decreases. Consider as a typical example the rule . Clearly the number of occurrences of preceding the occurrence of to which this rewrite rule is applied decreases. It further does not affect the other parameters. So it decreases the above component, which causes an overall decrease, because the above component is unaffected. As another example consider the rule . Since this rule generates a new , it may increase the above component. However, the number of occurrences of preceding the occurrence of to which this rewrite rule is applied decreases, and as such it decreases the above component (which thus causes an overall decrease). A similar argument applies to the rule : The increase of the number of occurrences of is compensated by the decrease of the number of occurrences of .
We also have checked termination of our rewriting system using the AProVE tool [20]. However, the automatic termination proof is not as legible as the description given above.
Next, we show that the rewrite system is confluent, which implies that for any sequence in there exists a unique normal form.
Confluence. By Newman’s Lemma, every rewrite system that is terminating and weakly confluent is also confluent (see Reference [32]). Thus, to show that our rewrite system is confluent, it suffices to show that it is weakly confluent. The Critical Pair Lemma states that a rewrite system is weakly confluent if and only if all its critical pairs are convergent (also called joinable, see Reference [32, Section 2.7.2]): The two reducible expressions of the critical pair have a common reduct. We thus establish confluence by analyzing all critical pairs that arise from our rewrite rules. This road to confluence is also known as the Knuth-Bendix Theorem.
We now show that all critical pairs are convergent. These critical pairs are identified by considering all ways in which the left-hand side patterns (the redexes) of the rewrite rules can overlap. Let , and range over , and (overlapping) redexes) be indicated by underlining/overlining. For all pairs and of redexes of two letters, we obtain the critical pair : It thus suffices to analyze for each redex of two letters all critical pairs obtained by either adding one letter after or adding one before. For the single redex consisting of three letters, it suffices to analyze , which is the single way it can overlap with itself, and analyze the remaining critical pairs and for in . This analysis is covered by the following cases (in some cases below the transitive closure abstracts from the order of applications of rewrite rules that do not have overlapping redexes).
•
The critical pair is convergent, for :
Applying the rewrite rule to the first redex or the second one, both give .
•
The critical pairs and are convergent, where and , or and :
—
Applying first the rewrite rule to the first redex of , gives
.
—
Applying first the rewrite rule to the second redex of , gives
.
—
Applying first the rewrite rule to the first redex of , gives
.
—
Applying first the rewrite rule to the second redex of , gives
.
•
The critical pair is convergent:
—
Applying first the rewrite rule to the first redex, gives
.
—
Applying first the rewrite rule to the second redex, gives
.
•
The critical pair is convergent:
—
Applying first the rewrite rule to the first redex, gives
.
—
Applying first the rewrite rule to the second redex, gives
.
•
The critical pair is convergent:
—
Applying first the rewrite rule to the first redex, gives
.
—
Applying first the rewrite rule to the second redex, gives
.
•
The critical pair is convergent:
—
Applying first the rewrite rule to the first redex, gives
.
—
Applying first the rewrite rule the second redex, gives
•
The critical pair is convergent:
—
Applying first the rewrite rule the first redex, gives
—
Applying first the rewrite rule to the second redex, gives
.
•
The critical pair is convergent:
—
Applying first the rewrite rule to the first redex, gives
.
—
Applying first the rewrite rule to the second redex, gives
.
•
The critical pair is convergent:
—
Applying first the rewrite rule to the first redex, gives
.
—
Applying first the rewrite rule to the second redex, gives
.
•
The critical pair is convergent:
—
Applying first the rewrite rule to the first redex, gives
.
—
Applying first the rewrite rule to the second redex, gives
.
We also have checked confluence of our rewriting system using the CSI tool [27]. However, also here the automatic confluence proof is not as legible as the description given above.
Scheduling strategy. For any sequence, we can derive the normal form of Equation (7) by scheduling the rewrite rules as follows:
(1)
For any sequence of letters , move to the front and collapse all consecutive applications.
(2)
For the resulting postfix , move to the front and collapse all consecutive applications.
(3)
For the resulting non-empty postfix , first collapse all consecutive applications to a single , and all consecutive applications to a single . Then we repeatedly apply the rewrite rule and collapse the possibly generated consecutive applications until at most one application is left (with possibly one before and possibly one after it).
Thus starting from any sequence of adaptation rules, we end up with at most five rule applications.
Linear proofs. Using the proof normalization procedure above, we can now prove the claim that our proof system admits linear proofs. Given a set of contracts , denote by
the existence of a proof of in from the assumptions that consists of at most applications of axioms and proof rules.
Lemma 5.1.
Suppose that . Then , where .
Proof.
The proof consists of at least applications of analytical axioms and rules, and between two analytical rules, or between an analytical rule and an assumption or an axiom application, we have an arbitrary sequence of adaptations. The latter can be reduced to a sequence of at most five rule applications. Thus the total number of axiom and rule applications needed in a proof is at most .□
We denote by the existence of a proof of in that consists of at most applications of axioms and proof rules.
Theorem 5.2.
Let and suppose that . Then , where is the length of seen as a string of symbols.
Proof.
The correctness formula was established using the RECURSION rule. By Lemma 5.1 to prove the premises of this rule, it takes at most steps, where are the bodies of the procedures declared in . Clearly, is less than the length of seen as a string of symbols.□
In the above result, we measure the complexity in size of the proof, being the number of axiom and rule applications. By inspection of the rewrite rules introduced above, it is easily seen that the weight of the proof (being the maximum complexity of the pre- and postconditions that occur within correctness formulas as they appear in rule applications, as measured by the number of connectives and quantifiers) remains constant: thus, the existence of a linear proof does not result in an explosion of the complexity of assertions.
6 Soundness
We first prove the soundness of . We treat soundness of the block rule and the rule for procedure calls in the context of a set of declarations (soundness of the rules for the remaining statements are standard).
But by the soundness of PARALLEL ASSIGNMENT axiom , so implies by the soundness of the COMPOSITION rule .□
We next introduce a semantic interpretation of that abstracts from the actual implementation of the procedures as specified by . Note that in such a proof only information about the variables of is used (in the INVARIANCE, SUBSTITUTION and -INTRODUCTION rules). We therefore introduce the notation to denote that and for every we have . Note that implies that , for every statement . It also holds that , and for every th approximation of (see Definition 3.1). We use the relation between programs in the soundness proof below, since syntactic approximations do not add more variables or variables that may be changed.
Further, let denote that , for every .
Definition 6.3.
denotes that implies , for all .
We then have the following corollary.
Corollary 6.4 (Soundness of )
implies .
Proof.
The proof proceeds by a straightforward induction on the length of proof, using the above lemmas for the BLOCK rule and the PROCEDURE CALL rule. The side conditions of the SUBSTITUTION and INVARIANCE rule are dealt with by the assumption that , for every .□
To prove soundness of the proof system CBV it then suffices to prove the soundness of the RECURSION rule (note that the RECURSION rule is the only rule for deriving a correctness formula about a program).
Theorem 6.5 (Soundness of the Recursion Rule).
Let and be such that , . Then
implies
Proof. By Definition 6.3, the conclusion follows from the first premise and that we have , if we show . For the latter, it suffices to show that , for . By the Approximation item of Lemma 3.2 this reduces to showing that , for every and . We prove this by induction on .
Base case: By Definition 3.1 and the Inlining item of Lemma 3.2 it suffices to observe that and that , for any assertions and .
Induction step: We show that the induction hypothesis implies . Since we have the second premise and , the induction hypothesis implies by Definition 6.3. It is sufficient to show that the latter is equivalent to
By Definition 3.1, Corollary 3.6, and , we have that
if and only if
for every . Observe that
holds by simplification and definition of . Further, we have that
since does not contain any procedure calls (thus allowing us to replace all declarations), and by the definition of and the Inlining item of Lemma 3.2. Thus we have established that
if and only if
7 Completeness
We now prove completeness of CBV in the sense of Cook, that is, assuming that the language is expressive (see Definition 3.8) and that all valid assertions can be used in proofs. To this end, following Gorelick [21], we introduce the most general correctness formulas. Given a set of declarations , in our setup these are contracts of the form
where
•
,
•
,
•
and are lists of fresh variables, of the same length as, respectively, and ,
•
is the strongest postcondition given in Definition 3.7.
The crucial difference between our most general correctness formulas and the ones used in [21] is that in our case the strongest postcondition of the generic call is defined in terms of a strongest postcondition of the body in which the formal parameters are quantified out. This has to do with the way we model the call-by-value parameter mechanism by a general notion of local variables, whereas, as already mentioned, in Reference [21] the call-by-name parameter mechanism is used in combination with a specific notion of local variables that ensures static scoping semantically by variable renaming.
To compensate for this loss of your information, we have introduced the variables that in the above postcondition denote the initial values of the formal parameters . The variables are used in the above postcondition to denote the initial values of the variables that could be changed by a call . In particular, note that and have no variables in common, because , where . In fact, it is important to note that the sets of variables listed in and are mutually disjoint.
The following crucial theorem shows that the assertion
encodes the semantics of a call , where is declared by . Note that since the sets of variables and are disjoint, equals . Further, since are used to denote in the postcondition the initial values of the variables , denotes in the postccondition the initial values of the actual parameters .
Theorem 7.1.
Let be declared by . Further, let the lists of variables and be defined as above and let
where for some sequence of elements (of the domain of ).
By the definition of the strongest postcondition there exists a state such that
•
and
•
.
Let . Assume first that
(9)
Then, given that and , Corollary 3.3 allows us to derive the following chain of equalities:
Figure 3 clarifies the relation between the introduced states and illustrates the construction of a computation of that starts in the state with the final state and that corresponds to the above equalities.
Fig. 3.
Fig. 3. Construction of a computation of .
It remains to prove Equation (23). First, note the following consequences of the Access and Change item of Lemma 3.2 that follow from the fact that the variables listed in and are fresh and that by the choice of we have :
(a)
,
(b)
,
(c)
, where .
By Equation (22), , so by the definition of (this is an instance of the Simultaneous Substitution Lemma in the textbook [4, p. 50]) , i.e.,
This, item (a) above, the fact that the sets of variables listed in and are mutually disjoint, and the definitions of and justifies the following chain of equalities:
Next, the same observations and item (b) above justifies the following chain of equalities:
Finally, take a variable . Then the above observations and item (c) above justifies the following chain of equalities:
We thus established Equation (23), which concludes the proof.□
From the above theorem, we derive the following corollary.
Corollary 7.2.
Let , where is declared by . Further, let the lists of variables and be defined as above and let
where . We are given that , so by the definition of . (This is again the contents of the Simultaneous Substitution Lemma in the textbook [4, p. 50].) We conclude by the assumption that .□
In the completeness proof below, we transform a given precondition of a procedure call into an invariant. The following corollary shows that any precondition logically implies its invariant transformation for some values of the variables and .
Corollary 7.3.
Let the lists of variables and be defined as above and let
Suppose that the variables listed in and do not appear in . Then
Proof.
Take a state such that . By assumption the variables listed in and do not occur in , so , where .
Note that , so . By the Simultaneous Substitution Lemma of Reference [4, p. 50] , i.e.,
Further, for an arbitrary we have
so
This shows that
and yields the conclusion by the definition of .□
As in Reference [21] the completeness proof is based on the following key lemma (see also Reference [3, pp. 450–452]). We denote by the set of most general correctness formulas for all procedures declared in .
Lemma 7.4.
Suppose that . Then .
Proof.
As in Reference [21] and Reference [5], we proceed by induction on the structure of the statement , with two essential cases being different.
Block statements. Suppose that . Let be some fresh variables corresponding to the local variables . Note that by the definition of ,
(10)
So from the soundness of the INVARIANCE rule it follows that
Consequently, by the soundness of the CONSEQUENCE rule
because implies . From Corollary 3.6 it then follows that
By the induction hypothesis we obtain
An application of the BLOCK rule then gives
Thanks to Equation (24), we can now apply the SUBSTITUTION rule with the substitution and subsequently the CONSEQUENCE rule to replace by . This yields
Procedure calls. Suppose that , where is declared by .
Assume the most general correctness formula
By applying the SUBSTITUTION rule to rename the variables listed in and , we may assume these variables not appear in . By the choice of the list and none of them contains a variable from . So by the PROCEDURE CALL rule with the substitution , we obtain
The proof system CBV is complete (in the sense of Cook).
Proof.
Let . To prove in CBV, we use the RECURSION rule with as the set of assumptions in the subsidiary proofs. Lemma 7.4 ensures the first premise. The remaining premises also follow by this lemma. Indeed, suppose
where .
Choose an arbitrary . By the definition of the strongest postcondition
so
by the soundness of the CONSEQUENCE rule. Hence by Lemma 7.4
We now obtain by the RECURSION rule.□
We conclude this section with the following simple calculation of the complexity of the completeness proof (measured in terms of the number of axioms and rules applied). Since the above completeness proof shows that the INVARIANCE, SUBSTITUTION and -INTRODUCTION rules are only used for the block statements and the procedure calls, we can lower the upper bound of Theorem 5.2 by
where denotes the number of assignments, block statements and iteration statements, denotes the number of block statements, and denotes the number of procedure calls.
8 Formalization in Coq
The main semantic argument underlying the completeness proof is the proof of Theorem 7.1 (and its Corollaries 7.2 and 7.3), which shows how the semantics of procedure calls can be expressed by the strongest postcondition. We checked this proof by means of the Coq theorem prover, and to this end we only need to formalize the semantics of the programming language and the strongest postcondition. Our formalization is publicly and freely accessible.3
Theorem 7.1 requires first of all a formalization of the syntax and semantics of the programming language and the assertion language. A main challenge is to abstract from syntax to avoid the overhead of irrelevant details, while still capturing essential syntactical notions like occurrences of variables and substitution. We formalize in Coq expressions semantically as particular functions from states to (abstract) values. Similarly, we formalize assertions semantically, as sets of states. Moreover, this extensional approach4 to the formalization of expressions and assertions also allows to abstract from the given interpretation and the assumption of the expressibility of the strongest postcondition. However, and this is where our approach crucially differs from, for example, References [34, 36], to capture essential syntactic notions like that of occurrences of free variables (this is required in the notion of freshness used in Theorem 7.1.) we introduce finitely-based functions and predicates as the semantic structures for expressions and assertions, as explained in more detail next.
An expression is formalized as a function from states to values together with an additional list of variables with the coincidence condition that for every such that we have . Similarly, an assertion consists of a set of states and a list of variables with the coincidence condition that for every such that we have iff . For assertion , we write to mean . The intuition is that the finite set of variables associated with an expression or assertion forms its basis: the semantic counterpart of the syntactical notion of free variable occurrences. Only the values assigned by a state to variables in its basis can influence an expression’s value or an assertion’s truth. Assertions are equal whenever their extension and basis are equal, regardless of the proof of the coincidence condition.5
For the formalization, we further need the following constructions of expressions and assertions. For a given value, we immediately can construct an expression that evaluates to that value with the empty basis. For a given variable, we can construct an expression that evaluates to the value of that variable and its basis consists of (at least) the given variable. Since one could always extend a basis, we take the smallest. Given two expressions, we can construct the assertion that states their equality: Its extension consists of those states in which the equality is evident, and its basis is the union of the bases of the equated expressions. We also have equality of lists of variables of equal length. For all these constructions, we verified the coincidence condition.
Further, we have the constructions of conjunction, implication, substitution, and existential quantification assertions. Given two assertions and , the conjunction consists of the intersection of the states of and and as basis the union of the bases of and . Similarly, we can define the implication . For the substitution construct , we take an assertion and assignment that is an association of variables in to expressions in . Let be a state update replacing the values of variables by the corresponding value of . We define the set of states of the substitution as . The basis of the substitution construct is the basis of with variables in removed, together with the union of the bases of expressions in . Thus, if a variable occurs both in and in some expression in , then it is still in the basis of . The Simultaneous Substitution Lemma, i.e., if and only if , then can be verified already by definition. Finally, the existential quantification is formalized by the set of states and as basis, the basis of with all variables in removed.
The syntax of statements we formalize does not include statements, but does include a statement that is needed for Approximation part of Lemma 3.1. This modification does not reduce expressivity of the language, as it is well known that while loops can be encoded using (tail) recursion, but it simplifies the definition of, and proofs about, the semantics of programs.
We have formalized the big-step operational semantics as given in Figure 1 by an inductive predicate, so that every program is associated to a relation of states denoted by . This relation can also be treated as a function mapping states to a subset of states. We then have formally verified the properties of Lemma 3.1, Corollary 3.2, Lemma 3.3, and Corollary 3.4. Not all of these results are needed in Theorem 7.1, but their verification increases our confidence that the formalized semantics contains no error.
Given an assertion and program , the strongest postcondition consists of an extension and a basis for which the coincidence condition holds. Its extension is defined by , and as its basis , we take the union of the set of variables occurring in the program and the basis of . The set of variables occurring in a program can be defined inductively by the structure of the program; it is the union of the bases of all expressions and all variables that occur in the program. Now, to show that the coincidence condition holds for the strongest postcondition, we need to show that for every state in its extension, any state obtained from in which variables not in the basis are possibly modified are also in the extension:
To show this property, it is sufficient to show a more general closure property on the meaning of programs. The following lemma establishes the latter property.
Lemma 8.1.
Given a list of variables such that every variable occurring in is also in , and given that and , then .
By , we mean a state, which has the value in for the variables in , and the value in otherwise. Intuitively, we can reconstruct a run backwards from a final state that simulates the original run of the program but with different values stored in non-essential variables.
The above formalization allows for a formal verification of the statements of Theorem 7.1, without adding any custom axioms to the Coq theorem prover. We have used the axioms of functional extensionality, propositional extensionality, and classical logic, all provided by the base system. Functional extensionality is necessary to show equality of states, which are total functions from variables to values. Functional and propositional extensionality is needed for showing (and using) the fact that our semantics is compositional. Classical logic is typically used when reasoning in Hoare logic. This concludes the description of the formalization effort of Reference [22].
9 Conclusions
We conclude that the proof system presented in this article and its relative completeness result consolidates and improves the proof complexity of the proof system in the textbook [4] and Reference [5]. Following this, it would be interesting to revisit related work.
The already-mentioned work of Clarke [10] led to a research on proof systems for programming languages in which in presence of static scope both nested declarations of mutually recursive procedures and procedure names as parameters of procedure calls were allowed. In particular in Reference [30], Reference [13], and Reference [19], sound and relatively complete Hoare-like proof systems were established, each time under different assumptions concerning the assertion language. In all these papers the call-by-name parameter mechanism was used and the actual parameters were variables. It would be interesting to see how to modify these proofs to programming languages in which the call-by-value parameter mechanism is used instead of the call-by-name mechanism.
It would be useful to extend (in an appropriate sense) the results of this article to total correctness of programs. In this context, we should mention [2], where a sound and relatively complete (in an appropriate sense) proof system for total correctness of programs in presence of recursive procedures was provided. However, in the article only procedures without parameters were considered.
Formally verified completeness and soundness theorems of Hoare logic in theorem provers have been established in, for example, Reference [28]. In future work, we intend to proceed in further formalizing the (syntactic) proof system as described in this article and verifying its soundness and relative completeness theorems in Coq. Such work is comparable to Von Oheimb’s thesis [35], who formalized a Hoare logic for reasoning about a subset of the Java language in Isabelle/HOL.
We can extend our completeness result to object-oriented Java-like programs by the syntax-directed transformation from object-oriented programs to recursive programs as described in [5]. However, separation logic (see Reference [29]) is particularly tailored to modular reasoning about aliasing as it arises in object (and pointer) structures. Completeness for recursive parameterless procedures in separation logic is established in Reference [17]. Of interest is that to obtain this completeness result the frame rules, which are important for the local reasoning in separation logic are not needed (as observed by the authors themselves). A slight modification of the usual adaptation rules for reasoning about invariance are sufficient. Therefore, we expect that the completeness result of Reference [17] can be extended to recursive procedures with call-by-value parameter passing, using our techniques.
Acknowledgment
Krzysztof R. Apt identified the problem of completeness of reasoning about call-by-value in Hoare logic. We also thank him for his contributions to earlier versions of the article. We thank Ernst-Rüdiger Olderog and Stijn de Gouw for helpful comments about the contributions of a number of relevant references. We further are most grateful for the comments of the anonymous referees that led to various improvements.
Footnotes
1
Both notions are explained in Section 2. Almost all programming languages assume static scope.
2
Not to be confused with generic types (e.g., as in Java) of the formal parameters. Our basic programming language does not have multiple different types, nor generic types.
For this, we may use proof irrelevance, which in Coq follows from propositional extensionality.
References
[1]
Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, and Mattias Ulbrich (Eds.). 2016. Deductive Software Verification—The KeY Book: From Theory to Practice. Lecture Notes in Computer Science, Vol. 10001. Springer. DOI:
Krzysztof R. Apt, Frank S. de Boer, Ernst-Rüdiger Olderog, and Stijn de Gouw. 2012. Verification of object-oriented programs: A transformational approach. J. Comput. Syst. Sci. 78, 3 (2012), 823–852.
Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph R. Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. 2005. An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transf. 7, 3 (2005), 212–232.
J. W. de Bakker. 1979. A sound and complete proof system for partial program correctness. In Proceedings of the 8th Symposium on Mathematical Foundations of Computer Science (Lecture Notes in Computer Science), Vol. 74. Springer, 1–12.
Stijn de Gouw, Frank S. de Boer, Richard Bubel, Reiner Hähnle, Jurriaan Rot, and Dominic Steinhöfel. 2019. Verifying OpenJDK’s sort method for generic collections. J. Autom. Reas. 62, 1 (2019), 93–126.
Steven M. German, Edmund M. Clarke, and Joseph Y. Halpern. 1989. Reasoning about procedures as parameters in the language L4. Inf. Comput. 83, 3 (1989), 265–359.
Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, and Stephan Falke. 2004. Automated termination proofs with AProVE. In Proceedings of the International Conference on Rewriting Techniques and Applications. Springer, 210–220.
G. A. Gorelick. 1975. A Complete Axiomatic System for Proving Assertions about Recursive and Non-recursive Programs. Master’s thesis. University of Toronto.
C. A. R. Hoare. 1971. Procedures and parameters: An axiomatic approach. In Proceedings of Symposium on the Semantics of Algorithmic Languages,Lecture Notes in Mathematics, Vol. 188. Springer-Verlag, 102–116.
Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp. 2017. CSI: New evidence—A progress report. In Proceedings of the Annual Conference on Automated Deduction (CADE’26). Springer, 385–397.
Tobias Nipkow. 2002. Hoare logics for recursive procedures and unbounded nondeterminism. In Proceedings of the International Workshop on Computer Science Logic,Lecture Notes in Computer Science, Vol. 2471. Springer.
Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cǎtǎlin Hriţcu, Vilhelm Sjöberg, Andrew Tolmach, and Brent Yorgey. 2020. Programming Language Foundations. Electronic textbook. Version 5.8. Available at https://softwarefoundations.cis.upenn.edu.
Terese, Marc Bezem, Jan Willem Klop, Roel de Vrijer, et al. 2003. Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, Vol. 55. Cambridge University Press.
David von Oheimb. 1999. Hoare logic for mutual recursion and local variables. In Foundations of Software Technology and Theoretical Computer Science (FSTTCS’99)Lecture Notes in Computer Science, Vol. 1738. Springer, 168–180. https://doi.org/10.1007/3-540-46691-6_13
David von Oheimb. 2001. Analyzing Java in Isabelle/HOL: Formalization, Type Safety and Hoare Logic. Ph.D. Dissertation. Technische Universität München. Available at http://ddvo.net/diss/.
David von Oheimb and Tobias Nipkow. 2002. Hoare logic for NanoJava: Auxiliary variables, side effects, and virtual methods revisited. In Proceedings of the Formal Methods—Getting IT Right (FME’02)Lecture Notes in Computer Science, Vol. 2391. Springer, 89–105. DOI:
We show how codatatypes can be employed to produce compact, high-level proofs of key results in logic: the soundness and completeness of proof systems for variations of first-order logic. For the classical completeness result, we first establish an ...
I present a formalization in Isabelle/HOL of the resolution calculus for first-order logic with formal soundness and completeness proofs. To prove the calculus sound, I use the substitution lemma, and to prove it complete, I use Herbrand interpretations ...
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
holds after
is executed. However, there is no way to prove it. In Gorelick’s thesis [21] this error does not arise, since all local variables are explicitly initialized to a given-in-advance value, both in the semantics and in the proof theory (by adjusting the precondition of the corresponding declaration rule).
holds after
the local variable 
is initialized to the value of the global variable 
. Consequently, according to our semantics, and also the semantics used in Reference [11], 
holds after execution of the statement
This cannot be proved in the proof system used in Reference [11]. However, we can prove it in our proof system (as shown in Example 4.2).
the local variable 
is initialized to the value of the global variable 
. Consequently, according to our semantics, and also the semantics used in Reference [11], 
holds after execution of the statement
. Expressions are terms in the language 
, Boolean expressions are quantifier-free formulas of 
, while assertions are formulas of 
, which are considered equal up to alphabetic renaming of quantified variables.
. Expressions are terms in the language 
, Boolean expressions are quantifier-free formulas of 
, while assertions are formulas of 
, which are considered equal up to alphabetic renaming of quantified variables.
by Var. For a sequence 
of distinct variables, we denote by 
its corresponding set. For a Boolean expression 
or a sequence 
of expressions, we denote the set of all variables occurring in 
or in 
by, respectively, 
and 
. The set of variables that occur free in an assertion 
is defined in a standard way and denoted by 
.
by Var. For a sequence 
of distinct variables, we denote by 
its corresponding set. For a Boolean expression 
or a sequence 
of expressions, we denote the set of all variables occurring in 
or in 
by, respectively, 
and 
. The set of variables that occur free in an assertion 
is defined in a standard way and denoted by 
.
for a list of distinct variables 
of the same length is written as 
and the result of applying it to an expression or an assertion 
as 
. To ensure a uniform presentation, we allow the empty substitution in which the list of variables 
is empty.
for a list of distinct variables 
of the same length is written as 
and the result of applying it to an expression or an assertion 
as 
. To ensure a uniform presentation, we allow the empty substitution in which the list of variables 
is empty.
where
denotes the “empty” statement,
is a parallel assignment, with 
a (possibly empty) list of distinct variables and 
a list of expressions of the same length as 
; when 
is empty, we identify 
with the 
statement,
is a procedure name; each procedure 
is defined by a declaration of the form
where 
is a (possibly empty) list of distinct variables, called formal parameters of the procedure 
, and 
is a statement, called the body of the procedure 
,
is a procedure call, with the actual parameters 
, which is a (possibly empty) list of expressions of the same length as the corresponding list of formal parameters,
is a Boolean expression,
is a block statement where 
is a (possibly empty) list of distinct local variables, all of which are explicitly initialized by means of the parallel assignment 
.
denotes the “empty” statement,
is a parallel assignment, with 
a (possibly empty) list of distinct variables and 
a list of expressions of the same length as 
; when 
is empty, we identify 
with the 
statement,
is a procedure name; each procedure 
is defined by a declaration of the form
is a (possibly empty) list of distinct variables, called formal parameters of the procedure 
, and 
is a statement, called the body of the procedure 
,
is a procedure call, with the actual parameters 
, which is a (possibly empty) list of expressions of the same length as the corresponding list of formal parameters,
is a Boolean expression,
is a block statement where 
is a (possibly empty) list of distinct local variables, all of which are explicitly initialized by means of the parallel assignment 
.
, where 
is a statement, called the main statement and 
is a set of procedure declarations such that each procedure (name) that appears in 
or 
has exactly one procedure declaration in 
. So we allow mutually recursive procedures but not nested procedures. We denote by 
the set of variables that occur in 
.
, where 
is a statement, called the main statement and 
is a set of procedure declarations such that each procedure (name) that appears in 
or 
has exactly one procedure declaration in 
. So we allow mutually recursive procedures but not nested procedures. We denote by 
the set of variables that occur in 
.
, where 
are assertions and 
is a statement, or a triple 
, where 
is a program. Of special interest in our approach will be the representation of contracts that specify by means of a precondition and postcondition the input/output behavior of a procedure. We represent them by the correctness formulas 
, where 
are the formal parameters of 
. Such a call 
is called a generic procedure call.2 Note that so defined contracts abstract from the implementation of the specified procedure.
, where 
are assertions and 
is a statement, or a triple 
, where 
is a program. Of special interest in our approach will be the representation of contracts that specify by means of a precondition and postcondition the input/output behavior of a procedure. We represent them by the correctness formulas 
, where 
are the formal parameters of 
. Such a call 
is called a generic procedure call.2 Note that so defined contracts abstract from the implementation of the specified procedure.
, where 
is declared by 
, is interpreted as the block statement 
, where 
models the parameter passing by value and the block statement ensures that the changes to the formal parameters 
are local. Such a replacement of a procedure call by an appropriately modified procedure body is called inlining or a copy rule.
, where 
is declared by 
, is interpreted as the block statement 
, where 
models the parameter passing by value and the block statement ensures that the changes to the formal parameters 
are local. Such a replacement of a procedure call by an appropriately modified procedure body is called inlining or a copy rule.
declared by 
and the main statement 
. Here the inlining results in the program
that yields 
upon termination. However, if we renamed the occurrence of 
in the block statement to a fresh variable, say, 
, and thus used the statement 
, then inlining would result in the program
that yields 
upon termination. Thus renaming of local variables (e.g., also known as alpha conversion in the lambda calculus) affects the semantics. However, renaming of local variables upon inlining, to avoid clashes between global and local variables, gives rise to a static scope of local variables, which ensures that each procedure call is evaluated in the environment in which it is declared.
declared by 
and the main statement 
. Here the inlining results in the program
upon termination. However, if we renamed the occurrence of 
in the block statement to a fresh variable, say, 
, and thus used the statement 
, then inlining would result in the program
upon termination. Thus renaming of local variables (e.g., also known as alpha conversion in the lambda calculus) affects the semantics. However, renaming of local variables upon inlining, to avoid clashes between global and local variables, gives rise to a static scope of local variables, which ensures that each procedure call is evaluated in the environment in which it is declared.
, we define the set of global variables 
as follows.
,
,
where 
,
,
,
,
,
, we define the set of global variables 
as follows.
,
,
where 
,
,
,
,
,
, where 
.
, where 
.
functions, where 
, defined as follows. For each of them, we reuse the above equalities as definitions, except for the case of the procedure calls for which we set
,
,
functions, where 
, defined as follows. For each of them, we reuse the above equalities as definitions, except for the case of the procedure calls for which we set
,
,
. A simple proof by induction shows that for all 
so for each procedure call 
Denote the least such 
by 
We identify then 
with 
, where 
. Clearly, 
thus defined satisfies the original equalities. 
. A simple proof by induction shows that for all 
by 
We identify then 
with 
, where 
. Clearly, 
thus defined satisfies the original equalities. 
the variables occurring in 
are global, and as such those variables 
appearing in 
are interpreted differently from the local ones that only exist in the context of the block statement (as formalized in Section 3). We view the variables from 
as the global variables of the procedure 
.
the variables occurring in 
are global, and as such those variables 
appearing in 
are interpreted differently from the local ones that only exist in the context of the block statement (as formalized in Section 3). We view the variables from 
as the global variables of the procedure 
.
appears in the (lexical) scope of a block statement 
, if 
appears in the list of local variables 
and 
contains a call of 
. A program 
is called clash-free if the following holds for every procedure 
declared in 
: no variable 
appears in the scope of a block statement that occurs in 
.
appears in the (lexical) scope of a block statement 
, if 
appears in the list of local variables 
and 
contains a call of 
. A program 
is called clash-free if the following holds for every procedure 
declared in 
: no variable 
appears in the scope of a block statement that occurs in 
.
, we define the set of variables that may be changed by it as follows. Consider the following equalities:
,
,
,
,
,
,
.
, we define the set of variables that may be changed by it as follows. Consider the following equalities:
,
,
,
,
,
,
,
,
.
. Each realization of this type (called a domain) yields an interpretation 
that assigns a meaning to the function symbols and relation symbols of the language 
.
. Each realization of this type (called a domain) yields an interpretation 
that assigns a meaning to the function symbols and relation symbols of the language 
.
. By a state, we mean a function that maps each variable to an element of the domain of 
. We denote the set of states by 
.
. By a state, we mean a function that maps each variable to an element of the domain of 
. We denote the set of states by 
.
of a state 
, where 
is a variable and 
an element of the domain of 
, is a state that coincides with 
on all variables except 
to which it assigns 
. A simultaneous update 
of a state 
, where 
is a list of (distinct) variables and 
is a list of domain elements of the same length, is defined analogously.
of a state 
, where 
is a variable and 
an element of the domain of 
, is a state that coincides with 
on all variables except 
to which it assigns 
. A simultaneous update 
of a state 
, where 
is a list of (distinct) variables and 
is a list of domain elements of the same length, is defined analogously.
and an expression 
, we define the element 
of the domain of 
inductively in the standard way and for 
we put 
.
and an expression 
, we define the element 
of the domain of 
inductively in the standard way and for 
we put 
.
of variables, we denote by 
the restriction of the state 
to the variables occurring in 
and write for two states 
and 
if 
. We extend the definitions of an update and equality 
to, respectively, a set of states and sets of states in the expected way. So for a set of states 
and for two sets of states 
and 
and a set of variables 
,
of variables, we denote by 
the restriction of the state 
to the variables occurring in 
and write for two states 
and 
. We extend the definitions of an update and equality 
to, respectively, a set of states and sets of states in the expected way. So for a set of states 
and 
and a set of variables 
,
is true in the state 
,” denoted by 
, is defined inductively in the standard way. The meaning of an assertion (with respect to the interpretation 
), written as 
, is defined by 
We say that 
is valid, and write 
, if 
.
is true in the state 
,” denoted by 
, is defined inductively in the standard way. The meaning of an assertion (with respect to the interpretation 
), written as 
, is defined by 
We say that 
is valid, and write 
, if 
.
is a function 
of which the small-step operational semantics is given in the textbook [4]. See Figure 1 for its big-step operational semantics. The operational definition of the assignment, sequential composition, choice and iteration constructs are standard. A procedure call is defined in terms of a corresponding block statement. The semantics of a block statement 
resets the local variables 
after the execution of the statement 
. Note that since 
are evaluated in the initial state, the variables 
appearing in 
also refer to their values in the initial state.
is a function 
of which the small-step operational semantics is given in the textbook [4]. See Figure 1 for its big-step operational semantics. The operational definition of the assignment, sequential composition, choice and iteration constructs are standard. A procedure call is defined in terms of a corresponding block statement. The semantics of a block statement 
resets the local variables 
after the execution of the statement 
. Note that since 
are evaluated in the initial state, the variables 
appearing in 
also refer to their values in the initial state.
, 
states the fact that the program 
terminates when started in the initial state 
, yielding the final state 
. If 
does not terminate when started in 
, then 
is the empty set.
, 
states the fact that the program 
terminates when started in the initial state 
, yielding the final state 
. If 
does not terminate when started in 
, then 
is the empty set.
to deal with sets of states 
by
to deal with sets of states 
by
and a statement 
, we define the 
th syntactic approximation 
of 
by induction on 
:
where 
denotes a diverging statement (e.g., 
) and 
is the result of a simultaneous replacement in 
of each procedure call 
by
Furthermore, let 
stand for 
.
and a statement 
, we define the 
th syntactic approximation 
of 
by induction on 
:
denotes a diverging statement (e.g., 
) and 
is the result of a simultaneous replacement in 
of each procedure call 
by
stand for 
.
and where 
,
and where 
,
As a special case, we have for any procedure 
declared by 
,
declared by 
,
and 
if 
then
and 
if 
then
It states that the execution of a block statement consists of the initialization of the local variables, followed by the execution of its body, and a subsequent reset of the local variables to their initial values. The Access and Change item formalizes the intuition that when executing a program 
only variables in 
can be modified. It can be equivalently stated as that 
implies
only variables in 
can be modified. It can be equivalently stated as that 
implies
is declared by 
. For all states 
where 
.
is declared by 
. For all states 
.
□
and a correctness formula 
, we write
if
We say then that 
is true in the sense of partial correctness.
and a correctness formula 
, we write
is true in the sense of partial correctness.
Then for all assertions 
and 
such that 
and 
such that 
, so for arbitrary states 
and 
such that 
we have 
iff 
. Hence for two sets of states 
and 
such that 
, we have
So the desired equivalence follows Equation (1) and the definition of 
.□
, so for arbitrary states 
and 
such that 
we have 
iff 
. Hence for two sets of states 
and 
such that 
, we have
.□
and 
such that 
,
iff 
.
iff 
,
and 
such that 
,
iff 
.
iff 
,
is declared by 
.
is declared by 
.
the strongest postcondition of the program 
with respect to an assertion 
, defined by
the strongest postcondition of the program 
with respect to an assertion 
, defined by
is the set of states that can be reached by executing 
starting in a state satisfying 
.
is the set of states that can be reached by executing 
starting in a state satisfying 
.
is definable (in the given interpretation 
) iff for some formula 
of 
we have 
. We say then that 
defines 
.
is definable (in the given interpretation 
) iff for some formula 
of 
we have 
. We say then that 
defines 
.
is expressive with respect to the given interpretation 
, if for for every assertion 
and program 
the set of states 
is definable.
is expressive with respect to the given interpretation 
, if for for every assertion 
and program 
the set of states 
is definable.
is expressive with respect to the given interpretation 
and identify 
with its defining formula.
is expressive with respect to the given interpretation 
and identify 
with its defining formula.
that 
can be proved by means of the proof system. We say that a proof system
can be proved by means of the proof system. We say that a proof system
,
,
,
,
. Hoare actually introduced two consequence rules, that soon after were combined into the rule listed here. The proof rule concerning the if-then-else statement was originally proposed by P. Lauer [25].
. Hoare actually introduced two consequence rules, that soon after were combined into the rule listed here. The proof rule concerning the if-then-else statement was originally proposed by P. Lauer [25].
, CBV (each includes all rules and axioms of the former).
denote the number of constructs of 
, inductively defined as follows.
denote the number of constructs of 
, inductively defined as follows.
as follows:
,
,
,
,
,
as follows:
,
,
,
,
,
that if 
is provable then there exists a proof that consists of at most 
rule applications.
that if 
is provable then there exists a proof that consists of at most 
rule applications.
about a recursive program 
, we extend the basic Hoare logic with the following proof strategy:
about a recursive program 
, we extend the basic Hoare logic with the following proof strategy:
of the main statement with respect to assumptions 
about the procedure calls (thus abstracting from their implementation),
of the main statement with respect to assumptions 
about the procedure calls (thus abstracting from their implementation),
. The 
sign refers to the provability in the basic Hoare logic extended with the following rule for the block statement from the textbook [4, p. 158]:
. The 
sign refers to the provability in the basic Hoare logic extended with the following rule for the block statement from the textbook [4, p. 158]:
where 
.
.
and 
denote the same procedure identifier, for some 
. In this rule there are 
subsidiary proofs in the premises, where 
is the total number of procedure calls that appear in 
. Note that the statements used on the right-hand sides of the last 
provability signs 
are the corresponding effects of inlining applied to the procedure calls on the left-hand side of 
. In this proof rule each procedure calls requires a separate subsidiary correctness proof. This results in inefficient correctness proofs.
and 
denote the same procedure identifier, for some 
. In this rule there are 
subsidiary proofs in the premises, where 
is the total number of procedure calls that appear in 
. Note that the statements used on the right-hand sides of the last 
provability signs 
are the corresponding effects of inlining applied to the procedure calls on the left-hand side of 
. In this proof rule each procedure calls requires a separate subsidiary correctness proof. This results in inefficient correctness proofs.
with 
procedure calls, each of the 
subsidiary proofs in the premises of the above recursion rule can be established in the number of steps linear in the length of 
. But 
is linear in the length of 
, as well, and as a result the bound on the length of the whole proof is quadratic in the length of 
. This bound remains quadratic even for programs with a single procedure, since 
remains then linear in the length of 
.
with 
procedure calls, each of the 
subsidiary proofs in the premises of the above recursion rule can be established in the number of steps linear in the length of 
. But 
is linear in the length of 
, as well, and as a result the bound on the length of the whole proof is quadratic in the length of 
. This bound remains quadratic even for programs with a single procedure, since 
remains then linear in the length of 
.
such that 
, where 
are the formal parameters of 
, by the block statement 
. This gives rise to so-called pure programs that only contain generic procedure calls (as introduced in Section 2). For pure programs the last 
premises of the above recursion rule reduce to
such that 
, where 
are the formal parameters of 
, by the block statement 
. This gives rise to so-called pure programs that only contain generic procedure calls (as introduced in Section 2). For pure programs the last 
premises of the above recursion rule reduce to
premises can be reduced to
provided that 
for 
.
premises can be reduced to
for 
.
This rule can be further simplified to a direct instantiation of the generic call using a BLOCK rule:
where 
.
.
is the number of different procedure calls that appear in 
. But for pure programs 
, where 
is the number of procedure declarations in 
(or 
if each procedure declared is also called).
is the number of different procedure calls that appear in 
. But for pure programs 
, where 
is the number of procedure declarations in 
(or 
if each procedure declared is also called).
-INTRODUCTION also used in Reference [21] (though the side conditions are slightly different).
-INTRODUCTION also used in Reference [21] (though the side conditions are slightly different).
refer to provability in the proof system that extends the basic Hoare logic with the above BLOCK, PROCEDURE CALL and adaptation rules. Provability depends on 
to extract global information about the program variables (see the side conditions in Figure 2). This notion of provability is used in the following recursion rule:
refer to provability in the proof system that extends the basic Hoare logic with the above BLOCK, PROCEDURE CALL and adaptation rules. Provability depends on 
to extract global information about the program variables (see the side conditions in Figure 2). This notion of provability is used in the following recursion rule:
and 
for 
.
and 
for 
.
for provability in CBV, and 
for the proof system CBV consisting of all the axioms and rules except the RECURSION rule. So 
refers to provability in 
(under the assumptions in 
).
for provability in CBV, and 
for the proof system CBV consisting of all the axioms and rules except the RECURSION rule. So 
refers to provability in 
(under the assumptions in 
).
and suppose that 
. We want to prove that
and suppose that 
. We want to prove that
is not possible, since then we cannot apply the BLOCK rule, because 
can occur in 
. So we introduce a fresh variable 
and proceed as follows. Let 
. By the ASSIGNMENT axiom, we have
and
so by the COMPOSITION rule, we have
Now we can apply the BLOCK rule, since 
, which yields
Applying the SUBSTITUTION rule on the above with the substitution 
, we then get (2) by the CONSEQUENCE rule, since 
and 
are valid. The crux here is that 
is not changed, because it is a local variable, so we may substitute 
by 
.
can occur in 
. So we introduce a fresh variable 
and proceed as follows. Let 
. By the ASSIGNMENT axiom, we have
, which yields
, we then get (2) by the CONSEQUENCE rule, since 
and 
are valid. The crux here is that 
is not changed, because it is a local variable, so we may substitute 
by 
.
(as discussed in the related work section). By the argument of above, we obtain
and
Applying to the last correctness formula the INVARIANCE rule, we get
Now Equation (3) follows by the COMPOSITION and CONSEQUENCE rules.
include only the procedure declaration
and consider the correctness formula
So the variable 
is here both a global variable that is changed in the procedure body and an actual parameter of the procedure call, a feature that is not allowed in existing Hoare logics for recursive procedures, e.g., Reference [21], as explained in the introduction.
include only the procedure declaration
is here both a global variable that is changed in the procedure body and an actual parameter of the procedure call, a feature that is not allowed in existing Hoare logics for recursive procedures, e.g., Reference [21], as explained in the introduction.
may consist of an arbitrary number of applications of the adaptation rules. However, we shall show in this section that we can normalize such a proof to obtain a proof that is still linear in the size of the statement 
, defined as in Definition 4.1 but with the additional clauses:
,
.
, defined as in Definition 4.1 but with the additional clauses:
,
.
into analytical rules and adaptation rules. Analytical rules are those rules that one applies by analyzing the structure of a specified statement: The premise or premises of analytical rules are correctness formulas of sub-statements of the statement of the conclusion. Thus the number of analytical rules one may apply in any correctness proof of a statement is bounded by the size of the statement. Adaptation can be applied on any statement, and have exactly one correctness formula as premise. So, given a derivation in the proof system 
, we have that between every two successive applications of analytical rules there is a (possibly empty) sequence of adaptation rule applications.
into analytical rules and adaptation rules. Analytical rules are those rules that one applies by analyzing the structure of a specified statement: The premise or premises of analytical rules are correctness formulas of sub-statements of the statement of the conclusion. Thus the number of analytical rules one may apply in any correctness proof of a statement is bounded by the size of the statement. Adaptation can be applied on any statement, and have exactly one correctness formula as premise. So, given a derivation in the proof system 
, we have that between every two successive applications of analytical rules there is a (possibly empty) sequence of adaptation rule applications.
denotes an application of the CONSEQUENCE rule,
denotes an application of the SUBSTITUTION rule,
denotes an application of the INVARIANCE rule, and
denotes an application of the 
-INTRODUCTION rule.
denotes an application of the CONSEQUENCE rule,
denotes an application of the SUBSTITUTION rule,
denotes an application of the INVARIANCE rule, and
denotes an application of the 
-INTRODUCTION rule.
, where 
denotes choice, and 
is Kleene’s star with respect to concatenation. Two such sequences are equivalent if their application to any correctness formula yields the same correctness formula. We will introduce a rewrite system by means of which any sequence in 
can be reduced to a equivalent normal form represented by the regular expression
where the juxtaposition of expressions is concatenation, and 
is the usual notation of optional acceptance, i.e., 
for any regular expression 
and the empty string 
. The regular expression (7) describes the empty sequence or non-empty sequences that consist of at most one application of the INVARIANCE followed by at most one application of the SUBSTITUTION rule that in turn is followed by a single application of the CONSEQUENCE rule or a single application of the 
-INTRODUCTION rule possibly preceded or followed by a single application of the CONSEQUENCE rule. Examples of such expressions are 
, 
, 
, 
. For technical convenience, to avoid trivial applications of the CONSEQUENCE rule, we assume below some basic logical equivalences in the specification of the correctness formulas.
, where 
denotes choice, and 
is Kleene’s star with respect to concatenation. Two such sequences are equivalent if their application to any correctness formula yields the same correctness formula. We will introduce a rewrite system by means of which any sequence in 
can be reduced to a equivalent normal form represented by the regular expression
is the usual notation of optional acceptance, i.e., 
for any regular expression 
and the empty string 
. The regular expression (7) describes the empty sequence or non-empty sequences that consist of at most one application of the INVARIANCE followed by at most one application of the SUBSTITUTION rule that in turn is followed by a single application of the CONSEQUENCE rule or a single application of the 
-INTRODUCTION rule possibly preceded or followed by a single application of the CONSEQUENCE rule. Examples of such expressions are 
, 
, 
, 
. For technical convenience, to avoid trivial applications of the CONSEQUENCE rule, we assume below some basic logical equivalences in the specification of the correctness formulas.
, for any 
.
, for any 
.
denotes the substitution with domain consisting of the variables of 
and those variables of 
that are not among 
such that
if 
does not appear in 
,
if 
and 
denote the same variable,
if 
does not appear in 
.
denotes the substitution with domain consisting of the variables of 
and those variables of 
that are not among 
such that
if 
does not appear in 
,
if 
and 
denote the same variable,
if 
does not appear in 
.
-INTRODUCTION rule, we have that two consecutive applications
-INTRODUCTION rule, we have that two consecutive applications
and 
are identical.)
and 
are identical.)
: A proof pattern
: A proof pattern
: By the rewrite rule 
(shown below) it suffices to show that a proof pattern
: A proof pattern
: A proof pattern
is a sequence of fresh variables of the same length as 
. In the SUBSTITUTION rule, we apply the (simultaneous) substitution 
. Note that 
equals 
(
do not appear free in 
) and 
equals 
.
is a sequence of fresh variables of the same length as 
. In the SUBSTITUTION rule, we apply the (simultaneous) substitution 
. Note that 
equals 
(
do not appear free in 
) and 
equals 
.
: By the rewrite rule 
(shown below) it suffices to show that a proof pattern
-INTRODUCTION rule followed by one application of the INVARIANCE rule, can be transformed into a pattern 
:
-INTRODUCTION rule followed by one application of the INVARIANCE rule, can be transformed into a pattern 
:
is a sequence of fresh variables of the same length as 
, and in the application of the SUBSTITUTION rule we apply the substitution 
. Note that in the application of the 
-INTRODUCTION rule we assume the logical equivalence between 
and 
, which holds, because 
does not appear in 
.
is a sequence of fresh variables of the same length as 
, and in the application of the SUBSTITUTION rule we apply the substitution 
. Note that in the application of the 
-INTRODUCTION rule we assume the logical equivalence between 
and 
, which holds, because 
does not appear in 
.
-INTRODUCTION rule, d by an application of the SUBSTITUTION rule.
: A proof pattern
: A proof pattern
-INTRODUCTION rule, d by an application of the SUBSTITUTION rule.
: A proof pattern
: A proof pattern
-INTRODUCTION rule followed by one of the SUBSTITUTION rule, can be transformed in the reverse pattern
-INTRODUCTION rule followed by one of the SUBSTITUTION rule, can be transformed in the reverse pattern
and 
are disjoint (note that we can simply remove the overlapping variables from the substitution 
) and 
and 
are disjoint (by an alphabetic conversion of the existentially quantified variables 
), and thus 
is logically equivalent to 
.
and 
are disjoint (note that we can simply remove the overlapping variables from the substitution 
) and 
and 
are disjoint (by an alphabetic conversion of the existentially quantified variables 
), and thus 
is logically equivalent to 
.
-INTRODUCTION rules do not allow a simple reversal of the ordering as above. This is because, on the one hand, the CONSEQUENCE rule may enable an application of the 
-INTRODUCTION rule by generating a postcondition that does not contain free occurrences of the quantified variable. However, the 
-INTRODUCTION may enable an application of the CONSEQUENCE rule by weakening the precondition. However, these dependencies can be unravelled by the following rewrite rule.
: A proof pattern
-INTRODUCTION rules do not allow a simple reversal of the ordering as above. This is because, on the one hand, the CONSEQUENCE rule may enable an application of the 
-INTRODUCTION rule by generating a postcondition that does not contain free occurrences of the quantified variable. However, the 
-INTRODUCTION may enable an application of the CONSEQUENCE rule by weakening the precondition. However, these dependencies can be unravelled by the following rewrite rule.
: A proof pattern
and 
are disjoint)
and 
are disjoint)
and 
in this single application of the SUBSTITUTION rule, because the above pattern 
ensures that the variables of 
do not appear free in 
and that the variables 
do not appear free in 
. But validity of 
implies that we may assume without loss of generality that 
also does not contain free occurrences of 
. Further, note that validity of 
implies that of 
.
and 
in this single application of the SUBSTITUTION rule, because the above pattern 
ensures that the variables of 
do not appear free in 
and that the variables 
do not appear free in 
. But validity of 
implies that we may assume without loss of generality that 
also does not contain free occurrences of 
. Further, note that validity of 
implies that of 
.
can be reduced to a equivalent normal form it thus suffices to show that the rewrite system terminates.
can be reduced to a equivalent normal form it thus suffices to show that the rewrite system terminates.
an element of a well-founded ordering that (strictly) decreases with each application of a rewrite rule. Relevant parameters to consider are
an element of a well-founded ordering that (strictly) decreases with each application of a rewrite rule. Relevant parameters to consider are
, 
, 
and 
,
, 
, 
and 
,
the number of preceding occurrences of 
, 
and 
,
the number of preceding occurrences of 
, 
and 
,
the number of preceding occurrences of 
and 
.
the number of preceding occurrences of 
and 
.
and 
increases the number of occurrences of 
and 
, and as such these rules will in general lead to an increase of the above second and third parameters. Therefore, we single out the two parameters that record for each occurrence of 
the number of preceding occurrences of 
and the number of occurrences of 
itself. To ensure each application of a rewrite rule causes an overall decrease, we use pairs of natural numbers, ordered lexicographically, that is, 
if 
, or 
and 
, and associate with each sequence in 
a pair 
such that 
sums up
and 
increases the number of occurrences of 
and 
, and as such these rules will in general lead to an increase of the above second and third parameters. Therefore, we single out the two parameters that record for each occurrence of 
the number of preceding occurrences of 
and the number of occurrences of 
itself. To ensure each application of a rewrite rule causes an overall decrease, we use pairs of natural numbers, ordered lexicographically, that is, 
if 
, or 
and 
, and associate with each sequence in 
a pair 
such that 
sums up
,
,
the number of preceding occurrences of 
,
the number of preceding occurrences of 
,
sums up
sums up
, 
an 
,
, 
an 
,
the number of preceding occurrences of 
and 
,
the number of preceding occurrences of 
and 
,
the number of preceding occurrences of 
and 
.
the number of preceding occurrences of 
and 
.
. Clearly the number of occurrences of 
preceding the occurrence of 
to which this rewrite rule is applied decreases. It further does not affect the other parameters. So it decreases the above 
component, which causes an overall decrease, because the above 
component is unaffected. As another example consider the rule 
. Since this rule generates a new 
, it may increase the above 
component. However, the number of occurrences of 
preceding the occurrence of 
to which this rewrite rule is applied decreases, and as such it decreases the above 
component (which thus causes an overall decrease). A similar argument applies to the rule 
: The increase of the number of occurrences of 
is compensated by the decrease of the number of occurrences of 
.
. Clearly the number of occurrences of 
preceding the occurrence of 
to which this rewrite rule is applied decreases. It further does not affect the other parameters. So it decreases the above 
component, which causes an overall decrease, because the above 
component is unaffected. As another example consider the rule 
. Since this rule generates a new 
, it may increase the above 
component. However, the number of occurrences of 
preceding the occurrence of 
to which this rewrite rule is applied decreases, and as such it decreases the above 
component (which thus causes an overall decrease). A similar argument applies to the rule 
: The increase of the number of occurrences of 
is compensated by the decrease of the number of occurrences of 
.
there exists a unique normal form.
there exists a unique normal form.
, and 
range over 
, and (overlapping) redexes) be indicated by underlining/overlining. For all pairs 
and 
of redexes of two letters, we obtain the critical pair 
: It thus suffices to analyze for each redex of two letters all critical pairs obtained by either adding one letter after or adding one before. For the single redex 
consisting of three letters, it suffices to analyze 
, which is the single way it can overlap with itself, and analyze the remaining critical pairs 
and 
for 
in 
. This analysis is covered by the following cases (in some cases below the transitive closure 
abstracts from the order of applications of rewrite rules that do not have overlapping redexes).
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
, and 
range over 
, and (overlapping) redexes) be indicated by underlining/overlining. For all pairs 
and 
of redexes of two letters, we obtain the critical pair 
: It thus suffices to analyze for each redex of two letters all critical pairs obtained by either adding one letter after or adding one before. For the single redex 
consisting of three letters, it suffices to analyze 
, which is the single way it can overlap with itself, and analyze the remaining critical pairs 
and 
for 
in 
. This analysis is covered by the following cases (in some cases below the transitive closure 
abstracts from the order of applications of rewrite rules that do not have overlapping redexes).
is convergent, for 
:
is convergent, for 
:
to the first redex or the second one, both give 
.
to the first redex or the second one, both give 
.
and 
are convergent, where 
and 
, or 
and 
:
and 
are convergent, where 
and 
, or 
and 
:
to the first redex of 
, gives
to the first redex of 
, gives
.
to the second redex of 
, gives
to the second redex of 
, gives
.
to the first redex of 
, gives
to the first redex of 
, gives
.
to the second redex of 
, gives
to the second redex of 
, gives
.
is convergent:
is convergent:
to the first redex, gives
to the first redex, gives
.
to the second redex, gives
to the second redex, gives
.
is convergent:
is convergent:
to the first redex, gives
to the first redex, gives
.
to the second redex, gives
to the second redex, gives
.
is convergent:
is convergent:
to the first redex, gives
to the first redex, gives
.
to the second redex, gives
to the second redex, gives
.
is convergent:
is convergent:
to the first redex, gives
to the first redex, gives
.
the second redex, gives
the second redex, gives
is convergent:
is convergent:
the first redex, gives
the first redex, gives
to the second redex, gives
to the second redex, gives
.
is convergent:
is convergent:
to the first redex, gives
to the first redex, gives
.
to the second redex, gives
to the second redex, gives
.
is convergent:
is convergent:
to the first redex, gives
to the first redex, gives
.
to the second redex, gives
to the second redex, gives
.
is convergent:
is convergent:
to the first redex, gives
to the first redex, gives
.
to the second redex, gives
to the second redex, gives
.
, move 
to the front and collapse all consecutive 
applications.
, move 
to the front and collapse all consecutive 
applications.
, move 
to the front and collapse all consecutive 
applications.
, move 
to the front and collapse all consecutive 
applications.
, first collapse all consecutive 
applications to a single 
, and all consecutive 
applications to a single 
. Then we repeatedly apply the rewrite rule 
and collapse the possibly generated consecutive 
applications until at most one 
application is left (with possibly one 
before and possibly one 
after it).
, first collapse all consecutive 
applications to a single 
, and all consecutive 
applications to a single 
. Then we repeatedly apply the rewrite rule 
and collapse the possibly generated consecutive 
applications until at most one 
application is left (with possibly one 
before and possibly one 
after it).
, denote by
the existence of a proof of 
in 
from the assumptions 
that consists of at most 
applications of axioms and proof rules.
, denote by
in 
from the assumptions 
that consists of at most 
applications of axioms and proof rules.
. Then 
, where 
.
. Then 
, where 
.
applications of analytical axioms and rules, and between two analytical rules, or between an analytical rule and an assumption or an axiom application, we have an arbitrary sequence of adaptations. The latter can be reduced to a sequence of at most five rule applications. Thus the total number of axiom and rule applications needed in a proof is at most 
.□
applications of analytical axioms and rules, and between two analytical rules, or between an analytical rule and an assumption or an axiom application, we have an arbitrary sequence of adaptations. The latter can be reduced to a sequence of at most five rule applications. Thus the total number of axiom and rule applications needed in a proof is at most 
.□
the existence of a proof of 
in 
that consists of at most 
applications of axioms and proof rules.
the existence of a proof of 
in 
that consists of at most 
applications of axioms and proof rules.
and suppose that 
. Then 
, where 
is the length of 
seen as a string of symbols.
and suppose that 
. Then 
, where 
is the length of 
seen as a string of symbols.
was established using the RECURSION rule. By Lemma 5.1 to prove the premises of this rule, it takes at most 
steps, where 
are the bodies of the procedures declared in 
. Clearly, 
is less than the length of 
seen as a string of symbols.□
was established using the RECURSION rule. By Lemma 5.1 to prove the premises of this rule, it takes at most 
steps, where 
are the bodies of the procedures declared in 
. Clearly, 
is less than the length of 
seen as a string of symbols.□
. We treat soundness of the block rule and the rule for procedure calls in the context of a set of declarations (soundness of the rules for the remaining statements are standard).
. We treat soundness of the block rule and the rule for procedure calls in the context of a set of declarations (soundness of the rules for the remaining statements are standard).
where 
. Then
. Then
.□
.□
where 
and 
. Then
and 
. Then
that abstracts from the actual implementation of the procedures as specified by 
. Note that in such a proof only information about the variables of 
is used (in the INVARIANCE, SUBSTITUTION and 
-INTRODUCTION rules). We therefore introduce the notation 
to denote that 
and for every 
we have 
. Note that 
implies that 
, for every statement 
. It also holds that 
, and 
for every 
th approximation of 
(see Definition 3.1). We use the relation 
between programs in the soundness proof below, since syntactic approximations do not add more variables or variables that may be changed.
that abstracts from the actual implementation of the procedures as specified by 
. Note that in such a proof only information about the variables of 
is used (in the INVARIANCE, SUBSTITUTION and 
-INTRODUCTION rules). We therefore introduce the notation 
to denote that 
and for every 
we have 
. Note that 
implies that 
, for every statement 
. It also holds that 
, and 
for every 
th approximation of 
(see Definition 3.1). We use the relation 
between programs in the soundness proof below, since syntactic approximations do not add more variables or variables that may be changed.
denote that 
, for every 
.
denote that 
, for every 
.
denotes that 
implies 
, for all 
.
)
)
implies 
.
, for every 
.□
, for every 
.□
and 
be such that 
, 
. Then
implies
and 
be such that 
, 
. Then
, if we show 
. For the latter, it suffices to show that 
, for 
. By the Approximation item of Lemma 3.2 this reduces to showing that 
, for every 
and 
. We prove this by induction on 
.
, if we show 
. For the latter, it suffices to show that 
, for 
. By the Approximation item of Lemma 3.2 this reduces to showing that 
, for every 
and 
. We prove this by induction on 
.
and that 
, for any assertions 
and 
.
and that 
, for any assertions 
and 
.
implies 
. Since we have the second premise 
and 
, the induction hypothesis implies 
by Definition 6.3. It is sufficient to show that the latter is equivalent to
By Definition 3.1, Corollary 3.6
, and 
, we have that
if and only if
for every 
. Observe that
holds by simplification and definition of 
. Further, we have that
since 
does not contain any procedure calls (thus allowing us to replace all declarations), and by the definition of 
and the Inlining item of Lemma 3.2. Thus we have established that
if and only if
implies 
. Since we have the second premise 
and 
, the induction hypothesis implies 
by Definition 6.3. It is sufficient to show that the latter is equivalent to
, and 
, we have that
. Observe that
. Further, we have that
does not contain any procedure calls (thus allowing us to replace all declarations), and by the definition of 
and the Inlining item of Lemma 3.2. Thus we have established that
is expressive (see Definition 3.8) and that all valid assertions can be used in proofs. To this end, following Gorelick [21], we introduce the most general correctness formulas. Given a set of declarations 
, in our setup these are contracts of the form
where
,
,
and 
are lists of fresh variables, of the same length as, respectively, 
and 
,
is the strongest postcondition given in Definition 3.7.
is expressive (see Definition 3.8) and that all valid assertions can be used in proofs. To this end, following Gorelick [21], we introduce the most general correctness formulas. Given a set of declarations 
, in our setup these are contracts of the form
,
,
and 
are lists of fresh variables, of the same length as, respectively, 
and 
,
is the strongest postcondition given in Definition 3.7.
is defined in terms of a strongest postcondition of the body 
in which the formal parameters are quantified out. This has to do with the way we model the call-by-value parameter mechanism by a general notion of local variables, whereas, as already mentioned, in Reference [21] the call-by-name parameter mechanism is used in combination with a specific notion of local variables that ensures static scoping semantically by variable renaming.
is defined in terms of a strongest postcondition of the body 
in which the formal parameters are quantified out. This has to do with the way we model the call-by-value parameter mechanism by a general notion of local variables, whereas, as already mentioned, in Reference [21] the call-by-name parameter mechanism is used in combination with a specific notion of local variables that ensures static scoping semantically by variable renaming.
that in the above postcondition denote the initial values of the formal parameters 
. The variables 
are used in the above postcondition to denote the initial values of the variables 
that could be changed by a call 
. In particular, note that 
and 
have no variables in common, because 
, where 
. In fact, it is important to note that the sets of variables listed in 
and 
are mutually disjoint.
that in the above postcondition denote the initial values of the formal parameters 
. The variables 
are used in the above postcondition to denote the initial values of the variables 
that could be changed by a call 
. In particular, note that 
and 
have no variables in common, because 
, where 
. In fact, it is important to note that the sets of variables listed in 
and 
are mutually disjoint.
encodes the semantics of a call 
, where 
is declared by 
. Note that since the sets of variables 
and 
are disjoint, 
equals 
. Further, since 
are used to denote in the postcondition the initial values of the variables 
, 
denotes in the postccondition the initial values of the actual parameters 
.
, where 
is declared by 
. Note that since the sets of variables 
and 
are disjoint, 
equals 
. Further, since 
are used to denote in the postcondition the initial values of the variables 
, 
denotes in the postccondition the initial values of the actual parameters 
.
be declared by 
. Further, let the lists of variables 
and 
be defined as above and let
be declared by 
. Further, let the lists of variables 
and 
be defined as above and let
where 
.
.
such that
and
.
such that
and
.
. Assume first that
Then, given that 
and 
, Corollary 3.3 allows us to derive the following chain of equalities:
. Assume first that
and 
, Corollary 3.3 allows us to derive the following chain of equalities:
that starts in the state 
with the final state 
and that corresponds to the above equalities.
that starts in the state 
with the final state 
and that corresponds to the above equalities.
.
and 
are fresh and that by the choice of 
we have 
:
,
,
, where 
.
and 
are fresh and that by the choice of 
we have 
:
,
,
, where 
.
, so by the definition of 
(this is an instance of the Simultaneous Substitution Lemma in the textbook [4, p. 50]) 
, i.e.,
This, item (a) above, the fact that the sets of variables listed in 
and 
are mutually disjoint, and the definitions of 
and 
justifies the following chain of equalities:
, so by the definition of 
(this is an instance of the Simultaneous Substitution Lemma in the textbook [4, p. 50]) 
, i.e.,
and 
are mutually disjoint, and the definitions of 
and 
justifies the following chain of equalities:
. Then the above observations and item (c) above justifies the following chain of equalities:
. Then the above observations and item (c) above justifies the following chain of equalities:
, where 
is declared by 
. Further, let the lists of variables 
and 
be defined as above and let
It follows that 
.
, where 
is declared by 
. Further, let the lists of variables 
and 
be defined as above and let
.
such that
By the above Theorem 7.1 it follows that
where 
. We are given that 
, so 
by the definition of 
. (This is again the contents of the Simultaneous Substitution Lemma in the textbook [4, p. 50].) We conclude by the assumption 
that 
.□
such that
. We are given that 
, so 
by the definition of 
. (This is again the contents of the Simultaneous Substitution Lemma in the textbook [4, p. 50].) We conclude by the assumption 
that 
.□
of a procedure call 
into an invariant
. The following corollary shows that any precondition 
logically implies its invariant transformation for some values of the variables 
and 
.
of a procedure call 
into an invariant
. The following corollary shows that any precondition 
logically implies its invariant transformation for some values of the variables 
and 
.
and 
be defined as above and let
Suppose that the variables listed in 
and 
do not appear in 
. Then
and 
be defined as above and let
and 
do not appear in 
. Then
such that 
. By assumption the variables listed in 
and 
do not occur in 
, so 
, where 
.
such that 
. By assumption the variables listed in 
and 
do not occur in 
, so 
, where 
.
, so 
. By the Simultaneous Substitution Lemma of Reference [4, p. 50] 
, i.e.,
, so 
. By the Simultaneous Substitution Lemma of Reference [4, p. 50] 
, i.e.,
we have
so
This shows that
and yields the conclusion by the definition of 
.□
we have
.□
the set of most general correctness formulas for all procedures declared in 
.
the set of most general correctness formulas for all procedures declared in 
.
. Then 
.
. Then 
.
, with two essential cases being different.
, with two essential cases being different.
. Let 
be some fresh variables corresponding to the local variables 
. Note that by the definition of 
,
So from the soundness of the INVARIANCE rule it follows that
Consequently, by the soundness of the CONSEQUENCE rule
because 
implies 
. From Corollary 3.6
it then follows that
By the induction hypothesis we obtain
An application of the BLOCK rule then gives
. Let 
be some fresh variables corresponding to the local variables 
. Note that by the definition of 
,
implies 
. From Corollary 3.6
it then follows that
and subsequently the CONSEQUENCE rule to replace 
by 
. This yields
Procedure calls. Suppose that 
, where 
is declared by 
.
and subsequently the CONSEQUENCE rule to replace 
by 
. This yields
, where 
is declared by 
.
and 
, we may assume these variables not appear in 
. By the choice of the list 
and 
none of them contains a variable from 
. So by the PROCEDURE CALL rule with the substitution 
, we obtain
and 
, we may assume these variables not appear in 
. By the choice of the list 
and 
none of them contains a variable from 
. So by the PROCEDURE CALL rule with the substitution 
, we obtain
and 
.
and 
.
and 
do not appear in 
or 
, so by the 
-INTRODUCTION rule
By Corollary 7.3
so we obtain the desired conclusion by the CONSEQUENCE rule.
and 
do not appear in 
or 
, so by the 
-INTRODUCTION rule
. To prove 
in CBV, we use the RECURSION rule with 
as the set of assumptions in the subsidiary proofs. Lemma 7.4 ensures the first premise. The remaining 
premises also follow by this lemma. Indeed, suppose
where 
.
. To prove 
in CBV, we use the RECURSION rule with 
as the set of assumptions in the subsidiary proofs. Lemma 7.4 ensures the first premise. The remaining 
premises also follow by this lemma. Indeed, suppose
.
. By the definition of the strongest postcondition
so
by the soundness of the CONSEQUENCE rule. Hence by Lemma 7.4
We now obtain 
by the RECURSION rule.□
. By the definition of the strongest postcondition
by the RECURSION rule.□
-INTRODUCTION rules are only used for the block statements and the procedure calls, we can lower the upper bound of Theorem 5.2 by
where 
denotes the number of assignments, block statements and iteration statements, 
denotes the number of block statements, and 
denotes the number of procedure calls.
-INTRODUCTION rules are only used for the block statements and the procedure calls, we can lower the upper bound of Theorem 5.2 by
denotes the number of assignments, block statements and iteration statements, 
denotes the number of block statements, and 
denotes the number of procedure calls.
and the assumption of the expressibility of the strongest postcondition. However, and this is where our approach crucially differs from, for example, References [34, 36], to capture essential syntactic notions like that of occurrences of free variables (this is required in the notion of freshness used in Theorem 7.1.) we introduce finitely-based functions and predicates as the semantic structures for expressions and assertions, as explained in more detail next.
and the assumption of the expressibility of the strongest postcondition. However, and this is where our approach crucially differs from, for example, References [34, 36], to capture essential syntactic notions like that of occurrences of free variables (this is required in the notion of freshness used in Theorem 7.1.) we introduce finitely-based functions and predicates as the semantic structures for expressions and assertions, as explained in more detail next.
from states to values together with an additional list of variables 
with the coincidence condition that for every 
such that 
we have 
. Similarly, an assertion consists of a set of states 
and a list of variables 
with the coincidence condition that for every 
such that 
we have 
iff 
. For assertion 
, we write 
to mean 
. The intuition is that the finite set of variables associated with an expression or assertion forms its basis: the semantic counterpart of the syntactical notion of free variable occurrences. Only the values assigned by a state to variables in its basis can influence an expression’s value or an assertion’s truth. Assertions are equal whenever their extension and basis are equal, regardless of the proof of the coincidence condition.5
from states to values together with an additional list of variables 
with the coincidence condition that for every 
such that 
we have 
. Similarly, an assertion consists of a set of states 
and a list of variables 
with the coincidence condition that for every 
such that 
we have 
iff 
. For assertion 
, we write 
to mean 
. The intuition is that the finite set of variables associated with an expression or assertion forms its basis: the semantic counterpart of the syntactical notion of free variable occurrences. Only the values assigned by a state to variables in its basis can influence an expression’s value or an assertion’s truth. Assertions are equal whenever their extension and basis are equal, regardless of the proof of the coincidence condition.5
and 
, the conjunction 
consists of the intersection of the states of 
and 
and as basis the union of the bases of 
and 
. Similarly, we can define the implication 
. For the substitution construct 
, we take an assertion 
and assignment 
that is an association of variables in 
to expressions in 
. Let 
be a state update replacing the values of variables 
by the corresponding value of 
. We define the set of states of the substitution 
as 
. The basis of the substitution construct is the basis of 
with variables in 
removed, together with the union of the bases of expressions in 
. Thus, if a variable occurs both in 
and in some expression in 
, then it is still in the basis of 
. The Simultaneous Substitution Lemma, i.e., 
if and only if 
, then can be verified already by definition. Finally, the existential quantification 
is formalized by the set of states 
and as basis, the basis of 
with all variables in 
removed.
and 
, the conjunction 
consists of the intersection of the states of 
and 
and as basis the union of the bases of 
and 
. Similarly, we can define the implication 
. For the substitution construct 
, we take an assertion 
and assignment 
that is an association of variables in 
to expressions in 
. Let 
be a state update replacing the values of variables 
by the corresponding value of 
. We define the set of states of the substitution 
as 
. The basis of the substitution construct is the basis of 
with variables in 
removed, together with the union of the bases of expressions in 
. Thus, if a variable occurs both in 
and in some expression in 
, then it is still in the basis of 
. The Simultaneous Substitution Lemma, i.e., 
if and only if 
, then can be verified already by definition. Finally, the existential quantification 
is formalized by the set of states 
and as basis, the basis of 
with all variables in 
removed.
statements, but does include a 
statement that is needed for Approximation part of Lemma 3.1. This modification does not reduce expressivity of the language, as it is well known that while loops can be encoded using (tail) recursion, but it simplifies the definition of, and proofs about, the semantics of programs.
statements, but does include a 
statement that is needed for Approximation part of Lemma 3.1. This modification does not reduce expressivity of the language, as it is well known that while loops can be encoded using (tail) recursion, but it simplifies the definition of, and proofs about, the semantics of programs.
is associated to a relation of states denoted by 
. This relation can also be treated as a function mapping states to a subset of states. We then have formally verified the properties of Lemma 3.1, Corollary 3.2, Lemma 3.3, and Corollary 3.4. Not all of these results are needed in Theorem 7.1, but their verification increases our confidence that the formalized semantics contains no error.
is associated to a relation of states denoted by 
. This relation can also be treated as a function mapping states to a subset of states. We then have formally verified the properties of Lemma 3.1, Corollary 3.2, Lemma 3.3, and Corollary 3.4. Not all of these results are needed in Theorem 7.1, but their verification increases our confidence that the formalized semantics contains no error.
and program 
, the strongest postcondition 
consists of an extension and a basis for which the coincidence condition holds. Its extension is defined by 
, and as its basis 
, we take the union of the set of variables occurring in the program and the basis of 
. The set of variables occurring in a program can be defined inductively by the structure of the program; it is the union of the bases of all expressions and all variables that occur in the program. Now, to show that the coincidence condition holds for the strongest postcondition, we need to show that for every state 
in its extension, any state 
obtained from 
in which variables not in the basis are possibly modified are also in the extension:
To show this property, it is sufficient to show a more general closure property on the meaning of programs. The following lemma establishes the latter property.
and program 
, the strongest postcondition 
consists of an extension and a basis for which the coincidence condition holds. Its extension is defined by 
, and as its basis 
, we take the union of the set of variables occurring in the program and the basis of 
. The set of variables occurring in a program can be defined inductively by the structure of the program; it is the union of the bases of all expressions and all variables that occur in the program. Now, to show that the coincidence condition holds for the strongest postcondition, we need to show that for every state 
in its extension, any state 
obtained from 
in which variables not in the basis are possibly modified are also in the extension:
such that every variable occurring in 
is also in 
, and given that 
and 
, then 
.
such that every variable occurring in 
is also in 
, and given that 
and 
, then 
.
, we mean a state, which has the value in 
for the variables in 
, and the value in 
otherwise. Intuitively, we can reconstruct a run backwards from a final state that simulates the original run of the program but with different values stored in non-essential variables.
, we mean a state, which has the value in 
for the variables in 
, and the value in 
otherwise. Intuitively, we can reconstruct a run backwards from a final state that simulates the original run of the program but with different values stored in non-essential variables.