11institutetext:  Beijing Key Laboratory of Electronic System Reliability and
Prognostics 22institutetext: Beijing Engineering Research Center of High
Reliable Embedded System 33institutetext: Beijing Advanced Innovation Center
for Imaging Theory and Technology
Capital Normal University, Beijing, China

# Reasoning about Iteration and Recursion Uniformly based on Big-step
Semantics

Ximeng Li 1133 Qianying Zhang 1122 Guohui Wang 2233 Zhiping Shi 11 Yong Guan
33

###### Abstract

A reliable technique for deductive program verification should be proven sound
with respect to the semantics of the programming language. For each different
language, the construction of a separate soundness proof is often a laborious
undertaking. In language-independent program verification, common aspects of
computer programs are addressed to enable sound reasoning for all languages.
In this work, we propose a solution for the sound reasoning about iteration
and recursion based on the big-step operational semantics of any programming
language. We give inductive proofs on the soundness and relative completeness
of our reasoning technique. We illustrate the technique at simplified
programming languages of the imperative and functional paradigms, with diverse
features. We also mechanism all formal results in the Coq proof assistant.

##  1 Introduction

It is commonly accepted that a reliable technique for deductive program
verification should be designed with the formal semantics of the programming
language as foundation. With the formal semantics used as axioms, a
mathematical proof of a desired property for the target program can be
constructed. Direct program proofs based on operational semantics are often
cumbersome. Due to language constructs that may incur unbounded program
behavior, inductive proofs along the structure of semantic derivations are
expected [24].

An established method for simplifying the verification is by devising a
program logic (e.g., [17, 28]) for the programming language. Program logics
effectively reduce the burdens in dealing with many aspects of the
verification, such as the reasoning about loops, recursive function calls,
memory layout of objects, concurrency, etc. The effectiveness of program
logics has been demonstrated by powerful tools (e.g., [6, 10, 9, 18]) and
significant projects (e.g., [31]).

A price to pay for enjoying the power of program logics, however, is the
considerable amount of effort often needed in establishing their soundness and
completeness wrt. the baseline semantics – often an operational semantics.
There have been a plethora of programming languages designed and implemented
to meet the needs of different domains. The recent development of blockchain
technology alone has led to the creation of multiple languages, such as
Solidity [5], Yul [7], Scilla [30], Move [3], Michelson [2], EVM bytecode
language [33], etc. Developing one program logic for each language that could
be used in scenarios where correctness is of serious concern would require a
huge amount of efforts.

To combat the cumbersomeness of direct program proofs based on operational
semantics, while avoiding the full complexity in the development of program
logics, one could seek to establish the infrastructure necessary for reasoning
about specific kinds of language features, for any languages with those
features. The results in [23] and [22] show how to deal with fundamental
language features that may cause unbounded behavior, such as iteration and
recursion, in a language-independent fashion. In [23], a technique is proposed
to generate inductive invariants from annotated loop invariants. In [22], a
method is presented to turn the semantics of a programming language into a
program verifier by applying coinductive reasoning principles. Both
developments are built on the small-step execution relation of a generic
programming language.

Small-step semantics [26] is known to be a fine-grained approach to the
definition of operational semantics. It supports a way to model concurrent
execution. It also enables the differentiation of looping and abnormal
termination. Big-step semantics (or natural semantics [14, 19]), on the other
hand, can be easier to formulate. For instance, the design of the semantic
configurations need not track the intermediate control states. Big-step
semantics can also be easier to use. It does not require the consideration of
both derivation sequences and derivation trees at the same time, in performing
proofs. There exist many formalizations of big-step semantics (e.g., [25, 20,
4, 11, 16, 34]) with practical uses.

In this work, we propose a technique for reasoning about iteration and
recursion in deductive program verification based on big-step operational
semantics. For any programming language with a big-step semantics, once a
generic predicate is defined to hold on the premises and corresponding
conclusions for the semantic rules, a theorem becomes available – the theorem
turns the verification of partial correctness results into symbolic execution
of the target program with auxiliary information from the user specification.
For loops and recursive function calls, this auxiliary information is provided
in the same form via the specification, enabling the same pattern of
reasoning. We illustrate our technique using verification tasks involving
simplified imperative and functional languages. We mechanize the proofs of all
formal results [8] in the Coq proof assistant [1].

The main technical contributions of this article are:

  * •

a language-independent technique simplifying the deductive verification of
iterative and recursive program structures based on big-step semantics,

  * •

proofs for the soundness and relative completeness of the technique,

  * •

illustration of the technique with the verification of example programs in
simplified programming languages of different paradigms,

  * •

mechanization of proofs and verification examples in the Coq proof assistant.

We provide an infrastructure that handles the routine part of the work in
reasoning about programming constructs with potentially unbounded behavior,
based on a common model of big-step execution in a proof assistant. This
provides a basis for a language-independent deductive program verifier.

##### Structure.

The remaining part of this article is structured as follows. In Section 2, we
discuss related work. In Section 3, we introduce the reasoning technique, and
prove its soundness. In Section 4, we illustrate the technique with a toy
example that is developed in detail. In Section 5, we present further
verification examples targeting simplified imperative and functional
languages. In Section 6, we discuss the completeness of the verification
technique. In Section 7, we discuss potential improvements of our technique.
Finally, we conclude in Section 8.

##  2 Related Work

Inductive invariants [21] are well-studied means to sound program verification
directly based on operational execution models. To avoid the difficulty of
specifying an inductive invariant that must be preserved by all the atomic
steps that can be performed by a program, a method is proposed to generate
inductive invariants from inductive assertions [23]. The verification of the
generated inductive invariants concludes the verification of the target
program. The soundness result of the generation is proven once and can be used
for different languages with a small-step execution relation. In comparison to
this work, our technique targets big-step operationals semantics, and its
soundness does not rely on the reduction of the verification problem to the
generation of inductive invariants. In [22], a technique is proposed to
generate sound program verifiers based on existing formalizations of small-
step semantics in proof assistants. The soundness of the technique is
established with an coinductive argument. In comparison, our technique targets
big-step operational semantics, and is based on inductive reasoning.
Nevertheless, we are inspired by this work in the style of language-
independent program specifications and the form of completeness statements.

In [32], a language-independent verification technique based on reachability
logics and semantics formulated in rewriting systems is introduced. In
comparison, our technique can only be used for big-step semantics. However,
our technique can be used with semantic definitions using inductive predicates
in a proof assistant, and requires only the logical foundation of the proof
assistant to function. Our technique also has a succinct, inductive argument
for soundness.

Several developments provide means to systematically derive abstract semantics
from concrete semantics such as big-step operational semantics and its
variants [12, 29, 13]. Among these, [12] proposes a language-independent
notion of skeletal semantics that can be instantiated to obtain concrete and
abstract semantic interpretations. However, the emphasis of these developments
is in obtaining automated static analyses of programs, rather than in
exploiting user-provided specification in the deductive verification of deep
correctness properties.

To some extent, language-independent program verification can also be
supported by encoding the target languages or target programs in the same
language (e.g., WhyML, Boogie, etc.) or calculus (e.g., CSP, the
$\pi$-calculus, etc.) supporting verification. This encoding can be
considerably more light-weight than the direct formalization of the syntax and
semantics of the source language. However, when the features of the source
language are sufficiently complicated, it can be highly non-trivial to justify
the encoding.

##  3 The Technique

Our verification technique can be used to check that the potential execution
results of a program satisfy pre-specified conditions. The potential execution
results are estimated by a combination of concrete computation according to
the big-step semantics of the programming language, and abstract inference
according to the auxiliary information in the specification. The abstract
inference helps realized what is usually accomplished wit loop invariants in
reasoning about loops, and with function contracts in reasoning about function
calls.

###  3.1 Specifications

Let $C$ be the set of _configurations_ ranged over by $c$. Let $R$ be the set
of _result configurations_ ranged over by $r$. A concrete example for a
configuration would be a pair of a program and a state (which may have its own
structure). A concrete example for a result configuration would be a state.

A specification is a function $\Phi\in C\to\mathcal{P}({R})$. For a
configuration $c$, if $c$ contains the complete program to be verified, then
$\Phi(c)$ is the set capturing the required range for the results of executing
the program from $c$. Otherwise, $\Phi(c)$ is the expected set of potential
results obtained by executing some statement within the overall program. This
set provides auxiliary information for the verification.

###  3.2 Semantic Derivation and Correctness

We model the set of rules of a big-step operational semantics by a predicate
$\mathit{rule}\in(C\times R)^{*}\to(C\times
R)\to\\{\mathit{tt},\mathit{ff}\\}$. Each semantic rule is captured as

$\mathit{rule}~{}{[({c_{1}},{r_{1}}),\dots,({c_{n}},{r_{n}})]}~{}{({c},{r})}$

Here, the list $[{({c_{1}},{r_{1}}),\dots,({c_{n}},{r_{n}})}]$ models the list
of premises of the rule, and $({c},{r})$ models the conclusion of the rule.
Each premise or conclusion consists of a configuration in the set $C$ and a
corresponding result configuration in the set $R$. A side condition in a
semantic rule can be captured by a condition on the parameters $c_{1}$, …,
$c_{n}$, $r_{1}$, …, $r_{n}$, $c$, and $r$, in the concrete definition of
$\mathit{rule}$.

A semantic derivation concluding that the configuration $c$ can be evaluated
to the result configuration $r$ in the big-step semantics is captured by

$\displaystyle\mathit{deriv}({c,r})~{}{:=}~{}\exists k\\!:$
$\displaystyle\,\exists c_{1},\dots,c_{k}\\!:\exists r_{1},\dots,r_{k}\\!:$
$\displaystyle\,\mathit{rule}~{}{[({c_{1}},{r_{1}}),\dots,({c_{k}},{r_{k}})]}~{}{({c},{r})}\,\land\,\forall
i\in\\{1,\dots,k\\}\\!:\mathit{deriv}({c_{i},r_{i}})$

Hence, the configuration $c$ can be evaluated to the result configuration $r$,
or $(c,r)$ can be derived in the big-step semantics, if there is a semantic
rule with $(c,r)$ as conclusion, and each premise of the rule can itself be
derived in the big-step semantics. Intuitively, if $\mathit{deriv}({c,r})$ can
be established, then there is a finite derivation tree rooted at $({c},{r})$.

With the notion of semantic derivation defined above, we formalize the notion
of partial correctness as the validity of specifications.

$\mathit{valid}({\Phi})~{}{:=}~{}\forall c,r:\mathit{deriv}({c,r})\Rightarrow
r\in\Phi(c)$

A specification $\Phi$ is valid, if for each configuration $c$, any result
configurations semantically derivable from $c$ is a member of $\Phi(c)$.

###  3.3 Specification-aware Inference and Verification

We infer the potential execution results of a configuration under a given
specification $\Phi$ according to the following definition.

$\displaystyle\mathit{infer}^{\Phi}({c},{r})~{}{:=}~{}$ $\displaystyle\exists
k\\!:c_{1},\dots,c_{k}\\!:\exists r_{1},\dots,r_{k}\\!:\,$
$\displaystyle\quad~{}~{}\,\mathit{rule}~{}{[({c_{1}},{r_{1}}),\dots,({c_{k}},{r_{k}})]}~{}{\\!({c},{r})}\land\,\forall
i\\!\in\\!\\{1,\dots,k\\}:\mathit{res}^{\Phi}({c_{i}},{r_{i}})$
$\displaystyle\mathit{res}^{\Phi}({c},{r})~{}{:=}~{}$ $\displaystyle
r\in\Phi(c)\,\land\,(\Phi(c)=R\Rightarrow\mathit{infer}^{\Phi}({c},{r}))$

The result configuration $r$ is infered from the configuration $c$ with the
help of the specification $\Phi$, if there is a semantic rule with $(c,r)$ as
conclusion, and for each premise $(c_{i},r_{i})$ of the semantic rule, $r_{i}$
is a potential result for $c_{i}$ according to $\Phi$, as is captured by the
auxiliary predicate $\mathit{res}^{\Phi}$. The expression
$\mathit{res}^{\Phi}({c_{i}},{r_{i}})$ says that the possible candidates for
$r_{i}$ are constrained by the information contained in the specification
about $c_{i}$. In addition, if $\Phi$ does not provide any useful information
about $c_{i}$ (i.e., $\Phi(c_{i})=R$), then $r_{i}$ should be inferable from
$c_{i}$.

Intuitively, the application of the semantic rules in the inference
corresponds to the symbolic execution of the target program. The information
in the specification can be used to overcome the inability to symbolically
execute the constructs with potentially unbounded behavior, such as iteration
and recursion.

We formulate the condition to be verified on specifications $\Phi$ using the
predicate $\mathit{verif}$. In other words, $\mathit{verif}({\Phi})$ is the
syntactical correctness condition.

$\displaystyle\mathit{verif}({\Phi})~{}{:=}~{}$ $\displaystyle\forall
c,r:\mathit{infer}^{\Phi}({c},{r})\Rightarrow r\in\Phi(c)$

A specification $\Phi$ is verified, if for each configuration $c$, any result
configurations that can be infered from $c$ with the help of $\Phi$ are
contained in $\Phi(c)$.

###  3.4 Soundness

We prove the implication from $\mathit{verif}({\Phi})$ to
$\mathit{infer}^{\Phi}({c},{r})$. The following lemma is a key component of
this proof.

###### Lemma 1

