Gradual Exact Logic
Unifying Hoare Logic and Incorrectness Logic via Gradual Verification

Conrad Zimmerman [email protected] Northeastern UniversityBostonMAUSA and Jenna DiVincenzo [email protected] Purdue UniversityWest LafayetteINUSA

Abstract.

Previously, gradual verification has been developed using overapproximating logics such as Hoare logic. We show that the static verification component of gradual verification is also connected to underapproximating logics like incorrectness logic. To do this, we use a novel definition of gradual verification and a novel gradualization of exact logic (Maksimovic et al., 2023) which we call gradual exact logic. Further, we show that Hoare logic, incorrectness logic, and gradual verification can be defined in terms of gradual exact logic.

We hope that this connection can be used to develop tools and techniques that apply to both gradual verification and bug-finding. For example, we envision that techniques defined in terms of exact logic can be directly applied to verification, bug-finding, and gradual verification, using the principles of gradual typing (Garcia et al., 2016).

1. Overview

Incorrectness logic (O’Hearn, 2020) has been recently developed as a formal basis for “true bug-finding” and has been applied in industrial-strength tools (Le et al., 2022). Deductions in this logic prove reachability, which enables bug-finding tools to prove the existence of an invalid state while selectively exploring the possible paths.

At the same time, gradual verification (GV) (Bader et al., 2018) addresses the complexity of traditional static verification. Gradually verified programs may contain imprecise specifications—logical formulas annotated to indicate that they contain only a partial specification of behavior. A gradual verifier checks the imprecise specifications using static verification where it can and run-time checks (i.e. dynamic verification) elsewhere. These run-time checks can be exercised, e.g. with testing, giving the programmer confidence that their code will not enter a state that violates their partial specifications. Using gradual verification, programmers can incrementally verify a program, incrementally learn verification constructs, and safely guard unverified components.

More recent work (Zilberstein et al., 2023; Maksimovic et al., 2023; Lööw et al., 2024) has produced logics and tools that unify over-approximating (OX) logic, often used in verification, and under-approximating (UX) logics including IL. In this paper, we propose another unification of OX and UX logics that we derive using the principles of gradual verification. The resulting characterization of IL demonstrates a previously unexplored connection between GV and IL.

1.1. Hoare logic

A triple in Hoare logic (HL) (Hoare, 1969) is denoted $\{P\}~{}C~{}\{Q\}$ . ( $P,Q$ refer to logical specifications; $C$ refers to a program statement.) Semantically, the triple is valid if, for every state $\sigma\in P$ (i.e., $P$ is true of $\sigma$ ), when $\sigma\stackrel{{\scriptstyle C}}{{\to}}\sigma^{\prime}$ (i.e., executing $C$ results in $\sigma^{\prime}$ ), then $\sigma^{\prime}\in Q$ :

Thus HL is an overapproximating (OX) logic—the postcondition $Q$ overapproximates the states that are reachable from $P$ ; precisely, $Q\supseteq\{\sigma^{\prime}\mid\exists\sigma\in P:\sigma\overset{C}{\to}\sigma^{\prime}\}$ . HL is a formal foundation for program verification precisely because the postcondition is true in all ending states.

1.2. Incorrectness logic

A triple in incorrectness logic (IL) (O’Hearn, 2020) is denoted $[P]~{}C~{}[Q]$ ¹¹1IL triples often include a specification for error states, but we omit error handling to simplify the comparison with other logics.. Semantically, the triple is valid if, for every $\sigma^{\prime}\in Q$ , there is some $\sigma\in P$ such that $\sigma\overset{C}{\to}\sigma^{\prime}$ :

Thus IL is an underapproximating (UX) logic—the postcondition $Q$ underapproximates the states that are reachable from $P$ ; precisely, $Q\subseteq\{\sigma^{\prime}\mid\exists\sigma\in P:\sigma\overset{C}{\to}\sigma^{\prime}\}$ . Interpreting $Q$ as a specification of a bug, IL is a logic for finding bugs since a valid triple indicates that the bug is reachable.

1.3. Gradual verification

Gradual verification (GV) (Bader et al., 2018) reduces the burden of static verification by allowing incomplete (imprecise) specifications. A gradual verifier may make optimistic assumptions when verifying imprecisely-specified code. Typically, the final program is elaborated to check these assumptions at run-time. However, in this work we focus solely on the static verification component of GV so that we can compare its logic with HL and IL.

We denote imprecise triples by $\{\textnormal{{?}}\wedge P\}~{}C~{}\{Q\}$ . Intuitively, this triple is valid if there is some $P^{\prime}\Rightarrow P$ such that $\{P^{\prime}\}~{}C~{}\{Q\}$ is valid in HL. One can think of ? as representing the additional assumptions introduced by $P^{\prime}$ .

For example, the following imprecise triple is valid:

\{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\textnormal{{?}}}\wedge\top\}~{}x\coloneq x+1~{}\{x>0\}

This follows from the validity of

\{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}x\geq 0}\wedge\top\}~{}x\coloneq x+1~{}\{x>0\}.

That is, the postcondition is ensured when assuming $x\geq 0$ .

However, the assumptions must be plausible; formally, $P^{\prime}$ (and thus $P$ ) must be satisfiable (i.e., $P^{\prime}\not\equiv\bot$ ). Otherwise, all imprecise triples would be vacuously valid by taking $P^{\prime}\equiv\bot$ . With this in mind, GV can be stated as a reachability problem—semantically, $\{\textnormal{{?}}\wedge P\}~{}C~{}\{Q\}$ is valid if there exists some states $\sigma$ and $\sigma^{\prime}$ such that $\sigma\in P$ , $\sigma\overset{C}{\to}\sigma^{\prime}$ , and $\sigma^{\prime}\in Q$ :

By contrapositive, the triple is invalid (i.e., static verification will error) if it is never possible for $C$ to ensure $Q$ , given $P$ .

By comparing this diagram with those in §1.1 and §1.2, we can deduce that HL and IL triples are valid imprecise triples, except for vacuous cases where $P\equiv\bot$ in HL or $Q\equiv\bot$ in IL.

Our semantic definition of validity is equivalent to the previous definition which uses Hoare triples: Let $P^{\prime}$ be a formula that represents $\sigma$ as specifically as possible, then (intuitively) $\{P^{\prime}\}~{}C~{}\{Q\}$ is valid since $\sigma\overset{C}{\to}\sigma^{\prime}$ and $\sigma^{\prime}\in Q$ .

But, we can also define valid imprecise triples in terms of IL— $\{\textnormal{{?}}\wedge P\}~{}C~{}\{Q\}$ is valid if $[P]~{}C~{}[Q^{\prime}]$ is valid for some $Q^{\prime}\Rightarrow Q$ . In §2.5 we will prove these definitions equivalent.

2. Formal foundations

We will now sketch our formal definitions and results. See the appendices for the full statements and proofs.

(1)

We define gradual exact logic—a consistent lifting (Garcia et al., 2016) of exact logic (Maksimovic et al., 2023).
(2)

We show that HL, IL, and GV can be characterized by gradual exact logic.
(3)

We show that GV contains OX and UX deductions.
(4)

We show that, for imprecise specifications, GV can be equivalently defined using OX or UX logics.

2.1. Exact logic

Exact logic (EL) (Maksimovic et al., 2023) is the intersection of HL and IL: an EL triple $(P)~{}C~{}(Q)$ is valid if $\{P\}~{}C~{}\{Q\}$ and $[P]~{}C~{}[Q]$ are both valid. Deductions are thus exact—they can neither under- or overapproximate behavior (see Appendix E for rules).

2.2. Gradual exact logic

We further define gradual exact logic ( $\widetilde{\text{EL}}$ ) as a consistent lifting (Garcia et al., 2016) of EL.

First, some definitions: Formula denotes all formulas in FOL with arithmetic; we call these precise. SatFormula denotes all satisfiable formulas. An imprecise formula is of the form $\textnormal{{?}}\wedge P$ where $P\in\textsc{Formula}$ . A gradual formula $\widetilde{P}\in\widetilde{\textsc{F}}\textsc{ormula}$ can be either precise or imprecise.

The concretization $\gamma:\widetilde{\textsc{F}}\textsc{ormula}\to\mathcal{P}(\textsc{Formula})$ interprets a gradual formulas as sets of precise formulas:

\gamma(\textnormal{{?}}\wedge P)=\{P^{\prime}\in\textsc{SatFormula}\mid P^{\prime}\Rightarrow P\},\quad\gamma(P)=\{P\}

Let $\vdash(P)~{}C~{}(Q)$ denote a valid EL triple. Deductions in $\widetilde{\text{EL}}$ , denoted $\mathrel{\widetilde{\vdash}}(\widetilde{P})~{}C~{}(\widetilde{Q})$ , are defined as a consistent lifting of EL deductions (Section E.2):

\mathrel{\widetilde{\vdash}}(\widetilde{P})~{}C~{}(\widetilde{Q})\mathrel{\stackrel{{\scriptstyle\text{def}}}{{\iff}}}\vdash(P)~{}C~{}(Q)~{}\text{for some $P\in\gamma(\widetilde{P})$, $Q\in\gamma(\widetilde{Q})$}

2.3. Strongest postconditions

$\operatorname{sp}(P,C)$ denotes the strongest (WRT $\Rightarrow$ ) $Q$ for which $\{P\}~{}C~{}\{Q\}$ is valid (calculated as usual; see Section B.2). Strongest postconditions are related to HL, IL, and EL as follows:

	$\displaystyle\vdash\{P\}~{}C~{}\{Q\}$	$\displaystyle\iff\operatorname{sp}(P,C)\Rightarrow Q$
	$\displaystyle\vdash[P]~{}C~{}[Q]$	$\displaystyle\iff\operatorname{sp}(P,C)\Leftarrow Q$
	$\displaystyle\vdash(P)~{}C~{}(Q)$	$\displaystyle\iff\operatorname{sp}(P,C)\equiv Q$

2.4. HL and IL via $\widetilde{\text{EL}}$

We can characterize valid HL triples as $\widetilde{\text{EL}}$ triples where the postcondition is made imprecise. Assuming that $P\not\equiv\bot$ and $C$ terminates (in either of these cases $\{P\}~{}C~{}\{Q\}$ is vacuous), we have $P,Q,\operatorname{sp}(P,C)\in\textsc{SatFormula}$ and thus (Theorem 6)

	$\displaystyle\vdash\{P\}~{}C~{}\{Q\}$	$\displaystyle\iff\operatorname{sp}(P,C)\Rightarrow Q$
		$\displaystyle\iff\operatorname{sp}(P,C)\in\gamma(\textnormal{{?}}\wedge Q)$
		$\displaystyle\iff\mathrel{\widetilde{\vdash}}(P)~{}C~{}(\textnormal{{?}}\wedge Q).$

Likewise, we can characterize valid IL triples as $\widetilde{\text{EL}}$ triples where the precondition is made imprecise. Weakest preconditions are not always defined for IL (O’Hearn, 2020), however, we can reuse weakest preconditions for HL to witness the necessary formula (see Section B.3). Assuming $Q\not\equiv\bot$ (otherwise $[P]~{}C~{}[Q]$ is vacuous), we have (Theorem 7)

	$\displaystyle\vdash[P]~{}C~{}[Q]$	$\displaystyle\iff Q\Rightarrow\operatorname{sp}(P,C)$
		$\displaystyle\iff Q\equiv\operatorname{sp}(\operatorname{wp}(Q,C)\wedge P,C)$
		$\displaystyle\iff\vdash(P\wedge\operatorname{wp}(Q,C))~{}C~{}(Q)$
		$\displaystyle\iff\mathrel{\widetilde{\vdash}}(\textnormal{{?}}\wedge P)~{}C~{}(Q).$

2.5. GV via HL, $\widetilde{\text{EL}}$ , and IL

We can now give a precise definition of GV in terms of HL, as sketched in §1.3²²2Here we define GV more generally for all gradual preconditions, whereas in §1.3 we defined it for imprecise preconditions.. We denote valid GV triples as $\mathrel{\widetilde{\vdash}}\{\widetilde{P}\}~{}C~{}\{Q\}$ .

\mathrel{\widetilde{\vdash}}\{\widetilde{P}\}~{}C~{}\{Q\}\mathrel{\stackrel{{\scriptstyle\text{def}}}{{\iff}}}\vdash\{P\}~{}C~{}\{Q\}~{}\text{for some $P\in\gamma(\widetilde{P})$}

Using this definition and applying the characterization of HL from §2.4 to characterize GV in terms of EL:

\mathrel{\widetilde{\vdash}}\{\widetilde{P}\}~{}C~{}\{Q\}\iff\mathrel{\widetilde{\vdash}}(\widetilde{P})~{}C~{}(\textnormal{{?}}\wedge Q)

For sake of comparison, we can define $\widetilde{\text{IL}}$ as a lifting of IL, the same way we have lifted HL to GV.

\mathrel{\widetilde{\vdash}}[P]~{}C~{}[\widetilde{Q}]\mathrel{\stackrel{{\scriptstyle\text{def}}}{{\iff}}}\vdash[P]~{}C~{}[Q]~{}\text{for some $Q\in\gamma(\widetilde{Q})$}

