## Proof rules for the Hoare calculus

In this section we turn to the task of giving a formal system for the verification of partial correctness assertions for while programs. Hoare’s proof system manipulates certain formulas, called Hoare formulas. The proof system is built up according to the traditions of logical calculi: it consists of a set of axioms together with a set of rules to derive conclusions from hypothesis. The axioms are themselves axiom schemata: the substitution of concrete elements in place of metavariables of the axioms render the concrete forms of the axioms. For example, if stands for the skip axiom, then is an instance of it. We defined an extended notion arithmetical expressions and logical formulas in the course of Section 1.3. Let and Form, respectively, stand for the sets of arithmetical expressions and first order formulas defined there. We define the set of Hoare formulae as follows.

Definition 35. Let P, . Let C be a program, then is a Hoare correctness formula. The set of Hoare correctness formulae are denoted by H, while gives the formulas of Hoare logic.

Now we present the axioms and rules of the Hoare calculus. The names next to the rules or axioms are the rule- or axiom names.

Definition 36.

In the consequence rule we denoted by the relation , where in the standard interpretation . In the next example we show in detail how to apply the Hoare rules as formal tools in proving a partial correctness assertion. We present the formal proof in a linear style rather than in a tree like form, we indicate by indices the order of deduction in the argument.

Example 37. Let C be . We intend to prove . As a loop invariant, we use the formula .

Definition 38. Let be a set of Hoare formulas, that is . We define inductively when a Hoare correctness formula is provable in the Hoare logic from . In notation .

1. , if

2. , if P is an axiom

3. , if is a rule and .

If we fix an interpretation, we can talk about the meaning of Hoare formulas. As before, assume that the base set of the interpretation is the set of natural numbers, function symbols like , , , etc., are interpreted as the usual functions on natural numbers, similar suppositions are made concerning the predicate symbols like , , , etc. For the sake of completeness, we give here the interpretation of terms and formulas. As before, let be an interpretation, where is the base set- in our case the set of natural numbers-, and is an interpretation of the constants, the and function- and predicate symbols. Let be a state, we denote by the state, which is the same as s except for the value at X, for which holds. Then the interpretation of terms is as follows:

Definition 39.

For a fixed interpretation , we denote by the function given by the expression . Now we can define the interpretation of formulas. Let A, B be subsets of some set S. Then should denote the set .

Definition 40.

We may also apply the notation instead of . is called the meaning of the predicate P under the interpretation . If is fixed, we simply write . As an abuse of notation we identify sets of states and their characteristic functions. Thus, may also stand for , where iff for a fixed interpretation . We say that P is true for the fixed interpretation , if for every . We may apply the notation , and , if , and are true, respectively.

The interpretation of a Hoare correctness formula is defined as follows.

Definition 41. Let be a Hoare correctness formula. Then the meaning of the formula is

which is , by Definition 22. We may write for , as well. We omit the superscripts , if the interpretation is fixed.

It is a natural question to ask whether our deductive system is sound and complete. The soundness of Hoare logic is an easy consequence of Theorem 28, we state it without repeating the proof. The only change is the presence of the assumption that the formulas in should hold in the interpretation .

Theorem 42. Let , let be an interpretation. Assume H is true in , if . Then

The case of the completeness assertion is somewhat more elaborate. First of all, observe that in rule the consequence depends on hypothesis two of which must be provable arithmetical formulas. But, by Gödel’s results, we know that there exist true formulas in usual first order arithmetic (Peano arithmetic) which are not provable. This already gives a boundary of provability in Hoare logic also. Besides this, there emerge other problems, too. Assume by some oracle we know about the truth values of the arithmetical formulas we use in our proofs. In the course of the proof of Theorem 30, for example, we encountered the necessity of finding an assertion i for which and hold, given that is true. This could be done by defining i as . In the case of Hoare logic, for pre- and postconditions of programs only assertions defined by first order Hoare formulas are allowed. Is it the case for every and program C that we can find a formula A such that is true iff implies . In general, the answer is no. But in the case of Peano arithmetic, we can find an affirmative answer, which the next section is about.
{"found_math": false, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "url": "https://gyires.inf.unideb.hu/GyBITT/15/ch01s07.html", "fetch_time": 1582714383000000000, "content_mime_type": "text/html", "warc_filename": "crawl-data/CC-MAIN-2020-10/segments/1581875146341.16/warc/CC-MAIN-20200226084902-20200226114902-00337.warc.gz", "warc_record_offset": 392051665, "warc_record_length": 4387, "token_count": 1112, "char_count": 5108, "score": 4.0, "int_score": 4, "crawl": "CC-MAIN-2020-10", "snapshot_type": "latest", "language": "en", "language_score": 0.8826953172683716, "file_path": "/sailhome/yjruan/project/latent-lm/data/processed/finemath-4plus/finemath-4plus/train-00046-of-00064.parquet"}