If $\mathit{verif}({\Phi})$, and $\mathit{deriv}({c,r})$ holds, then
$\mathit{infer}^{\Phi}({c},{r})$ holds.

###### Proof

According to the definition of $\mathit{deriv}({c,r})$, if this predicate
holds, then there is a finite derivation tree generated by the following
inference rule.

$\begin{array}[]{@{}c@{}}\mathit{deriv}({c_{1},r_{1}})\quad\dots\quad\mathit{deriv}({c_{m},r_{m}})\qquad\qquad\mathit{rule}~{}{[({c_{1}},{r_{1}}),\dots,({c_{m}},{r_{m}})]}~{}{({c},{r})}\\\\[0.0pt]
\hline\cr\\\\[-8.09995pt] \mathit{deriv}({c,r})\\\ \end{array}$

The proof is by induction on the derivation tree for $\mathit{deriv}({c,r})$.

From $\mathit{deriv}({c,r})$, we have $\mathit{deriv}({c_{1},r_{1}})$, …,
$\mathit{deriv}({c_{m},r_{m}})$, and

$\mathit{rule}~{}{[({c_{1}},{r_{1}}),\dots,({c_{m}},{r_{m}})]}~{}{({c},{r})}$
(1)

for some $m$, $c_{1}$, …, $c_{m}$, $r_{1}$, …, $r_{m}$.

For each $i\in\\{1,\dots,m\\}$, we have
$\mathit{infer}^{\Phi}({c_{i}},{r_{i}})$ from $\mathit{deriv}({c_{i},r_{i}})$
and the induction hypothesis. We show that
$\mathit{res}^{\Phi}({c_{i}},{r_{i}})$ holds by distinguishing between the
cases where $\Phi(c_{i})=R$ and where $\Phi(c_{i})\neq R$.

  * •

Suppose $\Phi(c_{i})=R$. Then, it holds that $r\in\Phi(c_{i})$. Hence, we have
$\mathit{res}^{\Phi}({c_{i}},{r_{i}})$ because of
$\mathit{infer}^{\Phi}({c_{i}},{r_{i}})$, and the definition of
$\mathit{res}^{\Phi}$.

  * •

Suppose $\Phi(c_{i})\neq R$. From $\mathit{infer}^{\Phi}({c_{i}},{r_{i}})$,
and $\mathit{verif}({\Phi})$, we have $r_{i}\in\Phi(c_{i})$. Hence, we have
$\mathit{res}^{\Phi}({c_{i}},{r_{i}})$ according to the definition of
$\mathit{res}^{\Phi}$.

Hence, for each $i\in\\{1,\dots,m\\}$, we have
$\mathit{res}^{\Phi}({c_{i}},{r_{i}})$. Thus, we can deduce
$\mathit{infer}^{\Phi}({c},{r})$ using Eq. 1 and the definition of
$\mathit{infer}^{\Phi}$. This completes the proof. ∎

Using this lemma, the soundness theorem can be obtained directly.

######  Theorem 3.1 (Soundness)

If $\mathit{verif}({\Phi})$ can be established, then $\mathit{valid}({\Phi})$
holds.

###### Proof

Assume $\mathit{verif}({\Phi})$ and $\mathit{deriv}({c,r})$. Then, we have
$\mathit{infer}^{\Phi}({c},{r})$ according to Lemma 1. Thus, we can deduce
$r\in\Phi(c)$ using $\mathit{verif}({\Phi})$. ∎

The application of this theorem reliably turns the problem of establishing the
validity of a specification $\Phi$ into the problem of proving
$\mathit{verif}({\Phi})$, irrespective of the language used for the program
that is specified in $\Phi$.

###### Remark 1

Lemma 1 suggests that an abstract form of computation is obtained leveraging
user specification that is verified. In abstract interpretation [15], the
focus is often to calculate the abstract form of the computation performed by
each kind of program statement, to support automated program analysis. On the
other hand, our focus is to leverage user specification for specific concrete
statements in a program, to provide hints in a deductive program verification.

##  4 Illustrative Example

In this section, we illustrate our technique using a toy example. In this
example, a program computing the factorial of a natural number is written in
the While language [24]. We show how the big-step semantics of the While
language can be formulated with the $\mathit{rule}$ predicate introduced in
Section 3.2. We then show how the functional correctness of the factorial
program can be specified and proven.

###  4.1 Big-step Semantics of the While Language

The While language consists of arithmetic expressions $a$, Boolean expressions
$b$, and statements $S\in Stmt$. A statement can be $\mathsf{skip}$ that
performs no operation, an assignment ${x}:={a}$, a sequential composition
$S_{1};S_{2}$, a branching statement
$\mathsf{if}~{}{b}~{}\mathsf{then}~{}{S_{1}}~{}\mathsf{else}~{}{S_{2}}$, or a
loop $\mathsf{while}~{}{b}~{}\mathsf{do}~{}{S}$.

For programs in the While language, the states $\sigma$ are elements of
$\Sigma{:=}\mathit{Var}\to\mathbb{Z}$. Here, $\mathit{Var}$ is the set of
variables and $\mathbb{Z}$ is the set of integers. The evaluation of
arithmetic expressions and Boolean expressions in states can be formalized by
defining the evaluation functions $\mathcal{A}$ and $\mathcal{B}$,
respectively, as in [24]. The set $C$ of configurations is $Stmt\times\Sigma$.
The set $R$ of result configurations is $\Sigma$. We formulate the big-step
semantics by defining the predicate $\mathit{rule}$, as in Fig. 1. In each
line, a combination of the parameter values for which $\mathit{rule}$ holds is
given.