But, in the case of imprecision this is equivalent to GV. We can see this using the characterization of IL given in §2.4:

	$\displaystyle\mathrel{\widetilde{\vdash}}[P]~{}C~{}[\textnormal{{?}}\wedge Q]$	$\displaystyle\iff\mathrel{\widetilde{\vdash}}(\textnormal{{?}}\wedge P)~{}C~{}(\textnormal{{?}}\wedge Q)$
		$\displaystyle\iff\mathrel{\widetilde{\vdash}}\{\textnormal{{?}}\wedge P\}~{}C~{}\{Q\}.$

Note: GV and $\widetilde{\text{IL}}$ differ on precise formulas— $\mathrel{\widetilde{\vdash}}[P]~{}C~{}[Q]$ is not equivalent to $\mathrel{\widetilde{\vdash}}\{P\}~{}C~{}\{Q\}$ . Also, we do not gradualize postconditions in HL or preconditions in IL because we can arbitrarily weaken these specifications already.

While verification of precise formulas is a key aspect of GV, this demonstrates that verification of imprecise formulas can be accomplished using IL, and moreover that GV, when verifying imprecisely-specified code, is proving an IL deduction. Finally, we can make precise our claim from §1.3 that both OX and UX deductions are valid in (the imprecise fragment of) GV. Assuming $P\not\equiv\bot$ , we have (immediate from definition of GV)

\vdash\{P\}~{}C~{}\{Q\}\implies\mathrel{\widetilde{\vdash}}\{\textnormal{{?}}\wedge P\}~{}C~{}\{Q\}.

Also, assuming $Q\not\equiv\bot$ , we have

	$\displaystyle\vdash[P]~{}C~{}[Q]$	$\displaystyle\implies\mathrel{\widetilde{\vdash}}(\textnormal{{?}}\wedge P)~{}C~{}(Q)$
		$\displaystyle\implies\mathrel{\widetilde{\vdash}}(\textnormal{{?}}\wedge P)~{}C~{}(\textnormal{{?}}\wedge Q)$
		$\displaystyle\implies\mathrel{\widetilde{\vdash}}\{\textnormal{{?}}\wedge P\}~{}C~{}\{Q\}.$

Thus GV (and $\widetilde{\text{EL}}$ ) represents the union of HL and IL, while EL represents the intersection.

3. Applications

GV and IL verifiers in practice operate quite similarly; for example, compare the core consume operation of Zimmerman et al. (2024) for a gradual verifier and of Lööw et al. (2024) for an IL verifier. Both types of verifiers make assumptions, including pruning paths, when establishing a postcondition. This work formalizes the connection between these methods of verification; in particular, gradual verification of imprecisely-specified code is equivalent to IL deductions. We hope that this will allow verifiers that already incorporate both OX and UX logics, for example Lööw et al. (2024), to be easily extended to GV.

Similarly, we hope our approach can be used as a framework for unifying techniques across static verification, GV, and bug-finding. For example, bi-abduction has been developed in OX logics (Calcagno et al., 2011), applied to UX verification (Lööw et al., 2024), and is related to GV (DiVincenzo, 2023). We expect that techniques like this could be developed in the context of an exact logic, and then their applications to OX, UX, and GV logics could be derived using AGT-style techniques (Garcia et al., 2016).

4. Caveats and future work

While we have proven the results described, we have done so only for a very restrictive language, and thus our results should be considered preliminary. In particular, we do not consider heaps, method calls, or loops. We expect our results extend to these constructs, but showing this will require significant work.

Our definition of GV differs from previous definitions (Bader et al., 2018; Wise et al., 2020; Zimmerman et al., 2024). Our novel definition more clearly demonstrates the connection with IL, and we believe it captures the essence of GV. However, this definition only considers static verification, and thus does not consider run-time assertions. We expect this could be added, and we have hopes that we may be able to model run-time assertions using an evidence-based calculus similar to that of gradual typing Garcia et al. (2016). In addition, further work is necessary to elucidate how the “gradual guarantees” (Garcia et al., 2016) affect the relation of GV to IL. In particular, the static gradual guarantee seems to prohibit arbitrarily dropping paths, which IL can do.

Finally, our work is (to our knowledge) the first to explore a gradualization of exact logic. It remains to be seen whether this is useful its own right. For example, if library developers write exact specifications, a gradual exact logic could be used to aid development of these specifications, similar to how GV aids OX verification. But significantly more work would be necessary for this.

5. Conclusion

We have demonstrated the similarities and differences of GV and IL. Specifically, the relation between IL deductions and $\widetilde{\text{EL}}$ deductions with imprecise preconditions shows that the notion of assumptions used in GV is equivalent to the consequence rule (and path pruning) in IL. We also have shown that GV with imprecise specifications is equivalent to IL. Furthermore, we have defined gradual exact logic and used this to formally compare IL, HL, and GV. While much work remains before it is widely applicable, we hope that this framework can be used to develop techniques that uniformly target all three methods of verification.

Acknowledgements.

We thank Devin Singh for his contributions to this work.

References

(1)
Bader et al. (2018) Johannes Bader, Jonathan Aldrich, and Éric Tanter. 2018. Gradual Program Verification. In Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings (Lecture Notes in Computer Science, Vol. 10747), Isil Dillig and Jens Palsberg (Eds.). Springer, 25–46. https://doi.org/10.1007/978-3-319-73721-8_2
Calcagno et al. (2011) Cristiano Calcagno, Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. 2011. Compositional Shape Analysis by Means of Bi-Abduction. J. ACM 58, 6, Article 26 (Dec. 2011), 66 pages. https://doi.org/10.1145/2049697.2049700
DiVincenzo (2023) Jenna Wise DiVincenzo. 2023. Gradual Verification of Recursive Heap Data Structures. Ph. D. Dissertation. Carnegie Mellon University.
Garcia et al. (2016) Ronald Garcia, Alison M. Clark, and Éric Tanter. 2016. Abstracting gradual typing. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, Rastislav Bodík and Rupak Majumdar (Eds.). ACM, 429–442. https://doi.org/10.1145/2837614.2837670
Hoare (1969) C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Programming. Commun. ACM 12, 10 (1969), 576–580. https://doi.org/10.1145/363235.363259
Le et al. (2022) Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, and Peter W. O’Hearn. 2022. Finding real bugs in big programs with incorrectness logic. Proc. ACM Program. Lang. 6, OOPSLA1 (2022), 1–27. https://doi.org/10.1145/3527325
Lööw et al. (2024) Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Petar Maksimovic, and Philippa Gardner. 2024. Compositional Symbolic Execution for Correctness and Incorrectness Reasoning. In 38th European Conference on Object-Oriented Programming, ECOOP 2024, September 16-20, 2024, Vienna, Austria (LIPIcs, Vol. 313), Jonathan Aldrich and Guido Salvaneschi (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 25:1–25:28. https://doi.org/10.4230/LIPICS.ECOOP.2024.25
Maksimovic et al. (2023) Petar Maksimovic, Caroline Cronjäger, Andreas Lööw, Julian Sutherland, and Philippa Gardner. 2023. Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding. In 37th European Conference on Object-Oriented Programming, ECOOP 2023, July 17-21, 2023, Seattle, Washington, United States (LIPIcs, Vol. 263), Karim Ali and Guido Salvaneschi (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 19:1–19:27. https://doi.org/10.4230/LIPICS.ECOOP.2023.19
O’Hearn (2020) Peter W. O’Hearn. 2020. Incorrectness logic. Proc. ACM Program. Lang. 4, POPL (2020), 10:1–10:32. https://doi.org/10.1145/3371078
Wise et al. (2020) Jenna Wise, Johannes Bader, Cameron Wong, Jonathan Aldrich, Éric Tanter, and Joshua Sunshine. 2020. Gradual verification of recursive heap data structures. Proc. ACM Program. Lang. 4, OOPSLA (2020), 228:1–228:28. https://doi.org/10.1145/3428296
Zilberstein et al. (2023) Noam Zilberstein, Derek Dreyer, and Alexandra Silva. 2023. Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning. Proc. ACM Program. Lang. 7, OOPSLA1 (2023), 522–550. https://doi.org/10.1145/3586045
Zimmerman et al. (2024) Conrad Zimmerman, Jenna DiVincenzo, and Jonathan Aldrich. 2024. Sound Gradual Verification with Symbolic Execution. Proc. ACM Program. Lang. 8, POPL (2024), 2547–2576. https://doi.org/10.1145/3632927

Appendix A Grammar

We define a basic language that includes mutable variables and conditionals. Note that we do not include while loops or functions; these constructs are left for future work.

	$\displaystyle\mathrm{Expr}\ni E~{}{\Coloneqq}~{}$	$\displaystyle n\mid\bot\mid\top\mid x\mid E\vee E\mid E\wedge E\mid$
		$\displaystyle E=E\mid E<E\mid\neg E$
	$\displaystyle\mathrm{Cmd}\ni C~{}{\Coloneqq}~{}$	$\displaystyle\textnormal{{skip}}\mid x\coloneq E\mid\textnormal{{if}}\ E\ \textnormal{{then}}\ C\ \textnormal{{else}}\ C\mid C;C$
	$\displaystyle\mathrm{Asrt}\ni P,Q,R~{}{\Coloneqq}~{}$	$\displaystyle E\mid\neg P\mid P\wedge P\mid P\vee P\mid\exists x\,P$

where $n\in\mathbb{Z}$ and $x$ a variable name.

We assume that programs are typed correctly; for example, expressions $E$ in $\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}$ will always evaluate to a boolean value.

Definition 0 (Implication).

$P\Rightarrow Q$ if all states that satisfy $P$ also satisfy $Q$ .

Note: we do not formalize states or the semantics of assertions; we assume that our logic is close enough to first-order logic and thus use FOL deductions to reason about assertions.

Note: We use ${\cdot}\Rightarrow{\cdot}$ to denote implication between formulas in first-order logic with booleans and arithmetic. ${\cdot}\implies{\cdot}$ denotes “if-then” in our metatheory.

Definition 0 (Equivalence of propositions).

$P\equiv Q$ denotes that $P$ and $Q$ are logically equivalent; that is,

P\equiv Q\mathrel{\stackrel{{\scriptstyle\text{def}}}{{\iff}}}P\Rightarrow Q~{}\text{and}~{}Q\Rightarrow P.

Throughout this paper, we assume that identity of propositions coincides with equivalence; that is, when we write an individual proposition, technically we are denoting the equivalence class that contains that proposition. For example, $\{\top,\bot\}=\{1=1,1=2\}$ .

Definition 0 (Replacement).

$P[x/E]$ denotes $P$ with all free occurrences of $x$ replaced by $E$ .

Definition 0.

$\operatorname{fv}(P)$ denotes the free variables in the assertion $P$ .

Definition 0.

$\operatorname{fv}(C)$ denotes all variables referenced or assigned in $C$ .

Definition 0.

$\operatorname{mod}(C)$ denotes all variables assigned in $C$ . Explicitly,

	$\displaystyle\operatorname{mod}(\textnormal{{skip}})$	$\displaystyle\coloneq\emptyset$
	$\displaystyle\operatorname{mod}(x\coloneq E)$	$\displaystyle\coloneq x$
	$\displaystyle\operatorname{mod}(C_{1};C_{2})$	$\displaystyle\coloneq\operatorname{mod}(C_{1})\cup\operatorname{mod}(C_{2})$
	$\displaystyle\operatorname{mod}(\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$	$\displaystyle\coloneq\operatorname{mod}(C_{1})\cup\operatorname{mod}(C_{2})$

Appendix B Predicate transformers

B.1. Weakest preconditions

Definition 0.

$P$ is the weakest precondition for a statement $C$ and postcondition $Q$ , denoted $\operatorname{wp}(C,Q)$ , if it is the weakest predicate (WRT $\Rightarrow$ ) that ensures that if a state satisfies $P$ , then after executing $C$ , $Q$ holds.

The following explicit calculations correspond to the previous definition (proved in Theorem 4):

	$\displaystyle\operatorname{wp}(\textnormal{{skip}},Q)=Q$
	$\displaystyle\operatorname{wp}(x\coloneq E,Q)=Q[x/E]$
	$\displaystyle\operatorname{wp}(C_{1};C_{2},Q)=\operatorname{wp}(C_{1},\operatorname{wp}(C_{2},Q))$
	$\displaystyle\operatorname{wp}(\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2},Q)=$
	$\displaystyle\quad(\operatorname{wp}(C_{1},Q)\wedge E)\vee(\operatorname{wp}(C_{2},Q)\wedge\neg E)$

Lemma 0 (Stronger postcondition).

If $Q\Rightarrow Q^{\prime}$ then
$\operatorname{wp}(C,Q)\Rightarrow\operatorname{wp}(C,Q^{\prime})$ .

Proof.

By induction on $C$ :

skip::

\operatorname{wp}(\textnormal{{skip}},Q)\equiv Q\Rightarrow Q^{\prime}\equiv\operatorname{wp}(\textnormal{{skip}},Q^{\prime})

$x\coloneq E$ ::

\operatorname{wp}(x\coloneq E,Q)\equiv Q[E/x]\Rightarrow Q^{\prime}[E/x]\equiv\operatorname{wp}(x\coloneq E,Q^{\prime})

$C_{1};C_{2}$ ::

(1):: $\operatorname{wp}(C_{2},Q)\Rightarrow\operatorname{wp}(C_{2},Q^{\prime})$ by induction
(2):: $\operatorname{wp}(C_{1},\operatorname{wp}(C_{2},Q))\Rightarrow\operatorname{wp}(C_{1},\operatorname{wp}(C_{2},Q^{\prime}))$ by induction using (1)
(3):: $\operatorname{wp}(C_{1};C_{2},Q)\Rightarrow\operatorname{wp}(C_{1};C_{2},Q^{\prime})$ by (2) and definition of $\operatorname{wp}$

$\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}$ ::

(1):

$\operatorname{wp}(C_{1},Q)\Rightarrow\operatorname{wp}(C_{1},Q^{\prime})$ by induction

(2):

$\operatorname{wp}(C_{2},Q)\Rightarrow\operatorname{wp}(C_{2},Q^{\prime})$ by induction

(3):

By (1) and (2)

	$\displaystyle(\operatorname{wp}(C_{1},Q)\wedge E)\vee(\operatorname{wp}(C_{2},Q)\wedge\neg E)$
	$\displaystyle\quad\Rightarrow(\operatorname{wp}(C_{1},Q^{\prime})\wedge E)\vee(\operatorname{wp}(C_{2},Q^{\prime})\wedge\neg E)$

(4):

By (3) and definition of $\operatorname{wp}$

	$\displaystyle\operatorname{wp}(\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2},Q)$
	$\displaystyle\quad\Rightarrow\operatorname{wp}(\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2},Q^{\prime})\qed$

B.2. Strongest postconditions

Definition 0.

$Q$ is the strongest postcondition for precondition $P$ and statement $C$ , denoted $\operatorname{sp}(P,C)$ , if it is the strongest predicate (WRT $\Rightarrow$ ) that ensures that if a state satisfies $P$ , then after executing $C$ , $Q$ holds.

The following explicit calculations correspond to the previous definition (proved in Theorem 8):

	$\displaystyle\operatorname{sp}(P,\textnormal{{skip}})=P$
	$\displaystyle\operatorname{sp}(P,x\coloneq E)=\exists v(x=E[x/v]\wedge P[x/v])$
	where $v\notin\operatorname{fv}(P)$
	$\displaystyle\operatorname{sp}(P,C_{1};C_{2})=\operatorname{sp}(\operatorname{sp}(P,C_{1}),C_{2})$
	$\displaystyle\operatorname{sp}(P,\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})=$
	$\displaystyle\quad\operatorname{sp}(P\wedge E,C_{1})\vee\operatorname{sp}(P\wedge\neg E,C_{2})$

Lemma 0 (Stronger precondition).

If $P\Rightarrow P^{\prime}$ then
$\operatorname{sp}(P,C)\Rightarrow\operatorname{sp}(P^{\prime},C)$ .

Proof.

By induction on $C$ :

skip::

$\operatorname{sp}(P,\textnormal{{skip}})\equiv P\Rightarrow P^{\prime}\equiv\operatorname{sp}(P^{\prime},\textnormal{{skip}})$ .

$x\coloneq E$ ::

Note that $P[x/v]\Rightarrow P^{\prime}[x/v]$ by logic. Then:

$\displaystyle\operatorname{sp}(P,x\coloneq E)$	$\displaystyle\equiv\exists v(x=E[x/v]\wedge P[x/v])$	defn $\operatorname{sp}$
	$\displaystyle\Rightarrow\exists v(x=E[x/v]\wedge P^{\prime}[x/v])$	logic
	$\displaystyle\equiv\operatorname{sp}(P^{\prime},x\coloneq E)$	defn $\operatorname{sp}$

$C_{1};C_{2}$ ::

(1):

$\operatorname{sp}(P,C_{1})\Rightarrow\operatorname{sp}(P^{\prime},C_{1})$ by induction

(2):

$\operatorname{sp}(\operatorname{sp}(P,C_{1}),C_{2})\Rightarrow\operatorname{sp}(\operatorname{sp}(P^{\prime},C_{1}),C_{2})$ by induction using (1)

(3):

By (2) and definition of $\operatorname{sp}$ ,

	$\displaystyle\operatorname{sp}(P,C_{1};C_{2})$	$\displaystyle\equiv\operatorname{sp}(\operatorname{sp}(P,C_{1}),C_{2})$
		$\displaystyle\Rightarrow\operatorname{sp}(\operatorname{sp}(P^{\prime},C_{1}),C_{2})$
		$\displaystyle\equiv\operatorname{sp}(P^{\prime},C_{1};C_{2})$

$\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}$ ::

(1):

$P\wedge E\Rightarrow P^{\prime}\wedge E$ by logic

(2):

$\operatorname{sp}(P\wedge E,C_{1})\Rightarrow\operatorname{sp}(P^{\prime}\wedge E,C_{1})$ by induction using (1)

(3):

$P\wedge\neg E\Rightarrow P^{\prime}\wedge\neg E$ by logic

(4):

$\operatorname{sp}(P\wedge\neg E,C_{2})\Rightarrow\operatorname{sp}(P^{\prime}\wedge\neg E,C_{2})$ by induction using (3)

(5):

	$\displaystyle\operatorname{sp}(P,\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$
	$\displaystyle\quad\equiv\operatorname{sp}(P\wedge E,C_{1})\vee\operatorname{sp}(P\wedge\neg E,C_{2})$	defn $\operatorname{sp}$
	$\displaystyle\quad\Rightarrow\operatorname{sp}(P^{\prime}\wedge E,C_{1})\vee\operatorname{sp}(P^{\prime}\wedge\neg E,C_{2})$	(2), (4), logic
	$\displaystyle\quad\equiv\operatorname{sp}(P^{\prime},\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$	defn $\operatorname{sp}$

Lemma 0.

$\operatorname{sp}(\bot,C)\equiv\bot$

Proof.

By induction on $C$ :

skip::

$\operatorname{sp}(\bot,\textnormal{{skip}})\equiv\bot$ by definition.

$x\coloneq E$ ::

$\operatorname{sp}(\bot,x\coloneq E)\equiv\exists v(x=E[x/v]\wedge\bot)\equiv\bot$ by logic.

$\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}$ ::

	$\displaystyle\operatorname{sp}(\bot,\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$
	$\displaystyle\quad\equiv\operatorname{sp}(\bot\wedge E,C_{1})\vee\operatorname{sp}(\bot\wedge\neg E,C_{2})$	defn $\operatorname{sp}$
	$\displaystyle\quad\equiv\operatorname{sp}(\bot,C_{1})\vee\operatorname{sp}(\bot,C_{2})$	logic
	$\displaystyle\quad\equiv\bot\vee\bot$	induction
	$\displaystyle\quad\equiv\bot$	logic

$C_{1};C_{2}$ ::

$\displaystyle\operatorname{sp}(\bot,C_{1};C_{2})$	$\displaystyle\equiv\operatorname{sp}(\operatorname{sp}(\bot,C_{1}),C_{2})$	defn $\operatorname{sp}$
	$\displaystyle\equiv\operatorname{sp}(\bot,C_{2})$	induction
	$\displaystyle\equiv\bot$	induction

Lemma 0.

$\operatorname{sp}(P,C)\equiv\bot\implies P\equiv\bot$

Note: for a more expressive language, we would also need termination for this to hold.

Proof.

By induction on $C$ :

skip::

$\bot\equiv\operatorname{sp}(P,\textnormal{{skip}})\equiv P$ by definition.

$x\coloneq E$ ::

(1):: $\bot\equiv\operatorname{sp}(P,x\coloneq E)$ by assumption
(2):: $\operatorname{sp}(P,x\coloneq E)\equiv\exists v(x=E[x/v]\wedge P[x/v])$
(3):: $\top\equiv\forall v(x\neq E[x/v]\vee\neg P[x/v])$ by logic using (1) and (2)
(4):: $\top\equiv\forall v\neg P[x/v]$ by logic using (3)

We prove this using a semantic argument (assuming standard Kripke semantics for FOL):

Let $\mathcal{M}$ be a model and $\mathsf{y}\in\lvert\mathcal{M}\rvert$ . By (3) we have $\mathcal{M}\vDash\forall v(x\neq E[x/v]\vee\neg P[x/v])$ , and thus $\mathcal{M}[v\mapsto\mathsf{y}]\vDash x\neq E[x/v]\vee\neg P[x/v]$ .

Let $\mathsf{z}=\llbracket E[x/v]\rrbracket_{\mathcal{M}[v\mapsto\mathsf{y}]}$ . Then we have $\mathcal{M}[v\mapsto\mathsf{y},x\mapsto\mathsf{z}]\nvDash x\neq E[x/v]$ .

Thus we have $\mathcal{M}[v\mapsto\mathsf{y},x\mapsto\mathsf{z}]\vDash\neg P[x/v]$ . Since $x\notin\operatorname{fv}(P[x/v])$ , we have $\mathcal{M}[v\mapsto\mathsf{y}]\vDash\neg P[x/v]$ . Thus we can conclude that $\mathcal{M}\vDash\forall v\neg P[x/v]$ .
(5):: $\top\equiv\neg P[x/v]\equiv\neg P$ by logic using (4) and since $v\notin\operatorname{fv}(P)$
(6):: $\bot\equiv P$ by logic using (5)

$C_{1};C_{2}$ :

(1):: $\bot\equiv\operatorname{sp}(P,C_{1};C_{2})$ by assumption
(2):: $\operatorname{sp}(P,C_{1};C_{2})\equiv\operatorname{sp}(\operatorname{sp}(P,C_{1}),C_{2})$ by definition
(3):: $\bot\equiv\operatorname{sp}(\operatorname{sp}(P,C_{1}),C_{2})$ by logic using (1) and (2)
(4):: $\bot\equiv\operatorname{sp}(P,C_{1})$ by induction using (3)
(5):: $\bot\equiv P$ by induction using (4)

[ $\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}$ ]

(1):: $\bot\equiv\operatorname{sp}(P,\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$ by assumption
(2):: $\operatorname{sp}(P,\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})\equiv\operatorname{sp}(P\wedge E,C_{1})\vee\operatorname{sp}(P\wedge\neg E,C_{2})$ by definition
(3):: $\bot\equiv\operatorname{sp}(P\wedge E,C_{1})\vee\operatorname{sp}(P\wedge\neg E,C_{2})$ by (1) and (2)
(4):: $\bot\equiv\operatorname{sp}(P\wedge E,C_{1})$ by logic using (3)
(5):: $\bot\equiv\operatorname{sp}(P\wedge\neg E,C_{2})$ by logic using (3)
(6):: $\bot\equiv P\wedge E$ by induction using (4)
(7):: $\bot\equiv P\wedge\neg E$ by induction using (5)
(8):: $\bot\equiv(P\wedge E)\vee(P\wedge\neg E)\equiv P\wedge(E\vee\neg E)\equiv P$ by logic using (6) and (7) ∎

Lemma 0.

If $P\in\textsc{SatFormula}$ then $\operatorname{sp}(P,C)\in\textsc{SatFormula}$ .

Proof.

We prove the contrapositive: assume $\operatorname{sp}(P,C)\notin\\ \textsc{SatFormula}$ , then $\operatorname{sp}(P,C)\equiv\bot$ , and thus by Lemma 6 $P\equiv\bot$ . Therefore $P\notin\textsc{SatFormula}$ . ∎

Lemma 0.

If $y\notin\operatorname{fv}(C)$ then $\operatorname{sp}(\exists y\,P,C)\equiv\exists y\operatorname{sp}(P,C)$ .

Proof.

By induction on $C$ :

skip::

$\operatorname{sp}(\exists y\,P,\textnormal{{skip}})\equiv\exists y\,P\equiv\exists y\,\operatorname{sp}(P,\textnormal{{skip}})$

$x\coloneq E$ ::

Assuming $y\not\equiv v$ ,

	$\displaystyle\operatorname{sp}(\exists y\,P,x\coloneq E)$
	$\displaystyle\quad\equiv\exists v(x=E[x/v]\wedge(\exists y\,P)[x/v])$	defn $\operatorname{sp}$
	$\displaystyle\quad\equiv\exists v(x=E[x/v]\wedge(\exists y\,P[x/v]))$	$\displaystyle y\not\equiv x\in\operatorname{fv}(x\coloneq E)$
	$\displaystyle\quad\equiv\exists y\exists v(x=E[x/v]\wedge P[x/v])$	$\displaystyle y\notin\operatorname{fv}(E[x/v])$
	$\displaystyle\quad\equiv\exists y\,\operatorname{sp}(P,x\coloneq E)$	defn $\operatorname{sp}$

$C_{1};C_{2}$ ::

$\displaystyle\operatorname{sp}(\exists y\,P,C_{1};C_{2})$	$\displaystyle\equiv\operatorname{sp}(\operatorname{sp}(\exists y\,P,C_{1}),C_{2})$	defn $\operatorname{sp}$
	$\displaystyle\equiv\operatorname{sp}(\exists y\,\operatorname{sp}(P,C_{1}),C_{2})$	induction
	$\displaystyle\equiv\exists y\,\operatorname{sp}(\operatorname{sp}(P,C_{1}),C_{2})$	induction
	$\displaystyle\equiv\exists y\,\operatorname{sp}(P,C_{1};C_{2})$	defn $\operatorname{sp}$

$\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}$ ::

	$\displaystyle\operatorname{sp}(\exists y\,P,\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$
	$\displaystyle\quad\equiv\operatorname{sp}((\exists y\,P)\wedge E,C_{1})\vee\operatorname{sp}((\exists y\,P)\wedge\neg E,C_{2})$	defn $\operatorname{sp}$
	$\displaystyle\quad\equiv\operatorname{sp}(\exists y(P\wedge E),C_{1})\vee\operatorname{sp}(\exists y(P\wedge\neg E),C_{2})$	$\displaystyle y\notin\operatorname{fv}(E)$
	$\displaystyle\quad\equiv(\exists y\,\operatorname{sp}(P\wedge E,C_{1}))\vee(\exists y\,\operatorname{sp}(P\wedge\neg E,C_{2}))$	induction
	$\displaystyle\quad\equiv\exists y(\operatorname{sp}(P\wedge E,C_{1})\vee\operatorname{sp}(P\wedge\neg E,C_{2}))$	logic
	$\displaystyle\quad\equiv\exists y\,\operatorname{sp}(P,\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$	defn $\operatorname{sp}$

Lemma 0.

$\operatorname{sp}(P_{1}\vee P_{2},C)\equiv\operatorname{sp}(P_{1},C)\vee\operatorname{sp}(P_{2},C)$

Proof.

By induction on $C$ :

skip::

$\operatorname{sp}(P_{1}\vee P_{2},\textnormal{{skip}})\equiv P_{1}\vee P_{2}\equiv\\ \operatorname{sp}(P_{1},\textnormal{{skip}})\vee\operatorname{sp}(P_{2},\textnormal{{skip}})$ .

$x\coloneq E$ ::

	$\displaystyle\operatorname{sp}(P_{1}\vee P_{2},x\coloneq E)$
	$\displaystyle\quad\equiv\exists v(x=E[x/v]\wedge(P_{1}\vee P_{2})[x/v])$	defn $\operatorname{sp}$
	$\displaystyle\quad\equiv\exists v(x=E[x/v]\wedge(P_{1}[x/v]\vee P_{2}[x/v]))$	subst.
	$\displaystyle\quad\equiv\exists v((x=E[x/v]\wedge P_{1}[x/v])~{}\vee$
	$\displaystyle\hskip 38.99998pt(x=E[x/v]\wedge P_{2}[x/v]))$	logic
	$\displaystyle\quad\equiv(\exists v(x=E[x/v]\wedge P_{1}[x/v]))~{}\vee$
	$\displaystyle\hskip 23.99997pt(\exists v(x=E[x/v]\wedge P_{2}[x/v]))$	logic
	$\displaystyle\quad\equiv\operatorname{sp}(P_{1},x\coloneq E)\vee\operatorname{sp}(P_{2},x\coloneq E)$	defn $\operatorname{sp}$

$C_{1};C_{2}$ ::

	$\displaystyle\operatorname{sp}(P_{1}\vee P_{2},C_{1};C_{2})$
	$\displaystyle\quad\equiv\operatorname{sp}(\operatorname{sp}(P_{1}\vee P_{2},C_{1}),C_{2})$	defn $\operatorname{sp}$
	$\displaystyle\quad\equiv\operatorname{sp}(\operatorname{sp}(P_{1},C_{1})\vee\operatorname{sp}(P_{2},C_{1}),C_{2})$	induction
	$\displaystyle\quad\equiv\operatorname{sp}(\operatorname{sp}(P_{1},C_{1}),C_{2})\vee\operatorname{sp}(\operatorname{sp}(P_{2},C_{1}),C_{2})$	induction
	$\displaystyle\quad\equiv\operatorname{sp}(P_{1},C_{1};C_{2})\vee\operatorname{sp}(P_{2},C_{1};C_{2})$	defn $\operatorname{sp}$

$\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}$ ::

\begin{array}[]{p{1em}rlp{1em}r}\lx@intercol\operatorname{sp}(P_{1}\vee P_{2},\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})\hfil\lx@intercol\\ &\equiv&\operatorname{sp}(E\wedge(P_{1}\vee P_{2}),C_{1})~{}\vee\\ &&\operatorname{sp}(\neg E\wedge(P_{1}\vee P_{2}),C_{2})&&\text{defn $\operatorname{sp}$}\\ &\equiv&\operatorname{sp}((E\wedge P_{1})\vee(E\wedge P_{2}),C_{1})~{}\vee\\ &&\operatorname{sp}((\neg E\wedge P_{1})\vee(\neg E\wedge P_{2}),C_{2})&&\text{logic}\\ &\equiv&\operatorname{sp}(E\wedge P_{1},C_{1})\vee\operatorname{sp}(E\wedge P_{2},C_{1})~{}\vee\\ &&\operatorname{sp}(\neg E\wedge P_{1},C_{2})\vee\operatorname{sp}(\neg E\wedge P_{2},C_{2})&&\text{\lx@cref{creftypecap~refnum}{lem:sp-disj}}\\ &\equiv&(\operatorname{sp}(E\wedge P_{1},C_{1})\vee\operatorname{sp}(\neg E\wedge P_{1},C_{2}))~{}\vee\\ &&(\operatorname{sp}(E\wedge P_{2},C_{1})\vee\operatorname{sp}(\neg E\wedge P_{2},C_{2}))&&\text{logic}\\ &\equiv&\operatorname{sp}(P_{1},\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})~{}\vee\\ &&\operatorname{sp}(P_{2},\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})&&\text{defn $\operatorname{sp}$}\end{array}\qed