$\begin{array}[]{l}}{}{\\\\[-27.1249pt]
\mathit{rule}~{}{[\,]}~{}{({\langle{\mathsf{skip}},{\sigma}\rangle},{\sigma})}\\\
\\\\[-7.74997pt]
\mathit{rule}~{}{[\,]}~{}{({\langle{{x}:={a}},{\sigma}\rangle},{\sigma[x\mapsto\mathcal{A}\llbracket{a}\rrbracket\sigma]})}\\\
\\\\[-7.74997pt]
\mathit{rule}~{}{[({\langle{S_{1}},{\sigma}\rangle},{\sigma^{\prime\prime}}),({\langle{S_{2}},{\sigma^{\prime\prime}}\rangle},{\sigma^{\prime}})]}~{}{({\langle{{S_{1}};{S_{2}}},{\sigma}\rangle},{\sigma^{\prime}})}\\\
\\\\[-7.74997pt]
\mathit{rule}~{}{[({\langle{S_{1}},{\sigma}\rangle},{\sigma^{\prime}})]}~{}{({\langle{\mathsf{if}~{}{b}~{}\mathsf{then}~{}{S_{1}}~{}\mathsf{else}~{}{S_{2}}},{\sigma}\rangle},{\sigma^{\prime}})}\quad\mathrm{if}~{}\mathcal{B}\llbracket{b}\rrbracket\sigma=\mathit{tt}\\\
\\\\[-7.74997pt]
\mathit{rule}~{}{[({\langle{S_{2}},{\sigma}\rangle},{\sigma^{\prime}})]}~{}{({\langle{\mathsf{if}~{}{b}~{}\mathsf{then}~{}{S_{1}}~{}\mathsf{else}~{}{S_{2}}},{\sigma}\rangle},{\sigma^{\prime}})}\quad\mathrm{if}~{}\mathcal{B}\llbracket{b}\rrbracket\sigma=\mathit{ff}\\\
\\\\[-7.74997pt]
\mathit{rule}~{}{[({\langle{S},{\sigma}\rangle},{\sigma^{\prime\prime}}),({\langle{\mathsf{while}~{}{b}~{}\mathsf{do}~{}{S}},{\sigma^{\prime\prime}}\rangle},{\sigma^{\prime}})]}~{}{({\langle{\mathsf{while}~{}{b}~{}\mathsf{do}~{}{S}},{\sigma}\rangle},{\sigma^{\prime}})}~{}\mathrm{if}~{}\mathcal{B}\llbracket{b}\rrbracket\sigma=\mathit{tt}\\\
\\\\[-7.74997pt]
\mathit{rule}~{}{[\,]}~{}{({\langle{\mathsf{while}~{}{b}~{}\mathsf{do}~{}{S}},{\sigma}\rangle},{\sigma})}~{}\mathrm{if}~{}\mathcal{B}\llbracket{b}\rrbracket\sigma=\mathit{ff}\end{array}$
Figure 1: The semantic rules for the statements of the While language

###  4.2 Factorial Program and its Specification

Consider the program $S_{\mathrm{fac}}$ in the While language. The program
computes the factorial ${m}!$ where $m$ is the initial value of the program
variable $\mathtt{m}$.

$\displaystyle S_{\mathrm{fac}}~{}{:=}~{}$
$\displaystyle({\mathtt{fac}}:={\mathtt{m}};S_{\mathrm{wh}})$ $\displaystyle
S_{\mathrm{wh}}~{}{:=}~{}$
$\displaystyle(\mathsf{while}~{}1<\mathtt{m}~{}\mathsf{do}~{}({\mathtt{m}}:={\mathtt{m}-\mathtt{1}};{\mathtt{fac}}:={\mathtt{fac}*\mathtt{m}}))$

Let $P_{m}$ be the set of states where $\mathtt{fac}$ has the value ${m}!$.
Let $P^{\prime}_{{m},{\mathit{fac}}}$ be the set of states where
$\mathtt{fac}$ has the value $\mathit{fac}*{(m-1)}!$.

$\displaystyle P_{m}~{}{:=}~{}$
$\displaystyle\\{\sigma^{\prime}[\mathtt{fac}\mapsto{m}!]\mid\sigma^{\prime}\in\Sigma\\}$
$\displaystyle P^{\prime}_{{m},{\mathit{fac}}}~{}{:=}~{}$
$\displaystyle\\{\sigma^{\prime}[\mathtt{fac}\mapsto\mathit{fac}*{(m-1)}!]\mid\sigma^{\prime}\in\Sigma\\}$

We consider the following specification for the program.

$\begin{array}[]{rll}\Phi_{\mathrm{fac}}(\langle{S_{\mathrm{fac}}},{\sigma}\rangle)~{}{:={}}&P_{m}&\mathrm{if}~{}m=\sigma(\mathtt{m})\,\land\,m>0\,\land\,\sigma\in\Sigma\\\
\\\\[-7.74997pt]
\Phi_{\mathrm{fac}}(\langle{S_{\mathrm{wh}}},{\sigma}\rangle)~{}{:={}}&P^{\prime}_{{m},{\mathit{fac}}}&\mathrm{if}~{}m=\sigma(\mathtt{m})\,\land\,m>0\,\land\,\mathit{fac}=\sigma(\mathtt{fac})\,\land\,\sigma\in\Sigma\\\
\\\\[-7.74997pt]
\Phi_{\mathrm{fac}}(c)~{}{:={}}&\Sigma&\mathrm{if}~{}c~{}\mathrm{is~{}not~{}of~{}the~{}above~{}forms}\end{array}$

The specification says that when $S_{\mathrm{fac}}$ finishes execution started
in a state where the value of $\mathtt{m}$ is $m>0$, the value of
$\mathtt{fac}$ will be ${m}!$. The specification also contains the auxiliary
claim that when the loop $S_{\mathrm{wh}}$ finishes execution started in a
state where $\mathtt{fac}$ has the value $\mathit{fac}$ and $\mathtt{m}$ has
the value $m>0$, the value of $\mathtt{fac}$ will be equal to the product of
$\mathit{fac}$ and ${(m-1)}!$ (noting that ${0}!=1$).

###  4.3 Proof of the Factorial Program

A direct proof of the factorial program $S_{\mathrm{fac}}$ based on the big-
step operational semantics of the While language would require an induction on
the shape of derivation trees (e.g., [24]) to establish a suitable invariant
for the loop $S_{\mathrm{wh}}$.

Using the technique of Section 3, we aim at establishing
$\mathit{valid}({\Phi_{\mathrm{fac}}})$. With Theorem 3.1, it suffices to show
$\mathit{verif}({\Phi_{\mathrm{fac}}})$ – for all $c$ and $r$, assuming
$\mathit{infer}^{\Phi_{\mathrm{fac}}}({c},{r})$, we attempt to show
$r\in\Phi_{\mathrm{fac}}(c)$.

  1. 1.

Firstly, assume $c$ is $\langle{S_{\mathrm{fac}}},{\sigma}\rangle$, where
${\sigma}(\mathtt{\mathtt{m}})>0$. Then, $\Phi_{\mathrm{fac}}(c)$ is $P_{m}$,
where $m={\sigma}(\mathtt{\mathtt{m}})$. Using
$\mathit{infer}^{\Phi_{\mathrm{fac}}}({\langle{S_{\mathrm{fac}}},{\sigma}\rangle},{r})$
and the semantics of the While language in Fig. 1, it is not difficult to
obtain

$\mathit{rule}~{}{[(\langle{{\mathtt{fac}}:={\mathtt{m}}},{\sigma}\rangle,\sigma^{\prime\prime}),(\langle{S_{\mathrm{wh}}},{\sigma^{\prime\prime}}\rangle,r)]}~{}{(\langle{S_{\mathrm{fac}}},{\sigma}\rangle,r)}$

for some $\sigma^{\prime\prime}$ such that
$\mathit{res}^{\Phi_{\mathrm{fac}}}({\langle{{\mathtt{fac}}:={\mathtt{m}}},{\sigma}\rangle},{\sigma^{\prime\prime}})$
and
$\mathit{res}^{\Phi_{\mathrm{fac}}}({\langle{S_{\mathrm{wh}}},{\sigma^{\prime\prime}}\rangle},{r})$.
Since
$\Phi_{\mathrm{fac}}(\langle{{\mathtt{fac}}:={\mathtt{m}}},{\sigma}\rangle)=R$,
we deduce
$\mathit{infer}^{\Phi_{\mathrm{fac}}}({\langle{{\mathtt{fac}}:={\mathtt{m}}},{\sigma}\rangle},{\sigma^{\prime\prime}})$
from
$\mathit{res}^{\Phi_{\mathrm{fac}}}({\langle{{\mathtt{fac}}:={\mathtt{m}}},{\sigma}\rangle},{\sigma^{\prime\prime}})$.
Hence, we deduce
$\sigma^{\prime\prime}=\sigma[\mathtt{fac}\mapsto{\sigma}(\mathtt{\mathtt{m}})]$.
Hence, we have
${\sigma^{\prime\prime}}(\mathtt{\mathtt{m}})={\sigma}(\mathtt{\mathtt{m}})>0$.
Hence, we have
$\Phi_{\mathrm{fac}}(\langle{S_{\mathrm{wh}}},{\sigma^{\prime\prime}}\rangle)=P^{\prime}_{{{\sigma^{\prime\prime}}(\mathtt{\mathtt{m}})},{{\sigma^{\prime\prime}}(\mathtt{\mathtt{fac}})}}=\\{\sigma^{\prime}[\mathtt{fac}\mapsto{\sigma^{\prime\prime}}(\mathtt{\mathtt{fac}})*{({\sigma^{\prime\prime}}(\mathtt{m})-1)}!]\mid\sigma^{\prime}\in\Sigma\\}=\\{\sigma^{\prime}[\mathtt{fac}\mapsto{{\sigma}(\mathtt{\mathtt{m}})}!]\mid\sigma^{\prime}\in\Sigma\\}=P_{m}$.
Moreover, from
$\mathit{res}^{\Phi_{\mathrm{fac}}}({\langle{S_{\mathrm{wh}}},{\sigma^{\prime\prime}}\rangle},{r})$
we have $r\in
P^{\prime}_{{{\sigma^{\prime\prime}}(\mathtt{\mathtt{m}})},{{\sigma^{\prime\prime}}(\mathtt{\mathtt{fac}})}}$.
Ultimately, we have $r\in P_{m}$.

  2. 2.

Secondly, assume $c$ is $\langle{S_{\mathrm{wh}}},{\sigma}\rangle$, where
${\sigma}(\mathtt{\mathtt{m}})>0$. Then, $\Phi_{\mathrm{fac}}(c)$ is
$P^{\prime}_{{m},{\mathit{fac}}}$, where $m={\sigma}(\mathtt{\mathtt{m}})$,
and $\mathit{fac}={\sigma}(\mathtt{\mathtt{fac}})$. Using
$\mathit{infer}^{\Phi_{\mathrm{fac}}}({\langle{S_{\mathrm{wh}}},{\sigma}\rangle},{r})$
and the semantics of the While language in Fig. 1, we have the following two
cases.

    1. (a)

We have $m\leq 1$,
$\mathit{rule}~{}{[~{}]}~{}{(\langle{S_{\mathrm{wh}}},{\sigma}\rangle,\sigma)}$,
and $r=\sigma$. Since $m>0$ and $m\leq 1$, we have $m=1$. Hence, it is not
difficult to deduce $r\in P^{\prime}_{m,\mathit{fac}}$.

    2. (b)

We have $m>1$, and

$\mathit{rule}~{}{[(\langle{{\mathtt{m}}:={\mathtt{m}-\mathtt{1}};{\mathtt{fac}}:={\mathtt{fac}*\mathtt{m}}},{\sigma}\rangle,\sigma^{\prime\prime}),(\langle{S_{\mathrm{wh}}},{\sigma^{\prime\prime}}\rangle,r)]}~{}{(\langle{S_{\mathrm{wh}}},{\sigma}\rangle,r)}$

for some $\sigma^{\prime\prime}$ such that
$\mathit{res}^{\Phi_{\mathrm{fac}}}({\langle{{\mathtt{m}}:={\mathtt{m}-\mathtt{1}};{\mathtt{fac}}:={\mathtt{fac}*\mathtt{m}}},{\sigma}\rangle},{\sigma^{\prime\prime}})$
and
$\mathit{res}^{\Phi_{\mathrm{fac}}}({\langle{S_{\mathrm{wh}}},{\sigma^{\prime\prime}}\rangle},{r})$.
From the former we have

$\mathit{infer}^{\Phi_{\mathrm{fac}}}({\langle{{\mathtt{m}}:={\mathtt{m}-\mathtt{1}};{\mathtt{fac}}:={\mathtt{fac}*\mathtt{m}}},{\sigma}\rangle},{\sigma^{\prime\prime}})$

The specification $\Phi_{\mathrm{fac}}$ provides no information about the two
assignments, ${\mathtt{m}}:={\mathtt{m}-\mathtt{1}}$ and
${\mathtt{fac}}:={\mathtt{fac}*\mathtt{m}}$. Hence,
$\mathit{infer}^{\Phi_{\mathrm{fac}}}$ applies also to these two assignments,
it can be deduced that $\sigma^{\prime\prime}=\sigma[\mathtt{m}\mapsto
m-1,\mathtt{fac}\mapsto\mathit{fac}*(m-1)]$. Hence, we have
${\sigma^{\prime\prime}}(\mathtt{\mathtt{m}})=m-1>0$. Hence,
$\Phi_{\mathrm{fac}}(\langle{S_{\mathrm{wh}}},{\sigma^{\prime\prime}}\rangle)=P^{\prime}_{{{\sigma^{\prime\prime}}(\mathtt{\mathtt{m}})},{{\sigma^{\prime\prime}}(\mathtt{\mathtt{fac}})}}=\\{\sigma^{\prime}[\mathtt{fac}\mapsto(\mathit{fac}*(m-1))*{(m-1-1)}!]\mid\sigma^{\prime}\in\Sigma\\}=P^{\prime}_{{m},{\mathit{fac}}}$.
Moreover, from
$\mathit{res}^{\Phi_{\mathrm{fac}}}({\langle{S_{\mathrm{wh}}},{\sigma^{\prime\prime}}\rangle},{r})$
we have $r\in
P^{\prime}_{{\sigma^{\prime\prime}}(\mathtt{\mathtt{m}}),{\sigma^{\prime\prime}}(\mathtt{\mathtt{fac}})}$.
Ultimately, we have $r\in P^{\prime}_{m,\mathit{fac}}$.

In the other cases, we have $\Phi_{\mathrm{fac}}(c)=R$. Hence, it trivially
holds that $r\in\Phi_{\mathrm{fac}}(c)$ The proof is thus complete. ∎

The above proof of the factorial program does not require the use of
induction. Essentially, the induction required for the loop is already
encapsulated in the proof of Theorem 3.1.

##  5 Verification of Iterative and Recursive Programs

In this section, we evaluate our technique with two further examples. In the
two examples, programming languages of the imperative and functional paradigms
are used, respectively, to implement the functionality of merging two sorted
lists of integers into a single sorted list of integers.

###  5.1 Extended While Language and Array-Merging Program

#### Extended While Language

The programming language of this section is an extension of the While
language. This extension contains the extra features of one-dimensional arrays
and functions.

##### Syntax.

We give the syntax for arithmetic expressions $a$, Boolean expressions $b$,
and statements $S$. We explain the constructs present in the extension only.

$\displaystyle a~{}::=~{}$ $\displaystyle n\mid x\mid
X\mid{X}[{a}]\mid{a}+{a}\mid{a}-{a}\mid{a}*{a}\mid{a}\,/\,{a}$ $\displaystyle
b~{}::=~{}$ $\displaystyle\mathsf{true}\mid\mathsf{false}\mid a=a\mid
a<a\mid{b}{\,\&\\!\&\,}{b}\mid{!{b}}$ $\displaystyle S~{}::=~{}$
$\displaystyle\mathsf{var}~{}{x}\mid\mathsf{arr}~{}{X}[{n}]\mid{x}:={a}\mid{{X}[{a}]}:={a}\mid\mathsf{skip}\mid$
$\displaystyle\mathsf{if}~{}{b}~{}\mathsf{then}~{}{S}~{}\mathsf{else}~{}{S}\mid\mathsf{while}~{}{b}~{}\mathsf{do}~{}{S}\mid{S};{S}\mid{f}({a,\dots,a})\to{[{x,\dots,x}]}$

Here, $X$ is an array identifier, and ${X}[{a_{1}}]$ is the expression used to
retrieve the element of the array $X$ at the index $a_{1}$. In addition,
$\mathsf{var}~{}{x}$ is the declaration of the variable $x$,
$\mathsf{arr}~{}{X}[{n}]$ is the declaration of the array with identifier $x$
and size $n$, ${{X}[{a_{1}}]}:={a_{2}}$ is an assignment of the result of
$a_{2}$ to the element of the array $X$ indexed at $a_{1}$, and
${f}({a_{1},\dots,a_{m}})\to{[{x_{1},\dots,x_{n}}]}$ is a call to the function
with identifier $f$ with arguments $a_{1}$, …, $a_{m}$ and return variables
$x_{1}$, …, $x_{n}$. If some argument $a_{i}$ is an array, then it is passed
by reference in the call.

A _program_ in the extended While language is a mapping $\rho$ from each
function identifier $f$ to a triple
$([{w_{1},\dots,w_{m}}],[{x_{1},\dots,x_{n}}],S)$ or $\bot$. Here, each
$w_{i}$ ($i\in\\{1,\dots,m\\}$) is a parameter of the function that is either
a variable $x$ or an array $X$. Each $x_{i}$ ($i\in\\{1,\dots,n\\}$) is a
return variable of the function. The $S$ is the statement of the function. If
$\rho(f)=\bot$, then there is no function defined for the function identifier
in the program.

##### Semantics.

A _state_ $\sigma$ is a pair $({s},{\iota})$. Here,
$s\in(\mathit{Var}\cup\mathit{Arr}\to{\mathbb{Z}}_{\bot})\cup(\mathbb{Z}\to\mathbb{Z})$
is a _store_ that maps each variable to an optional integer that is the value
of the variable, maps each array name to an optional integer representing the
starting location of the array, and maps each location to an integer that is
the value stored at the location. In addition, $\iota\in\mathbb{Z}$ is the
_next fresh location_ that can be used as the starting location of an array.
For a state $\sigma=({s},{\iota})$, we write ${\sigma}.{s}$ to refer to the
store $s$, write ${\sigma}.{\iota}$ to refer to the next fresh location
$\iota$ for arrays, write $\sigma(a)$ for $s(a)$, and write $\sigma[a\mapsto
b]$ for $s[a\mapsto b]$.

$\displaystyle\mathit{rule}~{}{[\,]}~{}{(\langle{\mathsf{skip}},{\sigma}\rangle_{\rho},\sigma)}$
$\displaystyle\mathit{rule}~{}{[\,]}~{}{(\langle{\mathsf{var}~{}{x}},{\sigma}\rangle_{\rho},{\sigma}[{x}\mapsto{0}])}\quad\mathrm{if}~{}\sigma(x)=\bot$
$\displaystyle\mathit{rule}~{}{[\,]}~{}{(\langle{\mathsf{arr}~{}{X}[{n}]},{({s},{\iota})}\rangle_{\rho},({s[X\mapsto\iota]},{\iota+\mathcal{N}\llbracket{n}\rrbracket}))}\quad\mathrm{if}~{}\sigma(X)=\bot$
$\displaystyle\mathit{rule}~{}{[\,]}~{}{(\langle{{x}:={a}},{\sigma}\rangle_{\rho},{\sigma}[{x}\mapsto{z}])}\quad\mathrm{if}~{}\mathcal{A}\llbracket{a}\rrbracket\sigma=z\land\sigma(x)\neq\bot$
$\displaystyle\mathit{rule}~{}{[\,]}~{}{(\langle{{{X}[{a_{1}}]}:={a_{2}}},{\sigma}\rangle_{\rho},\sigma^{\prime})}$
$\displaystyle\qquad\mathrm{if}~{}\exists\ell:\exists
z_{1},z_{2}:(\sigma(X)=\ell\,\land\,\mathcal{A}\llbracket{a_{1}}\rrbracket\sigma=z_{1}\,\land\,z_{1}\geq
0\,\land\,\mathcal{A}\llbracket{a_{2}}\rrbracket\sigma=z_{2}\,\land\,$
$\displaystyle\qquad\qquad\qquad\qquad~{}~{}\,\ell+z_{1}<{\sigma}.{\iota}\land\sigma^{\prime}={\sigma}[{\ell+z_{1}}\mapsto{z_{2}}])$
$\displaystyle\mathit{rule}~{}{[(\langle{S_{1}},{\sigma}\rangle_{\rho},\sigma^{\prime})]}~{}{(\langle{\mathsf{if}~{}{b}~{}\mathsf{then}~{}{S_{1}}~{}\mathsf{else}~{}{S_{2}}},{\sigma}\rangle_{\rho},\sigma^{\prime})}\quad\mathrm{if}~{}\mathcal{B}\llbracket{b}\rrbracket\sigma=\mathit{tt}$
$\displaystyle\mathit{rule}~{}{[(\langle{S_{2}},{\sigma}\rangle_{\rho},\sigma^{\prime})]}~{}{(\langle{\mathsf{if}~{}{b}~{}\mathsf{then}~{}{S_{1}}~{}\mathsf{else}~{}{S_{2}}},{\sigma}\rangle_{\rho},\sigma^{\prime})}\quad\mathrm{if}~{}\mathcal{B}\llbracket{b}\rrbracket\sigma=\mathit{ff}$
$\displaystyle\mathit{rule}~{}{[(\langle{S},{\sigma}\rangle_{\rho},\sigma^{\prime\prime}),(\langle{\mathsf{while}~{}{b}~{}\mathsf{do}~{}{S}},{\sigma^{\prime\prime}}\rangle_{\rho},\sigma^{\prime})]}~{}{(\langle{\mathsf{while}~{}{b}~{}\mathsf{do}~{}{S}},{\sigma}\rangle_{\rho},\sigma^{\prime})}~{}~{}\mathrm{if}~{}\mathcal{B}\llbracket{b}\rrbracket\sigma=\mathit{tt}$
$\displaystyle\mathit{rule}~{}{[\,]}~{}{(\langle{\mathsf{while}~{}{b}~{}\mathsf{do}~{}{S}},{\sigma}\rangle_{\rho},\sigma)}\quad\mathrm{if}~{}\mathcal{B}\llbracket{b}\rrbracket\sigma=\mathit{ff}$
$\displaystyle\mathit{rule}~{}{[(\langle{S_{1}},{\sigma}\rangle_{\rho},\sigma^{\prime\prime}),(\langle{S_{2}},{\sigma^{\prime\prime}}\rangle_{\rho},\sigma^{\prime})]}~{}{(\langle{{S_{1}};{S_{2}}},{\sigma}\rangle_{\rho},\sigma^{\prime})}$
$\displaystyle\mathit{rule}~{}{[(\langle{S},{({s^{\prime\prime}},{{\sigma}.{\iota}})}\rangle_{\rho},\sigma^{\prime}_{0})]}~{}{(\langle{{f}({a_{1},\dots,a_{m}})\to{[{x^{\prime}_{1},\dots,x^{\prime}_{n}}]}},{\sigma}\rangle_{\rho},({s^{\prime}},{{\sigma}.{\iota}}))}$
$\displaystyle\qquad\mathrm{if}~{}\exists v_{1},\dots,v_{m}:$
$\displaystyle\qquad\qquad\rho(f)=([{w_{1},\dots,w_{m}}],[{x_{1},\dots,x_{n}}],S)\,\land\,\mathcal{A}\llbracket{a_{1}}\rrbracket\sigma=v_{1}\land\dots\land\mathcal{A}\llbracket{a_{m}}\rrbracket\sigma=v_{m}\,\land\,$
$\displaystyle\qquad\qquad\mathit{call}\mbox{-}\mathit{ini}({{\sigma}.{s}},{[{w_{1},\dots,w_{m}}]},{[{v_{1},\dots,v_{m}}]},{[{x_{1},\dots,x_{n}}]})=s^{\prime\prime}\,\land\,$
$\displaystyle\qquad\qquad\mathit{call}\mbox{-}\mathit{fin}({{\sigma}.{s}},{{\sigma^{\prime}_{0}}.{s}},{[{x_{1},\dots,x_{n}}]},{[{x^{\prime}_{1},\dots,x^{\prime}_{n}}]})=s^{\prime}$
Figure 2: The semantic rules for the statements of the extended While language

We define the big-step semantics of the extended While language by defining
the predicate $\mathit{rule}$ as in Fig. 2. According to the rule for the
array declaration $\mathsf{arr}~{}{X}[{n}]$, the array identifier should be
mapped to the undefined location $\bot$ before the declaration. This array
identifier is then associated to the next fresh location $\iota$ that can be
used for arrays, and the next fresh location for arrays is incremented by the
size of the array after the declaration. According to the rule for the
assignment ${{X}[{a_{1}}]}:={a_{2}}$, the location of the target array element
should not surpass the boundary as given by the next fresh location $\iota$.
The result of the right-hand side is then placed at this location. In the rule
for function calls, the auxiliary function $\mathit{call}\mbox{-}\mathit{ini}$
is used to initialize the store for the execution of the callee. The resulting
initial store $s^{\prime\prime}$ for the callee maps the parameters of the
callee to the values of the corresponding arguments, and maps each return
variable of the callee to $0$. In the same rule, the auxiliary function
$\mathit{call}\mbox{-}\mathit{fin}$ is used to finalize the store after the
execution of the callee. The resulting store $s^{\prime}$ maps the caller’s
variables that receive the return values to the values of the callee’s return
variables. In addition, $s^{\prime}$ maps the memory locations according to
the store ${\sigma^{\prime}_{0}}.{s}$ reached after the execution of the
callee’s statement. Hence, the effects of the callee on the arrays passed in
by reference are recorded. On the other hand, the next fresh location
${\sigma}.{\iota}$ for arrays before the call is kept after the call returns.
Hence, any arrays that are stack-allocated (at their declarations) in the
callee are discarded.

In Fig. 2, $\mathcal{A}$ and $\mathcal{B}$ are evaluation functions for
arithmetic expressions and Boolean expressions, respectively. The detailed
definitions for these two functions, and for the functions
$\mathit{call}\mbox{-}\mathit{ini}$ and $\mathit{call}\mbox{-}\mathit{fin}$,
are given in Appendix 0.A.

#### Array-Merging Program and its Verification

$\displaystyle\rho_{\mathrm{mg}}~{}{:=}~{}$
$\displaystyle[\,\mathsf{merge}\mapsto([{\mathsf{S},\mathsf{T},\mathtt{i},\mathtt{m},\mathtt{n}}],[\,],S_{\mathrm{mg}})\,]$
$\displaystyle S_{\mathrm{mg}}~{}{:=}~{}$
$\displaystyle\mathsf{var}~{}{\mathtt{j}};\mathsf{var}~{}{\mathtt{k}};{\mathtt{j}}:={\mathtt{m}+1};{\mathtt{k}}:={\mathtt{i}};S_{\mathrm{wh}};S_{{\mathtt{i}},{\mathtt{m}}};S_{{\mathtt{j}},{\mathtt{n}}}$
$\displaystyle S_{\mathrm{wh}}~{}{:=}~{}$
$\displaystyle\mathsf{while}~{}{\mathtt{i}\leq\mathtt{m}}{\,\&\\!\&\,}{\mathtt{j}\leq\mathtt{n}}~{}\mathsf{do}~{}($
$\displaystyle\quad(\mathsf{if}~{}{\mathsf{S}}[{\mathtt{i}}]\leq{\mathsf{S}}[{\mathtt{j}}]~{}\mathsf{then}~{}{{\mathsf{T}}[{\mathtt{k}}]}:={{\mathsf{S}}[{\mathtt{i}}]};{\mathsf{i}}:={\mathsf{i}+1}~{}\mathsf{else}~{}{{\mathsf{T}}[{\mathtt{k}}]}:={{\mathsf{S}}[{\mathtt{j}}]};{\mathsf{j}}:={\mathsf{j}+1});$
$\displaystyle\quad{\mathtt{k}}:={\mathtt{k}+1}\,)$ $\displaystyle
S_{{\mathtt{i}},{\mathtt{m}}}~{}{:=}~{}$
$\displaystyle\mathsf{while}~{}\mathtt{i}\leq\mathtt{m}~{}\mathsf{do}~{}({{\mathsf{T}}[{\mathtt{k}}]}:={{\mathsf{S}}[{\mathtt{i}}]};{\mathsf{i}}:={\mathsf{i}+1};{\mathsf{k}}:={\mathsf{k}+1})$
$\displaystyle S_{{\mathtt{j}},{\mathtt{n}}}~{}{:=}~{}$
$\displaystyle\mathsf{while}~{}\mathtt{j}\leq\mathtt{n}~{}\mathsf{do}~{}({{\mathsf{T}}[{\mathtt{k}}]}:={{\mathsf{S}}[{\mathtt{j}}]};{\mathsf{j}}:={\mathsf{j}+1};{\mathsf{k}}:={\mathsf{k}+1})$
Figure 3: The program $\rho_{\mathrm{mg}}$ that merges sorted array fragments

The program $\rho_{\mathrm{mg}}$ as shown in Fig. 3 merges the elements in two
sorted fragments of an array $\mathsf{S}$ into one sorted fragment in a
different array $\mathsf{T}$.

The only function in this program is $\mathsf{merge}$. Formally, this function
is the triple
$([{\mathsf{S},\mathsf{T},\mathtt{i},\mathtt{m},\mathtt{n}}],[\,],S_{\mathrm{mg}})$.
The parameters $\mathtt{i}$ and $\mathtt{m}$ represent the initial and final
index, respectively, for the first fragment of the array $\mathsf{S}$
participating in the merger. The second fragment participating in the merger
is from the index represented by $\mathtt{m}+1$ to the index represented by
$\mathtt{n}$ in the same array $\mathsf{S}$. The target array fragment of the
merger is from the index represented by $\mathtt{i}$ to the index represented
by $\mathtt{n}$, in the array $\mathsf{T}$.

For the specification of the program, we use a few pieces of auxiliary
notation. We write ${X}^{h}_{l}$ for a triple $(X,l,h)$ that represents the
fragment of the array $X$ from the index $l$ to the index $h$. We write
$(\\!|{{X}^{h}_{l}}|\\!)_{\sigma}$ for the list
$[{\sigma(\ell+l),\dots,\sigma(\ell+h)}]$ where $\ell=\sigma(X)$, i.e., the
list of elements of the array $X$ from the index $l$ to the index $h$. We
write $\mathit{occ}\,{[{z_{1},\dots,z_{n}}]}$ for the function $h$ mapping
each integer $z$ to the number of occurrences of $z$ in the list
$[{z_{1},\dots,z_{n}}]$ of integers. For two such functions $h_{1}$ and
$h_{2}$, we write ${h_{1}}\oplus{h_{2}}$ for the function $\lambda
z.h_{1}(z)+h_{2}(z)$. We write $\mathit{sorted}\,{[{z_{1},\dots,z_{n}}]}$ to
express that the list $[{z_{1},\dots,z_{n}}]$ of integers is sorted in
ascending order. We write
$\mathit{sep}({{X}^{h_{1}}_{l_{1}}},{{Y}^{h_{2}}_{l_{2}}},{\sigma})$ to
express that the elements of the array $X$ from the index $l_{1}$ to the index
$h_{1}$ occupy a separate memory area from that occupied by the elements of
the array $Y$ from the index $l_{2}$ to the index $h_{2}$, in the state
$\sigma$. In addition, we write
$[{{u_{1},\dots,u_{n}}}]^{\sigma^{\prime}}_{\sigma}$ to express for each
$i\in\\{1,\dots,n\\}$, the value of each $u_{i}$ is the same in the states
$\sigma$ and $\sigma^{\prime}$. Here, $u_{i}$ can be a variable $x$ or an
array fragment ${X}^{h}_{l}$. In the latter case, that the value of
${X}^{h}_{l}$ is the same in the two states means $\forall i:l\leq i\leq
h\Rightarrow\sigma(\sigma(X)+i)=\sigma^{\prime}(\sigma^{\prime}(X)+i)$.

For the program $\rho_{\mathrm{mg}}$, we devise the specification
$\Phi_{\mathrm{mga}}$. We denote the starting index for the first source array
fragment in $\mathsf{S}$ as well as for the target array fragment in
$\mathsf{T}$ by $l$. We use $l$ as a global parameter in the specification.

We specify the function $\mathsf{merge}$ as

$\displaystyle\Phi_{\mathrm{mga}}(\langle{{\mathsf{merge}}({X,Y,a_{\mathrm{l}},a_{\mathrm{m}},a_{\mathrm{h}}})\to{[{}]}},{\sigma}\rangle_{\rho_{\mathrm{ms}}})\,{:=}\,$
$\displaystyle\quad\begin{aligned}
&\\{\sigma^{\prime}\mid\mathit{occ}\,{(\\!|{{X}^{h}_{l}}|\\!)_{\sigma}}=\mathit{occ}\,{(\\!|{{Y}^{h}_{l}}|\\!)_{\sigma^{\prime}}}\,\land\,\mathit{sorted}\,{(\\!|{{Y}^{h}_{l}}|\\!)_{\sigma^{\prime}}}\,\\}\\\
\\\\[-9.68745pt]
&\mathrm{if}~{}\mathcal{A}\llbracket{a_{\mathrm{l}}}\rrbracket\sigma\\!=\\!l\,\land\,0\\!\leq\\!l\\!\leq\\!m\\!<\\!h\,\land\,\mathit{sorted}\,{(\\!|{{X}^{m}_{l}}|\\!)_{\sigma}}\land\mathit{sorted}\,{(\\!|{{X}^{h}_{m+1}}|\\!)_{\sigma}}\land\mathit{sep}({{X}^{h}_{l}},{{Y}^{h}_{l}},{\sigma})\\\
&\mathrm{where}~{}m=\mathcal{A}\llbracket{a_{\mathrm{m}}}\rrbracket\sigma\,\land\,h=\mathcal{A}\llbracket{a_{\mathrm{h}}}\rrbracket\sigma\end{aligned}$

This specification says that if we call the function $\mathsf{merge}$ with two
array identifiers $X$ and $Y$, and expressions $a_{\mathrm{l}}$,
$a_{\mathrm{m}}$, $a_{\mathrm{h}}$ that evaluate to $l$, $m$ and $h$, such
that

  * •

$0\leq l\leq m<h$ holds,

  * •

the array fragments ${X}^{m}_{l}$ and ${X}^{h}_{m+1}$ are sorted in the pre-
state,

  * •

the array fragments ${X}^{m}_{l}$ and ${X}^{h}_{m+1}$ are separated in the
pre-state,

then the number of occurrences of each integer in the target array fragment
${Y}^{h}_{l}$ in the post-state is the same as its number of occurrences in
the source array fragment ${X}^{h}_{l}$ in the pre-state, and the target array
fragment ${Y}^{h}_{l}$ is sorted in ascending order in the post-state.

The core part of the function $\mathsf{merge}$ is the loop statement
$S_{\mathrm{wh}}$ (see Fig. 3). We specify this loop as

$\displaystyle\Phi_{\mathrm{mga}}(\langle{S_{\mathrm{wh}}},{\sigma}\rangle_{\rho_{\mathrm{ms}}})\,{:=}\,$
$\displaystyle\quad\begin{aligned}
&\\{\sigma^{\prime}\mid(i\leq\sigma^{\prime}(\mathtt{i})=m+1\land
j\leq\sigma^{\prime}(\mathtt{j})\leq n\lor
j\leq\sigma^{\prime}(\mathtt{j})=n+1\land i\leq\sigma^{\prime}(\mathtt{i})\leq
m)\,\land\,\\\
&\qquad~{}\sigma^{\prime}(\mathtt{k})=k+\sigma^{\prime}(\mathtt{i})-i+\sigma^{\prime}(\mathtt{j})-j\,\land\,[{{\mathtt{m},\mathtt{n},\mathsf{S},\mathsf{T},{\mathsf{S}}^{n}_{l},{\mathsf{T}}^{k-1}_{l}}}]^{\sigma^{\prime}}_{\sigma}\,\land\,\\\
&\qquad~{}{\mathit{occ}\,{(\\!|{{\mathsf{S}}^{\sigma^{\prime}(\mathtt{i})-1}_{i}}|\\!)_{\sigma}}}\oplus{\mathit{occ}\,{(\\!|{{\mathsf{S}}^{\sigma^{\prime}(\mathtt{j})-1}_{j}}|\\!)_{\sigma}}}=\mathit{occ}\,{(\\!|{{\mathsf{T}}^{\sigma^{\prime}(\mathtt{k})-1}_{k}}|\\!)_{\sigma^{\prime}}}\,\land\,\mathit{sorted}\,{(\\!|{{\mathsf{T}}^{\sigma^{\prime}(\mathtt{k})-1}_{l}}|\\!)_{\sigma^{\prime}}}\,\land\,\\\
&\qquad~{}(\sigma^{\prime}(\mathtt{i})\leq
m\land\sigma^{\prime}(\mathtt{k})\geq
l+1\Rightarrow\mathcal{A}\llbracket{{\mathsf{S}}[{\mathtt{i}}]}\rrbracket\sigma^{\prime}\\!\geq\\!\mathcal{A}\llbracket{{\mathsf{T}}[{\mathtt{k}\\!-\\!1}]}\rrbracket\sigma^{\prime})\,\land\,\\\
&\qquad~{}(\sigma^{\prime}(\mathtt{j})\leq
n\land\sigma^{\prime}(\mathtt{k})\geq
l+1\Rightarrow\mathcal{A}\llbracket{{\mathsf{S}}[{\mathtt{j}}]}\rrbracket\sigma^{\prime}\\!\geq\\!\mathcal{A}\llbracket{{\mathsf{T}}[{\mathtt{k}\\!-\\!1}]}\rrbracket\sigma^{\prime})\,\\}\\\
\\\\[-9.68745pt] &\mathrm{if}~{}0\leq l\leq i\leq m<j\leq
n\,\land\,k=i+j-m-1\,\land\,\\\ &\quad(k\geq
l+1\,\Rightarrow\,\mathcal{A}\llbracket{{\mathsf{S}}[{\mathtt{i}}]}\rrbracket\sigma\\!\geq\\!\mathcal{A}\llbracket{{\mathsf{T}}[{\mathtt{k}\\!-\\!1}]}\rrbracket\sigma\land\mathcal{A}\llbracket{{\mathsf{S}}[{\mathtt{j}}]}\rrbracket\sigma\\!\geq\\!\mathcal{A}\llbracket{{\mathsf{T}}[{\mathtt{k}\\!-\\!1}]}\rrbracket\sigma)\,\land\,\\\
&\quad\mathit{sorted}\,{(\\!|{{\mathsf{S}}^{m}_{i}}|\\!)_{\sigma}}\,\land\,\mathit{sorted}\,{(\\!|{{\mathsf{S}}^{n}_{j}}|\\!)_{\sigma}}\,\land\,\mathit{sorted}\,{(\\!|{{\mathsf{T}}^{k-1}_{l}}|\\!)_{\sigma}}\,\land\,\mathit{sep}({{\mathsf{S}}^{n}_{l}},{{\mathsf{T}}^{n}_{l}},{\sigma})\\\
&\mathrm{where}~{}i=\sigma(\mathtt{i})\,\land\,j=\sigma(\mathtt{j})\,\land\,k=\sigma(\mathtt{k})\,\land\,m=\sigma(\mathtt{m})\,\land\,n=\sigma(\mathtt{n})\end{aligned}$

In the specification, we are concerned with pre-states in which either the
overall loop is yet to be executed, or some rounds of the loop have been
completed and some further rounds are to be executed. We constrain these pre-
states with a few further conditions. One of these conditions states that the
elements with indexes $\mathtt{i}$ and $\mathtt{j}$ that are to be compared in
the next round are both greater than or equal to the last element that has
been set in the target array fragment. For each pre-state that satisfies all
the conditions in the “if” part, several conditions are asserted for the
potential post-state $\sigma^{\prime}$. A key condition here says that the two
fragments ${\mathsf{S}}^{\sigma^{\prime}(\mathtt{i})-1}_{i}$ and
${\mathsf{S}}^{\sigma^{\prime}(\mathtt{j})-1}_{j}$ in the source array that
are scanned between the reaching of the pre-state and the post-state agree
with the fragment ${\mathsf{T}}^{\sigma^{\prime}(\mathtt{k})-1}_{k}$ that is
filled between the reaching of the pre-state and the post-state. Another key
condition says that the fragment
${\mathsf{T}}^{\sigma^{\prime}(\mathtt{k})-1}_{l}$ of the target array that is
already filled in the post-state for the loop is sorted in ascending order.

Without specification inference, the two remaining loops in the array-merging
program also need to be explicitly specified. The specification of these two
loops is much less involved than that for the first loop, and it is defered to
Appendix 0.A. With the technique of Section 3, the validity of
$\Phi_{\mathrm{mga}}$ can be established.

###### Theorem 5.1

It holds that $\mathit{valid}({\Phi_{\mathrm{mga}}})$.

With the help of Theorem 3.1, the proof requires no induction for reasoning
about the loops. This proof boils down to symbolic execution with the help of
a series of auxiliary lemmas about the memory layout.

###### Remark 2

The global parameter $l$ in the specification $\Phi_{\mathrm{mga}}$ relates
the auxiliary information about calls to $\mathsf{merge}$ and about the loops
in this function. The role of $l$ can be compared to that of a logical
variable in a concrete program logic. Such global parameters are captured in
the Coq formalization by an explicit argument in the specifications. The type
of this argument can be instantiated according to the needs in verifying each
specific program. The verification of a program is required to go through for
all possible values of this argument.

###  5.2 Eager Functional Language and List-Merging Program

#### Eager Functional Language

The language considered in this section is a fragment of the eager functional
language as discussed in [27]. The expressions and canonical forms of this
language are given in Fig. 4.

$\displaystyle e\,::=~{}$ $\displaystyle
n\mid\mathsf{true}\mid\mathsf{false}\mid$
$\displaystyle{e}+{e}\mid{e}-{e}\mid{e}*{e}\mid{e}/{e}\mid$
$\displaystyle{e}={e}\mid{e}<{e}\mid\lnot{e}\mid{e}\land{e}\mid$
$\displaystyle\mathsf{if}~{}{e}~{}\mathsf{then}~{}{e}~{}\mathsf{else}~{}{e}\mid$
$\displaystyle\mathsf{nil}\mid{e}::{e}\mid\mathsf{listcase}~{}{e}~{}\mathsf{of}~{}({e},{e})\mid$
$\displaystyle
x\mid{e}\,{e}\mid\lambda{x}.{e}\mid\mathsf{letrec}~{}{x}={\lambda{x^{\prime}}.{e}}~{}\mathsf{in}~{}{e}$

$\displaystyle\mathit{cf}\,::=\,$
$\displaystyle\mathit{icf}\mid\mathit{bcf}\mid\mathit{fcf}\mid\mathit{lcf}$
$\displaystyle\mathit{icf}\,::=\,$ $\displaystyle\ldots\mid-2\mid-1\mid 0\mid
1\mid 2\mid\ldots$ $\displaystyle\mathit{bcf}\,::=\,$
$\displaystyle\mathsf{true}\mid\mathsf{false}$
$\displaystyle\mathit{fcf}\,::=\,$ $\displaystyle\lambda{x}.{e}$
$\displaystyle\mathit{lcf}\,::=\,$
$\displaystyle\mathsf{nil}\mid{\mathit{cf}}::{\mathit{cf}}$

Figure 4: The expressions and canonical forms of the eager functional language

##### Syntax.

A program of the eager functional language is an expression. The syntax for
expressions is given in the left part of Fig. 4. Here, $n$ is a numeral, $x$
is a variable, ${e}\,{e^{\prime}}$ is an application, $\lambda{x}.{e}$ is a
lambda abstraction, $\mathsf{nil}$ is the empty list, and ${e_{1}}::{e_{2}}$
is the list obtained by prefixing the list $e_{2}$ with the element $e_{1}$.
The expression
$\mathsf{listcase}~{}{e}~{}\mathsf{of}~{}({e^{\prime}},{e^{\prime\prime}})$
branches to $e^{\prime}$ or $e^{\prime\prime}$ depending on whether the result
of $e$ is the empty list $\mathsf{nil}$. The expression
$\mathsf{letrec}~{}{x}={\lambda{x^{\prime}}.{e^{\prime}}}~{}\mathsf{in}~{}{e}$
binds $x$ to $\lambda{x^{\prime}}.{e^{\prime}}$ in $e$. This expression allows
$x$ to be used in $e^{\prime}$, thereby allowing recursion.

##### Semantics.

The evaluation of the expressions results in canonical forms $\mathit{cf}$ as
given in the right part of Fig. 4. A canonical form $\mathit{cf}$ can be a
canonical form for integers ($\mathit{icf}$), a canonical form for Boolean
values ($\mathit{bcf}$), a canonical form for functions ($\mathit{fcf}$), or a
canonical form for lists ($\mathit{lcf}$).

$\displaystyle\mathit{rule}~{}{[\,]}~{}{(\mathit{cf},\mathit{cf})}$
$\displaystyle\mathit{rule}~{}{[(e_{1},\mathit{icf}_{\\!1}),(e_{2},\mathit{icf}_{\\!2})]}~{}{(e_{1}\,\mathit{op}\,e_{2},\llbracket{\mathit{op}}\rrbracket_{\mathrm{icf}}(\mathit{icf}_{\\!1},\mathit{icf}_{\\!2}))}~{}\mathrm{where}~{}\mathit{op}\in\\{+,-,*,/,=,<\\}$
$\displaystyle\mathit{rule}~{}{[(e,\mathit{bcf})]}~{}{(\lnot
e,\llbracket{\lnot}\rrbracket_{\mathrm{bcf}}(\mathit{bcf}))}$
$\displaystyle\mathit{rule}~{}{[(e_{1},\mathit{bcf}_{\\!1}),(e_{2},\mathit{bcf}_{\\!2})]}~{}{(e_{1}\,\land\,e_{2},\llbracket{\land}\rrbracket_{\mathrm{bcf}}(\mathit{bcf}_{\\!1},\mathit{bcf}_{\\!2}))}$
$\displaystyle\mathit{rule}~{}{[(e,\mathsf{true}),(e^{\prime},\mathit{cf})]}~{}{(\mathsf{if}~{}{e}~{}\mathsf{then}~{}{e^{\prime}}~{}\mathsf{else}~{}{e^{\prime\prime}},\mathit{cf})}$
$\displaystyle\mathit{rule}~{}{[(e,\mathsf{false}),(e^{\prime\prime},\mathit{cf})]}~{}{(\mathsf{if}~{}{e}~{}\mathsf{then}~{}{e^{\prime}}~{}\mathsf{else}~{}{e^{\prime\prime}},\mathit{cf})}$
$\displaystyle\mathit{rule}~{}{[(e,\mathit{cf}),(e^{\prime},\mathit{cf}^{\prime})]}~{}{({e}::{e^{\prime}},{\mathit{cf}}::{\mathit{cf}^{\prime}})}$
$\displaystyle\mathit{rule}~{}{[(e,\mathsf{nil}),(e^{\prime},\mathit{cf})]}~{}{(\mathsf{listcase}~{}{e}~{}\mathsf{of}~{}({e^{\prime}},{e^{\prime\prime}}),\mathit{cf})}$
$\displaystyle\mathit{rule}~{}{[(e,{\mathit{cf}}::{\mathit{cf}^{\prime}}),({{e^{\prime\prime}}\,{\mathit{cf}}}\,{\mathit{cf}^{\prime}},\mathit{cf}^{\prime\prime})]}~{}{(\mathsf{listcase}~{}{e}~{}\mathsf{of}~{}({e^{\prime}},{e^{\prime\prime}}),\mathit{cf}^{\prime\prime})}$
$\displaystyle\mathit{rule}~{}{[(e,\lambda{x}.{e^{\prime\prime}}),(e^{\prime},\mathit{cf}^{\prime}),(e^{\prime\prime}[\mathit{cf}^{\prime}/x],\mathit{cf})]}~{}{({e}\,{e^{\prime}},\mathit{cf})}$
$\displaystyle\mathit{rule}~{}{[({(\lambda{x}.{e})}\,{(\lambda{x^{\prime}}.{\mathsf{letrec}~{}{x}={\lambda{x^{\prime}}.{e^{\prime}}}~{}\mathsf{in}~{}{e^{\prime}}})},\mathit{cf})]}~{}{(\mathsf{letrec}~{}{x}={\lambda{x^{\prime}}.{e^{\prime}}}~{}\mathsf{in}~{}{e},\mathit{cf})}~{}~{}\mathrm{if}~{}x^{\prime}\neq
x$ Figure 5: The semantic rules for the eager functional language

We formulate the big-step semantics of the eager functional language by
defining the predicate $\mathit{rule}$ as in Fig. 5. In this figure, the fist
rule says that an expression that is a canonical form evaluates to itself. In
the next few rules, $\llbracket{\mathit{op}}\rrbracket_{\mathrm{icf}}$ is used
to represent the interpretation of the binary operation $\mathit{op}$ on
integer canonical forms. In addition,
$\llbracket{\lnot}\rrbracket_{\mathrm{bcf}}$ and
$\llbracket{\land}\rrbracket_{\mathrm{bcf}}$ represent the interpretations of
the logical operations $\lnot$ and $\land$, respectively, on Boolean canonical
forms. The expression ${e}[{\mathit{cf}}/{x}]$ represents substitutions of
$\mathit{cf}$ for $x$ in $e$. This expression is defined in Appendix 0.B. In
the rule for $\mathsf{letrec}$, the evaluation of the expression
$\mathsf{letrec}~{}{x}={\lambda{x^{\prime}}.{e}^{\prime}}~{}\mathsf{in}~{}{e}$
is turned into the evaluation of
${(\lambda{x}.{e})}\,{(\lambda{x^{\prime}}.{\mathsf{letrec}~{}{x}={\lambda{x^{\prime}}.{e^{\prime}}}~{}\mathsf{in}~{}{e^{\prime}}})}$.
Intuitively, when $e$ is evaluated, $x$ can be applied as
$(\lambda{x^{\prime}}.{\mathsf{letrec}~{}{x}={\lambda{x^{\prime}}.{e^{\prime}}}~{}\mathsf{in}~{}{e^{\prime}}})$.
When the second $e^{\prime}$ in
$(\lambda{x^{\prime}}.{\mathsf{letrec}~{}{x}={\lambda{x^{\prime}}.{e^{\prime}}}~{}\mathsf{in}~{}{e^{\prime}}})$
is evaluated, the name $x$ is still available and bound to a
$\lambda$-abstraction.

#### List-Merging Program and its Verification

The program $e_{\mathrm{mg}}(\mathit{lcf}_{\\!1},\mathit{lcf}_{\\!2})$ below
merges two sorted lists into a single sorted list. More concretely, the
variable $\mathsf{merge}$ is bound to the expression
$\lambda\mathtt{x}.\lambda\mathtt{x^{\prime}}.e_{\mathrm{lcase}}$ that
destructs the lists that are bound to $\mathtt{x}$ and $\mathtt{x^{\prime}}$,
respectively. In case one of the lists is empty, the result of the merger is
the other list. Otherwise, the result of the merger is obtained by prefixing
the smaller head element of the two given lists over the merging result of the
remaining parts of the lists.

$\displaystyle
e_{\mathrm{mg}}(\mathit{lcf}_{\\!1},\mathit{lcf}_{\\!2})\,{:=}\,$
$\displaystyle\mathsf{letrec}~{}\mathtt{merge}=(\lambda\mathtt{x}.\lambda\mathtt{x^{\prime}}.e_{\mathrm{lcase}})~{}\mathsf{in}~{}{{\mathtt{merge}}\,{\mathit{lcf}_{\\!1}}}\,{\mathit{lcf}_{\\!2}}$
$\displaystyle e_{\mathrm{lcase}}\,{:=}\,$
$\displaystyle\mathsf{listcase}~{}\mathtt{x}~{}\mathsf{of}~{}(\mathtt{x^{\prime}},\lambda\mathtt{i}.\lambda\mathtt{r}.\mathsf{listcase}~{}\mathtt{x^{\prime}}~{}\mathsf{of}~{}(\mathtt{x},\lambda\mathtt{i^{\prime}}.\lambda\mathtt{r^{\prime}}.e_{\mathrm{if}}))$
$\displaystyle e_{\mathrm{if}}\,{:=}\,$
$\displaystyle\mathsf{if}~{}{\mathtt{i}\leq\mathtt{i^{\prime}}}~{}\mathsf{then}~{}{{\mathtt{i}}::{{{\mathtt{merge}}\,{\mathtt{r}}}\,{\mathtt{x^{\prime}}}}}~{}\mathsf{else}~{}{{\mathtt{i}^{\prime}}::{{{\mathtt{merge}}\,{\mathtt{x}}}\,{\mathtt{r^{\prime}}}}}$

To develop a specification for the list-merging program, we define a piece of
auxiliary notation. We write $\langle\\!|{\mathit{lcf}}|\\!\rangle$ for the
mathematical list of integers represented by the canonical form $\mathit{lcf}$
for lists. Formally, we define $\langle\\!|{\mathsf{nil}}|\\!\rangle{:=}[\,]$,
$\langle\\!|{{\mathit{icf}}::{\mathit{lcf}}}|\\!\rangle$
${:=}{\mathit{icf}}::{\mathit{zs}}$ if
$\mathit{zs}=\langle\\!|{\mathit{lcf}}|\\!\rangle\,\land\,\mathit{zs}\in\mathbb{Z}^{*}$,
and $\langle\\!|{\mathit{lcf}}|\\!\rangle{:=}\bot$ otherwise.

We devise the a specification for the list-merging program,
$\Phi_{\mathrm{mgl}}$. Using the function $\mathit{occ}$ and the predicate
$\mathit{sorted}$ introduced in Section 5.1, we specify the expression
$e_{\mathrm{mg}}(\mathit{lcf}_{\\!1},\mathit{lcf}_{\\!2})$ as

$\displaystyle\begin{aligned}
&\Phi_{\mathrm{mgl}}(e_{\mathrm{mg}}(\mathit{lcf}_{\\!1},\mathit{lcf}_{\\!2}))\,{:=}\,\\\
&\qquad\\{\mathit{lcf}\mid\exists\mathit{zs}\in\mathbb{Z}^{*}\\!:\mathit{zs}=\langle\\!|{\mathit{lcf}}|\\!\rangle\,\land\mathit{occ}\,{\mathit{zs}}={\mathit{occ}\,{\mathit{zs}_{1}}}\oplus{\mathit{occ}\,{\mathit{zs}_{2}}}\,\land\,\mathit{sorted}\,{\mathit{zs}}\\}\end{aligned}$
$\displaystyle\mathrm{if}~{}\mathit{zs}_{1}\in\mathbb{Z}^{*}\,\land\,\mathit{zs}_{2}\in\mathbb{Z}^{*}\,\land\,\mathit{sorted}\,{\mathit{zs}_{1}}\,\land\,\mathit{sorted}\,{\mathit{zs}_{2}}$
$\displaystyle\mathrm{where}~{}\mathit{zs}_{1}=\langle\\!|{\mathit{lcf}_{\\!1}}|\\!\rangle\,\land\,\mathit{zs}_{2}=\langle\\!|{\mathit{lcf}_{\\!2}}|\\!\rangle$

This specification says that given list canonical forms $\mathit{lcf}_{\\!1}$
and $\mathit{lcf}_{\\!2}$ that are both sorted in ascending order, the result
of executing $e_{\mathrm{mg}}(\mathit{lcf}_{\\!1},\mathit{lcf}_{\\!2})$ is a
list canonical form $\mathit{lcf}$. The list canonical form $\mathit{lcf}$
contains the elements as contained in either $\mathit{lcf}_{\\!1}$ or
$\mathit{lcf}_{\\!2}$. Furthermore, the list canonical form $\mathit{lcf}$ is
sorted in ascending order.

To support the verification of the specification for
$e_{\mathrm{mg}}(\mathit{lcf}_{\\!1},\mathit{lcf}_{\\!2})$, we specify an
unfolded form of this expression. The execution of this unfolded form either
terminates directly, or gives the same form again.

$\displaystyle\begin{aligned}
&\Phi_{\mathrm{mgl}}(\,(\lambda{\mathtt{x}}.{\mathsf{letrec}~{}{\mathsf{merge}}={\lambda{\mathtt{x}}.{\lambda{\mathtt{x^{\prime}}}.{e_{\mathrm{lcase}}}}}~{}\mathsf{in}~{}{\lambda{\mathtt{x^{\prime}}}.{e_{\mathrm{lcase}}}}})\,\,\mathit{lcf}_{\\!1}\,\mathit{lcf}_{\\!2}\,)\,{:=}\,\\\
&\qquad\\{\mathit{lcf}\mid\exists\mathit{zs}\in\mathbb{Z}^{*}\\!:\mathit{zs}=\langle\\!|{\mathit{lcf}}|\\!\rangle\,\land\,\mathit{occ}\,{\mathit{zs}}={\mathit{occ}\,{\mathit{lcf}_{\\!1}}}\oplus{\mathit{occ}\,{\mathit{lcf}_{\\!2}}}\,\land\,\mathit{sorted}\,{\mathit{zs}}\\}\end{aligned}$
$\displaystyle\mathrm{if}~{}\mathit{zs}_{1}\in\mathbb{Z}^{*}\,\land\,\mathit{zs}_{2}\in\mathbb{Z}^{*}\,\land\,\mathit{sorted}\,{\mathit{zs}_{1}}\,\land\,\mathit{sorted}\,{\mathit{zs}_{2}}$
$\displaystyle\mathrm{where}~{}\mathit{zs}_{1}=\langle\\!|{\mathit{lcf}_{\\!1}}|\\!\rangle\,\land\,\mathit{zs}_{2}=\langle\\!|{\mathit{lcf}_{\\!2}}|\\!\rangle$

This specification reflects that the unfolded expression
$(\lambda\mathtt{x}.\mathsf{letrec}~{}\mathsf{merge}\,=\,\lambda\mathtt{x}.\lambda\mathtt{x^{\prime}}.$
$e_{\mathrm{lcase}}\,\mathsf{in}\,\lambda\mathtt{x^{\prime}}.e_{\mathrm{lcase}})\,\,\mathit{lcf}_{\\!1}\,\mathit{lcf}_{\\!2}$
delivers analogous guarantees to those delivered by the original expression
$e_{\mathrm{mg}}(\mathit{lcf}_{\\!1},\mathit{lcf}_{\\!2})$.

With the technique of Section 3, the validity of $\Phi_{\mathrm{mgl}}$ can be
established.

###### Theorem 5.2

It holds that $\mathit{valid}({\Phi_{\mathrm{mgl}}})$.

With the help of Theorem 3.1, the proof requires no induction for reasoning
about the recursive applications of the function bound to $\mathsf{merge}$.
This proof boils down to symbolic execution with the help of a few auxiliary
lemmas about substitution and evaluation related to canonical forms.

###### Remark 3

It might appear that the auxiliary information needed for the verification of
the list-merging program should be for expressions of the form
$\mathsf{merge}~{}{\\_}~{}{\\_}$. However, these expressions cannot be
evaluated, because information about the actual function bound to
$\mathsf{merge}$ is missing. The form that recurs in the evaluation of
$e_{\mathrm{mg}}(\mathit{lcf}_{\\!1},\mathit{lcf}_{\\!2})$ is actually
$(\lambda{\mathtt{x}}.{\mathsf{letrec}~{}{\mathsf{merge}}={\lambda{\mathtt{x}}.{\lambda{\mathtt{x^{\prime}}}.{e_{\mathrm{lcase}}}}}~{}\mathsf{in}~{}{\lambda{\mathtt{x^{\prime}}}.{e_{\mathrm{lcase}}}}})\,\,{\\_}\,\,{\\_}$.

##  6 On Completeness of the Technique

It is untrue that any valid specification can be verified. Intuitively, a
specification $\Phi$ that is valid but missing the necessary auxiliary
information such as loop invariants might not be verifiable. However, we show
that there is always a more informative specification $\Phi^{\prime}$ than
$\Phi$ that is verifiable.

Formally, a specification $\Phi_{2}$ is _at least as informative as_ a
specification $\Phi_{1}$, as denoted by ${\Phi_{1}}\preceq{\Phi_{2}}$, if for
each configurations $c$, it holds that $\Phi_{1}(c)\supseteq\Phi_{2}(c)$.

The lemma below says the specification mapping each configuration to the set
of all the semantically derivable result configurations can be verified.

###### Lemma 2

Let $\Phi_{\star}{:=}\lambda c.\\{r\mid\mathit{deriv}({c,r})\\}$. Then,
$\mathit{verif}({\Phi_{\star}})$ can be established.

###### Proof

See Appendix 0.C and the mechanization in Coq. ∎

The following theorem says that for each valid specification $\Phi$, there is
a valid specification that is at least as informative as $\Phi$, and that can
be verified.

######  Theorem 6.1 (Relative Completeness)

For each valid specification $\Phi$, there exists a specification
$\Phi^{\prime}$ such that ${\Phi}\preceq{\Phi^{\prime}}$, and
$\mathit{verif}({\Phi^{\prime}})$ can be established.

###### Proof

It is not difficult to show that the specification $\Phi_{\star}$ is at least
as informative as any valid specification. Thus, the conclusion of the theorem
follows from Lemma 2. ∎

If the program contained in a configuration exhibits only bounded behavior,
then the corresponding result configuration can be obtained through symbolic
execution. Hence, it is not necessary that a verifiable specification should
cover these configurations. In an informal sense, this argument supports that
for a specification to be verified, it is only necessary to provide auxiliary
information about constructs such as loops and recursive function calls in the
specification.

##  7 Discussion

#### Reuse of Existing Formalization of Semantics

With the verification techniques based on small-step semantics [23, 22], it is
not difficult to obtain a verification infrastructure by reusing an existing
formalization of semantics. This is because a small-step semantics readily
provides a step relation that can be used to interface with the verification
framework. In comparison, we have only shown that our language-independent
verification technique can be applied after the big-step semantics of the
target language is formalized via a predicate that explicitly captures the
premises and conclusions of the semantic rules. Although we have demonstrated
in Section 5 with different types of languages that the big-step semantics
formulated using this predicate closely resemble their classical formulation,
it is desirable if a higher level of reusability can be enabled. A potential
solution is to construct a program that automatically transforms a
formalization of big-step semantics into a formulation with the
$\mathit{rule}$ predicate.

#### Integration of Techniques Dealing with other Aspects

The purpose of the present work is not to simplify the overall task of
deductive program verification beyond achievable by existing techniques.
Instead, the focus has been the simplification of the verification for
constructs causing potentially unbounded behavior, based on a common model of
big-step operational semantics. To construct a full-fledged language-
independent program verifier in a proof assistant, effective treatment of
other aspects of deductive program verification (e.g., memory layout,
mathematical reasoning for specific problem domains, etc.), as well as further
techniques for increasing the level of automation, is required. Existing work
in program logics, program verifiers, and theory libraries in proof assistants
are expected to be a crucial source of inspiration as well as concrete
technical components in dealing with the remaining aspects of the
verification.

##  8 Conclusion

To tackle the problem caused by the proliferation of programming languages in
deductive program verification, we provide a technique to address the cross-
cutting concern of reasoning about language features causing unbounded
behavior, including loops and recursive function calls. The technique can be
applied to any programming language, as long as the big-step operational
semantics of the language is formulated with an explicit characterization of
the premises and conclusions of inference rules. The user of this technique
need not set up inductions for the loops and recursive calls in performing a
program proof, but formulates invariants and function contracts in a uniform
style with a specification, and perform symbolic execution of the program with
the help of this specification. The technique admits succinct, inductive
arguments for soundness and relative completeness that are verified in the Coq
proof assistant along with other formal claims [8]. It has been illustrated
with verification examples targeting languages of different paradigms. It
provides a basis for a language-independent tool for program verification
based on big-step operational semantics in proof assistants.

#### Acknowledgment

The research was supported by the National Natural Science Foundation of China
(61876111, 61877040, 62002246), the general project numbered KM202010028010 of
Beijing Municipal Education Commission, and the Open Project CARCH201920 of
State Key Laboratory of Computer Architecture, Institute of Computing
Technology, Chinese Academy of Sciences.

## References

  * [1] The Coq proof assistant.  https://coq.inria.fr/.
  * [2] Michelson – the language of Tezos.  https://www.michelson.org/.
  * [3] The move language.  https://developers.libra-china.org/docs/crates/move-language/index.html.
  * [4] A sequential imperative programming language – syntax, semantics, Hoare logics and verification environment.  https://www.isa-afp.org/entries/Simpl.html.
  * [5] Solidity.  https://docs.soliditylang.org/en/v0.8.0/.
  * [6] VCC: A verifier for concurrent C.  https://www.microsoft.com/en-us/research/project/vcc-a-verifier-for-concurrent-c/.
  * [7] Yul.  https://docs.soliditylang.org/en/v0.8.0/yul.html.
  * [8] Formalization of the verification technique in Coq.  https://github.com/lixm/ind-verify/tree/master, 2021.
  * [9] W. Ahrendt, B. Beckert, R. Bubel, R. Hähnle, P. H. Schmitt, and M. Ulbrich, editors.  Deductive Software Verification - The KeY Book - From Theory to Practice, volume 10001 of Lecture Notes in Computer Science.  Springer, 2016.
  * [10] A. W. Appel.  Verified software toolchain - (invited talk).  In Proceedings of 20th European Symposium on Programming (ESOP), pages 1–17, 2011.
  * [11] S. Blazy and X. Leroy.  Mechanized semantics for the Clight subset of the C language.  Journal of Automated Reasoning, 43(3):263–288, 2009.
  * [12] M. Bodin, P. Gardner, T. P. Jensen, and A. Schmitt.  Skeletal semantics and their interpretations.  Proc. ACM Program. Lang., 3(POPL):44:1–44:31, 2019.
  * [13] M. Bodin, T. P. Jensen, and A. Schmitt.  Certified abstract interpretation with pretty-big-step semantics.  In Proceedings of the 2015 Conference on Certified Programs and Proofs (CPP), pages 29–40, 2015.
  * [14] D. Clément, J. Despeyroux, T. Despeyroux, and G. Kahn.  A simple applicative language: Mini-ML.  In Proceedings of the 1986 ACM Conference on LISP and Functional Programming (LFP), pages 13–27, 1986.
  * [15] P. Cousot and R. Cousot.  Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints.  In Fourth ACM Symposium on Principles of Programming Languages (POPL), pages 238–252, 1977.
  * [16] Y. Hirai.  Defining the ethereum virtual machine for interactive theorem provers.  In Financial Cryptography and Data Security - FC 2017 International Workshops, pages 520–535, 2017.
  * [17] C. A. R. Hoare.  An axiomatic basis for computer programming.  Communications of the ACM, 12(10):576–580, 1969.
  * [18] R. Jung, R. Krebbers, J. Jourdan, A. Bizjak, L. Birkedal, and D. Dreyer.  Iris from the ground up: A modular foundation for higher-order concurrent separation logic.  Journal of Functional Programming, 28:e20, 2018.
  * [19] G. Kahn.  Natural semantics.  In Proceedings of 4th Annual Symposium on Theoretical Aspects of Computer Science (STACS), pages 22–39, 1987.
  * [20] G. Klein and T. Nipkow.  Jinja is not Java.  Arch. Formal Proofs, 2005.
  * [21] J. McCarthy.  Towards a mathematical science of computation.  In Information Processing, Proceedings of the 2nd IFIP Congress, pages 21–28, 1962.
  * [22] B. M. Moore, L. Peña, and G. Rosu.  Program verification by coinduction.  In Programming Languages and Systems - Proceedings of 27th European Symposium on Programming (ESOP), pages 589–618, 2018.
  * [23] J. S. Moore.  Inductive assertions and operational semantics.  In Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference (CHARME), pages 289–303, 2003\.
  * [24] H. R. Nielson and F. Nielson.  Semantics with Applications: An Appetizer.  Undergraduate Topics in Computer Science. Springer, 2007.
  * [25] T. Nipkow and D. von Oheimb.  Java _${}_{\mbox{light}}$_ is type-safe - definitely.  In Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 161–170, 1998.
  * [26] G. D. Plotkin.  A structural approach to operational semantics.  Lecture notes, DAIMI FN-19, 1981.
  * [27] J. C. Reynolds.  Theories of programming languages.  Cambridge University Press, 1998.
  * [28] J. C. Reynolds.  Separation logic: A logic for shared mutable data structures.  In Proceeding of 17th IEEE Symposium on Logic in Computer Science (LICS), pages 55–74, 2002.
  * [29] D. A. Schmidt.  Natural-semantics-based abstract interpretation (preliminary version).  In Proceedings of Second International Symposium on Static Analysis (SAS), pages 1–18, 1995.
  * [30] I. Sergey, V. Nagaraj, J. Johannsen, A. Kumar, A. Trunov, and K. C. G. Hao.  Safer smart contract programming with Scilla.  Proc. ACM Program. Lang., 3(OOPSLA):185:1–185:30, 2019.
  * [31] T. A. L. Sewell, M. O. Myreen, and G. Klein.  Translation validation for a verified OS kernel.  In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 471–482, 2013.
  * [32] A. Stefanescu, D. Park, S. Yuwen, Y. Li, and G. Rosu.  Semantics-based program verifiers for all languages.  In 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pages 74–91, 2016\.
  * [33] G. Wood.  Ethereum: A secure decentralised generlised transaction ledger.  https://gavwood.com/paper.pdf.
  * [34] Z. Yang and H. Lei.  Lolisa: Formal syntax and semantics for a subset of the Solidity programming language.  CoRR, abs/1803.09885, 2018.

##  Appendix 0.A Supplementary Material for Section 5.1

#### Definitions for the Extended While Language

We define the evaluation function $\mathcal{A}$ for arithmetic expressions
below.

$\displaystyle\mathcal{A}\llbracket{n}\rrbracket\sigma~{}{:=}~{}$
$\displaystyle\mathcal{N}\llbracket{n}\rrbracket$
$\displaystyle\mathcal{A}\llbracket{x}\rrbracket\sigma~{}{:=}~{}$
$\displaystyle\sigma(x)$
$\displaystyle\mathcal{A}\llbracket{X}\rrbracket\sigma~{}{:=}~{}$
$\displaystyle\sigma(X)$
$\displaystyle\mathcal{A}\llbracket{{X}[{a_{1}}]}\rrbracket\sigma~{}{:=}~{}$
$\displaystyle\begin{cases}\sigma(\ell+z)&\mathrm{if}~{}\exists\ell,z:\ell=\mathcal{A}\llbracket{X}\rrbracket\sigma\,\land\,z=\mathcal{A}\llbracket{a_{1}}\rrbracket\sigma\geq
0\,\land\,\ell+z<\iota\\\ \bot&\mathrm{otherwise}\end{cases}$
$\displaystyle\mathcal{A}\llbracket{a_{1}\,\mathit{aop}\,a_{2}}\rrbracket\sigma~{}{:=}~{}$
$\displaystyle\llbracket{\mathit{aop}}\rrbracket(\mathcal{A}\llbracket{a_{1}}\rrbracket\sigma,\mathcal{A}\llbracket{a_{2}}\rrbracket\sigma)$

The evaluation of an array identifier $X$ in the state $\sigma$ yields the
starting location of the array identified by $\sigma$. The evaluation of the
array element expression ${a_{1}}[{a_{2}}]$ is the value at the location
$\ell+z$, where $\ell$ is the starting location of the array, and $z$ is the
index of the array element, if $z$ is non-negative, and the location is within
the range bounded by the next fresh location for arrays. Otherwise, the
evaluation of this expression yields the undefined value $\bot$.

We define the evaluation function $\mathcal{B}$ for Boolean expressions of the
extended While language as

$\displaystyle\mathcal{B}\llbracket{\mathsf{true}}\rrbracket\sigma~{}{:=}~{}$
$\displaystyle\mathit{tt}$
$\displaystyle\mathcal{B}\llbracket{\mathsf{false}}\rrbracket\sigma~{}{:=}~{}$
$\displaystyle\mathit{ff}$
$\displaystyle\mathcal{B}\llbracket{a_{1}\,\mathit{cop}\,a_{2}}\rrbracket\sigma~{}{:=}~{}$
$\displaystyle\llbracket{\mathit{cop}}\rrbracket(\mathcal{A}\llbracket{a_{1}}\rrbracket\sigma,\mathcal{A}\llbracket{a_{2}}\rrbracket\sigma)$
$\displaystyle\mathcal{B}\llbracket{{b_{1}}{\,\&\\!\&\,}{b_{2}}}\rrbracket\sigma~{}{:=}~{}$
$\displaystyle\begin{cases}\mathit{tt}&\mathrm{if}~{}\mathcal{B}\llbracket{b_{1}}\rrbracket\sigma=\mathit{tt}\land\mathcal{B}\llbracket{b_{2}}\rrbracket\sigma=\mathit{tt}\\\
\mathit{ff}&\mathrm{otherwise}\end{cases}$
$\displaystyle\mathcal{B}\llbracket{{!{b_{1}}}}\rrbracket\sigma~{}{:=}~{}$
$\displaystyle\lnot\mathcal{B}\llbracket{b_{1}}\rrbracket\sigma$

We denote by
$\mathit{call}\mbox{-}\mathit{ini}({s},{\mathit{ws}},{\mathit{vs}},{\mathit{xs}})$
the initial store for a function with parameters
$\mathit{ws}=[{w_{1},\dots,w_{m}}]$, argument values
$\mathit{vs}=[{v_{1},\dots,v_{m}}]$, and return variables
$\mathit{vs}=[{x_{1},\dots,x_{n}}]$, that is invoked when the store is $s$.
Formally,
$\mathit{call}\mbox{-}\mathit{ini}({s},{\mathit{ws}},{\mathit{vs}},{\mathit{xs}})$
is the store $s^{\prime}$ such that for each
$w\in\mathit{Var}\cup\mathit{Arr}$, it holds that

$s^{\prime}(w)=\begin{cases}v_{i}&\mathrm{if}~{}i\in\\{1,\dots,m\\}\,\land\,w=w_{i}\\\
0&\mathrm{if}~{}\exists i\in\\{1,\dots,n\\}:w=x_{i}\\\
\bot&\mathrm{otherwise}\end{cases}$

and for each $\ell\in\mathbb{N}$, it holds that $s^{\prime}(\ell)=s(\ell)$.

We denote by
$\mathit{call}\mbox{-}\mathit{fin}({s},{s^{\prime}},{\mathit{xs}},{\mathit{xs}^{\prime}})$
the final store resulting from a call to a function with return variables
$\mathit{xs}=[{x_{1},\dots,x_{n}}]$ and the variables
$\mathit{xs}^{\prime}=[{x^{\prime}_{1},\dots,x^{\prime}_{n}}]$ in the caller
receiving the return values. Here, $s$ is the store immediately before the
call, and $s^{\prime}$ is the store when the body of the callee stops
execution. Formally,
$\mathit{call}\mbox{-}\mathit{fin}({s},{s^{\prime}},{\mathit{xs}},{\mathit{xs}^{\prime}})$
is the store $s^{\prime\prime}$ such that for each
$w\in\mathit{Var}\cup\mathit{Arr}$, it holds that

$s^{\prime\prime}(w)=\begin{cases}s^{\prime}(x_{i})&\mathrm{if}~{}i\in\\{1,\dots,n\\}\,\land\,w=x^{\prime}_{i}\\\
s(w)&\mathrm{otherwise}\end{cases}$

and for each $\ell\in\mathbb{N}$, it holds that
$s^{\prime\prime}(\ell)=s^{\prime}(\ell)$.

#### Definitions for the Array-merging Program and its Verification

We define the expression
$\mathit{sep}({{X}^{h_{1}}_{l_{1}}},{{Y}^{h_{2}}_{l_{2}}},{\sigma})$ by

$\displaystyle\mathit{sep}({{X}^{h_{1}}_{l_{1}}},{{Y}^{h_{2}}_{l_{2}}},{\sigma})~{}{:=}~{}$
$\displaystyle\qquad\begin{aligned}
\exists\ell_{1},\ell_{2}\in\mathbb{Z}:\,&\sigma(X_{1})=\ell_{1}\,\land\,\sigma(X_{2})=\ell_{2}\,\land\,(\ell_{1}+h_{1}<\ell_{2}+l_{2}\lor\ell_{2}+h_{2}<\ell_{1}+l_{1})\end{aligned}$

We specify the second loop in the function $\mathsf{merge}$ as

$\displaystyle\Phi_{\mathrm{mga}}(\langle{S_{{\mathtt{i}},{\mathtt{m}}}},{\sigma}\rangle_{\rho_{\mathrm{ms}}})~{}{:=}~{}$
$\displaystyle\quad\begin{aligned}
\\{\sigma^{\prime}\mid\,&\sigma^{\prime}(\mathtt{i})\geq
i\,\land\,\sigma^{\prime}(\mathtt{i})=m+1\,\land\,\sigma^{\prime}(\mathtt{j})=j\,\land\,\sigma^{\prime}(\mathtt{k})=k+\sigma^{\prime}(\mathtt{i})-i\,\land\\\
&[{{\mathtt{m},\mathtt{n},\mathsf{T},{\mathsf{T}}^{k-1}_{l}}}]^{\sigma^{\prime}}_{\sigma}\,\land\,(\\!|{{\mathsf{S}}^{\sigma^{\prime}(\mathtt{i})-1}_{i}}|\\!)_{\sigma}=(\\!|{{\mathsf{T}}^{\sigma^{\prime}(\mathtt{k})-1}_{k}}|\\!)_{\sigma^{\prime}}\,\\}\end{aligned}$
$\displaystyle\mathrm{if}~{}0\leq l\leq i\leq
m<n\,\land\,j=n+1\,\land\,k=i+j-m-1\,\land\,\mathit{sep}({{\mathsf{S}}^{n}_{l}},{{\mathsf{T}}^{n}_{l}},{\sigma})$
$\displaystyle\mathrm{where}~{}i=\sigma(\mathtt{i})\,\land\,j=\sigma(\mathtt{j})\,\land\,k=\sigma(\mathtt{k})\,\land\,m=\sigma(\mathtt{m})\,\land\,n=\sigma(\mathtt{n})$

We specify the third (last) loop of the function $\mathsf{merge}$ as

$\displaystyle\Phi_{\mathrm{mga}}(\langle{S_{{\mathtt{j}},{\mathtt{n}}}},{\sigma}\rangle_{\rho_{\mathrm{ms}}})~{}{:=}~{}$
$\displaystyle\quad\begin{aligned}
\\{\sigma^{\prime}\mid\,&\sigma^{\prime}(\mathtt{i})=i\,\land\,\sigma^{\prime}(\mathtt{j})\geq
j\,\land\,\sigma^{\prime}(\mathtt{j})=n+1\,\land\,\sigma^{\prime}(\mathtt{k})=k+\sigma^{\prime}(\mathtt{j})-j\,\land\,\\\
&[{{\mathtt{m},\mathtt{n},\mathsf{T},{\mathsf{T}}^{k-1}_{l}}}]^{\sigma^{\prime}}_{\sigma}\,\land\,(\\!|{{\mathsf{S}}^{\sigma^{\prime}(\mathtt{j})-1}_{j}}|\\!)_{\sigma}=(\\!|{{\mathsf{T}}^{\sigma^{\prime}(\mathtt{k})-1}_{k}}|\\!)_{\sigma^{\prime}}\,\\}\end{aligned}$
$\displaystyle\mathrm{if}~{}0\leq l\,\leq m<\,j\leq
n\,\land\,i=m+1\,\land\,k=i+j-m-1\,\land\,\mathit{sep}({{\mathsf{S}}^{n}_{l}},{{\mathsf{T}}^{n}_{l}},{\sigma})$
$\displaystyle\mathrm{where}~{}i=\sigma(\mathtt{i})\,\land\,j=\sigma(\mathtt{j})\,\land\,k=\sigma(\mathtt{k})\,\land\,m=\sigma(\mathtt{m})\,\land\,n=\sigma(\mathtt{n})$

##  Appendix 0.B Supplementary Material for Section 5.2

We define the substitution of canonical forms for variables in expressions,
denoted by ${e}[{\mathit{cf}}/{x}]$, as follows.

$\displaystyle{n}[{\mathit{cf}}/{x}]\,{:=}\,$ $\displaystyle n$
$\displaystyle{\mathsf{true}}[{\mathit{cf}}/{x}]\,{:=}\,$
$\displaystyle\mathsf{true}$
$\displaystyle{\mathsf{false}}[{\mathit{cf}}/{x}]\,{:=}\,$
$\displaystyle\mathsf{false}$
$\displaystyle{(e_{1}\,\mathit{op}\,e_{2})}[{\mathit{cf}}/{x}]\,{:=}\,$
$\displaystyle{e_{1}}[{\mathit{cf}}/{x}]\,\mathit{op}\,{e_{2}}[{\mathit{cf}}/{x}]\quad\mathrm{where}~{}\mathit{op}\in\\{+,-,*,/,=,<\\}$
$\displaystyle{(\lnot e_{1})}[{\mathit{cf}}/{x}]\,{:=}\,$
$\displaystyle\lnot({e_{1}}[{\mathit{cf}}/{x}])$
$\displaystyle{({e_{1}}\land{e_{2}})}[{\mathit{cf}}/{x}]\,{:=}\,$
$\displaystyle{{e_{1}}[{\mathit{cf}}/{x}]}\land{{e_{2}}[{\mathit{cf}}/{x}]}$
$\displaystyle{(\mathsf{if}~{}{e_{1}}~{}\mathsf{then}~{}{e_{2}}~{}\mathsf{else}~{}{e_{3}})}[{\mathit{cf}}/{x}]\,{:=}\,$
$\displaystyle\mathsf{if}~{}{{e_{1}}[{\mathit{cf}}/{x}]}~{}\mathsf{then}~{}{{e_{2}}[{\mathit{cf}}/{x}]}~{}\mathsf{else}~{}{{e_{3}}[{\mathit{cf}}/{x}]}$
$\displaystyle{\mathsf{nil}}[{\mathit{cf}}/{x}]\,{:=}\,$
$\displaystyle\mathsf{nil}$
$\displaystyle{({e_{1}}::{e_{2}})}[{\mathit{cf}}/{x}]\,{:=}\,$
$\displaystyle{{e_{1}}[{\mathit{cf}}/{x}]}::{{e_{2}}[{\mathit{cf}}/{x}]}$
$\displaystyle{(\mathsf{listcase}~{}{e_{1}}~{}\mathsf{of}~{}({e_{2}},{e_{3}}))}[{\mathit{cf}}/{x}]\,{:=}\,$
$\displaystyle\mathsf{listcase}~{}{{e_{1}}[{\mathit{cf}}/{x}]}~{}\mathsf{of}~{}({{e_{2}}[{\mathit{cf}}/{x}]},{{e_{3}}[{\mathit{cf}}/{x}]})$
$\displaystyle{x}[{\mathit{cf}}/{x^{\prime}}]\,{:=}\,$
$\displaystyle\begin{cases}\mathit{cf}&\mathrm{if}~{}x=x^{\prime}\\\
x&\mathrm{otherwise}\end{cases}$
$\displaystyle{({e_{1}}\,{e_{2}})}[{\mathit{cf}}/{x}]\,{:=}\,$
$\displaystyle{{e_{1}}[{\mathit{cf}}/{x}]\,}\,{{e_{2}}[{\mathit{cf}}/{x}]}$
$\displaystyle{(\lambda{x}.{e_{1}})}[{\mathit{cf}}/{x^{\prime}}]\,{:=}\,$
$\displaystyle\begin{cases}\lambda{x}.{({e_{1}}[{\mathit{cf}}/{x^{\prime}}])}&\mathrm{if}~{}x\neq
x^{\prime}\\\ \lambda{x}.{e_{1}}&\mathrm{otherwise}\end{cases}$
$\displaystyle{(\mathsf{letrec}~{}{x_{1}}={\lambda{x_{2}}.{e_{2}}}~{}\mathsf{in}~{}{e_{1}})}[{\mathit{cf}}/{x}]\,{:=}\,$
$\displaystyle\begin{cases}\mathsf{letrec}~{}{x_{1}}={{(\lambda{x_{2}}.{e_{2}})}[{\mathit{cf}}/{x}]}~{}\mathsf{in}~{}{{e_{1}}[{\mathit{cf}}/{x}]}&\mathrm{if}~{}x\neq
x_{1}\\\
\mathsf{letrec}~{}{x_{1}}={({\lambda{x_{2}}.{e_{2}})}[{\mathit{cf}}/{x}]}~{}\mathsf{in}~{}{e_{1}}&\mathrm{otherwise}\end{cases}$

##  Appendix 0.C Supplementary Material for Section 6

Below, we present the proof of Lemma 2 that is central to the establishment of
the completeness result of the proposed reasoning technique.

######  Proof (of Lemma 2)

We show that for all $c$, $r$, if $\mathit{infer}^{\Phi_{\star}}({c},{r})$,
then $r\in\Phi_{\star}(c)$. This boils down to showing if
$\mathit{infer}^{\Phi_{\star}}({c},{r})$, then $\mathit{deriv}({c,r})$. Below,
we give an inductive proof of this statement.

Assume $\mathit{infer}^{\Phi_{\star}}({c},{r})$. Then, there exist some $m$,
$c_{1}$, …, $c_{m}$, $r_{1}$, …, $r_{m}$, and $r$, such that
$\mathit{res}^{\Phi_{\star}}({c_{1}},{r_{1}})$, …,
$\mathit{res}^{\Phi_{\star}}({c_{m}},{r_{m}})$, and

$\mathit{rule}~{}{[({c_{1}},{r_{1}}),\dots,({c_{m}},{r_{m}})]}~{}{({c},{r})}$
(2)

For each $i$, we show that $\mathit{deriv}({c_{i},r_{i}})$ holds by
distinguishing between the cases where $\Phi_{\star}(c_{i})=R$ and
$\Phi_{\star}(c_{i})\neq R$.

  * •

Suppose $\Phi_{\star}(c_{i})=R$. Then we deduce
$\mathit{infer}^{\Phi_{\star}}({c_{i}},{r_{i}})$ from
$\mathit{res}^{\Phi_{\star}}({c_{i}},{r_{i}})$. Hence, we have
$\mathit{deriv}({c_{i},r_{i}})$ from the induction hypothesis.

  * •

Suppose $\Phi_{\star}(c_{i})\neq R$. Then we have
$r_{i}\in\Phi_{\star}(c_{i})$ using
$\mathit{res}^{\Phi_{\star}}({c_{i}},{r_{i}})$. Hence, we have
$\mathit{deriv}({c_{i},r_{i}})$ using the definition of $\Phi_{\star}$.

Ultimately, we have $\mathit{deriv}({c_{i},r_{i}})$ for each
$i\in\\{1,\dots,m\\}$, and we obtain $\mathit{deriv}({c,r})$ using Eq. 2. This
completes the proof. ∎