Lemma 0 (Frame rule).

If $\operatorname{mod}(C)\cap\operatorname{fv}(P)=\emptyset$ then
$\operatorname{sp}(P\wedge R,C)\equiv P\wedge\operatorname{sp}(R,C)$ .

Proof.

By induction on $C$ :

skip::

$\operatorname{sp}(P\wedge R,\textnormal{{skip}})\equiv P\wedge R\equiv P\wedge\operatorname{sp}(R,\textnormal{{skip}})$

$x\coloneq E$ ::

Let $v\notin\operatorname{fv}(P)$ . Note that $x\in\operatorname{fv}(x\coloneq E)$ , thus from our assumptions $x\notin\operatorname{fv}(P)$ Then,

	$\displaystyle\operatorname{sp}(P\wedge R,x\coloneq E)$
	$\displaystyle\quad\equiv\exists v(x=E[x/v]\wedge P[x/v]\wedge R[x/v])$	defn $\operatorname{sp}$
	$\displaystyle\quad\equiv\exists v(x=E[x/v]\wedge P\wedge R[x/v])$	$x\notin\operatorname{fv}(P)$
	$\displaystyle\quad\equiv P\wedge\exists v(x=E[x/v]\wedge R[x/v])$	$v\notin\operatorname{fv}(P)$
	$\displaystyle\quad\equiv P\wedge\operatorname{sp}(R,x\coloneq E)$	defn $\operatorname{sp}$

$C_{1};C_{2}$ ::

Note that $x\notin\operatorname{mod}(C_{1};C_{2})$ thus $x\notin\operatorname{mod}(C_{1})$ and $x\ClassNoteNoLine{classname}{notetext}\operatorname{mod}(C_{2})$ . Then,

$\displaystyle\operatorname{sp}(P\wedge R,C_{1};C_{2})$	$\displaystyle\equiv\operatorname{sp}(\operatorname{sp}(P\wedge R,C_{1}),C_{2})$	defn $\operatorname{sp}$
	$\displaystyle\equiv\operatorname{sp}(P\wedge\operatorname{sp}(R,C_{1}),C_{2})$	induction
	$\displaystyle\equiv P\wedge\operatorname{sp}(\operatorname{sp}(R,C_{1}),C_{2})$	induction
	$\displaystyle\equiv P\wedge\operatorname{sp}(R,C_{1};C_{2})$	defn $\operatorname{sp}$

$\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}$ ::

Note that by assumption
$x\notin\operatorname{mod}(\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$ thus $x\notin\operatorname{mod}(C_{1})$ and $x\notin\operatorname{mod}(C_{2})$ . Then,

	$\displaystyle\operatorname{sp}(P\wedge R,\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$
	$\displaystyle\quad\equiv\operatorname{sp}(P\wedge R\wedge E,C_{1})\vee\operatorname{sp}(P\wedge R\wedge\neg E,C_{2})$	defn $\operatorname{sp}$
	$\displaystyle\quad\equiv(P\wedge\operatorname{sp}(R\wedge E,C_{1}))\vee(P\wedge\operatorname{sp}(R\wedge\neg E,C_{2}))$	ind.
	$\displaystyle\quad\equiv P\wedge(\operatorname{sp}(R\wedge E,C_{1})\vee\operatorname{sp}(R\wedge\neg E,C_{2}))$	logic
	$\displaystyle\quad\equiv P\wedge\operatorname{sp}(R,\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$	defn $\operatorname{sp}$

Lemma 0.

	$\displaystyle\operatorname{sp}(P\wedge E,\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$	$\displaystyle\equiv\operatorname{sp}(P\wedge E,C_{1})$
	$\displaystyle\operatorname{sp}(P\wedge\neg E,\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$	$\displaystyle\equiv\operatorname{sp}(P\wedge\neg E,C_{2})$

Proof.

	$\displaystyle\operatorname{sp}(P\wedge E,\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$
	$\displaystyle\quad\equiv\operatorname{sp}(P\wedge E\wedge E,C_{1})\vee\operatorname{sp}(P\wedge E\wedge\neg E,C_{2})$	defn $\operatorname{sp}$
	$\displaystyle\quad\equiv\operatorname{sp}(P\wedge E,C_{1})\vee\operatorname{sp}(\bot,C_{2})$	logic
	$\displaystyle\quad\equiv\operatorname{sp}(P\wedge E,C_{1})\vee\bot$
	$\displaystyle\quad\equiv\operatorname{sp}(P\wedge E,C_{1})$	logic

	$\displaystyle\operatorname{sp}(P\wedge\neg E,\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$
	$\displaystyle\quad\equiv\operatorname{sp}(P\wedge E\wedge\neg E,C_{1})\vee\operatorname{sp}(P\wedge\neg E\wedge\neg E,C_{2})$	defn sp
	$\displaystyle\quad\equiv\operatorname{sp}(\bot,C_{1})\vee\operatorname{sp}(P\wedge\neg E,C_{2})$	logic
	$\displaystyle\quad\equiv\bot\vee\operatorname{sp}(P\wedge\neg E,C_{2})$
	$\displaystyle\quad\equiv\operatorname{sp}(P\wedge\neg E,C_{2})$	logic ∎

B.3. Fixpoint

We can define a function $Q\mapsto\operatorname{sp}(\operatorname{wp}(C,Q),C)$ . We demonstrate that this function reaches a fixpoint.

Lemma 0.

$\operatorname{sp}(\operatorname{wp}(C,Q)\wedge P,C)\equiv Q\wedge\operatorname{sp}(P,C)$

Proof.

By induction on $C$ :

skip::

$\operatorname{sp}(\operatorname{wp}(\textnormal{{skip}},Q)\wedge P,\textnormal{{skip}})\equiv Q\wedge P\equiv\\ Q\wedge\operatorname{sp}(P,\textnormal{{skip}})$

$x\coloneq E$ ::

Let $v\notin\operatorname{fv}(Q)$ . Then,

	$\displaystyle\operatorname{sp}(\operatorname{wp}(x\coloneq E,Q)\wedge P,x\coloneq E)$
	$\displaystyle\quad\equiv\exists v(x=E[x/v]~{}\wedge$
	$\displaystyle\hskip 37.00002pt(\operatorname{wp}(x\coloneq E,Q)\wedge P)[x/v])$	defn $\operatorname{sp}$
	$\displaystyle\quad\equiv\exists v(x=E[x/v]\wedge(Q[x/E]\wedge P)[x/v])$	defn $\operatorname{wp}$
	$\displaystyle\quad\equiv\exists v(x=E[x/v]\wedge Q[x/E[x/v]]\wedge P[x/v])$	subst
	$\displaystyle\quad\equiv\exists v(x=E[x/v]\wedge Q[x/x]\wedge P[x/v])$	subst =
	$\displaystyle\quad\equiv\exists v(x=E[x/v]\wedge Q\wedge P[x/v])$	redundant
	$\displaystyle\quad\equiv Q\wedge(\exists v\,x=E[x/v]\wedge P[x/v])$	$\displaystyle v\notin\operatorname{fv}(Q)$
	$\displaystyle\quad\equiv Q\wedge\operatorname{sp}(P,x\coloneq E)$	defn $\operatorname{sp}$

$\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}$ ::

(1):

$Q\wedge\operatorname{sp}(P\wedge E,C_{1})\equiv\operatorname{sp}(\operatorname{wp}(C_{1},Q)\wedge P\wedge E,C_{1})$ by induction using $C_{1}$

(2):

$Q\wedge\operatorname{sp}(P\wedge\neg E,C_{2})\equiv\operatorname{sp}(\operatorname{wp}(C_{2},Q)\wedge P\wedge\neg E,C_{2})$ by induction using $C_{2}$

(3):

	$\displaystyle Q\wedge\operatorname{sp}(P,\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$
	$\displaystyle\quad\equiv Q\wedge(\operatorname{sp}(P\wedge E,C_{1})\vee\operatorname{sp}(P\wedge\neg E,C_{2}))$	defn $\operatorname{sp}$
	$\displaystyle\quad\equiv(Q\wedge\operatorname{sp}(P\wedge E,C_{1}))~{}\vee$
	$\displaystyle\hskip 23.50009pt(Q\wedge\operatorname{sp}(P\wedge\neg E,C_{2}))$	logic
	$\displaystyle\quad\equiv\operatorname{sp}(\operatorname{wp}(C_{1},Q)\wedge P\wedge E,C_{1})~{}\vee$
	$\displaystyle\hskip 21.00009pt\operatorname{sp}(\operatorname{wp}(C_{2},Q)\wedge P\wedge\neg E,C_{2})$	(1), (2)
	$\displaystyle\quad\equiv\operatorname{sp}(\operatorname{wp}(C_{1},Q)\wedge P\wedge E,$
	$\displaystyle\hskip 36.0001pt\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})~{}\vee$
	$\displaystyle\hskip 22.50003pt\operatorname{sp}(\operatorname{wp}(C_{2},Q)\wedge P\wedge\neg E,$
	$\displaystyle\hskip 36.0001pt\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$
	$\displaystyle\quad\equiv\operatorname{sp}(((\operatorname{wp}(C_{1},Q)\wedge E)~{}\vee$
	$\displaystyle\hskip 40.00006pt(\operatorname{wp}(C_{2},Q)\wedge\neg E))\wedge P,$
	$\displaystyle\hskip 38.00008pt\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$
	$\displaystyle\quad\equiv\operatorname{sp}(\operatorname{wp}(\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2},Q)\wedge P,$
	$\displaystyle\hskip 35.00005pt\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$	defn $\operatorname{wp}$

$C_{1};C_{2}$ ::

(1):: $\operatorname{wp}(C_{2},Q)\wedge\operatorname{sp}(P,C_{1})\equiv\operatorname{sp}(\operatorname{wp}(C_{1},\\ \operatorname{wp}(C_{2},Q))\wedge P,C_{1})$ by induction using $C_{1}$
(2):: $Q\wedge\operatorname{sp}(\operatorname{sp}(P,C_{1}),C_{2})\equiv\operatorname{sp}(\operatorname{wp}(C_{2},Q)\wedge\\ \operatorname{sp}(P,C_{1}),C_{2})$ by induction using $C_{2}$ . Then,

	$\displaystyle Q\wedge\operatorname{sp}(P,C_{1};C_{2})$
	$\displaystyle\quad\equiv Q\wedge\operatorname{sp}(\operatorname{sp}(P,C_{1}),C_{2})$	defn $\operatorname{sp}$
	$\displaystyle\quad\equiv\operatorname{sp}(\operatorname{wp}(C_{2},Q)\wedge\operatorname{sp}(P,C_{1}),C_{2})$	(2)
	$\displaystyle\quad\equiv\operatorname{sp}(\operatorname{sp}(\operatorname{wp}(C_{1},\operatorname{wp}(C_{2},Q))\wedge P,C_{1}),C_{2})$	(1)
	$\displaystyle\quad\equiv\operatorname{sp}(\operatorname{sp}(\operatorname{wp}(C_{1};C_{2},Q)\wedge P,C_{1}),C_{2})$	defn $\operatorname{wp}$
	$\displaystyle\quad\equiv\operatorname{sp}(\operatorname{wp}(C_{1};C_{2},Q)\wedge P,C_{1};C_{2})$	defn $\operatorname{sp}$

Lemma 0 (Fixpoint property).

If $Q\Rightarrow\operatorname{sp}(\top,C)$ then
$Q\equiv\operatorname{sp}(\operatorname{wp}(C,Q),C)$ .

Proof.

Immediate from Lemma 12, noting that $Q\equiv Q\wedge\operatorname{sp}(\top,C)$ in this case. ∎

Lemma 0.

If $Q\Rightarrow\operatorname{sp}(P,C)$ then $Q\equiv\operatorname{sp}(P\wedge\operatorname{wp}(C,Q),C)$ .

Proof.

	$\displaystyle Q$	$\displaystyle\equiv Q\wedge\operatorname{sp}(P,C)$	$\displaystyle Q\Rightarrow\operatorname{sp}(P,C)$
		$\displaystyle\equiv\operatorname{sp}(P\wedge\operatorname{wp}(C,Q),C)$

Appendix C Hoare logic

Hoare triples are denoted by $\vdash\{P\}~{}C~{}\{Q\}$ . Deductions in Hoare logic are characterized by the following rules:

{mathpar}\inferrule

[OX-Skip] ⊢{P} skip {P} \inferrule[OX-Assign] ⊢{P[x/E]} x :-E {P} \inferrule[OX-Seq] ⊢{P} C_1 {R}

⊢{R} C_2 {Q} ⊢{P} C_1; C_2 {Q} \inferrule[OX-If] ⊢{E ∧P} C_1 {Q}

⊢{¬E ∧P} C_2 {Q} ⊢{P} if E then C_1 else C_2 {Q} \inferrule[OX-Cons] P ⇒P’
⊢{P’} C {Q’}
Q’ ⇒Q ⊢{P} C {Q}

C.1. Weakest preconditions

Lemma 0.

If $\vdash\{P\}~{}C~{}\{Q\}$ then $P\Rightarrow\operatorname{wp}(C,Q)$ .

Proof.

By induction on the derivation of $\vdash\{P\}~{}C~{}\{Q\}$ :

OX-Skip::

(1):: $P\equiv Q$ by inversion
(2):: $P\equiv Q\equiv\operatorname{wp}(\textnormal{{skip}},Q)$ by definition

OX-Assign::

(1):: $P\equiv Q[E/x]$ by inversion
(2):: $P\equiv Q[E/x]\equiv\operatorname{wp}(x\coloneq E,Q)$ by definition

OX-Seq::

(1):

$\vdash\{P\}~{}C_{1}~{}\{R\}$ for some $R$ by inversion

(2):

$P\Rightarrow\operatorname{sp}(C_{1},R)$ by induction using (1)

(3):

$\vdash\{R\}~{}C_{2}~{}\{Q\}$ by inversion

(4):

$R\Rightarrow\operatorname{wp}(C_{2},Q)$ by induction using (3)

(5):

$\operatorname{wp}(C_{1},R)\Rightarrow\operatorname{wp}(C_{1},\operatorname{wp}(C_{2},Q))$ by Lemma 2 using (4)

(6):

By (4), (5), and definition of $\operatorname{wp}$ ,

	$\displaystyle P$	$\displaystyle\Rightarrow\operatorname{wp}(C_{1},R)$
		$\displaystyle\Rightarrow\operatorname{wp}(C_{1},\operatorname{wp}(C_{2},Q))$
		$\displaystyle\equiv\operatorname{wp}(C_{1};C_{2},Q)$

OX-If::

(1):

$\vdash\{E\wedge P\}~{}C_{1}~{}\{Q\}$ by inversion

(2):

$E\wedge P\Rightarrow\operatorname{wp}(C_{1},Q)$ by induction using (1)

(3):

$\vdash\{\neg E\wedge P\}~{}C_{2}~{}\{Q\}$ by inversion

(4):

$\neg E\wedge P\Rightarrow\operatorname{wp}(C_{2},Q)$ by induction using (3)

(5):

$\displaystyle P$	$\displaystyle\equiv(P\wedge E)\vee(P\wedge\neg E)$	logic
	$\displaystyle\Rightarrow(\operatorname{wp}(C_{1},Q)\wedge E)\vee(\operatorname{wp}(C_{2},Q)\wedge\neg E)$	(2) and (4)
	$\displaystyle\Rightarrow\operatorname{wp}(\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2},Q)$	defn $\operatorname{wp}$

OX-Cons::

(1):: $P\Rightarrow P^{\prime}$ for some $P^{\prime}$ by inversion
(2):: $Q^{\prime}\Rightarrow Q$ for some $Q^{\prime}$ by inversion
(3):: $\vdash\{P^{\prime}\}~{}C~{}\{Q^{\prime}\}$ by inversion
(4):: $P^{\prime}\Rightarrow\operatorname{wp}(C,Q^{\prime})$ by induction using (3)
(5):: $\operatorname{wp}(C,Q^{\prime})\Rightarrow\operatorname{wp}(C,Q)$ by Lemma 2 using (4)
(6):: $P\Rightarrow P^{\prime}\Rightarrow\operatorname{wp}(C,Q^{\prime})\Rightarrow\operatorname{wp}(C,Q)$ by (1), (4), and (5) ∎

Lemma 0.

$\vdash\{\operatorname{wp}(C,Q)\}~{}C~{}\{Q\}$

Proof.

By induction on $C$ :

skip::

$\operatorname{wp}(\textnormal{{skip}},Q)\equiv Q$ by definition; $\vdash(Q)~{}\textnormal{{skip}}~{}(Q)$ by OX-Skip.

$x\coloneq E$ ::

(1):: $\operatorname{wp}(x\coloneq E,Q)\equiv Q[x/E]$ by definition
(2):: $\vdash\{Q[x/E]\}~{}x\coloneq E~{}\{Q\}$ by OX-Assign using (1)

$C_{1};C_{2}$ ::

(1):: $\vdash\{\operatorname{wp}(C_{1},\operatorname{wp}(C_{2},Q))\}~{}C_{1}~{}\{\operatorname{wp}(C_{2},Q)\}$ by induction
(2):: $\vdash\{\operatorname{wp}(C_{2},Q)\}~{}C_{2}~{}\{Q\}$ by induction
(3):: $\vdash\{\operatorname{wp}(C_{1},\operatorname{wp}(C_{2},Q))\}~{}C_{1};C_{2}~{}\{Q\}$ by OX-Seq using (1) and (2)
(4):: $\operatorname{wp}(C_{1};C_{2},Q)\equiv\operatorname{wp}(C_{1},\operatorname{wp}(C_{2},Q))$ by definition
(5):: $\vdash\{\operatorname{wp}(C_{1};C_{2},Q)\}~{}C_{1};C_{2}~{}\{Q\}$ by (3) and (4)

$\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}$ ::

(1):: Let $P\equiv(\operatorname{wp}(C_{1},Q)\wedge E)\vee(\operatorname{wp}(C_{2},Q)\wedge\neg E)$
(2):: $\vdash\{\operatorname{wp}(C_{1},Q)\}~{}C_{1}~{}\{Q\}$ by induction
(3):: $P\wedge E\Rightarrow\operatorname{wp}(C_{1},Q)$ by logic
(4):: $\vdash\{P\wedge E\}~{}C_{1}~{}\{Q\}$ by OX-Cons using (2) and (3)
(5):: $\vdash\{\operatorname{wp}(C_{2},Q)\}~{}C_{2}~{}\{Q\}$ by induction
(6):: $P\wedge\neg E\Rightarrow\operatorname{wp}(C_{2},Q)$ by logic
(7):: $\vdash\{P\wedge\neg E\}~{}C_{2}~{}\{Q\}$ by OX-Cons using (5) and (6)
(8):: $\vdash\{P\}~{}\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}~{}\{Q\}$ by OX-If using (4) and (7)
(9):: $P\equiv\operatorname{wp}(\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2},Q)$ by (1) and definition of $\operatorname{wp}$
(10):: $\vdash\{\operatorname{wp}(\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})\}\\ \textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}\ \{Q\}$ by (8) and (9) ∎

Lemma 0.

If $P\Rightarrow\operatorname{wp}(C,Q)$ then $\vdash\{P\}~{}C~{}\{Q\}$ .

Proof.

By Lemma 2, $\vdash\{\operatorname{wp}(C,Q)\}~{}C~{}\{Q\}$ , thus by OX-Cons $\vdash\{P\}~{}C~{}\{Q\}$ . ∎

Theorem 4.

$P\Rightarrow\operatorname{wp}(C,Q)\iff\vdash\{P\}~{}C~{}\{Q\}$ .

Proof.

$\Longrightarrow$ : Lemma 3; $\Longleftarrow$ : Lemma 1. ∎

C.2. Strongest postconditions

Lemma 0.

If $\vdash\{P\}~{}C~{}\{Q\}$ then $\operatorname{sp}(P,C)\Rightarrow Q$ .

Proof.

By induction on $\vdash\{P\}~{}C~{}\{Q\}$ :

OX-Skip::

Then $P\equiv Q$ and $C\equiv\textnormal{{skip}}$ , thus
$\operatorname{sp}(P,\textnormal{{skip}})\equiv P\equiv Q$ .

OX-Assign::

Then $P\equiv Q[x/E]$ and $C\equiv x\coloneq E$ . Assuming $v\notin\operatorname{fv}(Q)$ :

	$\displaystyle\operatorname{sp}(Q[x/E],x\coloneq E)$
	$\displaystyle\quad\equiv\exists v(x=E[x/v]\wedge Q[x/E][x/v])$	defn
	$\displaystyle\quad\equiv\exists v(x=E[x/v]\wedge Q[x/E[x/v]))$	substitution
	$\displaystyle\quad\equiv\exists v(x=E[x/v]\wedge Q[x/x])$	subst. equality
	$\displaystyle\quad\equiv\exists v(x=E[x/v]\wedge Q)$	redundant
	$\displaystyle\quad\Rightarrow Q$	$\displaystyle v\notin\operatorname{fv}(Q)$

OX-Seq::

(1):: $C\equiv C_{1};C_{2}$ for some $C_{1},C_{2}$ by inversion
(2):: $\vdash\{P\}~{}C_{1}~{}\{R\}$ for some $R$ by inversion
(3):: $\vdash\{R\}~{}C_{2}~{}\{Q\}$ by inversion
(4):: $\operatorname{sp}(P,C_{1})\Rightarrow R$ by induction using (2)
(5):: $\operatorname{sp}(\operatorname{sp}(P,C_{1}),C_{2})\Rightarrow\operatorname{sp}(R,C_{2})$ by Lemma 4 using (4)
(6):: $\operatorname{sp}(R,C_{2})\Rightarrow Q$ by induction using (3)
(7):: $\operatorname{sp}(\operatorname{sp}(P,C_{1}),C_{2})\Rightarrow Q$ by (5) and (6)
(8):: $\operatorname{sp}(P,C)\equiv\operatorname{sp}(P,C_{1};C_{2})\Rightarrow Q$ by (1), (7), and definition of $\operatorname{sp}$

OX-If::

(1):: $C\equiv\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}$ for some $E,C_{1},C_{2}$ by inversion
(2):: $\vdash\{E\wedge P\}~{}C_{1}~{}\{Q\}$ by inversion
(3):: $\vdash\{\neg E\wedge P\}~{}C_{2}~{}\{Q\}$ by inversion
(4):: $\operatorname{sp}(E\wedge P,C_{1})\Rightarrow Q$ by induction using (2)
(5):: $\operatorname{sp}(\neg E\wedge P,C_{2})\Rightarrow Q$ by induction using (3)
(6):: $\operatorname{sp}(E\wedge P,C_{1})\vee\operatorname{sp}(\neg E\wedge P,C_{2})\Rightarrow Q$ by logic using (4) and (5)
(7):: $\operatorname{sp}(P,\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})\Rightarrow Q$ by (6) and definition of $\operatorname{sp}$

OX-Cons::

(1):: $P\Rightarrow P^{\prime}$ for some $P^{\prime}$ by inversion
(2):: $Q^{\prime}\Rightarrow Q$ for some $Q^{\prime}$ by inversion
(3):: $\vdash\{P^{\prime}\}~{}C~{}\{Q^{\prime}\}$ by inversion
(4):: $\operatorname{sp}(P,C)\Rightarrow\operatorname{sp}(P^{\prime},C)$ by Lemma 4 and (1)
(5):: $\operatorname{sp}(P^{\prime},C)\Rightarrow Q^{\prime}$ by induction using (3)
(6):: $\operatorname{sp}(P,C)\Rightarrow Q$ by (4), (5), and (2) ∎

Lemma 0.

$\vdash\{P\}~{}C~{}\{\operatorname{sp}(P,C)\}$

Proof.

By induction on $C$ :

skip::

(1):: $\vdash\{P\}~{}\textnormal{{skip}}~{}\{P\}$ by OX-Skip
(2):: $P\equiv\operatorname{sp}(P,\textnormal{{skip}})$ by OX-Skip
(3):: $\vdash\{P\}~{}\textnormal{{skip}}~{}\{\operatorname{sp}(P,\textnormal{{skip}})\}$ by OX-Cons using (1) and (2)

$x\coloneq E$ ::

(1):: Let $Q\equiv\exists v(x=E[x/v]\wedge P[x/v])$ where $v\notin\operatorname{fv}(P)$ .
(2):: $\vdash\{Q[E/x]\}~{}x\coloneq E~{}\{Q\}$ by OX-Assign
(3):: $P\Rightarrow\exists v(E=E[x/v]\wedge P[x/v])\equiv Q[x/E]$ by logic (witnessed by letting $v=x$ ).
(4):: $\vdash\{P\}~{}x\coloneq E~{}\{Q\}$ by OX-Cons using (2) and (3)
(5):: $\vdash\{P\}~{}x\coloneq E~{}\{\operatorname{sp}(P,x\coloneq E)\}$ by (1), (4), and definition of $\operatorname{sp}$

$C_{1};C_{2}$ ::

(1):: $\vdash\{P\}~{}C_{1}~{}\{\operatorname{sp}(P,C_{1})\}$ by induction
(2):: $\vdash\{\operatorname{sp}(P,C_{1})\}~{}C_{2}~{}\{\operatorname{sp}(\operatorname{sp}(P,C_{1}),C_{2})\}$ by induction
(3):: $\vdash\{P\}~{}C_{1};C_{2}~{}\{\operatorname{sp}(\operatorname{sp}(P,C_{1}),C_{2})\}$ by OX-Seq using (1) and (2)
(4):: $\operatorname{sp}(P,C_{1};C_{2})\equiv\operatorname{sp}(\operatorname{sp}(P,C_{1}),C_{2})$ by definition
(5):: $\vdash\{P\}~{}C_{1};C_{2}~{}\{\operatorname{sp}(P,C_{1};C_{2})\}$ by (3) and (4)

$\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}$ ::

(1):: $\vdash\{P\wedge E\}~{}C_{1}~{}\{\operatorname{sp}(P\wedge E,C_{1})\}$ by induction
(2):: $\vdash\{P\wedge\neg E\}~{}C_{2}~{}\{\operatorname{sp}(P\wedge\neg E,C_{2})\}$ by induction
(3):: $\vdash\{P\wedge E\}~{}C_{1}~{}\{\operatorname{sp}(P\wedge E,C_{1})\vee\operatorname{sp}(P\wedge\neg E,C_{2})\}$ by OX-Cons using (1)
(4):: $\vdash\{P\wedge\neg E\}~{}C_{2}~{}\{\operatorname{sp}(P\wedge E,C_{1})\vee\operatorname{sp}(P\wedge\neg E,C_{2})\}$ by OX-Cons using (2)
(5):: $\vdash\{P\}~{}\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}~{}\{\operatorname{sp}(P\wedge E,C_{1})\vee\operatorname{sp}(P\wedge\neg E,C_{2})\}$ by OX-If using (3) and (4)
(6):: $\vdash\{P\}~{}\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}\\ \{\operatorname{sp}(P,\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})\}$ by (5) and definition of $\operatorname{sp}$ ∎

Lemma 0.

If $\operatorname{sp}(P,C)\Rightarrow Q$ then $\vdash\{P\}~{}C~{}\{Q\}$ .

Proof.

Immediate from Lemma 6, applying OX-Cons. ∎

Theorem 8.

$\operatorname{sp}(P,C)\Rightarrow Q\iff\vdash\{P\}~{}C~{}\{Q\}$

Proof.

$\Longrightarrow$ : Lemma 7; $\Longleftarrow$ : Lemma 5 ∎

Appendix D Incorrectness logic

Incorrectness logic triples are denoted $\vdash[P]~{}C~{}[Q]$ . Deductions in incorrectness logic are defined as follows: {mathpar} \inferrule[UX-Skip] ⊢[P] skip [P] \inferrule[UX-Seq] ⊢[P] C_1 [Q]
⊢[Q] C_2 [R] ⊢[P] C_1; C_2 [R] \inferrule[UX-Assign] ⊢[P] x :-E [∃v (x = E[x/v] ∧P[x/v])] \inferrule[UX-IfThen] ⊢[E ∧P] C_1 [Q] ⊢[E ∧P] if E then C_1 else C_2 [Q] \inferrule[UX-IfElse] ⊢[¬E ∧P] C_2 [Q] ⊢[¬E ∧P] if E then C_1 else C_2 [Q]
\inferrule[UX-Cons] P’ ⇒P

⊢[P’] C [Q’]

Q ⇒Q’ ⊢[P] C [Q] \inferrule[UX-Disj] ⊢[P_1] C [Q_1]

⊢[P_2] C [Q_2] ⊢[P_1 ∨P_2] C [Q_1 ∨Q_2]

D.1. Strongest postconditions

Lemma 0.

$\vdash[P]~{}C~{}[\operatorname{sp}(P,C)]$

Proof.

By induction on $C$ :

skip::

By UX-Skip $\vdash[P]~{}\textnormal{{skip}}~{}[P]$ and $P\equiv\operatorname{sp}(P,\textnormal{{skip}})$ by definition.

$x\coloneq E$ ::

(1):: $\vdash[P]~{}x\coloneq E~{}[\exists v(x=E[x/v]\wedge P[x/v])]$ by UX-Assign
(2):: $\operatorname{sp}(P,x\coloneq E)\equiv\exists v(x=E[x/v]\wedge P[x/v])$ by definition of $\operatorname{sp}$
(3):: $\vdash[P]~{}x\coloneq E~{}[sp(P,x\coloneq E)]$ by (1) and (2)

$C_{1};C_{2}$ ::

(1):: $\vdash[P]~{}C_{1}~{}[\operatorname{sp}(P,C_{1})]$ by induction
(2):: $\vdash[\operatorname{sp}(P,C_{1})]~{}C_{2}~{}[\operatorname{sp}(\operatorname{sp}(P,C_{1}),C_{2})]$ by induction
(3):: $\vdash[P]~{}C_{1};C_{2}~{}[\operatorname{sp}(\operatorname{sp}(P,C_{1}),C_{2})]$ by UX-Seq using (1), (2)
(4):: $\operatorname{sp}(P,C_{1};C_{2})\equiv\operatorname{sp}(\operatorname{sp}(P,C_{1}),C_{2})$ by definition
(5):: $\vdash[P]~{}C_{1};C_{2}~{}[\operatorname{sp}(P,C_{1};C_{2})]$ by (3), (4)

$\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}$ ::

(1):: $\vdash[E\wedge P]~{}C_{1}~{}[\operatorname{sp}(E\wedge P,C_{1})]$ by induction
(2):: $\vdash[\neg E\wedge P]~{}C_{2}~{}[\operatorname{sp}(\neg E\wedge P,C_{2})]$ by induction
(3):: $\vdash[E\wedge P]~{}\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}~{}[\operatorname{sp}(E\wedge P,C_{1})]$ by UX-IfThen using (1)
(4):: $\vdash[\neg E\wedge P]~{}\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}~{}[\operatorname{sp}(\neg E\wedge P,C_{2})]$ by UX-IfElse using (2)
(5):: $\vdash[P]~{}\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}~{}[\operatorname{sp}(E\wedge P,C_{1})\vee\operatorname{sp}(\neg E\wedge P,C_{2})]$ by UX-Disj using (3) and (4)
(6):: $\operatorname{sp}(P,\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})\equiv\operatorname{sp}(E\wedge P,C_{1})\vee\operatorname{sp}(\neg E\wedge P,C_{2})$ by definition
(7):: $\vdash[P]~{}\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}\\ {}[\operatorname{sp}(P,\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})]$ by (5) and (6) ∎

Lemma 0.

If $Q\Rightarrow\operatorname{sp}(P,C)$ then $\vdash[P]~{}C~{}[Q]$ .

Proof.

Immediate from Lemma 1 and UX-Cons. ∎

Lemma 0.

If $\vdash[P]~{}C~{}[Q]$ then $Q\Rightarrow\operatorname{sp}(P,C)$ .

Proof.

By induction on the derivation $\vdash[P]~{}C~{}[Q]$ :

UX-Skip::

(1):: $Q\equiv P$ by inversion
(2):: $\operatorname{sp}(P,\textnormal{{skip}})\equiv P$ by definition
(3):: $Q\equiv\operatorname{sp}(P,\textnormal{{skip}})$ by (1) and (2)

UX-Assign::

(1):: $Q\equiv\exists v(x=E[x/v]\wedge P[x/v])$ by inversion
(2):: $\operatorname{sp}(P,x\coloneq E)\equiv\exists v(x=E[x/v]\wedge P[x/v])$ by definition
(3):: $Q\equiv\operatorname{sp}(P,x\coloneq E)$ by (1) and (2)

UX-Seq::

(1):

$\vdash[P]~{}C_{1}~{}[R]$ for some $R$ by inversion

(2):

$\vdash[R]~{}C_{2}~{}[Q]$ by inversion

(3):

$Q\Rightarrow\operatorname{sp}(R,C_{2})$ by induction using (2)

(4):

$R\Rightarrow\operatorname{sp}(P,C_{1})$ by induction using (1)

(5):

$\operatorname{sp}(R,C_{2})\Rightarrow\operatorname{sp}(\operatorname{sp}(P,C_{1}),C_{2})$ by Lemma 4 using (4)

(6):

$\displaystyle Q$	$\displaystyle\Rightarrow\operatorname{sp}(R,C_{2})$	(3)
	$\displaystyle\Rightarrow\operatorname{sp}(\operatorname{sp}(P,C_{1}),C_{2})$	(5)
	$\displaystyle\equiv\operatorname{sp}(P,C_{1};C_{2})$	defn $\operatorname{sp}$

UX-IfThen::

(1):

$C\equiv\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}$ for some $E,C_{1},C_{2}$ by inversion

(2):

$P\equiv E\wedge P^{\prime}$ for some $P^{\prime}$ by inversion

(3):

$\vdash[E\wedge P^{\prime}]~{}C_{1}~{}[Q]$ by inversion

(4):

$Q\Rightarrow\operatorname{sp}(E\wedge P^{\prime},C_{1})$ by induction using (3)

(5):

$\operatorname{sp}(E\wedge P^{\prime},C_{1})\equiv\operatorname{sp}(E\wedge P^{\prime},\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$ by Lemma 11

(6):

$\displaystyle Q$	$\displaystyle\Rightarrow\operatorname{sp}(E\wedge P^{\prime},C_{1})$	(4)
	$\displaystyle\equiv\operatorname{sp}(E\wedge P^{\prime},\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$	(5)
	$\displaystyle\equiv\operatorname{sp}(P,\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$	(2)

UX-IfElse::

(1):

$C\equiv\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}$ for some $E,C_{1},C_{2}$ by inversion

(2):

$P\equiv\neg E\wedge P^{\prime}$ for some $P^{\prime}$ by inversion

(3):

$\vdash[\neg E\wedge P^{\prime}]~{}C_{2}~{}[Q]$ by inversion

(4):

$Q\Rightarrow\operatorname{sp}(\neg E\wedge P^{\prime},C_{2})$ by induction using (3)

(5):

$\operatorname{sp}(\neg E\wedge P^{\prime},C_{2})\equiv\operatorname{sp}(\neg E\wedge P^{\prime},\\ \textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$ by Lemma 11

(6):

$\displaystyle Q$	$\displaystyle\Rightarrow\operatorname{sp}(\neg E\wedge P^{\prime},C_{2})$	(4)
	$\displaystyle\equiv\operatorname{sp}(\neg E\wedge P^{\prime},\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$	(5)
	$\displaystyle\equiv\operatorname{sp}(P,\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$	(2)

UX-Cons::

(1):: $\vdash[P^{\prime}]~{}C~{}[Q^{\prime}]$ for some $P^{\prime},Q^{\prime}$ by inversion
(2):: $P^{\prime}\Rightarrow P$ by inversion
(3):: $Q\Rightarrow Q^{\prime}$ by inversion
(4):: $Q^{\prime}\Rightarrow\operatorname{sp}(P^{\prime},C)$ by induction using (1)
(5):: $\operatorname{sp}(P^{\prime},C)\Rightarrow\operatorname{sp}(P,C)$ by Lemma 4 using (2)
(6):: $Q\Rightarrow Q^{\prime}\Rightarrow\operatorname{sp}(P^{\prime},C)\Rightarrow\operatorname{sp}(P,C)$ by (3), (4), and (5)

UX-Disj::

(1):

$\vdash[P_{1}]~{}C~{}[Q_{1}]$ for some $P_{1},Q_{1}$ by inversion

(2):

$\vdash[P_{2}]~{}C~{}[Q_{2}]$ for some $P_{2},Q_{2}$ by inversion

(3):

$P\equiv P_{1}\vee P_{2}$ by inversion

(4):

$Q\equiv Q_{1}\vee Q_{2}$ by inversion

(5):

$Q_{1}\Rightarrow\operatorname{sp}(P_{1},C)$ by induction using (1)

(6):

$Q_{2}\Rightarrow\operatorname{sp}(P_{2},C)$ by induction using (2)

(7):

$Q_{1}\vee Q_{2}\Rightarrow\operatorname{sp}(P_{1},C)\vee\operatorname{sp}(P_{2},C)$ by logic using (5) and (6)

(8):

$\displaystyle Q$	$\displaystyle\equiv Q_{1}\vee Q_{2}$	(4)
	$\displaystyle\Rightarrow\operatorname{sp}(P_{1},C)\vee\operatorname{sp}(P_{2},C)$	(7)
	$\displaystyle\equiv\operatorname{sp}(P_{1}\vee P_{2},C)$
	$\displaystyle\equiv\operatorname{sp}(P,C)$	(3)

Theorem 4.

$\vdash[P]~{}C~{}[Q]\iff Q\Rightarrow\operatorname{sp}(P,C)$

Proof.

$\Longrightarrow$ : Lemma 3; $\Longleftarrow$ : Lemma 2. ∎

D.2. Satisfiability

Lemma 0.

If $\vdash[\bot]~{}C~{}[Q]$ then $Q\equiv\bot$ .

Proof.

(1):: $Q\Rightarrow\operatorname{sp}(\bot,C)$ by Theorem 8
(2):: $\operatorname{sp}(\bot,C)\equiv\bot$ by Lemma 5
(3):: $Q\Rightarrow\bot$ logic using (1) and (2)
(4):: $Q\equiv\bot$ by logic using (3) ∎

Lemma 0.

If $\vdash[P]~{}C~{}[Q]$ and $Q\in\textsc{SatFormula}$ then $P\in\textsc{SatFormula}$ .

Proof.

Assume $\vdash[P]~{}C~{}[Q]$ , then we prove the contrapositive; that is, $P\notin\textsc{SatFormula}\implies Q\notin\textsc{SatFormula}$ .

Assuming $P\notin\textsc{SatFormula}$ , since $P\in\textsc{Formula}$ we get $P\equiv\bot$ , and thus $\vdash[\bot]~{}C~{}[Q]$ by assumption. Then by Lemma 5, $Q\equiv\bot$ thus $Q\notin\textsc{SatFormula}$ . ∎

Lemma 0.

If $\vdash[P]~{}C~{}[Q]$ and $Q\in\textsc{SatFormula}$ then $P\wedge\operatorname{wp}(P,C)\in\textsc{SatFormula}$ .

Proof.

(1):: $\vdash[P]~{}C~{}[Q]$ by assumption
(2):: $Q\in\textsc{SatFormula}$ by assumption
(3):: $Q\Rightarrow\operatorname{sp}(P,C)$ by Lemma 3 using (1)
(4):: $\operatorname{sp}(P\wedge\operatorname{wp}(P,C),C)\equiv Q$ by Lemma 14 using (3)
(5):: $\vdash[P\wedge\operatorname{wp}(P,C)]~{}C~{}[Q]$ by Lemma 2 using (4)
(6):: $P\wedge\operatorname{wp}(C,Q)\in\textsc{SatFormula}$ by Lemma 6 using (2) and (5) ∎

Appendix E Exact logic

Exact logic triples are denoted by $\vdash(P)~{}C~{}(Q)$ . Deductions in exact logic are characterized by the following rules: {mathpar} \inferrule[EX-Skip] ⊢(⊤) skip (⊤) \inferrule[EX-Assign] x ∉fv(E’) ⊢(x = E’) x :-E (x = E[x/E’])
\inferrule[EX-IfThen] ⊢(P ∧E) C_1 (Q) ⊢(P ∧E) if E then C_1 else C_2 (Q) \inferrule[EX-Seq] ⊢(P) C_1 (R)

⊢(R) C_2 (Q) ⊢(P) C_1; C_2 (Q)
\inferrule[EX-IfElse] ⊢(P ∧¬E) C_2 (Q) ⊢(P ∧¬E) if E then C_1 else C_2 (Q) \inferrule[EX-Frame] mod(C) ∩fv(R) = ∅

⊢(P) C (Q) ⊢(P ∧R) C (Q ∧R)
\inferrule[EX-Exists] ⊢(P) C (Q)

x ∉fv(C) ⊢(∃x P) C (∃x Q) \inferrule[EX-Disj] ⊢(P_1) C (Q_1)

⊢(P_2) C (Q_2) ⊢(P_1 ∨P_2) C (Q_1 ∨Q_2)

Note: We drop the equivalence rule, since it is immediately valid by our characterization of formulas by equivalence classes.

E.1. Strongest postconditions

Lemma 0.

$\vdash(P)~{}C~{}(\operatorname{sp}(P,C))$

Proof.

By induction on $C$ :

skip::

By EX-Skip $\vdash(P)~{}\textnormal{{skip}}~{}(P)$ and $P\equiv\operatorname{sp}(P,\textnormal{{skip}})$ by definition.

$C\equiv x\coloneq E$ ::

(1):

$P\equiv\exists y(x=y\wedge P^{\prime})$ for some $P^{\prime}$ since $\exists y(x=y)$ is a tautology. WLOG assume $x\notin\operatorname{fv}(P^{\prime})$ (instances of $x$ can be replaced with $y$ ).

(2):

$\vdash(x=y)~{}x\coloneq E~{}(x=E[x/y])$ by EX-Assign.

(3):

$\vdash(x=y\wedge P^{\prime})~{}x\coloneq E~{}(x=E[x/y]\wedge P^{\prime})$ by EX-Frame and (2).

(4):

$\vdash(\exists y(x=y\wedge P^{\prime}))~{}x\coloneq E~{}(\exists y(x=E[x/y]\wedge P^{\prime}))$ by EX-Exists and (3).

(5):

$\displaystyle\operatorname{sp}(P,x\coloneq E)$	$\displaystyle\equiv\exists v(x=E[x/v]\wedge P[x/v])$	defn
	$\displaystyle\equiv\exists v(x=E[x/v]\wedge(\exists y(v=y\wedge P^{\prime})))$	(1)
	$\displaystyle\equiv\exists y(x=E[x/y]\wedge P^{\prime})$	logic

(6):

$\vdash(P)~{}x\coloneq E~{}(\operatorname{sp}(P,x\coloneq E))$ by (1), (4), and (5).

$C_{1};C_{2}$ ::

(1):: $\vdash(P)~{}C~{}(\operatorname{sp}(P,C_{1}))$ by induction
(2):: $\vdash(\operatorname{sp}(P,C_{1}))~{}C_{2}~{}(\operatorname{sp}(\operatorname{sp}(P,C_{1}),C_{2}))$ by induction
(3):: $\vdash(P)~{}C_{1};C_{2}~{}(\operatorname{sp}(\operatorname{sp}(P,C_{1}),C_{2}))$ by EX-Seq using (1), (2)
(4):: $\operatorname{sp}(\operatorname{sp}(P,C_{1}),C_{2})\equiv\operatorname{sp}(P,C_{1};C_{2})$ by definition
(5):: $\vdash(P)~{}C_{1};C_{2}~{}(\operatorname{sp}(P,C_{1};C_{2}))$ by (3) and (4)

$\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}$ ::

(1):: $\vdash(P\wedge E)~{}C_{1}~{}(\operatorname{sp}(P\wedge E,C_{1}))$ by induction
(2):: $\vdash(P\wedge\neg E)~{}C_{2}~{}(\operatorname{sp}(P\wedge\neg E,C_{2}))$ by induction
(3):: $\vdash(P\wedge E)~{}\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}~{}(\operatorname{sp}(P\wedge E,C_{1}))$ by EX-IfThen using (1)
(4):: $\vdash(P\wedge\neg E)~{}\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}~{}(\operatorname{sp}(P\wedge\neg E,C_{2}))$ by EX-IfElse using (2)
(5):: $\vdash((P\wedge E)\vee(P\wedge\neg E))~{}\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}\\ (\operatorname{sp}(P\wedge E,C_{1})\vee\operatorname{sp}(P\wedge\neg E,C_{2}))$ by EX-Disj using (3), (4)
(6):: $(P\wedge E)\vee(P\wedge\neg E)\equiv P$ by logic
(7):: $\operatorname{sp}(P\wedge E,C_{1})\vee\operatorname{sp}(P\wedge\neg E,C_{2})\equiv\\ \operatorname{sp}(P,\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$ by definition
(8):: $\vdash(P)~{}\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}\\ (\operatorname{sp}(P,\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}))$ by (5), (6), and (7) ∎

Lemma 0.

If $\vdash(P)~{}C~{}(Q)$ then $Q\equiv\operatorname{sp}(P,C)$ .

Proof.

By induction on the derivation $\vdash(P)~{}C~{}(Q)$ :

EX-Skip::

By inversion $C\equiv\textnormal{{skip}}$ and $Q\equiv P$ , and by definition $\operatorname{sp}(P,\textnormal{{skip}})\equiv P$ . Thus $\operatorname{sp}(P,C)\equiv\operatorname{sp}(P,\textnormal{{skip}})\\ \equiv P\equiv Q$ .

EX-Assign::

(1):

$C\equiv x\coloneq E$ for some $x,E$ by inversion

(2):

$P\equiv x=E^{\prime}$ for some $E^{\prime}$ by inversion

(3):

$Q\equiv x=E[x/E^{\prime}]$ by inversion

(4):

$x\notin\operatorname{fv}(E^{\prime})$ by inversion

(5):

	$\displaystyle\operatorname{sp}(P,C)$
	$\displaystyle\quad\equiv\operatorname{sp}(x=E^{\prime},x\coloneq E)$	(1), (2)
	$\displaystyle\quad\equiv\exists v(x=E[x/v]\wedge(x=E^{\prime})[x/v])$	defn $\operatorname{sp}$
	$\displaystyle\quad\equiv\exists v(x=E[x/v]\wedge v=E^{\prime})$	(4)
	$\displaystyle\quad\equiv\exists v(x=E[x/E^{\prime}]\wedge v=E^{\prime})$	logic
	$\displaystyle\quad\equiv x=E[x/E^{\prime}]\wedge\exists v\,v=E^{\prime}$	(4)
	$\displaystyle\quad\equiv x=E[x/E^{\prime}]$	logic
	$\displaystyle\quad\equiv Q$	(3)

EX-IfThen::

(1):

$C\equiv\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}$ by inversion

(2):

$P\equiv P^{\prime}\wedge E$ for some $P^{\prime}$ by inversion

(3):

$\vdash(P^{\prime}\wedge E)~{}C_{1}~{}(Q)$ by inversion

(4):

$Q\equiv\operatorname{sp}(P^{\prime}\wedge E,C_{1})$ by induction using (3)

(5):

	$\displaystyle\operatorname{sp}(P,C)$
	$\displaystyle\quad\equiv\operatorname{sp}(P^{\prime}\wedge E,\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$	(1), (2)
	$\displaystyle\quad\equiv\operatorname{sp}(P^{\prime}\wedge E,C_{1})$
	$\displaystyle\quad\equiv Q$	(4)

EX-IfElse::

(1):

$C\equiv\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2}$ by inversion

(2):

$P\equiv P^{\prime}\wedge\neg E$ for some $P^{\prime}$ by inversion

(3):

$\vdash(P^{\prime}\wedge\neg E)~{}C_{2}~{}(Q)$ by inversion

(4):

$Q\equiv\operatorname{sp}(P^{\prime}\wedge\neg E,C_{2})$ by induction using (3)

(5):

	$\displaystyle\operatorname{sp}(P,C)$
	$\displaystyle\quad\equiv\operatorname{sp}(P^{\prime}\wedge\neg E,\textnormal{{if}}\ E\ \textnormal{{then}}\ C_{1}\ \textnormal{{else}}\ C_{2})$	(1), (2)
	$\displaystyle\quad\equiv\operatorname{sp}(P^{\prime}\wedge\neg E,C_{2})$
	$\displaystyle\quad\equiv Q$	(4)

EX-Seq::

(1):

$C\equiv C_{1};C_{2}$ for some $C_{1},C_{2}$ by inversion

(2):

$\vdash(P)~{}C_{1}~{}(R)$ for some $R$ by inversion

(3):

$\vdash(R)~{}C_{2}~{}(Q)$ by inversion

(4):

$R\equiv\operatorname{sp}(P,C_{1})$ by induction using (2)

(5):

$Q\equiv\operatorname{sp}(R,C_{2})$ by induction using (3)

(6):

$\displaystyle\operatorname{sp}(P,C)$	$\displaystyle\equiv\operatorname{sp}(P,C_{1};C_{2})$	(1)
	$\displaystyle\equiv\operatorname{sp}(\operatorname{sp}(P,C_{1}),C_{2})$	defn $\operatorname{sp}$
	$\displaystyle\equiv\operatorname{sp}(R,C_{2})$	(4)
	$\displaystyle\equiv Q$	(5)

EX-Exists::

(1):

$P\equiv\exists x\,P^{\prime}$ for some $P^{\prime}$ by inversion

(2):

$Q\equiv\exists x\,Q^{\prime}$ for some $Q^{\prime}$ by inversion

(3):

$\vdash(P^{\prime})~{}C~{}(Q^{\prime})$ by inversion

(4):

$x\notin\operatorname{fv}(C)$ by inversion

(5):

$Q^{\prime}\equiv\operatorname{sp}(P^{\prime},C)$ by induction using (3)

(6):

$\displaystyle\operatorname{sp}(P,C)$	$\displaystyle\equiv\operatorname{sp}(\exists x\,P^{\prime},C)$	(2)
	$\displaystyle\equiv\exists x\,\operatorname{sp}(P^{\prime},C)$
	$\displaystyle\equiv\exists x\,Q^{\prime}$	(5)
	$\displaystyle\equiv Q$	(2)

EX-Disj::

(1):

$P\equiv P_{1}\vee P_{2}$ for some $P_{1},P_{2}$ by inversion

(2):

$Q\equiv Q_{1}\vee Q_{2}$ for some $Q_{1},Q_{2}$ by inversion

(3):

$\vdash(P_{1})~{}C~{}(Q_{1})$ by inversion

(4):

$\vdash(P_{2})~{}C~{}(Q_{2})$ by inversion

(5):

$Q_{1}\equiv\operatorname{sp}(P_{1},C)$ by induction using (3)

(6):

$Q_{2}\equiv\operatorname{sp}(P_{2},C)$ by induction using (4)

(7):

$\displaystyle\operatorname{sp}(P,C)$	$\displaystyle\equiv\operatorname{sp}(P_{1}\vee P_{2},C)$	(1)
	$\displaystyle\equiv\operatorname{sp}(P_{1},C)\vee\operatorname{sp}(P_{2},C)$
	$\displaystyle\equiv Q_{1}\vee Q_{2}$	(5), (6)
	$\displaystyle\equiv Q$	(2)

EX-Frame::

(1):

$P\equiv P^{\prime}\wedge R$ for some $P^{\prime},R$ by inversion

(2):

$Q\equiv Q^{\prime}\wedge R$ for some $Q^{\prime}$ by inversion

(3):

$\operatorname{mod}(C)\cap\operatorname{fv}(R)=\emptyset$ by inversion

(4):

$\vdash(P^{\prime})~{}C~{}(Q^{\prime})$ by inversion

(5):

$\operatorname{sp}(P^{\prime},C)\equiv Q$ by induction using (4)

(6):

$\operatorname{sp}(P^{\prime}\wedge R,C)\equiv R\wedge\operatorname{sp}(P^{\prime},C)$ by Lemma 10 using (3)

(7):

$\displaystyle\operatorname{sp}(P,C)$	$\displaystyle\equiv\operatorname{sp}(P^{\prime}\wedge R,C)$	(1)
	$\displaystyle\equiv R\wedge\operatorname{sp}(P^{\prime},C)$	(6)
	$\displaystyle\equiv R\wedge Q^{\prime}$	(5)
	$\displaystyle\equiv Q$	(2)

Theorem 3.

$\vdash(P)~{}C~{}(Q)\iff Q\equiv\operatorname{sp}(P,C)$

Proof.

$\Longrightarrow$ : Lemma 2; $\Longleftarrow$ : Lemma 1 ∎

E.2. Gradual exact logic

Valid triples in gradual exact logic are denoted $\mathrel{\widetilde{\vdash}}(\widetilde{P})~{}C~{}(\widetilde{Q})$ .

Definition 0.

The concretization $\gamma:\widetilde{\textsc{F}}\textsc{ormula}\to\\ \mathcal{P}(\textsc{Formula})$ maps a gradual formula to the set of all formulas it can represent:

	$\displaystyle\gamma(P)$	$\displaystyle\coloneq\{P\}$
	$\displaystyle\gamma(\textnormal{{?}}\wedge P)$	$\displaystyle\coloneq\{P^{\prime}\in\textsc{SatFormula}\mid P^{\prime}\Rightarrow P\}$

Definition 0.

Deductions in gradual exact logic directly are lifted deductions in exact logic:

	$\displaystyle\mathrel{\widetilde{\vdash}}(\widetilde{P})~{}C~{}(\widetilde{Q})\mathrel{\stackrel{{\scriptstyle\text{def}}}{{\iff}}}\vdash(P)~{}C~{}(Q)$
	for some $P\in\gamma(\widetilde{P})$ and $Q\in\gamma(\widetilde{Q})$

Theorem 6.

For $P\in\textsc{SatFormula}$ ,

\mathrel{\widetilde{\vdash}}(P)~{}C~{}(\textnormal{{?}}\wedge Q)\iff\vdash\{P\}~{}C~{}\{Q\}.

That is, except for the vacuous case where $P\equiv\bot$ , gradualizing the postcondition exactly characterizes deductions in Hoare logic.

Proof.

$\Longrightarrow$ :

(1):: $\mathrel{\widetilde{\vdash}}(P)~{}C~{}(\textnormal{{?}}\wedge Q)$ by assumptino
(2):: $\vdash(P)~{}C~{}(Q^{\prime})$ for some $Q^{\prime}\in\gamma(\textnormal{{?}}\wedge Q)$ by (1)
(3):: $\operatorname{sp}(P,C)\equiv Q^{\prime}$ by Lemma 2 using (2)
(4):: $Q^{\prime}\Rightarrow Q$ by definition of $\gamma$ and (2)
(5):: $\operatorname{sp}(P,C)\Rightarrow Q$ by (3) and (4)
(6):: $\vdash\{P\}~{}C~{}\{Q\}$ by Lemma 7 using (5)

$\Longleftarrow$ :

(1):: $\vdash\{P\}~{}C~{}\{Q\}$ by assumption
(2):: $P\in\textsc{SatFormula}$ by assumption
(3):: $\operatorname{sp}(P,C)\Rightarrow Q$ by Lemma 5 using (1)
(4):: $\operatorname{sp}(P,C)\in\textsc{SatFormula}$ by Lemma 7 using (2)
(5):: $\operatorname{sp}(P,C)\in\gamma(\textnormal{{?}}\wedge Q)$ by definition of $\gamma$ using (3) and (4)
(6):: $\vdash(P)~{}C~{}(\operatorname{sp}(P,C))$ by Lemma 1
(7):: $\mathrel{\widetilde{\vdash}}(P)~{}C~{}(\textnormal{{?}}\wedge Q)$ by definition using (5) and (6) ∎

Theorem 7.

If $Q\in\textsc{SatFormula}$ ,

\mathrel{\widetilde{\vdash}}(\textnormal{{?}}\wedge P)~{}C~{}(Q)\iff\vdash[P]~{}C~{}[Q]

That is, except in the vacuous case where $Q\equiv\bot$ , gradualizing the precondition exactly characterizes deductions in incorrectness logic.

Proof.

$\Longrightarrow$ :

(1):: $\mathrel{\widetilde{\vdash}}(\textnormal{{?}}\wedge P)~{}C~{}(Q)$ by assumption
(2):: $\vdash(P^{\prime})~{}C~{}(Q)$ for some $P^{\prime}\in\gamma(\textnormal{{?}}\wedge P)$ by definition using (1)
(3):: $P^{\prime}\Rightarrow P$ by definition of $\gamma$ using (2)
(4):: $Q\equiv\operatorname{sp}(P^{\prime},C)$ by Lemma 2 using (2)
(5):: $\operatorname{sp}(P^{\prime},C)\Rightarrow\operatorname{sp}(P,C)$ by Lemma 4 using (3)
(6):: $Q\Rightarrow\operatorname{sp}(P,C)$ by (4) and (5)
(7):: $\vdash[P]~{}C~{}[Q]$ by Theorem 8 using (6)

$\Longleftarrow$ :

(1):: $\vdash[P]~{}C~{}[Q]$ by assumption
(2):: $Q\in\textsc{SatFormula}$ by assumption
(3):: $P\wedge\operatorname{wp}(C,Q)\in\textsc{SatFormula}$ by Lemma 7 using (1) and (2)
(4):: $P\wedge\operatorname{wp}(C,Q)\Rightarrow P$ by logic
(5):: $P\wedge\operatorname{wp}(C,Q)\in\gamma(\textnormal{{?}}\wedge P)$ by definition of $\gamma$ using (3) and (4)
(6):: $Q\Rightarrow\operatorname{sp}(P,C)$ by Theorem 8 using (1)
(7):: $\operatorname{sp}(P\wedge\operatorname{wp}(C,Q),C)\equiv Q$ by Lemma 14 using (6)
(8):: $\vdash(P\wedge\operatorname{wp}(C,Q))~{}C~{}(Q)$ by Theorem 3 using (7)
(9):: $\mathrel{\widetilde{\vdash}}(\textnormal{{?}}\wedge P)~{}C~{}(Q)$ by (5) and (8) ∎

Gradual Exact Logic Unifying Hoare Logic and Incorrectness Logic via Gradual Verification

Abstract.

1. Overview

1.1. Hoare logic

1.2. Incorrectness logic

1.3. Gradual verification

2. Formal foundations

2.1. Exact logic

2.2. Gradual exact logic

2.3. Strongest postconditions

2.4. HL and IL via EL~\widetilde{\text{EL}}

2.5. GV via HL, EL~\widetilde{\text{EL}}, and IL

3. Applications

4. Caveats and future work

5. Conclusion

Acknowledgements.

References

Appendix A Grammar

Definition 0 (Implication).

Definition 0 (Equivalence of propositions).

Definition 0 (Replacement).

Definition 0.

Definition 0.

Definition 0.

Appendix B Predicate transformers

B.1. Weakest preconditions

Definition 0.

Lemma 0 (Stronger postcondition).

Proof.

B.2. Strongest postconditions

Definition 0.

Lemma 0 (Stronger precondition).

Proof.

Lemma 0.

Proof.

Lemma 0.

Proof.

Lemma 0.

Proof.

Lemma 0.

Proof.

Lemma 0.

Proof.

Lemma 0 (Frame rule).

Proof.

Lemma 0.

Proof.

B.3. Fixpoint

Lemma 0.

Proof.

Lemma 0 (Fixpoint property).

Proof.

Lemma 0.

Proof.

Appendix C Hoare logic

C.1. Weakest preconditions

Lemma 0.

Proof.

Lemma 0.

Proof.

Lemma 0.

Proof.

Theorem 4.

Proof.

C.2. Strongest postconditions

Lemma 0.

Proof.

Lemma 0.

Proof.

Lemma 0.

Proof.

Theorem 8.

Proof.

Appendix D Incorrectness logic

D.1. Strongest postconditions

Lemma 0.

Proof.

Lemma 0.

Proof.

Lemma 0.

Gradual Exact Logic
Unifying Hoare Logic and Incorrectness Logic via Gradual Verification

2.4. HL and IL via $\widetilde{\text{EL}}$

2.5. GV via HL, $\widetilde{\text{EL}}$ , and IL