# Formal Semantics of a Classical-Quantum Language

Yuxin Deng<EMAIL_ADDRESS>Yuan Feng<EMAIL_ADDRESS>Shanghai
Key Laboratory of Trustworthy Computing, East China Normal University
University of Technology Sydney, Australia

###### Abstract

We investigate the formal semantics of a simple imperative language that has
both classical and quantum constructs. More specifically, we provide an
operational semantics, a denotational semantics and two Hoare-style proof
systems: an abstract one and a concrete one. The two proof systems are
satisfaction-based, as inspired by the program logics of Barthe et al for
probabilistic programs. The abstract proof system turns out to be sound and
relatively complete, while the concrete one is sound only.

###### keywords:

Classical-quantum language , Formal semantics , Soundness , Completeness

##  1 Introduction

Programming is the core of software development, but it is also an inherently
error-prone activity. The likelihood of errors will even be significantly
higher when programming with a quantum computer, as the techniques used for
classical programming are, unfortunately, hard to apply to quantum computers
because quantum systems are essentially different from classical ones. Thus,
there is a pressing need to provide verification and analysis techniques for
reasoning about the correctness of quantum programs. Furthermore, these
techniques would also be very useful for compiling and optimising quantum
programs.

Among other techniques, Hoare logic [11] provides a syntax-oriented proof
system to reason about program correctness. After decades of development,
Hoare logic has been successfully applied in analysis of programs with non-
determinism, recursion, parallel execution, etc [2, 1]. It was also extended
to programming languages with probabilistic features. Remarkably, as the
program states for probabilistic languages are (sub)distributions over
evaluations of program variables, the extension naturally follows two
different approaches, depending on how assertions of probabilistic states are
defined. The first one takes subsets of distributions as (qualitative)
assertions, similar to the non-probabilistic case, and the _satisfaction_
relation between distributions and assertions is then just the ordinary
membership [20, 7, 5, 3]. In contrast, the other approach takes non-negative
functions on evaluations as (quantitative) assertions. Consequently, one is
concerned with the _expectation_ of a distribution satisfying an assertion
[17, 16, 19, 13, 14].

In the past two decades, several Hoare-type logic systems for quantum programs
(QHL) have been proposed, also following the two approaches as in the
probabilistic setting.

Expectation-based QHLs. In the logic systems proposed in [25, 26, 27, 15] for
purely quantum programs, the assertions $P$ and $Q$ in a Hoare triple
$\\{P\\}S\\{Q\\}$ are both positive operators with the eigenvalues lying in
$[0,1]$, and such a triple is valid in the sense of total correctness if for
any initial quantum state $\rho$, ${\rm tr}(P\rho)\leq{\rm
tr}(Q\rho^{\prime})$ where $\rho^{\prime}$ is the final state obtained by
executing $S$ on $\rho$, and ${\rm tr}(P\rho)$ denotes the expectation/degree
of $\rho$ satisfying $P$ (or physically, the average outcome when measuring
$\rho$ according to the projective measurement determined by $P$). This
definition captures the idea that the precondition $P$ (on the initial state)
provides a lower bound on the degree of satisfaction of the postcondition $Q$
(on the finial state). More recently, this type of expectation-based QHL has
been extended to quantum programs with classical variables [9] as well as
distributed quantum programs with classical communication [8]. These logic
systems have proven to be useful in describing and verifying correctness of a
wide range of quantum algorithms such as Shor’s algorithm [21], Grover’s
algorithm [10], etc. Moreover, they are theoretically elegant: all of these
systems are (relatively) complete in the sense that every semantically valid
Hoare triple can be deduced from the corresponding proof system.

Limit of the expectation-based approach. However, the expectation-based
quantum Hoare logic systems proposed in the literature all suffer from the
following _expressiveness_ problems.

  * 1.

Unlike the classical boolean-valued assertions, the positive operator
assertions cannot exclude undesirable quantum inputs. Note that the
correctness of many algorithms such as quantum teleportation (an EPR pair is
assumed as part of the input) and phase estimation (the corresponding
eigenstate is given) all have some restrictions on the input. The
expressiveness of expectation-based QHL might be limited, as the following
artificial example suggests. Let

$S\equiv x:=M_{\pm}[q]$

where $M_{\pm}$ is the measurement according to the $|\pm\rangle$ basis.
Obviously, starting with $|0\rangle$, the program ends at $|+\rangle$ with
probability 0.5. However, expectation-based QHL cannot describe this property:
the natural candidate

$\\{0.5|0\rangle\langle 0|\\}\ S\ \\{|+\rangle\langle+|\\}$ (1)

is actually not valid. The reason is, it somehow _over-specifies_ the
correctness: in addition to the above desirable property, it also puts certain
requirement for _all other_ possible input states. To see this, take
$\rho=|-\rangle\langle-|$. Then $[\\![S]\\!](\rho)=|-\rangle\langle-|$. Thus

${\rm tr}(0.5|0\rangle\langle 0|\rho)=0.25>{\rm
tr}(|+\rangle\langle+|[\\![S]\\!](\rho))=0,$

making the Hoare triple in Eq. (1) invalid.

  * 2.

As logic operations such as conjunction and disjunction are difficult, if at
all possible, to define for positive operators, complicated properties can
only be analysed separately, making the verification process cumbersome. This
has been pointed out in [3] for expectation-based probabilistic Hoare logics.
The same is obviously true for expectation-based QHLs as well.

Satisfaction-based QHLs. An Ensemble Exogenous Quantum Propositional Logic
(EEQPL) was proposed in [6] for a simple quantum language with bounded
iteration. The assertions in EEQPL can access amplitudes of quantum states,
which makes it very strong in expressiveness but also hinders its use in
applications such as debugging, as amplitudes are not physically accessible
through measurements. The completeness of EEQPL is only proven in a special
case where all real and complex values involved range over a finite set. In
contrast, the QHL proposed in [12] takes as the assertion language an extended
first-order logic with the primitives of applying a matrix on a set of qubits
and computing the probability that a classical predicate is satisfied by the
outcome of a quantum measurement. The proof system is shown to be sound, but
no completeness result was established.

Another way of defining satisfaction-based QHLs proposed in [28, 22] regard
subspaces of the Hilbert space as assertions, and a quantum state $\rho$
satisfies an assertion $P$ iff the support (the image space of linear
operators) of $\rho$ is included in $P$. The subspace assertion makes it easy
to describe and determine properties of quantum programs, but the expressive
power of the assertions is limited: they only assert if a given quantum state
lies completely within a subspace. Consequently, quantum algorithms which
succeed with certain probability cannot be verified in their logic systems.

Contribution of the current paper. In this paper, motivated by [3], we propose
two Hoare-style proof systems: an abstract one and a concrete one. It is worth
noting that the imperative language we consider here involves both classical
and quantum constructs. Our work distinguishes itself from the works on QHLs
mentioned above in the following aspects:

  * 1.

_Assertion language_. The assertions used in our logic systems are boolean-
typed, so that they can be easily combined using logic operations such as
disjunction and conjunction. On the other hand, all information used in the
assertions are physically accessible: they can be obtained through quantum
measurement applying on the program states. For example, consider the protocol
of superdense coding (see Section 6). In order to send a message of two bits
stored in two variables $x_{0}x_{1}$, Alice actually sends a qubit to Bob.
From the received quantum information Bob can recover the message
$y_{0}y_{1}$. The property we would expect is $x_{0}=y_{0}\wedge x_{1}=y_{1}$.
Indeed, by letting $SC$ be a quantum program to implement the protocol, we can
prove that the following judgement is derivable:

$\\{{\textbf{true}}\\}\;SC\;\\{\Box(x_{0}=y_{0}\wedge x_{1}=y_{1})\\}$

where the precondition true is satisfied by any program state. Intuitively,
the judgement says that the message received by Bob is always the same as that
sent by Alice, no matter what the initial program state is. There is no need
to mention the concrete values of $x_{0}$ and $x_{1}$. This is a natural and
concise way of specifying the correctness of the program $SC$.

  * 2.

_Satisfaction-based complete QHL_. The existing satisfaction-based QHLs
proposed in the literature all lack of completeness; the only exception is
[28], but as mentioned above, the assertions there are not expressive enough
to verify probabilistic correctness. The abstract proof system proposed in the
current work is shown to be sound and relatively complete, while the concrete
proof system is sound only. By soundness, we mean that if the Hoare triple
$\\{P\\}\;c\;\\{Q\\}$ is derivable, then for any program state $\mu$ that
satisfies $P$, the program state $[\\![c]\\!]_{\mu}$ after the execution of
command $c$ always satisfies $Q$. Completeness means the converse. We only
have relative completeness because our assertion language allows for first-
order logic operators such as implication. Note that in the presence of both
classical and quantum variables, we represent each program state $\mu$ as a
partial density operator valued distribution (POVD), and interpret a program
as a transformer of POVDs. We establish a consistence result between the
denotational semantics and the small-step operational semantics based on
POVDs.

The rest of the paper is structured as follows. In Section 2 we recall some
basic notations from linear algebra and quantum mechanics. In Section 3 we
define the syntax and operational semantics of a simple classical-quantum
imperative language. In Section 4 we present an abstract proof system and show
its soundness and relative completeness. In Section 5 we provide a concrete
proof system. In Section 6 we use the example of superdense coding to
illustrate the concrete proof system. Finally, we conclude in Section 7.

##  2 Preliminaries

We briefly recall some basic notations from linear algebra and quantum
mechanics which are needed in this paper. For more details, we refer to [18].

A Hilbert space $\mathcal{H}$ is a complete vector space with an inner product
$\langle\cdot|\cdot\rangle:\mathcal{H}\times\mathcal{H}\rightarrow\mathbf{C}$
such that

  1. 1.

$\langle\psi|\psi\rangle\geq 0$ for any $|\psi\rangle\in\mathcal{H}$, with
equality if and only if $|\psi\rangle=0$;

  2. 2.

$\langle\varphi|\psi\rangle=\langle\psi|\varphi\rangle^{\ast}$;

  3. 3.

$\langle\varphi|\sum_{i}c_{i}|\psi_{i}\rangle=\sum_{i}c_{i}\langle\varphi|\psi_{i}\rangle$,

where $\mathbf{C}$ is the set of complex numbers, and for each
$c\in\mathbf{C}$, $c^{\ast}$ stands for the complex conjugate of $c$. For any
vector $|\psi\rangle\in\mathcal{H}$, its length $|||\psi\rangle||$ is defined
to be $\sqrt{\langle\psi|\psi\rangle}$, and it is said to be normalised if
$|||\psi\rangle||=1$. Two vectors $|\psi\rangle$ and $|\varphi\rangle$ are
orthogonal if $\langle\psi|\varphi\rangle=0$. An orthonormal basis of a
Hilbert space $\mathcal{H}$ is a basis $\\{|i\rangle\\}$ where each
$|i\rangle$ is normalised and any pair of them are orthogonal.

Let $\mathcal{L(H)}$ be the set of linear operators on $\mathcal{H}$. For any
$A\in\mathcal{L(H)}$, $A$ is Hermitian if $A^{\dagger}=A$ where $A^{\dagger}$
is the adjoint operator of $A$ such that
$\langle\psi|A^{\dagger}|\varphi\rangle=\langle\varphi|A|\psi\rangle^{*}$ for
any $|\psi\rangle,|\varphi\rangle\in\mathcal{H}$. A linear operator
$A\in\mathcal{L(H)}$ is unitary if $A^{\dagger}A=AA^{\dagger}=I_{\mathcal{H}}$
where $I_{\mathcal{H}}$ is the identity operator on $\mathcal{H}$. The trace
of $A$ is defined as ${\rm tr}(A)=\sum_{i}\langle i|A|i\rangle$ for some given
orthonormal basis $\\{|i\rangle\\}$ of $\mathcal{H}$. A linear operator
$A\in\mathcal{L(H)}$ is positive if $\langle\varphi|A|\varphi\rangle\geq 0$
for any state $|\varphi\rangle\in\mathcal{H}$. The _Löwner order_
$\sqsubseteq$ on the set of Hermitian operators on $\mathcal{H}$ is defined by
letting $A\sqsubseteq B$ iff $B-A$ is positive.

Let $\mathcal{H}_{1}$ and $\mathcal{H}_{2}$ be two Hilbert spaces. Their
tensor product $\mathcal{H}_{1}\otimes\mathcal{H}_{2}$ is defined as a vector
space consisting of linear combinations of the vectors
$|\psi_{1}\psi_{2}\rangle=|\psi_{1}\rangle|\psi_{2}\rangle=|\psi_{1}\rangle\otimes|\psi_{2}\rangle$
with $|\psi_{1}\rangle\in\mathcal{H}_{1}$ and
$|\psi_{2}\rangle\in\mathcal{H}_{2}$. Here the tensor product of two vectors
is defined by a new vector such that

$\left(\sum_{i}\lambda_{i}|\psi_{i}\rangle\right)\otimes\left(\sum_{j}\mu_{j}|\varphi_{j}\rangle\right)=\sum_{i,j}\lambda_{i}\mu_{j}|\psi_{i}\rangle\otimes|\varphi_{j}\rangle.$

Then $\mathcal{H}_{1}\otimes\mathcal{H}_{2}$ is also a Hilbert space where the
inner product is defined as the following: for any
$|\psi_{1}\rangle,|\varphi_{1}\rangle\in\mathcal{H}_{1}$ and
$|\psi_{2}\rangle,|\varphi_{2}\rangle\in\mathcal{H}_{2}$,

$\langle\psi_{1}\otimes\psi_{2}|\varphi_{1}\otimes\varphi_{2}\rangle=\langle\psi_{1}|\varphi_{1}\rangle_{\mathcal{H}_{1}}\langle\psi_{2}|\varphi_{2}\rangle_{\mathcal{H}_{2}}$

where $\langle\cdot|\cdot\rangle_{\mathcal{H}_{i}}$ is the inner product of
$\mathcal{H}_{i}$.

By applying quantum gates to qubits, we can change their states. For example,
the Hadamard gate (H gate) can be applied on a single qubit, while the CNOT
gate can be applied on two qubits. Some commonly used gates and their
representation in terms of matrices are as follows.

${\textit{CNOT}}=\left(\begin{array}[]{cccc}1&0&0&0\\\ 0&1&0&0\\\ 0&0&0&1\\\
0&0&1&0\end{array}\right),$
$H=\frac{1}{\sqrt{2}}\left(\begin{array}[]{cc}1&1\\\ 1&-1\\\
\end{array}\right),\ \ I_{2}=\left(\begin{array}[]{cc}1&0\\\ 0&1\\\
\end{array}\right),\ \ X=\left(\begin{array}[]{cc}0&1\\\ 1&0\\\
\end{array}\right),\ \ Z=\left(\begin{array}[]{cc}1&0\\\ 0&-1\\\
\end{array}\right).$

According to von Neumann’s formalism of quantum mechanics [23], an isolated
physical system is associated with a Hilbert space which is called the state
space of the system. A pure state of a quantum system is a normalised vector
in its state space, and a mixed state is represented by a density operator on
the state space. Here a _density operator_ $\rho$ on Hilbert space
$\mathcal{H}$ is a positive linear operator such that ${\rm tr}(\rho)=1$. A
_partial density operator_ $\rho$ is a positive linear operator with ${\rm
tr}(\rho)\leq 1$.

The evolution of a closed quantum system is described by a unitary operator on
its state space: if the states of the system at times $t_{1}$ and $t_{2}$ are
$\rho_{1}$ and $\rho_{2}$, respectively, then
$\rho_{2}=U\rho_{1}U^{{\dagger}}$ for some unitary operator $U$ which depends
only on $t_{1}$ and $t_{2}$.

A quantum measurement is described by a collection $\\{M_{m}\\}$ of
measurement operators, where the indices $m$ refer to the measurement
outcomes. It is required that the measurement operators satisfy the
completeness equation $\sum_{m}M_{m}^{{\dagger}}M_{m}=I_{\mathcal{H}}$. If the
system is in state $\rho$, then the probability that measurement result $m$
occurs is given by

$p(m)={\rm tr}(M_{m}^{{\dagger}}M_{m}\rho),$

and the state of the post-measurement system is $M_{m}\rho
M_{m}^{{\dagger}}/p(m).$

##  3 QIMP

We define the syntax and operational semantics of a simple classical-quantum
imperative language called QIMP. The language is essentially extended from IMP
[24] by adding quantum data and a few operations for manipulating quantum
data.

###  3.1 Syntax

We assume three types of data in our language: Bool for booleans, Int for
integers, and qubits Qbt for quantum data. Let $\mathbb{Z}$ be the set of
constant integer numbers, ranged over by $n$. Let Cvar, ranged over by
$x,y,...$, be the set of classical variables, and Qvar, ranged over by
$q,q^{\prime},...$, the set of quantum variables. It is assumed that both Cvar
and Qvar are countably infinite. We assume a set Aexp of arithmetic
expressions over Int, which includes Cvar as a subset and is ranged over by
$a,a^{\prime},...$, and a set of boolean-valued expressions Bexp, ranged over
by $b,b^{\prime},...$, with the usual boolean constants true, false and
boolean operators $\neg,\wedge,\vee$. In particular, we let $a=a^{\prime}$ and
$a\leq a^{\prime}$ be boolean expressions for any
$a,a^{\prime}\in{\textbf{Aexp}}$. We further assume that only classical
variables can occur free in both arithmetic and boolean expressions.

We let $U$ range over unitary operators, which can be user-defined matrices or
built in if the language is implemented. For example, a concrete $U$ could be
the $1$-qubit Hadamard operator $H$, or the 2-qubit controlled-NOT operator
CNOT, etc. Similarly, we write $M$ for the measurement described by a
collection $\\{M_{i}\\}$ of measurement operators, with each index $i$
representing a measurement outcome. For example, to describe the measurement
of the qubit referred to by variable $q$ in the computational basis, we can
write $M:=\\{M_{0},M_{1}\\}$, where $M_{0}=|0\rangle_{q}\langle 0|$ and
$M_{1}=|1\rangle_{q}\langle 1|$.

Sometimes we use metavariables which are primed or subscripted, e.g.
$x^{\prime},x_{0}$ for classical variables. We abbreviate a tuple of quantum
variables $\langle q_{1},...,q_{n}\rangle$ as $\bar{q}$ if the length $n$ of
the tuple is not important. The formation rules for arithmetic and boolean
expressions as well as commands are defined by the following grammar.

  * 1.

For Aexp: $a::=n\mid x\mid a_{0}+a_{1}\mid a_{0}-a_{1}\mid a_{0}\times a_{1}$

  * 2.

For Bexp: $b::={\textbf{true}}\mid{\textbf{false}}\mid a_{0}=a_{1}\mid
a_{0}\leq a_{1}\mid\neg b\mid b_{0}\wedge b_{1}\mid b_{0}\vee b_{1}$

  * 3.

For Com:

$\begin{array}[]{rl}c::=&{\textbf{skip}}\mid x:=a\mid
c_{0};c_{1}\mid\textbf{if}~{}b~{}\textbf{then}~{}c_{0}~{}\textbf{else}~{}c_{1}\mid\textbf{while}~{}b~{}\textbf{do}~{}c\\\
&\mid q:=|0\rangle\mid{U}[\bar{q}]\mid x:={M}[\bar{q}]\end{array}$

An arithmetic expression can be an integer, a variable, or built from other
arithmetic expressions by addition, subtraction, or multiplication. A boolean
expression can be formed by comparing arithmetic expressions or by using the
usual boolean operators. A command can be a skip statement, a classical
assignment, a conditional statement, or a while-loop, as in many classical
imperative languages. In addition, there are three commands that involve
quantum data. The command $q:=|0\rangle$ initialises the qubit referred to by
variable $q$ to be the basis state $|0\rangle$. The command ${U}[\bar{q}]$
applies the unitary operator ${U}$ to the quantum system referred to by
$\bar{q}$. The command $x:={M}[\bar{q}]$ performs a measurement $M$ on
$\bar{q}$ and assigns the measurement outcome to $x$. It differs from a
classical assignment because the measurement $M$ may change the quantum state
of $\bar{q}$, besides the fact that the value of $x$ is updated.

###  3.2 Operational Semantics

Since the execution of a QIMP program may involve both classical and quantum
data, we consider the setting where the CPU that processes the program has two
registers: one stores classical data and the other quantum data. Therefore, we
will model a machine state as a pair composed of a classical state and a
quantum state.

The notion of classical state is standard. Formally, a _classical state_ is a
function $\sigma:{\textbf{Cvar}}\rightarrow\mathbb{Z}$ from classical
variables to integers. Thus $\sigma(x)$ is the value of variable $x$ in state
$\sigma$. The notion of quantum state is slightly more complicated. For each
quantum variable $q\in{\textbf{Qvar}}$, we assume a $2$-dimensional Hilbert
space ${\cal H}_{q}$ to be the state space of the $q$-system. For any finite
subset $V$ of Qvar, we denote

${\cal H}_{V}\ =\ \bigotimes_{q\in V}{\cal H}_{q}.$

That is, ${\cal H}_{V}$ is the tensor product of the individual state spaces
of all the quantum variables in $V$. Throughout the paper, when we refer to a
subset of Qvar, it is always assumed to be finite. Given
$V\subseteq{\textbf{Qvar}}$, the set of _quantum states_ consists of all
partial density operators in the space ${\cal H}_{V}$, denoted by
$\mathop{\mbox{$\mathcal{D}^{-}$}}({{\cal H}_{V}})$. A _machine state_ is a
pair $\langle\sigma,\rho\rangle$ where $\sigma$ is a classical state and
$\rho$ a quantum state. In the presence of measurements, we often need to
consider an ensemble of states. For that purpose, we introduce a notion of
distribution.

###### Definition 3.1

Suppose $V\subseteq{\textbf{Qvar}}$ and $\Sigma$ is the set of classical
states, i.e., the set of functions of type
${\textbf{Cvar}}\rightarrow\mathbb{Z}$. A _partial density operator valued
distribution (POVD)_ is a function
$\mu:\Sigma\rightarrow\mathop{\mbox{$\mathcal{D}^{-}$}}({{\cal H}_{V}})$ with
$\sum_{\sigma\in\Sigma}{\rm tr}(\mu(\sigma))\leq 1$.

Intuitively, a POVD $\mu$ represents a collection of machine states where each
classical state $\sigma$ is associated with a quantum state $\mu(\sigma)$. The
notation of POVD is called classical-quantum state in [9]. If the collection
has only one element $\sigma$, we explicitly write $(\sigma,\mu(\sigma))$ for
$\mu$. The support of $\mu$, written $\lceil{\mu}\rceil$, is the set
$\\{\sigma\in\Sigma\mid\mu(\sigma)\not=0\\}$. We can also define the addition
of two distributions by letting
$(\mu_{1}+\mu_{2})(\sigma)=\mu_{1}(\sigma)+\mu_{2}(\sigma)$.

A _configuration_ is a pair $\langle e,\sigma,\rho\rangle$, where $e$ is an
expression and $(\sigma,\rho)$ is a POVD. We define the small-step operational
semantics of arithmetic and boolean expressions as well as commands in a
syntax-directed way by using an evaluation relation $\hookrightarrow$ between
configurations. In Figure 1 we list the rules for evaluating integer
variables, sums, and expressions of the form $a_{0}\leq a_{1}$; the rules for
other arithmetic and boolean expressions are similar. When evaluating an
arithmetic or boolean expression, we only rely on the information from the
given classical state, therefore we omit the quantum state in the
configuration. This is not the case when we execute commands.

$\begin{array}[]{l}\begin{array}[]{l}\langle
x,\sigma\rangle\hookrightarrow\langle\sigma(x),\sigma\rangle\end{array}\vspace{2mm}\\\
\prooftree\langle a_{0},\sigma\rangle\hookrightarrow\langle
a_{0}^{\prime},\sigma\rangle\justifies\langle
a_{0}+a_{1},\sigma\rangle\hookrightarrow\langle
a_{0}^{\prime}+a_{1},\sigma\rangle\endprooftree\qquad\prooftree\langle
a_{1},\sigma\rangle\hookrightarrow\langle
a_{1}^{\prime},\sigma\rangle\justifies\langle
n+a_{1},\sigma\rangle\hookrightarrow\langle
n+a^{\prime}_{1},\sigma\rangle\endprooftree\vspace{2mm}\\\ \langle
n+m,\sigma\rangle\hookrightarrow\langle p,\sigma\rangle\qquad\mbox{if $p$ is
the sum of $n$ and $m$}\vspace{2mm}\\\ \prooftree\langle
a_{0},\sigma\rangle\hookrightarrow\langle
a^{\prime}_{0},\sigma\rangle\justifies\langle a_{0}\leq
a_{1},\sigma\rangle\hookrightarrow\langle a^{\prime}_{0}\leq
a_{1},\sigma\rangle\endprooftree\qquad\prooftree\langle
a_{1},\sigma\rangle\hookrightarrow\langle
a^{\prime}_{1},\sigma\rangle\justifies\langle n\leq
a_{1},\sigma\rangle\hookrightarrow\langle n\leq
a^{\prime}_{1},\sigma\rangle\endprooftree\vspace{2mm}\\\ \langle n\leq
m,\sigma\rangle\hookrightarrow\langle{\textbf{true}},\sigma\rangle\qquad\mbox{if
$n$ is less than or equal to $m$.}\vspace{2mm}\\\ \langle n\leq
m,\sigma\rangle\hookrightarrow\langle{\textbf{false}},\sigma\rangle\qquad\mbox{if
$n$ is greater than $m$.}\end{array}$ Figure 1: Evaluation of arithmetic and
boolean expressions (selected rules)

Let $\sigma$ be a classical state and $n\in\mathbb{Z}$. We write $\sigma[n/x]$
for the updated state satisfying

$\sigma[n/x](y)=\left\\{\begin{array}[]{ll}n&\mbox{if $y=x$,}\\\
\sigma(y)&\mbox{if $y\not=x$.}\end{array}\right.$

We are going to write $\rightarrow$ for the execution of commands. The
transition rules are given in Figure 2. Here we introduce a special command
nil that stands for a successful termination of programs. We follow [25] to
define the operational semantics of quantum measurements in a non-
deterministic way, and the probabilities of different branches are encoded in
the quantum part of the configurations. For that reason we need to take
partial density operators instead of the normalised density operators to
represent quantum states. After the measurement $M$ defined by some
measurement operators $M_{i}$, the original state $(\sigma,\rho)$ may evolve
into a new state whose classical part is the updated state $\sigma[i/x]$ and
the quantum part is the new quantum state $M_{i}\rho M_{i}^{\dagger}$. In all
other rules, the execution of a command changes a configuration to another
one. Among them, the rules for initialising qubits and unitary transformations
only affect the quantum part of the original machine state. On the contrary,
the commands for manipulating classical data only update the classical part of
a state.

$\begin{array}[]{l}\langle{\textbf{skip}},\sigma,\rho\rangle\rightarrow\langle\textbf{nil},\sigma,\rho\rangle\vspace{2mm}\\\
\prooftree\langle a,\sigma\rangle\hookrightarrow\langle
a^{\prime},\sigma^{\prime}\rangle\justifies\langle
x:=a,\sigma,\rho\rangle\rightarrow\langle
x:=a^{\prime},\sigma^{\prime},\rho\rangle\endprooftree\qquad\langle
x:=n,\sigma,\rho\rangle\rightarrow\langle\textbf{nil},\sigma[n/x],\rho\rangle\vspace{2mm}\\\
\prooftree\langle c_{0},\sigma,\rho\rangle\rightarrow\langle
c^{\prime}_{0},\sigma^{\prime},\rho^{\prime}\rangle\justifies\langle
c_{0};c_{1},\sigma,\rho\rangle\rightarrow\langle
c^{\prime}_{0};c_{1},\sigma^{\prime},\rho^{\prime}\rangle\endprooftree\qquad\prooftree\langle
c_{1},\sigma,\rho\rangle\rightarrow\langle
c^{\prime}_{1},\sigma^{\prime},\rho^{\prime}\rangle\justifies\langle\textbf{nil};c_{1},\sigma,\rho\rangle\rightarrow\langle
c^{\prime}_{1},\sigma^{\prime},\rho^{\prime}\rangle\endprooftree\vspace{2mm}\\\
\prooftree\langle b,\sigma\rangle\hookrightarrow\langle
b^{\prime},\sigma^{\prime}\rangle\justifies\langle\textbf{if}~{}b~{}\textbf{then}~{}c_{0}~{}\textbf{else}~{}c_{1},\sigma,\rho\rangle\rightarrow\langle\textbf{if}~{}b^{\prime}~{}\textbf{then}~{}c_{0}~{}\textbf{else}~{}c_{1},\sigma^{\prime},\rho^{\prime}\rangle\endprooftree\vspace{2mm}\\\
\langle\textbf{if}~{}{\textbf{true}}~{}\textbf{then}~{}c_{0}~{}\textbf{else}~{}c_{1},\sigma,\rho\rangle\rightarrow\langle
c_{0},\sigma,\rho\rangle\qquad\langle\textbf{if}~{}{\textbf{false}}~{}\textbf{then}~{}c_{0}~{}\textbf{else}~{}c_{1},\sigma,\rho\rangle\rightarrow\langle
c_{1},\sigma,\rho\rangle\vspace{2mm}\\\
\langle\textbf{while}~{}b~{}\textbf{do}~{}c,\sigma,\rho\rangle\rightarrow\langle\textbf{if}~{}b~{}\textbf{then}~{}(c;\textbf{while}~{}b~{}\textbf{do}~{}c)~{}\textbf{else}~{}{\textbf{skip}},\sigma,\rho\rangle\vspace{2mm}\\\
\langle
q:=|0\rangle,\sigma,\rho\rangle\rightarrow\langle\textbf{nil},\sigma,\rho^{\prime}\rangle\qquad\mbox{
with }\rho^{\prime}=|0\rangle_{q}\langle 0|\rho|0\rangle_{q}\langle
0|+|0\rangle_{q}\langle 1|\rho|1\rangle_{q}\langle 0|\vspace{2mm}\\\
\langle{U}[\bar{q}],\sigma,\rho\rangle\rightarrow\langle\textbf{nil},\sigma,{U}\rho{U}^{\dagger}\rangle\vspace{2mm}\\\
\prooftree M:=\\{M_{i}\\}_{i\in I}\justifies\langle
x:={M}[\bar{q}],\sigma,\rho\rangle\rightarrow\langle\textbf{nil},\sigma[i/x],M_{i}\rho
M_{i}^{\dagger}\rangle\endprooftree\end{array}$ Figure 2: Execution of
commands

###  3.3 Denotational Semantics

For the purpose of presenting the denotational semantics, we add an abort
command that halts the computation with no result. We interpret programs as
POVD transformers. We write POVD for the set of POVDs called distribution
states.

###### Lemma 3.2

We impose an order between POVDs by letting $\mu_{1}\leq\mu_{2}$ if for any
classical state $\sigma$ we have $\mu_{1}(\sigma)\sqsubseteq\mu_{2}(\sigma)$,
where $\sqsubseteq$ is the Löwner order. Let
$(\mu_{n})_{n\in{\mathbb{N}}}\in{\textbf{POVD}}$ be an increasing sequence of
POVDs. This sequence converges to some POVD $\mu_{\infty}$ and
$\mu_{n}\leq\mu_{\infty}$ for any $n\in{\mathbb{N}}$.

Given an expression $e$, we denote its interpretation with respect to machine
state $(\sigma,\rho)$ by $[\\![e]\\!]_{(\sigma,\rho)}$. The denotational
semantics of commands is displayed in Figure 3, where we omit the denotational
semantics of arithmetic and boolean expressions such as $[\\![a]\\!]_{\sigma}$
and $[\\![b]\\!]_{\sigma}$, which is almost the same as in the classical
setting because the quantum part plays no role for those expressions. This is
an extension of the semantics for probabilistic programs presented in [3].
Instead of probabilistic assignments are measurements of quantum systems. A
state evolves into a POVD after some quantum qubits are measured, with the
measurement outcomes assigned to a classical variable. Two other quantum
commands, initialisation of qubits and unitary operations, are deterministic
and only affect the quantum part of a state. As usual, we define the semantics
of a loop ($\textbf{while}~{}b~{}\textbf{do}~{}c$) as the limit of its lower
approximations, where the $n$-th lower approximation of
$[\\![\textbf{while}~{}b~{}\textbf{do}~{}c]\\!]_{(\sigma,\rho)}$ is
$[\\![(\textbf{if}~{}b~{}\textbf{then}~{}c)^{n};\textbf{if}~{}b~{}\textbf{then}~{}\textbf{abort}]\\!]_{(\sigma,\rho)}$,
where ($\textbf{if}~{}b~{}\textbf{then}~{}c$) is shorthand for
($\textbf{if}~{}b~{}\textbf{then}~{}c~{}\textbf{else}~{}{\textbf{skip}}$) and
$c^{n}$ is the command $c$ iterated $n$ times with
$c^{0}\equiv{\textbf{skip}}$. The limit exists because the sequence
$([\\![(\textbf{if}~{}b~{}\textbf{then}~{}c)^{n};\textbf{if}~{}b~{}\textbf{then}~{}\textbf{abort}]\\!]_{(\sigma,\rho)})_{n\in{\mathbb{N}}}$
is increasing and bounded. We write $\varepsilon$ for the special POVD whose
support is the empty set.

###### Proposition 3.3

The semantics $[\\![c]\\!]_{(\sigma,\rho)}$ of a command $c$ in initial state
${(\sigma,\rho)}$ is a POVD. The lifted semantics $[\\![c]\\!]_{\mu}$ of a
command $c$ in initial POVD $\mu$ is a POVD.

$\begin{array}[]{rcl}[\\![{\textbf{skip}}]\\!]_{(\sigma,\rho)}&=&(\sigma,\rho)\vspace{2mm}\\\
[\\![\textbf{abort}]\\!]_{(\sigma,\rho)}&=&\varepsilon\vspace{2mm}\\\
[\\![x:=a]\\!]_{(\sigma,\rho)}&=&(\sigma[[\\![a]\\!]_{\sigma}/x],\rho)\vspace{2mm}\\\
[\\![c_{0};c_{1}]\\!]_{(\sigma,\rho)}&=&[\\![c_{1}]\\!]_{[\\![c_{0}]\\!]_{(\sigma,\rho)}}\vspace{2mm}\\\
[\\![\textbf{if}~{}b~{}\textbf{then}~{}c_{0}~{}\textbf{else}~{}c_{1}]\\!]_{(\sigma,\rho)}&=&\left\\{\begin{array}[]{ll}[\\![c_{0}]\\!]_{(\sigma,\rho)}&\mbox{if
$[\\![b]\\!]_{\sigma}={\textbf{true}}$}\\\
[\\![c_{1}]\\!]_{(\sigma,\rho)}&\mbox{if
$[\\![b]\\!]_{\sigma}={\textbf{false}}$}\end{array}\right.\vspace{2mm}\\\
[\\![\textbf{while}~{}b~{}\textbf{do}~{}c]\\!]_{(\sigma,\rho)}&=&\lim_{n\rightarrow\infty}[\\![(\textbf{if}~{}b~{}\textbf{then}~{}c)^{n};\textbf{if}~{}b~{}\textbf{then}~{}\textbf{abort}]\\!]_{(\sigma,\rho)}\vspace{2mm}\\\
[\\![q:=|0\rangle]\\!]_{(\sigma,\rho)}&=&\langle\sigma,\rho^{\prime}\rangle\\\
&&\mbox{where $\rho^{\prime}:=|0\rangle_{q}\langle 0|\rho|0\rangle_{q}\langle
0|+|0\rangle_{q}\langle 1|\rho|1\rangle_{q}\langle 0|$}\vspace{2mm}\\\
[\\![{U}[\bar{q}]]\\!]_{(\sigma,\rho)}&=&\langle\sigma,{U}\rho{U}^{\dagger}\rangle\vspace{2mm}\\\
[\\![x:={M}[\bar{q}]]\\!]_{(\sigma,\rho)}&=&\mu\vspace{2mm}\\\ &&\mbox{where
$M=\\{M_{i}\\}_{i\in I}$ and $\mu(\sigma^{\prime})=\sum_{i}\\{M_{i}\rho
M_{i}^{\dagger}\mid\sigma[i/x]=\sigma^{\prime}\\}$}\vspace{4mm}\\\
[\\![c]\\!]_{\mu}&=&\sum_{\sigma\in\lceil{\mu}\rceil}[\\![c]\\!]_{(\sigma,\mu(\sigma))}.\end{array}$
Figure 3: Denotational semantics of commands

The operational and denotational semantics are related by the following
theorem.

###### Theorem 3.4

For any command $c$ and state $(\sigma,\rho)$, we have

$[\\![c]\\!]_{(\sigma,\rho)}=\sum_{i}\\{(\sigma_{i},\rho_{i})\mid\langle
c,\sigma,\rho\rangle\rightarrow^{*}\langle\textbf{nil},\sigma_{i},\rho_{i}\rangle\\}\
.$

  * Proof:

We proceed by induction on the structure of $c$. The most difficult case is
when $c\equiv\textbf{while}~{}b~{}\textbf{do}~{}c^{\prime}$ for some command
$c^{\prime}$. Below we consider this case.

Let
$\textbf{While}^{n}=(\textbf{if}~{}b~{}\textbf{then}~{}c^{\prime})^{n};\textbf{if}~{}b~{}\textbf{then}~{}\textbf{abort}$
and $\langle
c,\sigma,\rho\rangle\rightarrow^{n}\langle\textbf{nil},\sigma^{\prime},\rho^{\prime}\rangle$
be the sequence of maximal transitions from $\langle c,\sigma,\rho\rangle$
such that the unfolding rule

$\langle\textbf{while}~{}b~{}\textbf{do}~{}c^{\prime},\sigma^{\prime\prime},\rho^{\prime\prime}\rangle\rightarrow\langle\textbf{if}~{}b~{}\textbf{then}~{}(c^{\prime};\textbf{while}~{}b~{}\textbf{do}~{}c^{\prime})~{}\textbf{else}~{}{\textbf{skip}},\sigma^{\prime\prime},\rho^{\prime\prime}\rangle\
,$

for any $\sigma^{\prime\prime}$ and $\rho^{\prime\prime}$, has been applied at
most $n$ times.

$\mbox{\bf Claim: }\hskip
56.9055pt[\\![\textbf{While}^{n}]\\!]_{(\sigma,\rho)}=\sum_{i}\\{(\sigma_{i},\rho_{i})\mid\langle
c,\sigma,\rho\rangle\rightarrow^{n+1}\langle\textbf{nil},\sigma_{i},\rho_{i}\rangle\\}\
.$

We prove the above claim by induction on $n$.

    * 1.

$n=0$. On the left hand side, we have

$[\\![\textbf{While}^{0}]\\!]_{(\sigma,\rho)}=[\\![\textbf{if}~{}b~{}\textbf{then}~{}\textbf{abort}]\\!]_{(\sigma,\rho)}=\left\\{\begin{array}[]{ll}\varepsilon&\mbox{if
$[\\![b]\\!]_{\sigma}={\textbf{true}}$}\\\ (\sigma,\rho)&\mbox{if
$[\\![b]\\!]_{\sigma}={\textbf{false}}$}\end{array}\right..$

On the right hand side, we observe that

$\begin{array}[]{rcl}\langle\textbf{while}~{}b~{}\textbf{do}~{}c^{\prime},\sigma,\rho\rangle&\rightarrow&\langle\textbf{if}~{}b~{}\textbf{then}~{}(c^{\prime};\textbf{while}~{}b~{}\textbf{do}~{}c^{\prime})~{}\textbf{else}~{}{\textbf{skip}},\sigma,\rho\rangle\\\
&\rightarrow^{*}&\left\\{\begin{array}[]{ll}\langle(c^{\prime};\textbf{while}~{}b~{}\textbf{do}~{}c^{\prime}),\sigma,\rho\rangle&\mbox{if
$[\\![b]\\!]_{\sigma}={\textbf{true}}$}\\\
\langle{\textbf{skip}},\sigma,\rho\rangle&\mbox{if
$[\\![b]\\!]_{\sigma}={\textbf{false}}$}\end{array}\right.\end{array}$ (2)

The unfolding rule has been used in the first reduction step in (2). If
$[\\![b]\\!]_{\sigma}={\textbf{false}}$ then the claim clearly holds. If
$[\\![b]\\!]_{\sigma}={\textbf{true}}$ then the configuration
$\langle(c^{\prime};\textbf{while}~{}b~{}\textbf{do}~{}c^{\prime}),\sigma,\rho\rangle$
cannot reduce to any
$\langle\textbf{nil},\sigma^{\prime\prime},\rho^{\prime\prime}\rangle$ without
using the unfolding rule again, which means that there is no maximal
transition from $\langle c,\sigma,\rho\rangle$ that uses the unfolding rule at
most once. It follows that the claim also holds in this case.

    * 2.

Suppose $n=k+1$ and the claim holds for some $k$. On the left hand side, we
have

$\begin{array}[]{rcl}[\\![\textbf{While}^{k+1}]\\!]_{(\sigma,\rho)}&=&[\\![\textbf{if}~{}b~{}\textbf{then}~{}c^{\prime};\textbf{While}^{k}]\\!]_{(\sigma,\rho)}\\\
&=&\left\\{\begin{array}[]{ll}[\\![\textbf{While}^{k}]\\!]_{[\\![c^{\prime}]\\!]_{(\sigma,\rho)}}&\mbox{if
$[\\![b]\\!]_{\sigma}={\textbf{true}}$}\\\ (\sigma,\rho)&\mbox{if
$[\\![b]\\!]_{\sigma}={\textbf{false}}$}\end{array}\right.\end{array}$ (3)

On the right hand side, we have the same transitions as in (2). If
$[\\![b]\\!]_{\sigma}={\textbf{false}}$ then the claim clearly holds. If
$[\\![b]\\!]_{\sigma}={\textbf{true}}$ then we infer as follows. Since
$c^{\prime}$ is a subterm of $c$, we know from the hypothesis of the
structural induction that

$[\\![c^{\prime}]\\!]_{(\sigma,\rho)}=\sum_{j\in
J}\\{(\sigma_{j},\rho_{j})\mid\langle
c^{\prime},\sigma,\rho\rangle\rightarrow^{*}\langle\textbf{nil},\sigma_{j},\rho_{j}\rangle\\}$
(4)

for some set $J$. It follows that

$[\\![\textbf{While}^{k}]\\!]_{[\\![c^{\prime}]\\!]_{(\sigma,\rho)}}=\sum_{j\in
J}[\\![\textbf{While}^{k}]\\!]_{(\sigma_{j},\rho_{j})}\ .$ (5)

By induction hypothesis on $k$,

$[\\![\textbf{While}^{k}]\\!]_{(\sigma_{j},\rho_{j})}=\sum_{i\in
I_{j}}\\{(\sigma_{i},\rho_{i})\mid\langle
c,\sigma_{j},\rho_{j}\rangle\rightarrow^{k+1}\langle\textbf{nil},\sigma_{i},\rho_{i}\rangle\\}$
(6)

for some index set $I_{j}$. As a result, when
$[\\![b]\\!]_{\sigma}={\textbf{true}}$, we have

$\begin{array}[]{rll}\langle
c,\sigma,\rho\rangle&\rightarrow&\langle\textbf{if}~{}b~{}\textbf{then}~{}(c^{\prime};c)~{}\textbf{else}~{}{\textbf{skip}},\sigma,\rho\rangle\\\
&\rightarrow^{*}&\langle(c^{\prime};c),\sigma,\rho\rangle\\\
&\rightarrow^{*}&\langle c,\sigma_{j},\rho_{j}\rangle\qquad\mbox{by
(\ref{eq:0})}\\\
&\rightarrow^{k+1}&\langle\textbf{nil},\sigma_{i},\rho_{i}\rangle\qquad\mbox{by
(\ref{eq:bb})}\end{array}$ (7)

for each $j\in J$ and $i\in I_{j}$. This means that

$\langle
c,\sigma,\rho\rangle\rightarrow^{k+2}\langle\textbf{nil},\sigma_{i},\rho_{i}\rangle$
(8)

for each $j\in J$ and $i\in I_{j}$. Thus, we rewrite (6) as follows.

$[\\![\textbf{While}^{k}]\\!]_{(\sigma_{j},\rho_{j})}=\sum_{i\in
I_{j}}\\{(\sigma_{i},\rho_{i})\mid\langle
c,\sigma,\rho\rangle\rightarrow^{k+2}\langle\textbf{nil},\sigma_{i},\rho_{i}\rangle\\}$
(9)

Combining (3), (5) and (9), we obtain the desired result that

$[\\![\textbf{While}^{k+1}]\\!]_{(\sigma,\rho)}=\sum_{j\in J}\sum_{i\in
I_{j}}\\{(\sigma_{i},\rho_{i})\mid\langle
c,\sigma,\rho\rangle\rightarrow^{k+2}\langle\textbf{nil},\sigma_{i},\rho_{i}\rangle\\}$

So far we have proved the claim. Then by taking the limit on both sides of the
claim, we see that
$[\\![c]\\!]_{(\sigma,\rho)}=\sum_{i}\\{(\sigma_{i},\rho_{i})\mid\langle
c,\sigma,\rho\rangle\rightarrow^{*}\langle\textbf{nil},\sigma_{i},\rho_{i}\rangle\\}$.
$\Box$

##  4 An Abstract Proof System

In this section, we present an abstract proof system, where assertions are
arbitrary predicates on POVDs. We show that the proof system is sound and
relatively complete.

###### Definition 4.1

The set Assn of assertions is defined as $\cal{P}({\textbf{POVD}})$, the
powerset of POVD. Each assertion $P$ can be constructed by the following
grammar.

$P~{}:=~{}{\bf 1}_{\mu}\mid S\mid\neg P\mid P_{1}\wedge P_{2}\mid\Box\psi\mid
P_{1}\oplus P_{2}\mid P[f]$

where $\mu\in{\textbf{POVD}}$, $S\subseteq{\textbf{POVD}}$, $\psi$ is a
predicate over states and $f$ is a function from POVD to POVD.

Here ${\bf 1}_{\mu}$ is also called the characteristic function of the POVD
$\mu$, which is a predicate requiring that ${\bf 1}_{\mu}$ holds on
$\mu^{\prime}$ if and only if $\mu^{\prime}=\mu$, for any distribution state
$\mu^{\prime}$. The satisfaction relation $\models$ between a POVD and an
assertion is defined as follows.

$\begin{array}[]{rcl}\mu\models{\bf
1}_{\mu^{\prime}}&\mbox{iff}&\mu=\mu^{\prime}\\\ \mu\models
S&\mbox{iff}&\mu\in S\\\ \mu\models\neg P&\mbox{iff}&\mbox{not }\mu\models
P\\\ \mu\models P_{1}\wedge P_{2}&\mbox{iff}&\mu\models P_{1}\wedge\mu\models
P_{2}\\\ \mu\models\Box\psi&\mbox{iff}&\forall\sigma.\
\sigma\in\lceil{\mu}\rceil\Rightarrow[\\![\psi]\\!]_{\sigma}={\textbf{true}}\\\
\mu\models P_{1}\oplus P_{2}&\mbox{iff}&\exists\mu_{1},\mu_{2}.\
\mu=\mu_{1}+\mu_{2}\wedge\mu_{1}\models P_{1}\wedge\mu_{2}\models P_{2}\\\
\mu\models P[f]&\mbox{iff}&f(\mu)\models P\end{array}$

Let $[\\![P]\\!]:=\\{\mu\mid\mu\models P\\}$ be the semantic interpretation of
assertion $P$. We see that boolean operations of assertions are represented by
set operations. For example, we have $[\\![\neg
P]\\!]=\mathcal{P}({\textbf{POVD}})\backslash[\\![P]\\!]$ and
$[\\![P_{1}\wedge P_{2}]\\!]=[\\![P_{1}]\\!]\cap[\\![P_{2}]\\!]$. The
predicate $\Box\psi$ is lifted from a state predicate by requiring that
$\Box\psi$ holds on the POVD $\mu$ when $\psi$ holds on all the states in the
support of $\mu$. For example, a particular predicate over states is a boolean
expression $b$ with $\sigma\models b$ iff
$[\\![b]\\!]_{\sigma}={\textbf{true}}$. Therefore, the predicate $\Box b$
holds on the POVD $\mu$ when $b$ evaluates to be true under any state $\sigma$
in the support of $\mu$. The assertion $P_{1}\oplus P_{2}$ holds on the POVD
$\mu$ if we can split $\mu$ into the sum of two POVDs such that $P_{1}$ and
$P_{2}$ hold on each of them. Lastly, $P[f]$ holds on a POVD $\mu$ only when
$P$ holds on the image of $\mu$ under $f$.

###### Definition 4.2

A sequence of assertions $(P_{n})_{n\in{\mathbb{N}}^{\infty}}$ is _u-closed_ ,
if for each increasing sequence of POVDs $(\mu_{n})_{n\in{\mathbb{N}}}$ such
that $\mu_{n}\models P_{n}$ for all $n\in{\mathbb{N}}$, we have
$\lim_{n\rightarrow\infty}\mu_{n}\models P_{\infty}$.

###### Definition 4.3

A judgement is a triple in the form $\\{P\\}\;c\;\\{P^{\prime}\\}$, where $c$
is a command, $P$ and $P^{\prime}$ are assertions. It is valid, written
$\models\\{P\\}\;c\;\\{P^{\prime}\\}$, if

$\forall\mu.\ \mu\models P\ \Rightarrow\ [\\![c]\\!]_{\mu}\models P^{\prime}.$

In Figure 4 we give the rules for an abstract proof system denoted by
$\mathcal{S}_{a}$. It extends the system in [3] with the last three rules to
handle the manipulations of quantum systems. In order to show the soundness of
$\mathcal{S}_{a}$, we need a few technical lemmas.

$\begin{array}[]{c}\frac{\hbox
to68.72916pt{\hbox{$\begin{array}[]{c}\end{array}$}\hfil}}{\hbox{$\begin{array}[]{c}\\{P\\}\;{\textbf{skip}}\;\\{P\\}\end{array}$}}{[\sf
Skip]}\qquad\frac{\hbox
to94.00354pt{\hbox{$\begin{array}[]{c}\end{array}$}\hfil}}{\hbox{$\begin{array}[]{c}\\{P\\}\;\textbf{abort}\;\\{\Box{\textbf{false}}\\}\end{array}$}}{[\sf
Abort]}\qquad\frac{\hbox
to107.62051pt{\hbox{$\begin{array}[]{c}\end{array}$}\hfil}}{\hbox{$\begin{array}[]{c}\\{P[[\\![x:=a]\\!]]\\}\;x:=a\;\\{P\\}\end{array}$}}{[\sf
Assgn]\vspace{2mm}}\\\
\prooftree\\{P_{0}\\}\;c_{0}\;\\{P_{1}\\}\quad\\{P_{1}\\}\;c_{1}\;\\{P_{2}\\}\justifies\\{P_{0}\\}\;c_{0};c_{1}\;\\{P_{2}\\}\using[\sf
Seq]\endprooftree\par\qquad\prooftree\\{P_{0}\\}\;c\;\\{P^{\prime}_{0}\\}\quad\\{P_{1}\\}\;c\;\\{P^{\prime}_{1}\\}\justifies\\{P_{0}\oplus
P_{1}\\}\;c\;\\{P^{\prime}_{0}\oplus P^{\prime}_{1}\\}\using[\sf
Split]\endprooftree\vspace{2mm}\\\ \prooftree\\{P_{0}\wedge\Box
b\\}\;c_{0}\;\\{P^{\prime}_{0}\\}\quad\\{P_{1}\wedge\Box\neg
b\\}\;c_{1}\;\\{P^{\prime}_{1}\\}\justifies\\{(P_{0}\wedge\Box
b)\oplus(P_{1}\wedge\Box\neg
b)\\}\;\textbf{if}~{}b~{}\textbf{then}~{}c_{0}~{}\textbf{else}~{}c_{1}\;\\{P^{\prime}_{0}\oplus
P^{\prime}_{1}\\}\using[\sf Cond]\endprooftree\vspace{2mm}\\\
\prooftree\justifies\\{{\textbf{false}}\\}\;c\;\\{P\\}\using[\sf
Absurd]\endprooftree\par\qquad\prooftree P_{0}\Rightarrow
P_{1}\quad\\{P_{1}\\}\;c\;\\{P_{2}\\}\quad P_{2}\Rightarrow
P_{3}\justifies\\{P_{0}\\}\;c\;\\{P_{3}\\}\using[\sf
Conseq]\endprooftree\par\qquad\prooftree\forall\mu.\ \\{{\bf 1}_{\mu}\wedge
P\\}\;c\;\\{P^{\prime}\\}\justifies\\{P\\}\;c\;\\{P^{\prime}\\}\using[\sf
All]\endprooftree\vspace{2mm}\\\ \prooftree\begin{array}[]{c}\sf
uclosed((P^{\prime}_{n})_{n\in{\mathbb{N}}^{\infty}})\\\ \forall n.\
\\{P_{n}\\}\;\textbf{if}~{}b~{}\textbf{then}~{}c\;\\{P_{n+1}\\}\quad\forall
n.\
\\{P_{n}\\}\;\textbf{if}~{}b~{}\textbf{then}~{}\textbf{abort}\;\\{P^{\prime}_{n}\\}\end{array}\justifies\\{P_{0}\\}\;\textbf{while}~{}b~{}\textbf{do}~{}c\;\\{P^{\prime}_{\infty}\wedge\Box\neg
b\\}\using[\sf While]\endprooftree\vspace{2mm}\\\ \frac{\hbox
to118.59741pt{\hbox{$\begin{array}[]{c}\end{array}$}\hfil}}{\hbox{$\begin{array}[]{c}\\{P[[\\![q:=|0\rangle]\\!]]\\}\;q:=|0\rangle\;\\{P\\}\end{array}$}}{[\sf
QInit]}\qquad\frac{\hbox
to101.45425pt{\hbox{$\begin{array}[]{c}\end{array}$}\hfil}}{\hbox{$\begin{array}[]{c}\\{P[[\\![{U}[\bar{q}]]\\!]]\\}\;{U}[\bar{q}]\;\\{P\\}\end{array}$}}{[\sf
QUnit]\vspace{2mm}}\\\ \frac{\hbox
to139.74323pt{\hbox{$\begin{array}[]{c}\end{array}$}\hfil}}{\hbox{$\begin{array}[]{c}\\{P[[\\![x:={M}[\bar{q}]]\\!]]\\}\;x:={M}[\bar{q}]\;\\{P\\}\end{array}$}}{[\sf
QMeas]}\end{array}$ Figure 4: Proof rules for $\mathcal{S}_{a}$

###### Lemma 4.4

Let $P$ be an assertion and $c$ a command. Then
$\models\\{P[[\\![c]\\!]]\\}\;c\;\\{P\\}$.

  * Proof:

Suppose $\mu$ is a distribution state and $\mu\models P[[\\![c]\\!]]$. By the
definition of $P[[\\![c]\\!]]$, this means that $[\\![c]\\!]_{\mu}\models P$,
which is the desired result. $\Box$

###### Lemma 4.5

Let $\sigma$ be a classical state, $\rho_{1},\rho_{2}$ be two quantum states,
and $\mu_{1},\mu_{2}$ be two POVDs. For any command $c$, we have

  1. 1.

$[\\![c]\\!]_{(\sigma,\rho_{1}+\rho_{2})}=[\\![c]\\!]_{(\sigma,\rho_{1})}+[\\![c]\\!]_{(\sigma,\rho_{2})}$;

  2. 2.

$[\\![c]\\!]_{(\mu_{1}+\mu_{2})}=[\\![c]\\!]_{\mu_{1}}+[\\![c]\\!]_{\mu_{2}}$.

  * Proof:

The two clauses can be proved by a simultaneous induction on the structure of
command $c$. $\Box$

###### Lemma 4.6

For any commands $c_{0},c_{1}$ and distribution state $\mu$, we have
$[\\![c_{0};c_{1}]\\!]_{\mu}=[\\![c_{1}]\\!]_{[\\![c_{0}]\\!]_{\mu}}$.

  * Proof:

$\begin{array}[]{rcl}[\\![c_{1}]\\!]_{[\\![c_{0}]\\!]_{\mu}}&=&\sum_{\sigma}[\\![c_{1}]\\!]_{(\sigma,[\\![c_{0}]\\!]_{\mu}(\sigma))}\\\
&=&\sum_{\sigma}[\\![c_{1}]\\!]_{(\sigma,\sum_{\sigma^{\prime}}[\\![c_{0}]\\!]_{(\sigma^{\prime},\mu(\sigma^{\prime}))}(\sigma))}\\\
&=&\sum_{\sigma}\sum_{\sigma^{\prime}}[\\![c_{1}]\\!]_{(\sigma,[\\![c_{0}]\\!]_{(\sigma^{\prime},\mu(\sigma^{\prime}))}(\sigma))}\qquad\mbox{by
Lemma~{}\ref{lem:split}(1)}\\\
&=&\sum_{\sigma^{\prime}}\sum_{\sigma}[\\![c_{1}]\\!]_{(\sigma,[\\![c_{0}]\\!]_{(\sigma^{\prime},\mu(\sigma^{\prime}))}(\sigma))}\\\
&=&\sum_{\sigma^{\prime}}[\\![c_{1}]\\!]_{[\\![c_{0}]\\!]_{(\sigma^{\prime},\mu(\sigma^{\prime}))}}\\\
&=&\sum_{\sigma^{\prime}}[\\![c_{0};c_{1}]\\!]_{(\sigma^{\prime},\mu(\sigma^{\prime}))}\\\
&=&[\\![c_{0};c_{1}]\\!]_{\mu}\end{array}$

$\Box$

###### Theorem 4.7

(Soundness) Every judgement provable using the proof system $\mathcal{S}_{a}$
is valid.

  * Proof:

We analyze the cases one by one.

  * 1.

Rule [Skip]. Suppose $\mu\models P$ for some distribution state $\mu$. Then we
have $[\\![{\textbf{skip}}]\\!]_{\mu}=\mu$ and thus
$[\\![{\textbf{skip}}]\\!]_{\mu}\models P$ as required.

  * 2.

Rule [Abort]. This case is easy by noting that
$[\\![\textbf{abort}]\\!]_{\mu}=\varepsilon$ and
$\varepsilon\models\Box{\textbf{false}}$ for any $\mu$.

  * 3.

The cases for rules [Assgn], [QInit], [QUnit], and [QMeas] follow from Lemma
4.4.

  * 4.

Rule [Seq]. Suppose $\mu\models P_{0}$ for some distribution state $\mu$. By
the premises, both $\\{P_{0}\\}\;c_{0}\;\\{P_{1}\\}$ and
$\\{P_{1}\\}\;c_{1}\;\\{P_{2}\\}$ are valid. It follows that
$[\\![c_{0}]\\!]_{\mu}\models P_{1}$ and then
$[\\![c_{1}]\\!]_{[\\![c_{0}]\\!]_{\mu}}\models P_{2}$, which is
$[\\![c_{0};c_{1}]\\!]_{\mu}\models P_{2}$ by Lemma 4.6 as required.

  * 5.

Rule [Split]. Suppose $\mu\models P_{0}\oplus P_{1}$ for some distribution
state $\mu$. Then there exist $\mu_{0}$ and $\mu_{1}$ such that
$\mu=\mu_{0}+\mu_{1}$, $\mu_{0}\models P_{0}$ and $\mu_{1}\models P_{1}$. By
the premises, both $\\{P_{0}\\}\;c_{0}\;\\{P^{\prime}_{0}\\}$ and
$\\{P_{1}\\}\;c_{1}\;\\{P^{\prime}_{1}\\}$ are valid. Therefore, we have that
$[\\![c]\\!]_{\mu_{0}}\models P^{\prime}_{0}$ and
$[\\![c]\\!]_{\mu_{1}}\models P^{\prime}_{1}$. By Lemma 4.5 we obtain
$[\\![c]\\!]_{\mu}=[\\![c]\\!]_{\mu_{0}}+[\\![c]\\!]_{\mu_{1}}$. It follows
that $[\\![c]\\!]_{\mu}\models P^{\prime}_{0}\oplus P^{\prime}_{1}$ as
required.

  * 6.

Rule [Cond]. We first claim that $\\{P_{0}\wedge\Box
b\\}\;\textbf{if}~{}b~{}\textbf{then}~{}c_{0}~{}\textbf{else}~{}c_{1}\;\\{P^{\prime}_{0}\\}$
is valid. To see this, suppose $\mu$ is a POVD with $\mu\models
P_{0}\wedge\Box b$. Obviously, we have $\mu\models\Box b$ and thus
$[\\![b]\\!]_{\sigma}={\textbf{true}}$ for each $\sigma\in\lceil{\mu}\rceil$.
It follows that

$\begin{array}[]{rcl}[\\![\textbf{if}~{}b~{}\textbf{then}~{}c_{0}~{}\textbf{else}~{}c_{1}]\\!]_{\mu}&=&\sum_{\sigma}[\\![\textbf{if}~{}b~{}\textbf{then}~{}c_{0}~{}\textbf{else}~{}c_{1}]\\!]_{(\sigma,\mu(\sigma))}\\\
&=&\sum_{\sigma}[\\![c_{0}]\\!]_{(\sigma,\mu(\sigma))}\\\
&=&[\\![c_{0}]\\!]_{\mu}.\end{array}$

By the first premise, $\\{P_{0}\wedge\Box b\\}\;c_{0}\;\\{P^{\prime}_{0}\\}$
is valid. Therefore, we have $[\\![c_{0}]\\!]_{\mu}\models P^{\prime}_{0}$,
and thus

$[\\![\textbf{if}~{}b~{}\textbf{then}~{}c_{0}~{}\textbf{else}~{}c_{1}]\\!]_{\mu}\models
P^{\prime}_{0}$

and the above claim is proved. Similarly, we can prove that
$\\{P_{1}\wedge\Box\neg
b\\}\;\textbf{if}~{}b~{}\textbf{then}~{}c_{0}~{}\textbf{else}~{}c_{1}\;\\{P^{\prime}_{1}\\}$
is valid. By the soundness of [Split], it follows that

$\\{(P_{0}\wedge\Box b)\oplus(P_{1}\wedge\Box\neg
b)\\}\;\textbf{if}~{}b~{}\textbf{then}~{}c_{0}~{}\textbf{else}~{}c_{1}\;\\{P^{\prime}_{0}\oplus
P^{\prime}_{1}\\}$

is also valid.

  * 7.

Rule [Absurd]. There exists no $\mu$ with $\mu\models{\textbf{false}}$. Thus,
we always have $\forall\mu.\
\mu\models{\textbf{false}}\Rightarrow[\\![c]\\!]_{\mu}\models P$.

  * 8.

Rule [Conseq]. Let $\mu$ be a distribution state and $\mu\models P_{0}$. The
first premise gives $\mu\models P_{1}$. The second premise tells us that
$[\\![c]\\!]_{\mu}\models P_{2}$. By the third premise, we derive that
$[\\![c]\\!]_{\mu}\models P_{3}$. It follows that
$\\{P_{0}\\}\;c\;\\{P_{3}\\}$ is valid.

  * 9.

Rule [All]. Let $\mu$ be a POVD and $\mu\models P$. It is clear that
$\mu\models{\bf 1}_{\mu}\wedge P$. By the premise, $\\{{\bf 1}_{\mu}\wedge
P\\}\;c\;\\{P^{\prime}\\}$ is valid. Therefore, we have
$[\\![c]\\!]_{\mu}\models P^{\prime}$, and thus $\\{P\\}\;c\;\\{P^{\prime}\\}$
is valid.

  * 10.

Rule [While]. We first observe that, for any state $(\sigma,\rho)$,

$[\\![\textbf{if}~{}b~{}\textbf{then}~{}\textbf{abort}]\\!]_{(\sigma,\rho)}=\left\\{\begin{array}[]{ll}\varepsilon&\mbox{if
$[\\![b]\\!]_{(\sigma,\rho)}={\textbf{true}}$}\\\ {(\sigma,\rho)}&\mbox{if
$[\\![b]\\!]_{(\sigma,\rho)}={\textbf{false}}$}\ .\end{array}\right.$

Thus, if a state $\sigma^{\prime}$ is in the support of
$[\\![\textbf{if}~{}b~{}\textbf{then}~{}\textbf{abort}]\\!]_{(\sigma,\rho)}$,
it must be the case that $\sigma^{\prime}\models\neg b$. Furthermore, for any
distribution state $\mu$, if a state $\sigma^{\prime}$ is in the support of
$[\\![\textbf{if}~{}b~{}\textbf{then}~{}\textbf{abort}]\\!]_{\mu}$ then
$\sigma^{\prime}\models\neg b$. It follows that, for any command $c^{\prime}$
and distribution state $\mu$, we have

$[\\![c^{\prime};\textbf{if}~{}b~{}\textbf{then}~{}\textbf{abort}]\\!]_{\mu}\models\Box\neg
b.$

By definition, $[\\![\textbf{while}~{}b~{}\textbf{do}~{}c]\\!]_{\mu}$ is the
limit of the sequence

$([\\![(\textbf{if}~{}b~{}\textbf{then}~{}c)^{n};\textbf{if}~{}b~{}\textbf{then}~{}\textbf{abort}]\\!]_{\mu})_{n\in{\mathbb{N}}}$

and so we have that

$[\\![\textbf{while}~{}b~{}\textbf{do}~{}c]\\!]_{\mu}\models\Box\neg b.$ (10)

By the first premise and the soundness of [Seq], it is easy to show by
induction that

$\forall n.\
\\{P_{0}\\}\;(\textbf{if}~{}b~{}\textbf{then}~{}c)^{n}\;\\{P_{n}\\}$

is valid. By the second premise and [Seg] again, the following judgement

$\forall n.\
\\{P_{0}\\}\;(\textbf{if}~{}b~{}\textbf{then}~{}c)^{n};\textbf{if}~{}b~{}\textbf{then}~{}\textbf{abort}\;\\{P^{\prime}_{n}\\}$

is valid. Let $\mu$ be any POVD with $\mu\models P_{0}$. Then

$\forall n.\
[\\![(\textbf{if}~{}b~{}\textbf{then}~{}c)^{n};\textbf{if}~{}b~{}\textbf{then}~{}\textbf{abort}]\\!]_{\mu}\models
P^{\prime}_{n}.$

By assumption, the sequence of assertions
$(P^{\prime}_{n})_{n\in{\mathbb{N}}^{\infty}}$ is u-closed. Hence, we can
infer that

$[\\![\textbf{while}~{}b~{}\textbf{do}~{}c]\\!]_{\mu}\models
P^{\prime}_{\infty},$

which means that the judgement

$\\{P_{0}\\}\;\textbf{while}~{}b~{}\textbf{do}~{}c\;\\{P^{\prime}_{\infty}\\}$
(11)

is valid. Combining (10) and (11), we finally obtain that
$\\{P_{0}\\}\;\textbf{while}~{}b~{}\textbf{do}~{}c\;\\{P^{\prime}_{\infty}\wedge\Box\neg
b\\}$ is valid.

$\Box$

Now we turn to the relative completeness of the proof system
$\mathcal{S}_{a}$. Formulas of the form ${\bf 1}_{\mu}$ will be helpful for
that purpose.

###### Lemma 4.8

For any distribution state $\mu$ and command $c$,

${\bf 1}_{\mu}\Rightarrow{\bf 1}_{[\\![c]\\!]_{\mu}}[[\\![c]\\!]].$

  * Proof:

Let $\mu^{\prime}$ be any distribution state.

$\begin{array}[]{rcl}\mu^{\prime}\models{\bf
1}_{\mu}&\Leftrightarrow&\mu^{\prime}=\mu\\\
&\Rightarrow&[\\![c]\\!]_{\mu^{\prime}}=[\\![c]\\!]_{\mu}\\\
&\Leftrightarrow&[\\![c]\\!]_{\mu^{\prime}}\models{\bf
1}_{[\\![c]\\!]_{\mu}}\\\ &\Leftrightarrow&\mu^{\prime}\models{\bf
1}_{[\\![c]\\!]_{\mu}}[[\\![c]\\!]]\end{array}$

$\Box$

###### Definition 4.9

Let $\mu$ be a distribution state and $b$ a boolean expression. The
restriction $\mu_{|b}$ of $\mu$ to $b$ is the distribution state such that
$\mu_{|b}(\sigma)=\mu(\sigma)$ if $[\\![b]\\!]_{\sigma}={\textbf{true}}$ and
$0$ otherwise.

According to the definition above, it is easy to see that we can split any
$\mu$ into two parts w.r.t. a boolean expression.

###### Lemma 4.10

For any distribution state $\mu$ and boolean expression b, we have
$\mu=\mu_{|b}+\mu_{|\neg b}$.

  * Proof:

This is straightforward because, at each state $\sigma$ in the support of
$\mu$, the boolean expression $b$ evaluates to either true or false. $\Box$

With Lemmas 4.10 and 4.5, it is easy to see that the denotational semantics of
conditional commands can be rewritten as follows.

$[\\![\textbf{if}~{}b~{}\textbf{then}~{}c_{0}~{}\textbf{else}~{}c_{1}]\\!]_{\mu}~{}=~{}[\\![c_{0}]\\!]_{\mu_{|b}}+[\\![c_{1}]\\!]_{\mu_{|\neg
b}}$ (12)

The following facts are also easy to show.

$\begin{array}[]{rcl}{\bf 1}_{\mu|b}&\Leftrightarrow&{\bf 1}_{\mu|b}\wedge\Box
b\\\ {\bf 1}_{\mu}&\Leftrightarrow&{\bf 1}_{\mu}\wedge P\qquad\mbox{if
$\mu\models P$}\\\ {\bf 1}_{\mu}&\Leftrightarrow&{\bf 1}_{\mu|b}\oplus{\bf
1}_{\mu|\neg b}\\\ {\bf 1}_{\mu_{1}+\mu_{2}}&\Leftrightarrow&{\bf
1}_{\mu_{1}}\oplus{\bf 1}_{\mu_{2}}\end{array}$ (13)

###### Lemma 4.11

For any POVD $\mu$, the following judgement is provable:

$\\{{\bf 1}_{\mu}\\}\;c\;\\{{\bf 1}_{[\\![c]\\!]_{\mu}}\\}.$

  * Proof:

We proceed by induction on the structure of $c$.

    * 1.

$c\equiv{\textbf{skip}}$. This case is immediate as
$[\\![{\textbf{skip}}]\\!]_{\mu}=\mu$ and by [Skip] we have $\vdash\\{{\bf
1}_{\mu}\\}\;c\;\\{{\bf 1}_{\mu}\\}.$

    * 2.

$c\equiv\textbf{abort}$. Then $[\\![c]\\!]_{\mu}=\varepsilon$. For any POVD
$\mu^{\prime}$, we note that

$\mu^{\prime}\models\Box{\textbf{false}}~{}\Leftrightarrow~{}\mu^{\prime}=\varepsilon~{}\Leftrightarrow~{}\mu^{\prime}\models{\bf
1}_{\varepsilon}.$

By rules [Abort] and [Conseq] we can infer $\vdash\\{{\bf
1}_{\mu}\\}\;c\;\\{{\bf 1}_{\varepsilon}\\}$.

    * 3.

$c\equiv x:=a,\ q:=|0\rangle,\ {U}[\bar{q}]$ or $x:={M}[\bar{q}]$. By the
corresponding rules [Assgn], [QInit], [QUnit] or [QMeas], we have

$\vdash\\{{\bf 1}_{[\\![c]\\!]_{\mu}}[[\\![c]\\!]]\\}\;c\;\\{{\bf
1}_{[\\![c]\\!]_{\mu}}\\}.$

By Lemma 4.8 and rule [Conseq], we obtain that $\vdash\\{{\bf
1}_{\mu}\\}\;c\;\\{{\bf 1}_{[\\![c]\\!]_{\mu}}\\}.$

    * 4.

$c\equiv c_{0};c_{1}$. By induction, we have $\vdash\\{{\bf
1}_{\mu}\\}\;c_{0}\;\\{{\bf 1}_{[\\![c_{0}]\\!]_{\mu}}\\}$ and $\vdash\\{{\bf
1}_{[\\![c_{0}]\\!]_{\mu}}\\}\;c_{1}\;\\{{\bf
1}_{[\\![c_{1}]\\!]_{[\\![c_{0}]\\!]_{\mu}}}\\}$. Using the rule [Seq], we
obtain that $\vdash\\{{\bf 1}_{\mu}\\}\;c\;\\{{\bf
1}_{[\\![c_{1}]\\!]_{[\\![c]\\!]_{\mu}}}\\}$.

    * 5.

$c\equiv\textbf{if}~{}b~{}\textbf{then}~{}c_{0}~{}\textbf{else}~{}c_{1}$. By
induction, we have $\vdash\\{{\bf 1}_{\mu_{|b}}\\}\;c_{0}\;\\{{\bf
1}_{[\\![c_{0}]\\!]_{\mu_{|b}}}\\}$. By the first clause in (13) and rule
[Conseq], we have $\vdash\\{{\bf 1}_{\mu_{|b}}\wedge\Box b\\}\;c_{0}\;\\{{\bf
1}_{[\\![c_{0}]\\!]_{\mu_{|b}}}\\}$. Similarly, $\vdash\\{{\bf 1}_{\mu_{|\neg
b}}\wedge\Box\neg b\\}\;c_{1}\;\\{{\bf 1}_{[\\![c_{1}]\\!]_{\mu_{|\neg
b}}}\\}$. Using rule [Cond], we infer

$\vdash\\{({\bf 1}_{\mu_{|b}}\wedge\Box b)\oplus({\bf 1}_{\mu_{|\neg
b}}\wedge\Box\neg
b)\\}\;\textbf{if}~{}b~{}\textbf{then}~{}c_{0}~{}\textbf{else}~{}c_{1}\;\\{{\bf
1}_{[\\![c_{0}]\\!]_{\mu_{|b}}}\oplus{\bf 1}_{[\\![c_{1}]\\!]_{\mu_{|\neg
b}}}\\}.$

Using (12), (13) and rule [Conseq], we finally obtain that

$\vdash\\{{\bf
1}_{\mu}\\}\;\textbf{if}~{}b~{}\textbf{then}~{}c_{0}~{}\textbf{else}~{}c_{1}\;\\{{\bf
1}_{[\\![\textbf{if}~{}b~{}\textbf{then}~{}c_{0}~{}\textbf{else}~{}c_{1}]\\!]_{\mu}}\\}.$

    * 6.

$c\equiv\textbf{while}~{}b~{}\textbf{do}~{}c^{\prime}$. For each
$n\in{\mathbb{N}}$, let

$\begin{array}[]{rcl}P_{n}&=&{\bf
1}_{[\\![(\textbf{if}~{}b~{}\textbf{then}~{}c^{\prime})^{n}]\\!]_{\mu}}\\\
P^{\prime}_{n}&=&{\bf
1}_{[\\![(\textbf{if}~{}b~{}\textbf{then}~{}c^{\prime})^{n};\textbf{if}~{}b~{}\textbf{then}~{}\textbf{abort}]\\!]_{\mu}}\\\
P^{\prime}_{\infty}&=&{\bf
1}_{\lim_{n\rightarrow\infty}[\\![(\textbf{if}~{}b~{}\textbf{then}~{}c^{\prime})^{n};\textbf{if}~{}b~{}\textbf{then}~{}\textbf{abort}]\\!]_{\mu}}\end{array}$

Obviously, the sequence of assertions
$(P^{\prime}_{n})_{n\in{\mathbb{N}}^{\infty}}$ is u-closed. As in the last
case, we can show that
$\vdash\\{P_{n}\\}\;\textbf{if}~{}b~{}\textbf{then}~{}c^{\prime}\;\\{P_{n+1}\\}$
by induction hypothesis and rules [Conseq], [Skip] and [Cond]. It is also easy
to see that
$\vdash\\{P_{n}\\}\;\textbf{if}~{}b~{}\textbf{then}~{}\textbf{abort}\;\\{P^{\prime}_{n}\\}$
for each $n\in{\mathbb{N}}$. Therefore, we can use rule [While] to infer that
$\vdash\\{P_{0}\\}\;\textbf{while}~{}b~{}\textbf{do}~{}c\;\\{P^{\prime}_{\infty}\wedge\Box\neg
b\\}$. Using (10), the second clause of (13), and rule [Conseq], we obtain
that
$\vdash\\{P_{0}\\}\;\textbf{while}~{}b~{}\textbf{do}~{}c\;\\{P^{\prime}_{\infty}\\}$,
which is exactly $\vdash\\{{\bf
1}_{\mu}\\}\;\textbf{while}~{}b~{}\textbf{do}~{}c^{\prime}\;\\{{\bf
1}_{[\\![\textbf{while}~{}b~{}\textbf{do}~{}c^{\prime}]\\!]_{\mu}}\\}$.

$\Box$

With the preparations above, we are in the position to show that the proof
system ${\cal{S}}_{a}$ is relatively complete.

###### Theorem 4.12

(Relative completeness) Every valid judgement is derivable in ${\cal{S}}_{a}$.

  * Proof:

Let $\\{P\\}\;c\;\\{P^{\prime}\\}$ be a valid judgement. Suppose $\mu$ be any
POVD. There are two possibilities:

    * 1.

$\mu\models P$. The validity of the judgement says that
$[\\![c]\\!]_{\mu}\models P^{\prime}$. By Lemma 4.11, we have that
$\vdash\\{{\bf 1}_{\mu}\\}\;c\;\\{{\bf 1}_{[\\![c]\\!]_{\mu}}\\}$. By the
second clause of (13) and rule [Conseq], we can obtain that $\vdash\\{{\bf
1}_{\mu}\wedge P\\}\;c\;\\{{\bf 1}_{[\\![c]\\!]_{\mu}}\wedge P^{\prime}\\}$.
Using [Conseq] again gives $\vdash\\{{\bf 1}_{\mu}\wedge
P\\}\;c\;\\{P^{\prime}\\}$.

    * 2.

$\mu\not\models P$. Then it is obvious that ${\bf 1}_{\mu}\wedge
P\Leftrightarrow{\textbf{false}}$. By rules [Absurd] and [Conseq], we also
obtain $\vdash\\{{\bf 1}_{\mu}\wedge P\\}\;c\;\\{P^{\prime}\\}$.

Since $\mu$ is arbitrarily chosen, the premise of rule [All] is derivable.
Therefore, we can use that rule to obtain
$\vdash\\{P\\}\;c\;\\{P^{\prime}\\}$. $\Box$

##  5 A Concrete Program Logic

In this section, we present a concrete program logic. We first define the
concrete syntax of assertions. Following [3], we define a two-level assertion
language in Figure 5. Formally, assertions are divided into two categories:
_state assertions_ are formulas that describe the properties of machine states
and _distribution assertions_ are used to describe the properties of POVDs.
Distribution assertions are based on comparison of distribution expressions,
or built with first-order quantifiers and connectives, as well as the
connective $\oplus$ mentioned in Section 4. A _distribution expression_ is
either the expectation ${\mathbb{E}}[e]$ of a state expression $e$, the
expectation ${\mathbb{E}}_{\bar{x}\sim M[\bar{q}]}[e]$ of state expression $e$
w.r.t. the measurement $M$, or an operator applied to distribution
expressions. A _state expression_ is either a classical variable, the
characteristic function ${\bf 1}_{\psi}$ of a state assertion $\psi$, or an
operator applied to state expressions. Finally, a _state assertion_ is either
a comparison of state expressions, or a first-order formula over state
assertions. In particular, the boolean expressions in Bexp are included as
state assertions. Note that the set of operators is left unspecified but we
assume that some basic operators such as addition, subtraction, scalar
multiplication for both arithmetic expressions and matrix representation of
partial density operators are included. With a slight abuse of notation, when
$\leq$ is used to compare matrices, we essentially mean $\sqsubseteq$.
Similarly for $<$ and $=$.

For convenience of presentation, in this section we consider a general form of
quantum measurement.

###### Definition 5.1

A _general measurement_ $M$ is a pair $\langle\\{M_{i}\\}_{i\in
I},{l}\rangle$, where each $M_{i}$ is a measurement operator as usual, and
${l}:I\mapsto J$ is a labelling function that maps each measurement outcome
$i$ to some some label ${l}(i)$.

If the state of a quantum system is specified by density operator $\rho$
immediately before the measurement $M$, then the probability with which those
results with label $j$ occur is given by

$p(j)=\sum_{i:{l}(i)=j}{\rm tr}(M^{\dagger}_{i}M_{i}\rho),$

and the state of the system after the measurement is

$\\\ \frac{\sum_{i:{l}(i)=j}M_{i}\rho M^{\dagger}_{i}}{p(j)}.$

General measurements are convenient to describe the situation where we would
like to group some measurement outcomes. For example, if $i_{1},i_{2}\in I$
are two different outcomes, but for some reasons we would not like to
distinguish them, then we simply give them the same label by letting
${l}(l_{1})={l}(l_{2})$. In the special case that $l$ is the identity function
${\it Id}$, then the labelling function has no effect and we degenerate to the
usual notion of measurements.

$\begin{array}[]{rcll}e&::=&x\mid{\bf 1}_{\psi}\mid o(\mathbf{e})&\mbox{(State
expressions)}\\\ \psi&::=&e\rhd\\!\\!\\!\lhd e\mid FO(\psi)&\mbox{(State
assertions)}\\\ r&::=&{\mathbb{E}}[e]\mid{\mathbb{E}}_{\bar{x}\sim
M[\bar{q}]}[e]\mid o(\mathbf{r})&\mbox{(Distribution expressions)}\\\
P&::=&r\rhd\\!\\!\\!\lhd r\mid P\oplus P\mid FO(P)&\mbox{(Distribution
assertions)}\\\ \rhd\\!\\!\lhd&\in&\\{=,\ <,\ \leq\\}\qquad o\in
Ops&\mbox{(Operations)}\end{array}$ Figure 5: Syntax of assertions
$\begin{array}[]{rcl}[\\![x]\\!]_{\sigma}&:=&\sigma(x)\\\ [\\![{\bf
1}_{\psi}]\\!]_{\sigma}&:=&{\bf 1}_{[\\![\psi]\\!]_{\sigma}}\\\
[\\![o(e)]\\!]_{\sigma}&:=&o([\\![e]\\!]_{\sigma})\\\ \hline\cr\\\
[\\![e_{1}\rhd\\!\\!\\!\lhd
e_{2}]\\!]_{\sigma}&:=&[\\![e_{1}]\\!]_{\sigma}\rhd\\!\\!\\!\lhd[\\![e_{2}]\\!]_{\sigma}\\\
[\\![FO(\psi)]\\!]_{\sigma}&:=&FO([\\![\psi]\\!]_{\sigma})\\\ \hline\cr\\\
[\\![{\mathbb{E}}[e]]\\!]_{\mu}&:=&\sum_{\sigma}\mu(\sigma)\cdot[\\![e]\\!]_{\sigma}\\\
[\\![{\mathbb{E}}_{\bar{x}\sim
M[\bar{q}]}[e]]\\!]_{\mu}&:=&\sum_{\sigma}\sum_{i}M_{i}\mu(\sigma)M_{i}^{\dagger}\cdot[\\![e]\\!]_{\sigma[l(i)/\bar{x}]}\\\
&&\mbox{where $M=\langle\\{M_{i}\\}_{i\in I},{l}\rangle$}\\\
[\\![o(r)]\\!]_{\mu}&:=&o([\\![r]\\!]_{\mu})\\\ \hline\cr\\\
[\\![r_{1}\rhd\\!\\!\\!\lhd
r_{2}]\\!]_{\mu}&:=&[\\![r_{1}]\\!]_{\mu}\rhd\\!\\!\\!\lhd[\\![r_{2}]\\!]_{\mu}\\\
[\\![P_{1}\oplus P_{2}]\\!]_{\mu}&:=&\exists\mu_{1},\mu_{2}.\
\mu=\mu_{1}+\mu_{2}\wedge[\\![P_{1}]\\!]_{\mu_{1}}\wedge[\\![P_{2}]\\!]_{\mu_{2}}\\\
[\\![FO(P)]\\!]_{\mu}&:=&FO([\\![P]\\!]_{\mu})\end{array}$ Figure 6: Semantics
of assertions

The interpretation of assertions is given in Figure 6. Comparing the
interpretation with that in [3], we see that the main difference is the
introduction of a distribution expression related to a quantum measurement.
The meaning of ${\mathbb{E}}_{\bar{x}\sim M[\bar{q}]}[e]$ is the expected
Hermitian operator weighted by the value of $e$ after a measurement entailed
by $M$.

Note that the formula $\Box\psi$, where $\psi$ is a state assertion, can now
be viewed as a syntactic sugar in view of the following lemma.

###### Lemma 5.2

  1. 1.

$\Box\psi\ \Leftrightarrow\ {\mathbb{E}}[{\bf 1}_{\psi}]={\mathbb{E}}[{\bf
1}_{{\textbf{true}}}]$

  2. 2.

$\Box\psi\ \Leftrightarrow\ {\mathbb{E}}_{\bar{x}\sim M[\bar{q}]}[{\bf
1}_{\psi}]={\mathbb{E}}_{\bar{x}\sim M[\bar{q}]}[{\bf 1}_{{\textbf{true}}}]$

  3. 3.

$\Box\psi\ \Leftrightarrow\ \Box(\psi\wedge b)\oplus\Box(\psi\wedge\neg b)$

  * Proof:

Let us consider the first clause; the second one is similar and the third one
is easier.

$\begin{array}[]{lcl}\mu\models\Box\psi&\mbox{iff}&\forall\sigma\in\lceil{\mu}\rceil.[\\![\psi]\\!]_{\sigma}={\textbf{true}}\\\
&\mbox{iff}&\sum_{\sigma}\mu(\sigma)\cdot[\\![{\bf
1}_{\psi}]\\!]_{\sigma}=\sum_{\sigma}\mu(\sigma)\cdot[\\![{\bf
1}_{{\textbf{true}}}]\\!]_{\sigma}\\\ &\mbox{iff}&[\\![{\mathbb{E}}[{\bf
1}_{\psi}]]\\!]_{\mu}=[\\![{\mathbb{E}}[{\bf 1}_{\textbf{true}}]]\\!]_{\mu}\\\
&\mbox{iff}&\mu\models({\mathbb{E}}[{\bf 1}_{\psi}]={\mathbb{E}}[{\bf
1}_{{\textbf{true}}}])\end{array}$

$\Box$

Using the concrete syntax for assertions, we propose a syntactic version of
the existing proof rules by avoiding the semantics of commands. We call the
concrete proof system $\mathcal{S}_{c}$. Specifically, we keep all proof rules
in Figure 4 but replace [Assgn], [QInit], [QUnit], and [QMeas] with the four
rules in Figure 7.

$\begin{array}[]{c}\frac{\hbox
to94.28705pt{\hbox{$\begin{array}[]{c}\end{array}$}\hfil}}{\hbox{$\begin{array}[]{c}\\{P[a/x]\\}\;x:=a\;\\{P\\}\end{array}$}}{[\sf
Assgn^{\prime}]}\qquad\prooftree\justifies\\{h(P)\\}\;q:=|0\rangle\;\\{P\\}\using[\sf
QInit^{\prime}]\endprooftree\vspace{2mm}\\\
\prooftree\justifies\\{g^{U}(P)\\}\;U[\bar{q}]\;\\{P\\}\using[\sf
QUnit^{\prime}]\endprooftree\qquad\prooftree\justifies\\{f_{x,\bar{q}}^{M}(P)\\}\;x:=M[\bar{q}]\;\\{P\\}\using[\sf
QMeas^{\prime}]\endprooftree\end{array}$ Figure 7: Selected syntactic proof
rules

In rule [QInit’] we use the notation $h(P)$ for a syntactic substitution. It
changes all ${\mathbb{E}}_{\bar{x}\sim M[\bar{q}]}[e]$ in $P$ into
${\mathbb{E}}_{\bar{x}\sim M^{\prime}[\bar{q}]}[e]$ and distributes over most
other syntactic constructors of assertions, where $M^{\prime}$ is obtained
from $M=\langle\\{M_{i}\\}_{i},l\rangle$ by constructing two measurement
operators $M_{i0},M_{i1}$ for each $M_{i}$ in $M$ with the mapping
${l}^{\prime}$ given by ${l}^{\prime}(i0)={l}^{\prime}(i1)=l(i)$. A formal
definition is given below.

$\begin{array}[]{rcl}h(o(\mathbf{r}))&:=&o(h(\mathbf{r}))\qquad\mbox{where
$o\in Ops$}\\\ h({\mathbb{E}}[e])&:=&{\mathbb{E}}_{x\sim
M[q]}[e]\qquad\mbox{where }M=\langle\\{M_{0},M_{1}\\},Id\rangle\mbox{ with
}M_{0}=|0\rangle\langle 0|,\ M_{1}=|0\rangle\langle 1|,\\\ &&\hfill\ x\mbox{
is fresh}\\\ h({\mathbb{E}}_{\bar{x}\sim
M[\bar{q}]}[e])&:=&{\mathbb{E}}_{\bar{x}\sim
M^{\prime}[\bar{q}]}[e]\quad\mbox{where
}M^{\prime}=\langle\\{M_{i0},M_{i1}\\}_{i},{l}^{\prime}\rangle\\\
&&\hfill\mbox{ with }M_{i0}=M_{i}|0\rangle\langle 0|,\
M_{i1}=M_{i}|0\rangle\langle 1|,{l}^{\prime}(i0)={l}^{\prime}(i1)=l(i)\\\
h(r_{1}\rhd\\!\\!\\!\lhd r_{2})&:=&h(r_{1})\rhd\\!\\!\\!\lhd h(r_{2})\\\
h(FO(P))&:=&FO(h(P))\\\ h(P_{1}\oplus P_{2})&:=&h(P_{1})\oplus
h(P_{2})\end{array}$

To ensure the freshness requirement on $x$ in $h({\mathbb{E}}[e])$, we assume
an enumeration of all the variables in Cvar. Each time a fresh variable is
needed, we take the next one which has not appeared in all the programs under
consideration.

In rule [QUnit’] we use the notation $g^{U}(P)$ for a syntactic substitution.
It changes all ${\mathbb{E}}_{\bar{x}\sim M[\bar{q}]}[e]$ in $P$ into
${\mathbb{E}}_{\bar{x}\sim M^{\prime}[\bar{q}]}[e]$, where
$M=\langle\\{M_{i}\\}_{i\in I},{l}\rangle$,
$M^{\prime}=\langle\\{M_{i}U\\}_{i\in I},{l}\rangle$, and distributes over
most other syntactic constructors of assertions. A formal definition is given
below.

$\begin{array}[]{rcl}g^{U}(o(r))&:=&o(g^{U}(r))\qquad\mbox{where $o\in
Ops$}\\\ g^{U}({\mathbb{E}}[e])&:=&{\mathbb{E}}_{x\sim
M[\bar{q}]}[e]\qquad\mbox{where }M=\langle\\{M_{0}\\},Id\rangle\mbox{ with
}M_{0}=U\mbox{ and $x$ is fresh}\\\ g^{U}({\mathbb{E}}_{\bar{x}\sim
M[\bar{q}]}[e])&:=&{\mathbb{E}}_{\bar{x}\sim
M^{\prime}[\bar{q}]}[e]\qquad\mbox{where }M^{\prime}=\langle\\{M_{i}U\\}_{i\in
I},{l}\rangle\\\ g^{U}(r_{1}\rhd\\!\\!\\!\lhd
r_{2})&:=&g^{U}(r_{1})\rhd\\!\\!\\!\lhd g^{U}(r_{2})\\\
g^{U}(FO(P))&:=&FO(g^{U}(P))\\\ g^{U}(P_{1}\oplus P_{2})&:=&g^{U}(P_{1})\oplus
g^{U}(P_{2})\end{array}$

In rule [QMeas’] we use the notation $f_{x,\bar{q}}^{M}(P)$ for a syntactic
substitution. It changes all ${\mathbb{E}}[e]$ in $P$ into
${\mathbb{E}}_{x\sim M[\bar{q}]}[e]$. For the distribution expression
${\mathbb{E}}_{\bar{y}\sim N[\bar{q}]}[e]$, it adds an outer layer of
measurement to $N$. A formal definition is given below.

$\begin{array}[]{rcl}f_{x,\bar{q}}^{M}(o(r))&:=&o(f_{x,\bar{q}}^{M}(r))\qquad\mbox{where
$o\in Ops$}\\\ f_{x,\bar{q}}^{M}({\mathbb{E}}[e])&:=&{\mathbb{E}}_{x\sim
M[\bar{q}]}[e]\\\ f_{x,\bar{q}}^{M}({\mathbb{E}}_{\bar{y}\sim
N[\bar{q^{\prime}}]}[e])&:=&\left\\{\begin{array}[]{ll}{\mathbb{E}}_{x\bar{y}\sim
M^{\prime}[\bar{q}\cup\bar{q^{\prime}}]}[e]\mbox{ with
}M^{\prime}=\langle\\{N_{j}M_{i}\\}_{ij},k^{\prime}\rangle\mbox{ and
}k^{\prime}(ij)=(k(i),l(j))&\mbox{if }x\not\in\bar{y}\\\
{\mathbb{E}}_{\bar{y}\sim M^{\prime}[\bar{q}\cup\bar{q^{\prime}}]}[e]\mbox{
with }M^{\prime}=\langle\\{N_{j}M_{i}\\}_{ij},k^{\prime}\rangle\mbox{ and
}k^{\prime}(ij)=l(j)&\mbox{if }x\in\bar{y}\end{array}\right.\\\
f_{x,\bar{q}}^{M}(r_{1}\rhd\\!\\!\\!\lhd
r_{2})&:=&f_{x,\bar{q}}^{M}(r_{1})\rhd\\!\\!\\!\lhd
f_{x,\bar{q}}^{M}(r_{2})\\\
f_{x,\bar{q}}^{M}(FO(P))&:=&FO(f_{x,\bar{q}}^{M}(P))\\\
f_{x,\bar{q}}^{M}(P_{1}\oplus P_{2})&:=&f_{x,\bar{q}}^{M}(P_{1})\oplus
f_{x,\bar{q}}^{M}(P_{2})\end{array}$

We are going to show that the three functions $h(\cdot)$, $g^{U}(\cdot)$ and
$f^{M}_{x,\bar{q}}(\cdot)$ behave well as they help to transform
postconditions into preconditions for three kinds of commands: initialisation,
applications of unitary operations, and measurements of quantum systems.

###### Lemma 5.3

The following two clauses hold.

  1. (i)

$[\\![h(r)]\\!]_{\mu}=[\\![r]\\!]_{[\\![q:=|0\rangle]\\!]_{\mu}}$.

  2. (ii)

$[\\![h(P)]\\!]_{\mu}\Rightarrow[\\![P]\\!]_{[\\![q:=|0\rangle]\\!]_{\mu}}$.

  * Proof:

We prove the two statements by structural induction.

    1. (i)

There are three cases for the structure of $r$.

       * (a)

$r\equiv{\mathbb{E}}[e]$. We note that
$[\\![e]\\!]_{\sigma}=[\\![e]\\!]_{\sigma[n/x]}$ for any number $n$ and fresh
variable $x$ in the sense that $x$ does not appear in $e$. Then we reason as
follows.

$\begin{array}[]{rcl}[\\![h(r)]\\!]_{\mu}&=&[\\![{\mathbb{E}}_{x\sim
M}[e]]\\!]_{\mu}\qquad\mbox{where }M=\langle\\{M_{0},M_{1}\\},Id\rangle\mbox{
with }M_{0}=|0\rangle\langle 0|,\ M_{1}=|0\rangle\langle 1|,\\\ &&\hfill\
x\mbox{ is fresh}\\\ &=&\sum_{\sigma}(|0\rangle\langle
0|\mu(\sigma)|0\rangle\langle
0|\cdot[\\![e]\\!]_{\sigma[0/x]}+|0\rangle\langle
1|\mu(\sigma)|1\rangle\langle 0|\cdot[\\![e]\\!]_{\sigma[1/x]})\\\
&=&\sum_{\sigma}(|0\rangle\langle 0|\mu(\sigma)|0\rangle\langle
0|\cdot[\\![e]\\!]_{\sigma}+|0\rangle\langle 1|\mu(\sigma)|1\rangle\langle
0|\cdot[\\![e]\\!]_{\sigma})\qquad x\mbox{ is fresh}\\\
&=&\sum_{\sigma}(|0\rangle\langle 0|\mu(\sigma)|0\rangle\langle
0|+|0\rangle\langle 1|\mu(\sigma)|1\rangle\langle
0|)\cdot[\\![e]\\!]_{\sigma}\\\
&=&\sum_{\sigma}[\\![q:=|0\rangle]\\!]_{\mu}(\sigma)\cdot[\\![e]\\!]_{\sigma}\\\
&=&[\\![{\mathbb{E}}[e]]\\!]_{[\\![q:=|0\rangle]\\!]_{\mu}}\\\
&=&[\\![r]\\!]_{[\\![q:=|0\rangle]\\!]_{\mu}}\end{array}$

       * (b)

$r\equiv{\mathbb{E}}_{\bar{x}\sim M[\bar{q}]}[e]$ for some
$M=\langle\\{M_{i}\\}_{i},{l}\rangle$. Then

$\begin{array}[]{rcl}[\\![h(r)]\\!]_{\mu}&=&[\\![{\mathbb{E}}_{\bar{x}\sim
M^{\prime}[\bar{q}]}[e]]\\!]_{\mu}\quad\mbox{where
}M^{\prime}=\langle\\{M_{i0},M_{i1}\\}_{i},{l}^{\prime}\rangle\\\ &&\hskip
71.13188pt\mbox{ with }M_{i0}=M_{i}|0\rangle\langle 0|,\
M_{i1}=M_{i}|0\rangle\langle 1|,{l}^{\prime}(i0)={l}^{\prime}(i1)=l(i)\\\
&=&\sum_{\sigma}\sum_{i}(M_{i}|0\rangle\langle 0|\mu(\sigma)|0\rangle\langle
0|M^{\dagger}_{i}+M_{i}|0\rangle\langle 1|\mu(\sigma)|1\rangle\langle
0|M^{\dagger}_{i})\cdot[\\![e]\\!]_{\sigma[l(i)/\bar{x}]}\\\
&=&\sum_{\sigma}\sum_{i}(M_{i}(|0\rangle\langle 0|\mu(\sigma)|0\rangle\langle
0|+|0\rangle\langle 1|\mu(\sigma)|1\rangle\langle
0|)M^{\dagger}_{i}\cdot[\\![e]\\!]_{\sigma[l(i)/\bar{x}]}\\\
&=&\sum_{\sigma}\sum_{i}M_{i}[\\![q:=|0\rangle]\\!]_{\mu}(\sigma)M^{\dagger}_{i}\cdot[\\![e]\\!]_{\sigma[l(i)/\bar{x}]}\\\
&=&[\\![{\mathbb{E}}_{\bar{x}\sim
M[\bar{q}]}[e]]\\!]_{[\\![q:=|0\rangle]\\!]_{\mu}}\\\
&=&[\\![r]\\!]_{[\\![q:=|0\rangle]\\!]_{\mu}}\end{array}$

       * (c)

$r\equiv o(r_{1},...,r_{k})$. The case can be proved by induction.

$\begin{array}[]{rcl}[\\![h(r)]\\!]_{\mu}&=&[\\![o(h(r_{1}),...,h(r_{k})]\\!]_{\mu}\\\
&=&o([\\![h(r_{1})]\\!]_{\mu},...,[\\![h(r_{k})]\\!]_{\mu})\\\
&=&o([\\![r_{1}]\\!]_{[\\![q:=|0\rangle]\\!]_{\mu}},...,[\\![r_{k}]\\!]_{[\\![q:=|0\rangle]\\!]_{\mu}})\\\
&=&[\\![o(r_{1},...,r_{k})]\\!]_{[\\![q:=|0\rangle]\\!]_{\mu}}\\\
&=&[\\![r]\\!]_{[\\![q:=|0\rangle]\\!]_{\mu}}\end{array}$

    2. (ii)

There are three cases for the structure of $P$.

       * (a)

$P\equiv r_{1}\rhd\\!\\!\\!\lhd r_{2}$. In this case, we need to use statement
(iii).

$\begin{array}[]{rcl}[\\![h(P)]\\!]_{\mu}&=&[\\![h(r_{1})\rhd\\!\\!\\!\lhd
h(r_{2})]\\!]_{\mu}\\\
&=&[\\![h(r_{1})]\\!]_{\mu}\rhd\\!\\!\\!\lhd[\\![h(r_{2})]\\!]_{\mu}\\\
&=&[\\![r_{1}]\\!]_{[\\![q:=|0\rangle]\\!]_{\mu}}\rhd\\!\\!\\!\lhd[\\![r_{2}]\\!]_{[\\![q:=|0\rangle]\\!]_{\mu}})\\\
&=&[\\![r_{1}\rhd\\!\\!\\!\lhd r_{2}]\\!]_{[\\![q:=|0\rangle]\\!]_{\mu}}\\\
&=&[\\![r]\\!]_{[\\![q:=|0\rangle]\\!]_{\mu}}\end{array}$

       * (b)

$P\equiv P_{1}\oplus P_{2}$. This case is proved by induction.

$\begin{array}[]{rcl}[\\![h(P)]\\!]_{\mu}&=&[\\![h(P_{1})\oplus
h(P_{2})]\\!]_{\mu}\\\ &=&\exists\mu_{1},\mu_{2}.\
\mu=\mu_{1}+\mu_{2}\wedge[\\![h(P_{1})]\\!]_{\mu_{1}}\wedge[\\![h(P_{2})]\\!]_{\mu_{2}}\\\
&\Rightarrow&\exists\mu_{1},\mu_{2}.\
[\\![q:=|0\rangle]\\!]_{\mu}=[\\![q:=|0\rangle]\\!]_{\mu_{1}}+[\\![q:=|0\rangle]\\!]_{\mu_{2}}\\\
&&\wedge[\\![P_{1}]\\!]_{[\\![q:=|0\rangle]\\!]_{\mu_{1}}}\wedge[\\![P_{2}]\\!]_{[\\![q:=|0\rangle]\\!]_{\mu_{2}}}\qquad\mbox{by
Lemma~{}\ref{lem:split}}\\\ &=&[\\![P_{1}\oplus
P_{2}]\\!]_{[\\![q:=|0\rangle]\\!]_{\mu}}\\\
&=&[\\![r]\\!]_{[\\![q:=|0\rangle]\\!]_{\mu}}\end{array}$

       * (c)

$P\equiv FO(P_{1},...,P_{k})$. Again, this case is proved by induction.

$\begin{array}[]{rcl}[\\![h(P)]\\!]_{\mu}&=&[\\![FO(h(P_{1}),...,h(P_{k})]\\!]_{\mu}\\\
&=&FO([\\![h(P_{1})]\\!]_{\mu},...,[\\![h(P_{k})]\\!]_{\mu})\\\
&=&FO([\\![P_{1}]\\!]_{[\\![q:=|0\rangle]\\!]_{\mu}},...,[\\![P_{k}]\\!]_{[\\![q:=|0\rangle]\\!]_{\mu}})\\\
&=&[\\![FO(P_{1},...,P_{k})]\\!]_{[\\![q:=|0\rangle]\\!]_{\mu}}\\\
&=&[\\![P]\\!]_{[\\![q:=|0\rangle]\\!]_{\mu}}\end{array}$

$\Box$

###### Lemma 5.4

The following two clauses hold.

  1. (i)

$[\\![g^{U}(r)]\\!]_{\mu}=[\\![r]\\!]_{[\\![U[\bar{q}]]\\!]_{\mu}}$.

  2. (ii)

$[\\![g^{U}(P)]\\!]_{\mu}\Rightarrow[\\![P]\\!]_{[\\![U[\bar{q}]]\\!]_{\mu}}$.

  * Proof:

The proof is similar to that of Lemma 5.3 except for the treatment of two
cases for statement (i).

    * 1.

$r\equiv{\mathbb{E}}[e]$. We infer that

$\begin{array}[]{rcl}[\\![g^{U}(r)]\\!]_{\mu}&=&[\\![{\mathbb{E}}_{x\sim
M[\bar{q}]}[e]]\\!]_{\mu}\qquad\mbox{where
}M=\langle\\{M_{0}\\},Id\rangle\mbox{ with }M_{0}=U\mbox{ and $x$ is fresh}\\\
&=&\sum_{\sigma}U\mu(\sigma)U^{\dagger}\cdot[\\![e]\\!]_{\sigma[0/x]}\\\
&=&\sum_{\sigma}U\mu(\sigma)U^{\dagger}\cdot[\\![e]\\!]_{\sigma}\\\
&=&\sum_{\sigma}[\\![U[\bar{q}]]\\!]_{\mu}(\sigma)\cdot[\\![e]\\!]_{\sigma}\\\
&=&[\\![{\mathbb{E}}[e]]\\!]_{[\\![U[\bar{q}]]\\!]_{\mu}}\\\
&=&[\\![r]\\!]_{[\\![U[\bar{q}]]\\!]_{\mu}}\end{array}$

    * 2.

$r\equiv{\mathbb{E}}_{\bar{x}\sim M[\bar{q}]}[e]$. Suppose
$M=\langle\\{M_{i}\\}_{i\in I},{l}\rangle$. We reason as follows.

$\begin{array}[]{rcl}[\\![g^{U}(r)]\\!]_{\mu}&=&[\\![{\mathbb{E}}_{\bar{x}\sim
M^{\prime}[\bar{q}]}[e]]\\!]_{\mu}\quad\mbox{where
}M^{\prime}=\langle\\{M_{i}U\\}_{i\in I},{l}\rangle\\\
&=&\sum_{\sigma}\sum_{i}M_{i}U\mu(\sigma)U^{\dagger}M^{\dagger}_{i}\cdot[\\![e]\\!]_{\sigma[l(i)/\bar{x}]}\\\
&=&\sum_{\sigma}\sum_{i}M_{i}[\\![U[\bar{q}]]\\!]_{\mu}(\sigma)M^{\dagger}_{i}\cdot[\\![e]\\!]_{\sigma[l(i)/\bar{x}]}\\\
&=&[\\![{\mathbb{E}}_{\bar{x}\sim
M[\bar{q}]}[e]]\\!]_{[\\![U[\bar{q}]]\\!]_{\mu}}\\\
&=&[\\![r]\\!]_{[\\![U[\bar{q}]]\\!]_{\mu}}\end{array}$

$\Box$

###### Lemma 5.5

Let $a$ be an arithmetic expression, $\sigma$ be any state and
$\sigma^{\prime}:=\sigma[[\\![a]\\!]_{\sigma}/x]$. The following four clauses
hold, where $x$ is not a bound variable in $e$, $\psi$, $r$ and $P$.

  1. (i)

$[\\![e[a/x]]\\!]_{\sigma}=[\\![e]\\!]_{\sigma^{\prime}}$

  2. (ii)

$[\\![\psi[a/x]]\\!]_{\sigma}=[\\![\psi]\\!]_{\sigma^{\prime}}$

  3. (iii)

$[\\![r[a/x]]\\!]_{\mu}=[\\![r]\\!]_{[\\![x:=a]\\!]_{\mu}}$.

  4. (iv)

$[\\![P[a/x]]\\!]_{\mu}\Rightarrow[\\![P]\\!]_{[\\![x:=a]\\!]_{\mu}}$.

  * Proof:

The proof is similar to that of Lemma 5.3. As an example, we only consider one
case for statement (iii).

Suppose $r\equiv{\mathbb{E}}_{\bar{y}\sim M[\bar{q}]}[e]$ with
$M=\langle\\{M_{i}\\}_{i},l\rangle$. There are two possibilities.

    * 1.

$x\in\bar{y}$. In this case, $x$ is a bound variable in $r$, which contradicts
our assumption.

    * 2.

$x\not\in\bar{y}$. Notice that

$[\\![x:=a]\\!]_{\mu}(\sigma^{\prime})\ =\
\sum_{\sigma}\\{\mu(\sigma)\mid\sigma[[\\![a]\\!]_{\sigma}/x]=\sigma^{\prime}\\}$
(14)

holds for any $\mu$ and $\sigma^{\prime}$. We reason as follows.

$\begin{array}[]{rcl}[\\![r[a/x]]\\!]_{\mu}&=&[\\![{\mathbb{E}}_{\bar{y}\sim
M[\bar{q}]}[e[a/x]]]\\!]_{\mu}\\\
&=&\sum_{\sigma}\sum_{i}M_{i}\mu(\sigma)M^{\dagger}_{i}[\\![e[a/x]]\\!]_{\sigma[l(i)/\bar{y}]}\\\
&=&\sum_{\sigma}\sum_{i}M_{i}\mu(\sigma)M^{\dagger}_{i}[\\![e]\\!]_{\sigma[l(i)/\bar{y}][[\\![a]\\!]_{\sigma[l(i)/\bar{y}]}/x]}\qquad\mbox{by
statement (i)}\\\
&=&\sum_{i}M_{i}\sum_{\sigma}\mu(\sigma)M^{\dagger}_{i}[\\![e]\\!]_{\sigma[[\\![a]\\!]_{\sigma}/x][l(i)/\bar{y}]}\\\
&=&\sum_{i}M_{i}\sum_{\sigma^{\prime}}\sum_{\sigma}\\{\mu(\sigma)\mid\sigma[[\\![a]\\!]_{\sigma}/x]=\sigma^{\prime}\\}M^{\dagger}_{i}[\\![e]\\!]_{\sigma^{\prime}[l(i)/\bar{y}]}\\\
&=&\sum_{i}M_{i}\sum_{\sigma^{\prime}}[\\![x:=a]\\!]_{\mu}(\sigma^{\prime})M^{\dagger}_{i}[\\![e]\\!]_{\sigma^{\prime}[l(i)/\bar{y}]}\qquad\mbox{by
}(\ref{eq:a})\\\
&=&\sum_{\sigma^{\prime}}\sum_{i}M_{i}[\\![x:=a]\\!]_{\mu}(\sigma^{\prime})M^{\dagger}_{i}[\\![e]\\!]_{\sigma^{\prime}[l(i)/\bar{y}]}\\\
&=&[\\![{\mathbb{E}}_{\bar{y}\sim
M[\bar{q}]}[e]]\\!]_{[\\![x:=a]\\!]_{\mu}}\\\
&=&[\\![r]\\!]_{[\\![x:=a]\\!]_{\mu}}\end{array}$

$\Box$

###### Lemma 5.6

  1. (i)

$[\\![f_{x,\bar{q}}^{M}(r)]\\!]_{\mu}=[\\![r]\\!]_{[\\![x:=M[\bar{q}]]\\!]_{\mu}}$.

  2. (ii)

$[\\![f_{x,\bar{q}}^{M}(P)]\\!]_{\mu}\Rightarrow[\\![P]\\!]_{[\\![x:=M[\bar{q}]]\\!]_{\mu}}$.

  * Proof:

We consider two cases for statement (i); the other cases are easier. Assume
that $M=\langle\\{M_{i}\\}_{i},k\rangle$.

    * 1.

$r\equiv{\mathbb{E}}[e]$. We reason as follows.

$\begin{array}[]{rcl}[\\![f_{x,\bar{q}}^{M}(r)]\\!]_{\mu}&=&[\\![{\mathbb{E}}_{x\sim
M[\bar{q}]}[e]]\\!]_{\mu}\\\
&=&\sum_{\sigma}\sum_{i}M_{i}\mu(\sigma)M_{i}^{\dagger}\cdot[\\![e]\\!]_{\sigma[l(i)/x]}\\\
&=&\sum_{\sigma^{\prime}}\sum_{\sigma}\sum_{i}\\{M_{i}\mu(\sigma)M_{i}^{\dagger}\mid\sigma[l(i)/x]=\sigma^{\prime}\\}\cdot[\\![e]\\!]_{\sigma^{\prime}}\\\
&=&\sum_{\sigma^{\prime}}\sum_{\sigma}\mu_{\sigma}(\sigma^{\prime})\cdot[\\![e]\\!]_{\sigma^{\prime}}\qquad\mbox{where
}\mu_{\sigma}(\sigma^{\prime})=\sum_{i}\\{M_{i}\mu(\sigma)M_{i}^{\dagger}\mid\sigma[l(i)/x]=\sigma^{\prime}\\}\\\
&=&[\\![{\mathbb{E}}[e]]\\!]_{\sum_{\sigma}\mu_{\sigma}}\\\
&=&[\\![{\mathbb{E}}[e]]\\!]_{[\\![x:=M[\bar{q}]]\\!]_{\mu}}\\\
&=&[\\![r]\\!]_{[\\![x:=M[\bar{q}]]\\!]_{\mu}}\end{array}$

The second last equality holds because
$[\\![x:=M[\bar{q}]]\\!]_{(\sigma,\mu(\sigma))}=\mu_{\sigma}$.

    * 2.

$r\equiv{\mathbb{E}}_{\bar{y}\sim N[\bar{q^{\prime}}]}[e]$. There are two
possibilities. Let us first assume that $x\not\in\bar{y}$ and
$N=\langle\\{N_{j}\\}_{j},l\rangle$.

$\begin{array}[]{rcl}[\\![f_{x,\bar{q}}^{M}(r)]\\!]_{\mu}&=&[\\![{\mathbb{E}}_{x\bar{y}\sim
M^{\prime}[\bar{q}\cup\bar{q^{\prime}}]}[e]]\\!]_{\mu}\mbox{ with
}M^{\prime}=\langle\\{N_{j}M_{i}\\}_{ij},k^{\prime}\rangle\mbox{ and
}k^{\prime}(ij)=(k(i),l(j))\\\
&=&\sum_{\sigma}\sum_{ij}N_{j}M_{i}\mu(\sigma)M_{i}^{\dagger}N_{j}^{\dagger}\cdot[\\![e]\\!]_{\sigma[k(i),l(j)/x\bar{y}]}\\\
&=&\sum_{\sigma}\sum_{j}N_{j}(\sum_{i}M_{i}\mu(\sigma)M_{i}^{\dagger})N_{j}^{\dagger}\cdot[\\![e]\\!]_{\sigma[k(i)/x][l(j)/\bar{y}]}\\\
&=&\sum_{\sigma^{\prime}}\sum_{\sigma}\sum_{j}N_{j}(\sum_{i}\\{M_{i}\mu(\sigma)M_{i}^{\dagger}\mid\sigma[k(i)/x]=\sigma^{\prime}\\})N_{j}^{\dagger}\cdot[\\![e]\\!]_{\sigma^{\prime}[l(j)/\bar{y}]}\\\
&=&\sum_{\sigma^{\prime}}\sum_{\sigma}\sum_{j}N_{j}\mu_{\sigma}(\sigma^{\prime})N_{j}^{\dagger}\cdot[\\![e]\\!]_{\sigma^{\prime}[l(j)/\bar{y}]}\\\
&&\qquad\mbox{where
}\mu_{\sigma}(\sigma^{\prime})=\sum_{i}\\{M_{i}\mu(\sigma)M_{i}^{\dagger}\mid\sigma[k(i)/x]=\sigma^{\prime}\\}\\\
&=&\sum_{\sigma^{\prime}}\sum_{j}N_{j}\sum_{\sigma}\mu_{\sigma}(\sigma^{\prime})N_{j}^{\dagger}\cdot[\\![e]\\!]_{\sigma^{\prime}[l(j)/\bar{y}]}\\\
&=&[\\![{\mathbb{E}}_{\bar{y}\sim
N[\bar{q^{\prime}}]}[e]]\\!]_{\sum_{\sigma}\mu_{\sigma}}\\\
&=&[\\![{\mathbb{E}}_{\bar{y}\sim
N[\bar{q^{\prime}}]}[e]]\\!]_{[\\![x:=M[\bar{q}]]\\!]_{\mu}}\\\
&=&[\\![r]\\!]_{[\\![x:=M[\bar{q}]]\\!]_{\mu}}\end{array}$

If $x\in\bar{y}$, the proof is similar by noting that
$\sigma[k(i)/x][l(j)/\bar{y}]=\sigma[l(j)/\bar{y}]$.

$\Box$

The next theorem states that the concrete proof system is sound.

###### Theorem 5.7

Every judgement provable in $\mathcal{S}_{c}$ is valid.

  * Proof:

We only need to prove that the four new rules [Assgn’], [QInit’], [QUnit’] and
[QMeas’] are sound, which follows from Lemmas 5.3 \- 5.6; the soundness of all
other rules are already shown in Theorem 4.7. $\Box$

We can define a precondition calculus to help with syntactic reasoning. Given
an assertion $P$ as a postcondition and a loop-free command $c$, we construct
an assertion as a precondition for $c$, written as $pc(c,P)$. The computation
rules for preconditions are given in Figure 8.

$\begin{array}[]{rcl}pc({\textbf{skip}},P)&:=&P\\\ pc(x:=a,P)&:=&P[a/x]\\\
pc(c_{0};c_{1},P)&:=&pc(c_{0},pc(c_{1},P))\\\
pc(\textbf{if}~{}b~{}\textbf{then}~{}c_{0}~{}\textbf{else}~{}c_{1},P)&:=&(pc(c_{0},P)\wedge\Box
b)\oplus(pc(c_{1},P)\wedge\Box\neg b)\\\
pc(\textbf{abort},P)&:=&\left\\{\begin{array}[]{ll}\top&\mbox{if
}P=\Box{\textbf{false}}\\\
\mbox{undefined}&\mbox{otherwise}\end{array}\right.\\\
pc(q:=|0\rangle,P)&:=&h(P)\\\ pc(U[\bar{q}],P)&:=&g^{U}(P)\\\
pc(x:=M[\bar{q}],P)&:=&f_{x,\bar{q}}^{M}(P)\par\end{array}$ Figure 8:
Precondition calculus

###### Theorem 5.8

Let $c$ be a non-looping command. The following rule is derivable.

$\prooftree\justifies\\{pc(c,P)\\}\;c\;\\{P\\}\using[\sf PC]\endprooftree$

  * Proof:

We proceed by induction on the structure of $c$.

    * 1.

$c\equiv{\textbf{skip}}$. Then $pc(c,P)=P$ and we have
$\vdash\\{P\\}\;c\;\\{P\\}$ by rule [Skip].

    * 2.

$c\equiv\textbf{abort}$. Then $pc(c,P)$ is only defined for
$P=\Box{\textbf{false}}$. In this case, we can infer that
$\vdash\\{\top\\}\;\textbf{abort}\;\\{\Box{\textbf{false}}\\}$ by rule
[Abort].

    * 3.

$c\equiv x:=a$. Then $pc(c,P)=P[a/x]$ and we have
$\vdash\\{P[a/x]\\}\;c\;\\{P\\}$ by rule [Assgn’].

    * 4.

$c\equiv c_{0};c_{1}$. Then $pc(c,P)=pc(c_{0},pc(c_{1},P))$. By induction, we
have $\vdash\\{pc(c_{1},P)\\}\;c_{1}\;\\{P\\}$ and
$\vdash\\{pc(c_{0},pc(c_{1},P))\\}\;c_{0}\;\\{pc(c_{1},P)\\}$. By using rule
[Seq], we obtain $\vdash\\{pc(c_{0},pc(c_{1},P))\\}\;c\;\\{P\\}$.

    * 5.

$c\equiv\textbf{if}~{}b~{}\textbf{then}~{}c_{0}~{}\textbf{else}~{}c_{1}$. Then
$pc(c,P)=(pc(c_{0},P)\wedge\Box b)\oplus(pc(c_{1},P)\wedge\Box\neg b)$. By
induction, we have that $\vdash\\{pc(c_{0},P)\\}\;c_{0}\;\\{P\\}$ and
$\vdash\\{pc(c_{1},P)\\}\;c_{1}\;\\{P\\}$. It is obvious that
$pc(c_{0},P)\wedge\Box b\Rightarrow pc(c_{0},P)$. We can use rule [Conseq] to
infer that $\vdash\\{pc(c_{0},P)\wedge\Box b\\}\;c_{0}\;\\{P\\}$. Similarly,
we have $\vdash\\{pc(c_{1},P)\wedge\Box\neg b\\}\;c_{1}\;\\{P\\}$. By applying
rule [Cond], we have that $\vdash\\{pc(c,P\oplus P)\\}\;c\;\\{P\oplus P\\}$.
Since $P\oplus P\Leftrightarrow P$, we use rule [Conseq] again to infer the
required result that $\vdash\\{pc(c,P)\\}\;c\;\\{P\\}$.

    * 6.

$c\equiv q:=|0\rangle$. A direct consequence of rule [QInit’].

    * 7.

$c\equiv U[\bar{q}]$. By using rule [QUnit’].

    * 8.

$c\equiv M[\bar{q}]$. By using rule [QMeas’].

$\Box$

##  6 Example: superdense coding

In this section, we illustrate the use of the proof system $\mathcal{S}_{c}$
via the example of superdense coding.

Superdense coding was proposed by Bennett and Wiesner in 1992 [4]. It is a
quantum communication protocol allowing two classical bits to be encoded in
one qubit during a transmission, so it needs only one quantum channel. Such
advantage is based on the use of a maximally entangled state, EPR state. An
EPR state can be transformed into all the four kinds of EPR states through
1-qubit operations, and these EPR states are mutually orthogonal.

#### Protocol.

We suppose the sender and the receiver of the communication are Alice and Bob,
then the protocol goes as follows:

  1. 1.

Alice and Bob prepare an EPR state $\frac{|00\rangle+|11\rangle}{\sqrt{2}}$
together. Then they share the qubits, Alice holding $q_{0}$ and Bob holding
$q_{1}$.

  2. 2.

Depending on the message Alice wants to send, she applies a gate to her qubit.
If Alice wants to send $00$, she does nothing. If Alice wants to send $01$,
she applies the X gate. To send $10$, she applies the Z gate. To send $11$,
she applies both $X$ and $Z$.

  3. 3.

Then Alice sends the qubit $q_{0}$ to Bob.

  4. 4.

Bob applies a CNOT operation on $q_{0},q_{1}$ and a Hadamard operation on
$q_{0}$ to remove the entanglement.

  5. 5.

Bob measures $q_{0}$ and $q_{1}$ to get the message.

After the execution of the protocol above, Bob gets the value that Alice wants
to send. The protocol exactly transmits two classical bits of information by
sending one qubit from Alice to Bob. A quantum circuit implementing the
protocol is illustrated in Figure 9.

$\Qcircuit@C=1.2em@R=2em{\lstick{x_{0}}&\cw\cw\cw\cw\cw\cw\cw\cctrl{2}\\\
\lstick{x_{1}}\cw\cw\cw\cw\cw\cctrl{1}\\\
\lstick{q_{0}}\qw\gate{H}\qw\ctrl{1}\qw\gate{X}\qw\gate{Z}\qw\ctrl{1}\qw\gate{H}\qw\meter\cw\cw
y_{0}\\\ \lstick{q_{1}}\qw\qw\qw\targ\qw\qw\qw\qw\qw\targ\qw\qw\qw\meter\cw\cw
y_{1}\\\ }$ Figure 9: Superdense coding

The protocol can also be described by the quantum program $SC$ given in Figure
10, where for any pure state $|\varphi\rangle$, we write $[|\varphi\rangle]$
for its density operator $|\varphi\rangle\langle\varphi|$.

$\begin{array}[]{cl}SC\equiv&\\\ 1:&q_{0}:=|0\rangle;\\\
2:&q_{1}:=|0\rangle;\\\ 3:&H[q_{0}];\\\ 4:&CNOT[q_{0}q_{1}];\\\
5:&\textbf{if}~{}x_{1}=1~{}\textbf{then}~{}X[q_{0}];\\\
6:&\textbf{if}~{}x_{0}=1~{}\textbf{then}~{}Z[q_{0}];\\\
7:&CNOT[q_{0}q_{1}];\\\ 8:&H[q_{0}];\\\ 9:&y_{0}:=M[q_{0}];\\\
10:&y_{1}:=M[q_{1}]\\\ &\quad\mbox{where
}M=\langle\\{M_{0},M_{1}\\},Id\rangle,M_{0}=[|0\rangle],M_{1}=[|1\rangle]\end{array}$
Figure 10: The quantum program of implementing superdense coding

According to the operational rules in Figure 2, we can derive the following
sequence of transitions, where the initial values of the four classical
variables in the first configuration can be arbitrary and we use $*$ to stand
for unimportant commands or the values of variables.

$\begin{array}[]{ll}&(SC,x_{0}x_{1}y_{0}y_{1},[|00\rangle])\vspace{2mm}\\\
\rightarrow&(*,*,[\frac{|0\rangle+|1\rangle}{\sqrt{2}}|0\rangle])\vspace{2mm}\\\
\rightarrow&(*,*,[\frac{|00\rangle+|11\rangle}{\sqrt{2}}])\vspace{2mm}\\\
\rightarrow&(*,*,[X_{0}^{x_{1}}\frac{|00\rangle+|11\rangle}{\sqrt{2}}])\vspace{2mm}\\\
\rightarrow&(*,*,[Z_{0}^{x_{0}}X_{0}^{x_{1}}\frac{|00\rangle+|11\rangle}{\sqrt{2}}])\vspace{2mm}\\\
\equiv&\left\\{\begin{array}[]{ll}(*,00y_{0}y_{1},[\frac{|00\rangle+|11\rangle}{\sqrt{2}}])&\mbox{
if }x_{0}=x_{1}=0\\\
(*,01y_{0}y_{1},[\frac{|10\rangle+|01\rangle}{\sqrt{2}}])&\mbox{ if
}x_{0}=0,x_{1}=1\\\
(*,10y_{0}y_{1},[\frac{|00\rangle-|11\rangle}{\sqrt{2}}])&\mbox{ if
}x_{0}=1,x_{1}=0\\\
(*,11y_{0}y_{1},[\frac{|10\rangle-|01\rangle}{\sqrt{2}}])&\mbox{ if
}x_{0}=x_{1}=1\end{array}\right.\vspace{2mm}\\\
\rightarrow&\left\\{\begin{array}[]{l}(*,00y_{0}y_{1},[\frac{|00\rangle+|10\rangle}{\sqrt{2}}])\\\
(*,01y_{0}y_{1},[\frac{|11\rangle+|01\rangle}{\sqrt{2}}])\\\
(*,10y_{0}y_{1},[\frac{|00\rangle-|10\rangle}{\sqrt{2}}])\\\
(*,11y_{0}y_{1},[\frac{|11\rangle-|01\rangle}{\sqrt{2}}])\end{array}\right.\vspace{2mm}\\\
\rightarrow&\left\\{\begin{array}[]{l}(*,00y_{0}y_{1},[|00\rangle])\\\
(*,01y_{0}y_{1},[|01\rangle])\\\ (*,10y_{0}y_{1},[|10\rangle])\\\
(*,11y_{0}y_{1},[|11\rangle])\end{array}\right.\vspace{2mm}\\\
\rightarrow&\left\\{\begin{array}[]{l}(*,000y_{1},[|00\rangle])\\\
(*,010y_{1},[|01\rangle])\\\ (*,101y_{1},[|10\rangle])\\\
(*,111y_{1},[|11\rangle])\end{array}\right.\vspace{2mm}\\\
\rightarrow&\left\\{\begin{array}[]{l}(\textbf{nil},0000,[|00\rangle])\\\
(\textbf{nil},0101,[|01\rangle])\\\ (\textbf{nil},1010,[|10\rangle])\\\
(\textbf{nil},1111,[|11\rangle])\end{array}\right.\\\ \end{array}$

We observe that in each case of the four last configurations, we always have
the value of $x_{0}x_{1}$ coincide with $y_{0}y_{1}$ as expected. Indeed, we
would like to show that the judgement

$\\{{\textbf{true}}\\}\;SC\;\\{\Box(x_{0}=y_{0}\wedge x_{1}=y_{1})\\}$ (15)

is provable in our concrete proof system. This can be accomplished by a
sequence of derivations; for every line of command in Figure 10 we need to
prove a Hoare triple. We start from line 10 and proceed backwards. The first
six steps can be derived by using the rules [QMeas’], [QUnit’], [Cond] and
[Split], as shown in Figure 11. Continue the reasoning until line 1, we obtain
the following precondition for SC.

$\begin{array}[]{l}\\{({\mathbb{E}}_{y_{0}y_{1}\sim M_{10}[q_{0}q_{1}]}[{\bf
1}_{\psi\wedge x_{0}=1\wedge x_{1}=1}]={\mathbb{E}}_{y_{0}y_{1}\sim
M_{10}[q_{0}q_{1}]}[{\bf 1}_{{\textbf{true}}}])\\\
\oplus({\mathbb{E}}_{y_{0}y_{1}\sim M_{9}[q_{0}q_{1}]}[{\bf 1}_{\psi\wedge
x_{0}=1\wedge x_{1}=0}]={\mathbb{E}}_{y_{0}y_{1}\sim M_{9}[q_{0}q_{1}]}[{\bf
1}_{{\textbf{true}}}])\qquad\qquad({\dagger})\\\
\oplus({\mathbb{E}}_{y_{0}y_{1}\sim M_{8}[q_{0}q_{1}]}[{\bf 1}_{\psi\wedge
x_{0}=0\wedge x_{1}=1}]={\mathbb{E}}_{y_{0}y_{1}\sim M_{8}[q_{0}q_{1}]}[{\bf
1}_{{\textbf{true}}}])\\\ \oplus({\mathbb{E}}_{y_{0}y_{1}\sim
M_{7}[q_{0}q_{1}]}[{\bf 1}_{\psi\wedge x_{0}=0\wedge
x_{1}=0}]={\mathbb{E}}_{y_{0}y_{1}\sim M_{7}[q_{0}q_{1}]}[{\bf
1}_{{\textbf{true}}}])\\},\\\ \mbox{where
}M_{10}\equiv\langle\\{E_{0000},E_{0001},...,E_{1111}\\},f\rangle\mbox{
with}\\\ \hskip 65.44142ptE_{0000}\equiv
E_{00}H_{q_{0}}CNOT_{q_{0}q_{1}}Z_{q_{0}}X_{q_{0}}CNOT_{q_{0}q_{1}}H_{q_{0}}|0\rangle_{q_{1}}\langle
0|\cdot|0\rangle_{q_{0}}\langle 0|,\\\ \hskip 65.44142ptE_{0001}\equiv
E_{00}H_{q_{0}}CNOT_{q_{0}q_{1}}Z_{q_{0}}X_{q_{0}}CNOT_{q_{0}q_{1}}H_{q_{0}}|0\rangle_{q_{1}}\langle
0|\cdot|0\rangle_{q_{0}}\langle 1|,\\\ \hskip 65.44142ptE_{0010}\equiv
E_{00}H_{q_{0}}CNOT_{q_{0}q_{1}}Z_{q_{0}}X_{q_{0}}CNOT_{q_{0}q_{1}}H_{q_{0}}|0\rangle_{q_{1}}\langle
1|\cdot|0\rangle_{q_{0}}\langle 0|,\\\ \hskip 65.44142ptE_{0011}\equiv
E_{00}H_{q_{0}}CNOT_{q_{0}q_{1}}Z_{q_{0}}X_{q_{0}}CNOT_{q_{0}q_{1}}H_{q_{0}}|0\rangle_{q_{1}}\langle
1|\cdot|0\rangle_{q_{0}}\langle 1|,\\\ \hskip 65.44142ptE_{0100}\equiv
E_{01}H_{q_{0}}CNOT_{q_{0}q_{1}}Z_{q_{0}}X_{q_{0}}CNOT_{q_{0}q_{1}}H_{q_{0}}|0\rangle_{q_{1}}\langle
0|\cdot|0\rangle_{q_{0}}\langle 0|,\\\ \hskip 93.89418pt\vdots\\\ \hskip
65.44142ptE_{1111}\equiv
E_{11}H_{q_{0}}CNOT_{q_{0}q_{1}}Z_{q_{0}}X_{q_{0}}CNOT_{q_{0}q_{1}}H_{q_{0}}|0\rangle_{q_{1}}\langle
1|\cdot|0\rangle_{q_{0}}\langle 1|,\\\ \hskip 65.44142ptf(00**)=00,\
f(01**)=01,\ f(10**)=10,\ f(11**)=11\\\
M_{9}\equiv\langle\\{E^{\prime}_{0000},E^{\prime}_{0001},...,E^{\prime}_{1111}\\},f\rangle\mbox{
with}\\\ \hskip 36.98866ptE^{\prime}_{0000}\equiv
E_{00}H_{q_{0}}CNOT_{q_{0}q_{1}}Z_{q_{0}}CNOT_{q_{0}q_{1}}H_{q_{0}}|0\rangle_{q_{1}}\langle
0|\cdot|0\rangle_{q_{0}}\langle 0|,\\\ \hskip 65.44142pt\vdots\\\ \hskip
36.98866ptE^{\prime}_{1111}\equiv
E_{11}H_{q_{0}}CNOT_{q_{0}q_{1}}Z_{q_{0}}CNOT_{q_{0}q_{1}}H_{q_{0}}|0\rangle_{q_{1}}\langle
1|\cdot|0\rangle_{q_{0}}\langle 1|\\\
M_{8}\equiv\langle\\{E^{\prime\prime}_{0000},E^{\prime\prime}_{0001},...,E^{\prime\prime}_{1111}\\},f\rangle\mbox{
with}\\\ \hskip 36.98866ptE^{\prime\prime}_{0000}\equiv
E_{00}H_{q_{0}}CNOT_{q_{0}q_{1}}X_{q_{0}}CNOT_{q_{0}q_{1}}H_{q_{0}}|0\rangle_{q_{1}}\langle
0|\cdot|0\rangle_{q_{0}}\langle 0|,\\\ \hskip 65.44142pt\vdots\\\ \hskip
36.98866ptE^{\prime\prime}_{1111}\equiv
E_{11}H_{q_{0}}CNOT_{q_{0}q_{1}}X_{q_{0}}CNOT_{q_{0}q_{1}}H_{q_{0}}|0\rangle_{q_{1}}\langle
1|\cdot|0\rangle_{q_{0}}\langle 1|\\\
M_{7}\equiv\langle\\{E^{\prime\prime\prime}_{0000},E^{\prime\prime\prime}_{0001},...,E^{\prime\prime\prime}_{1111}\\},f\rangle\mbox{
with}\\\ \hskip 36.98866ptE^{\prime\prime\prime}_{0000}\equiv
E_{00}H_{q_{0}}CNOT_{q_{0}q_{1}}CNOT_{q_{0}q_{1}}H_{q_{0}}|0\rangle_{q_{1}}\langle
0|\cdot|0\rangle_{q_{0}}\langle 0|,\\\ \hskip 65.44142pt\vdots\\\ \hskip
36.98866ptE^{\prime\prime\prime}_{1111}\equiv
E_{11}H_{q_{0}}CNOT_{q_{0}q_{1}}CNOT_{q_{0}q_{1}}H_{q_{0}}|0\rangle_{q_{1}}\langle
1|\cdot|0\rangle_{q_{0}}\langle 1|\\\ \end{array}$

The measurement operators in $M_{10}$ look complicated. However, a simple
calculation shows that among the 16 operators only four of them are non-zero.
Indeed, the simplified form of $M_{10}$ is

$M_{10}=\langle\\{E_{1100},E_{1101},E_{1110},E_{1111}\\},f\rangle$

where

$E_{1100}=\begin{bmatrix}0&0&0&0\\\ 0&0&0&0\\\ 0&0&0&0\\\
1&0&0&0\end{bmatrix}\quad E_{1101}=\begin{bmatrix}0&0&0&0\\\ 0&0&0&0\\\
0&0&0&0\\\ 0&0&1&0\end{bmatrix}\quad E_{1110}=\begin{bmatrix}0&0&0&0\\\
0&0&0&0\\\ 0&0&0&0\\\ 0&1&0&0\end{bmatrix}\quad
E_{1111}=\begin{bmatrix}0&0&0&0\\\ 0&0&0&0\\\ 0&0&0&0\\\ 0&0&0&1\end{bmatrix}$

Similarly, the simplified form of $M_{9}$ is
$M_{9}=\langle\\{E^{\prime}_{1000},E^{\prime}_{1001},E^{\prime}_{1010},E^{\prime}_{1011}\\},f\rangle$,
where

$E^{\prime}_{1000}=\begin{bmatrix}0&0&0&0\\\ 0&0&0&0\\\ 1&0&0&0\\\
0&0&0&0\end{bmatrix}\quad E^{\prime}_{1001}=\begin{bmatrix}0&0&0&0\\\
0&0&0&0\\\ 0&0&1&0\\\ 0&0&0&0\end{bmatrix}\quad
E^{\prime}_{1010}=\begin{bmatrix}0&0&0&0\\\ 0&0&0&0\\\ 0&1&0&0\\\
0&0&0&0\end{bmatrix}\quad E^{\prime}_{1011}=\begin{bmatrix}0&0&0&0\\\
0&0&0&0\\\ 0&0&0&1\\\ 0&0&0&0\end{bmatrix}$

The simplified form of $M_{8}$ is
$M_{8}=\langle\\{E^{\prime\prime}_{0100},E^{\prime\prime}_{0101},E^{\prime\prime}_{0110},E^{\prime\prime}_{0111}\\},f\rangle$,
where

$E^{\prime\prime}_{0100}=\begin{bmatrix}0&0&0&0\\\ 1&0&0&0\\\ 0&0&0&0\\\
0&0&0&0\end{bmatrix}\quad E^{\prime\prime}_{0101}=\begin{bmatrix}0&0&0&0\\\
0&0&1&0\\\ 0&0&0&0\\\ 0&0&0&0\end{bmatrix}\quad
E^{\prime\prime}_{0110}=\begin{bmatrix}0&0&0&0\\\ 0&1&0&0\\\ 0&0&0&0\\\
0&0&0&0\end{bmatrix}\quad E^{\prime\prime}_{0111}=\begin{bmatrix}0&0&0&0\\\
0&0&0&1\\\ 0&0&0&0\\\ 0&0&0&0\end{bmatrix}$

Finally, the simplified form of $M_{7}$ is
$M_{7}=\langle\\{E^{\prime\prime\prime}_{0000},E^{\prime\prime\prime}_{0001},E^{\prime\prime\prime}_{0010},E^{\prime\prime\prime}_{0011}\\},f\rangle$,
where

$E^{\prime\prime\prime}_{0000}=\begin{bmatrix}1&0&0&0\\\ 0&0&0&0\\\ 0&0&0&0\\\
0&0&0&0\end{bmatrix}\quad
E^{\prime\prime\prime}_{0001}=\begin{bmatrix}0&0&1&0\\\ 0&0&0&0\\\ 0&0&0&0\\\
0&0&0&0\end{bmatrix}\quad
E^{\prime\prime\prime}_{0010}=\begin{bmatrix}0&1&0&0\\\ 0&0&0&0\\\ 0&0&0&0\\\
0&0&0&0\end{bmatrix}\quad
E^{\prime\prime\prime}_{0011}=\begin{bmatrix}0&0&0&1\\\ 0&0&0&0\\\ 0&0&0&0\\\
0&0&0&0\end{bmatrix}$

$\begin{array}[]{cl}&{\color[rgb]{0,0,1}\\{{\textbf{true}}\\}}\\\ SC\equiv&\\\
1:&q_{0}:=|0\rangle;\\\ 2:&q_{1}:=|0\rangle;\\\ 3:&H[q_{0}];\\\
4:&CNOT[q_{0}q_{1}];\\\ &{\color[rgb]{0,0,1}\\{({\mathbb{E}}_{y_{0}y_{1}\sim
M_{6}[q_{0}q_{1}]}[{\bf 1}_{\psi\wedge x_{0}=1\wedge
x_{1}=1}]={\mathbb{E}}_{y_{0}y_{1}\sim M_{6}[q_{0}q_{1}]}[{\bf
1}_{{\textbf{true}}}])}\\\
&{\color[rgb]{0,0,1}\oplus({\mathbb{E}}_{y_{0}y_{1}\sim
M_{4}[q_{0}q_{1}]}[{\bf 1}_{\psi\wedge x_{0}=1\wedge
x_{1}=0}]={\mathbb{E}}_{y_{0}y_{1}\sim M_{4}[q_{0}q_{1}]}[{\bf
1}_{{\textbf{true}}}])}\\\
&{\color[rgb]{0,0,1}\oplus({\mathbb{E}}_{y_{0}y_{1}\sim
M_{5}[q_{0}q_{1}]}[{\bf 1}_{\psi\wedge x_{0}=0\wedge
x_{1}=1}]={\mathbb{E}}_{y_{0}y_{1}\sim M_{5}[q_{0}q_{1}]}[{\bf
1}_{{\textbf{true}}}])}\\\
&{\color[rgb]{0,0,1}\oplus({\mathbb{E}}_{y_{0}y_{1}\sim
M_{3}[q_{0}q_{1}]}[{\bf 1}_{\psi\wedge x_{0}=0\wedge
x_{1}=0}]={\mathbb{E}}_{y_{0}y_{1}\sim M_{3}[q_{0}q_{1}]}[{\bf
1}_{{\textbf{true}}}])\\},}\\\ &{\color[rgb]{0,0,1}\mbox{where
}M_{6}\equiv\langle\\{E_{00}H_{q_{0}}CNOT_{q_{0}q_{1}}Z_{q_{0}}X_{q_{0}},\
E_{01}H_{q_{0}}CNOT_{q_{0}q_{1}}Z_{q_{0}}X_{q_{0}},}\\\ &\hskip
65.44142pt{\color[rgb]{0,0,1}E_{10}H_{q_{0}}CNOT_{q_{0}q_{1}}Z_{q_{0}}X_{q_{0}},\
E_{11}H_{q_{0}}CNOT_{q_{0}q_{1}}Z_{q_{0}}X_{q_{0}}\\},Id\rangle,}\\\
&{\color[rgb]{0,0,1}M_{5}\equiv\langle\\{E_{00}H_{q_{0}}CNOT_{q_{0}q_{1}}X_{q_{0}},\
E_{01}H_{q_{0}}CNOT_{q_{0}q_{1}}X_{q_{0}},}\\\ &\hskip
65.44142pt{\color[rgb]{0,0,1}E_{10}H_{q_{0}}CNOT_{q_{0}q_{1}}X_{q_{0}},\
E_{11}H_{q_{0}}CNOT_{q_{0}q_{1}}X_{q_{0}}\\},Id\rangle}\\\
5:&\textbf{if}~{}x_{1}=1~{}\textbf{then}~{}X[q_{0}];\\\
&{\color[rgb]{0,0,1}\\{({\mathbb{E}}_{y_{0}y_{1}\sim M_{4}[q_{0}q_{1}]}[{\bf
1}_{\psi\wedge x_{0}=1}]={\mathbb{E}}_{y_{0}y_{1}\sim M_{4}[q_{0}q_{1}]}[{\bf
1}_{{\textbf{true}}}])}\\\
&{\color[rgb]{0,0,1}\oplus({\mathbb{E}}_{y_{0}y_{1}\sim
M_{3}[q_{0}q_{1}]}[{\bf 1}_{\psi\wedge x_{0}=0}]={\mathbb{E}}_{y_{0}y_{1}\sim
M_{3}[q_{0}q_{1}]}[{\bf 1}_{{\textbf{true}}}])\\},}\\\
&{\color[rgb]{0,0,1}\mbox{where
}M_{4}\equiv\langle\\{E_{00}H_{q_{0}}CNOT_{q_{0}q_{1}}Z_{q_{0}},\
E_{01}H_{q_{0}}CNOT_{q_{0}q_{1}}Z_{q_{0}},}\\\ &\hskip
65.44142pt{\color[rgb]{0,0,1}E_{10}H_{q_{0}}CNOT_{q_{0}q_{1}}Z_{q_{0}},\
E_{11}H_{q_{0}}CNOT_{q_{0}q_{1}}Z_{q_{0}}\\},Id\rangle}\\\
6:&\textbf{if}~{}x_{0}=1~{}\textbf{then}~{}Z[q_{0}];\\\
&{\color[rgb]{0,0,1}\\{{\mathbb{E}}_{y_{0}y_{1}\sim M_{3}[q_{0}q_{1}]}[{\bf
1}_{\psi}]={\mathbb{E}}_{y_{0}y_{1}\sim M_{3}[q_{0}q_{1}]}[{\bf
1}_{{\textbf{true}}}]\\},}\\\ &{\color[rgb]{0,0,1}\mbox{where
}M_{3}\equiv\langle\\{E_{00}H_{q_{0}}CNOT_{q_{0}q_{1}},E_{01}H_{q_{0}}CNOT_{q_{0}q_{1}},E_{10}H_{q_{0}}CNOT_{q_{0}q_{1}},E_{11}H_{q_{0}}CNOT_{q_{0}q_{1}}\\},Id\rangle}\\\
7:&CNOT[q_{0}q_{1}];\\\ &{\color[rgb]{0,0,1}\\{{\mathbb{E}}_{y_{0}y_{1}\sim
M_{2}[q_{0}q_{1}]}[{\bf 1}_{\psi}]={\mathbb{E}}_{y_{0}y_{1}\sim
M_{2}[q_{0}q_{1}]}[{\bf 1}_{{\textbf{true}}}]\\},}\\\
&{\color[rgb]{0,0,1}\mbox{where
}M_{2}\equiv\langle\\{E_{00}H_{q_{0}},E_{01}H_{q_{0}},E_{10}H_{q_{0}},E_{11}H_{q_{0}}\\},Id\rangle}\\\
8:&H[q_{0}];\\\ &{\color[rgb]{0,0,1}\\{{\mathbb{E}}_{y_{0}y_{1}\sim
M_{1}[q_{0}q_{1}]}[{\bf 1}_{\psi}]={\mathbb{E}}_{y_{0}y_{1}\sim
M_{1}[q_{0}q_{1}]}[{\bf 1}_{{\textbf{true}}}]\\}}\\\
&{\color[rgb]{0,0,1}\mbox{where
}M_{1}\equiv\langle\\{E_{00},E_{01},E_{10},E_{11}\\},Id\rangle,}\\\
&{\color[rgb]{0,0,1}E_{00}\equiv[|0\rangle]_{q_{1}}\cdot[|0\rangle]_{q_{0}},\
E_{01}\equiv[|1\rangle]_{q_{1}}\cdot[|0\rangle]_{q_{0}},\
E_{10}\equiv[|0\rangle]_{q_{1}}\cdot[|1\rangle]_{q_{0}},\
E_{11}\equiv[|1\rangle]_{q_{1}}\cdot[|1\rangle]_{q_{0}}}\\\
9:&y_{0}:=M[q_{0}];\\\ &{\color[rgb]{0,0,1}\\{{\mathbb{E}}_{y_{1}\sim
M[q_{1}]}[{\bf 1}_{\psi}]={\mathbb{E}}_{y_{1}\sim M[q_{1}]}[{\bf
1}_{{\textbf{true}}}]\\}}\\\ 10:&y_{1}:=M[q_{1}]\\\ &\quad\mbox{where
}M=\langle\\{E_{0},E_{1}\\},Id\rangle,E_{0}=[|0\rangle],E_{1}=[|1\rangle]\\\
&{\color[rgb]{0,0,1}\\{\Box\psi\\},\mbox{ where }\psi\equiv x_{0}=y_{0}\wedge
x_{1}=y_{1}}\end{array}$ Figure 11: The quantum program with pre- and
postconditions

Write $P$ for the assertion in (${\dagger}$). We have seen that

$\\{P\\}\;SC\;\\{\Box\psi\\}.$ (16)

We observe that ${\textbf{true}}\Leftrightarrow P$. This can be seen as
follows. Let

$\begin{array}[]{rcl}P_{11}&\equiv&({\mathbb{E}}_{y_{0}y_{1}\sim
M_{10}[q_{0}q_{1}]}[{\bf 1}_{\psi\wedge x_{0}=1\wedge
x_{1}=1}]={\mathbb{E}}_{y_{0}y_{1}\sim M_{10}[q_{0}q_{1}]}[{\bf
1}_{{\textbf{true}}}])\\\ P_{10}&\equiv&({\mathbb{E}}_{y_{0}y_{1}\sim
M_{9}[q_{0}q_{1}]}[{\bf 1}_{\psi\wedge x_{0}=1\wedge
x_{1}=0}]={\mathbb{E}}_{y_{0}y_{1}\sim M_{9}[q_{0}q_{1}]}[{\bf
1}_{{\textbf{true}}}])\\\ P_{01}&\equiv&({\mathbb{E}}_{y_{0}y_{1}\sim
M_{8}[q_{0}q_{1}]}[{\bf 1}_{\psi\wedge x_{0}=0\wedge
x_{1}=1}]={\mathbb{E}}_{y_{0}y_{1}\sim M_{8}[q_{0}q_{1}]}[{\bf
1}_{{\textbf{true}}}])\\\ P_{00}&\equiv&({\mathbb{E}}_{y_{0}y_{1}\sim
M_{7}[q_{0}q_{1}]}[{\bf 1}_{\psi\wedge x_{0}=0\wedge
x_{1}=0}]={\mathbb{E}}_{y_{0}y_{1}\sim M_{7}[q_{0}q_{1}]}[{\bf
1}_{{\textbf{true}}}])\\\ b_{11}&\equiv&x_{0}=1\wedge x_{1}=1\\\
b_{10}&\equiv&x_{0}=1\wedge x_{1}=0\\\ b_{01}&\equiv&x_{0}=0\wedge x_{1}=1\\\
b_{00}&\equiv&x_{0}=0\wedge x_{1}=0\end{array}$

We have $P=P_{11}\oplus P_{10}\oplus P_{10}\oplus P_{00}$. For any POVD $\mu$,
it is easy to see that

$\mu=\mu_{|b_{11}}+\mu_{|b_{10}}+\mu_{|b_{01}}+\mu_{|b_{00}}$

We have that $\mu_{|b_{11}}\models P_{11}$ because

$\begin{array}[]{ll}&[\\![{\mathbb{E}}_{y_{0}y_{1}\sim
M_{10}[q_{0}q_{1}]}[{\bf 1}_{\psi\wedge x_{0}=1\wedge
x_{1}=1}]]\\!]_{\mu_{|b_{11}}}\\\
=&\sum_{\sigma}\sum_{i}E_{i}\mu_{|b_{11}}(\sigma)M^{\dagger}_{i}\cdot{\bf
1}_{[\\![\psi\wedge x_{0}=1\wedge x_{1}=1]\\!]_{\sigma[f(i)/y_{0}y_{1}]}}\\\
&\mbox{where }i\in\\{1100,1101,1110,1100\\}\\\
=&\sum_{\sigma}\sum_{i}E_{i}\mu_{|b_{11}}(\sigma)M^{\dagger}_{i}\cdot{\bf
1}_{[\\![\psi\wedge x_{0}=1\wedge x_{1}=1]\\!]_{\sigma[11/y_{0}y_{1}]}}\\\
=&\sum_{\sigma}\sum_{i}E_{i}\mu_{|b_{11}}(\sigma)M^{\dagger}_{i}\cdot 1\\\
=&\sum_{\sigma}\sum_{i}E_{i}\mu_{|b_{11}}(\sigma)M^{\dagger}_{i}\cdot{\bf
1}_{[\\![{\textbf{true}}]\\!]_{\sigma[11/y_{0}y_{1}]}}\\\
=&[\\![{\mathbb{E}}_{y_{0}y_{1}\sim M_{10}[q_{0}q_{1}]}[{\bf
1}_{{\textbf{true}}}]]\\!]_{\mu_{|b_{11}}}\end{array}$

which implies $[\\![P_{11}]\\!]_{\mu_{|b_{11}}}={\textbf{true}}$. Similarly,
we can check that $\mu_{|b_{10}}\models P_{10}$, etc. Therefore, we obtain
that $\mu\models P$. As $\mu$ is arbitrarily chosen, we have verified that
${\textbf{true}}\Leftrightarrow P$. By (16) and rule [Conseq], we finally see
that the triple $\\{{\textbf{true}}\\}\;SC\;\\{\Box\psi\\}$ is provable.

As we can see in (15), the postcondition of that Hoare triple is an assertion
about classical variables, even though quantum computation takes place during
the execution of the program $SC$. For such scenario, it is very natural to
prove the correctness of programs via an satisfaction-based proof system,
rather than an expectation-based one.

##  7 Conclusion and future work

We have introduced a simple quantum imperative language that has both
classical and quantum constructs by extending the language IMP studied in
depth by Winskel. We have investigated its formal semantics by providing a
small-step operational semantics, a denotational semantics and two Hoare-style
proof systems: an abstract one and a concrete one. In order to define the
semantics, we have used the notion of POVDs to represent the states of
programs. Therefore, a program can be considered as a transformer of POVDs.
Following the work of Barthe et al, we have designed two satisfaction-based
proof systems, as opposed to the usual expectation-based systems. The abstract
proof system turns out to be sound and relatively complete, while the concrete
one is sound.

As to the future work, at least two immediate improvements are interesting and
worth being considered.

  * 1.

The proof rule [While] is not satisfactory because it involves two sequences
of assertions $(P_{n})$ and $(P^{\prime}_{n})$. In either the purely classical
[11] or purely quantum setting [25], the rule can be elegantly formulated.
However, in the presence of both classical and quantum variables, it remains a
challenge to find a more concise formulation of the rule.

  * 2.

The reasoning in Section 6 about the example of superdense coding was done
manually. In the future, we would like to embed our program logic in a proof
assistant so as to facilitate the reasoning.

## References

  * [1] K. Apt, F. S. De Boer, and E.-R. Olderog.  Verification of sequential and concurrent programs.  Springer Science & Business Media, 2010.
  * [2] K. R. Apt and E.-R. Olderog.  Fifty years of Hoare’s logic.  Formal Aspects of Computing, 31(6):751–807, 2019.
  * [3] G. Barthe, T. Espitau, M. Gaboardi, B. Grégoire, J. Hsu, and P. Strub.  An assertion-based program logic for probabilistic programs.  In Proceedings of the 27th European Symposium on Programming, volume 10801 of Lecture Notes in Computer Science, pages 117–144. Springer, 2018.
  * [4] C. Bennett and S. Wiesner.  Communication via one- and two-particle operators on Einstein-Podolsky-Rosen states.  Physical Review Letters, 69(20):2881–2884, 1992.
  * [5] R. Chadha, L. Cruz-Filipe, P. Mateus, and A. Sernadas.  Reasoning about probabilistic sequential programs.  Theoretical Computer Science, 379(1-2):142–165, 2007.
  * [6] R. Chadha, P. Mateus, and A. Sernadas.  Reasoning about imperative quantum programs.  Electronic Notes in Theoretical Computer Science, 158:19–39, 2006\.
  * [7] J. Den Hartog and E. P. de Vink.  Verifying probabilistic programs using a Hoare like logic.  International journal of foundations of computer science, 13(03):315–340, 2002.
  * [8] Y. Feng, S. Li, and M. Ying.  Verification of distributed quantum programs.  arXiv preprint arXiv:2104.14796, 2021.
  * [9] Y. Feng and M. Ying.  Quantum Hoare logic with classical variables.  arXiv preprint arXiv:2008.06812, 2020.
  * [10] L. K. Grover.  A fast quantum mechanical algorithm for database search.  In Proceedings of the 28th Annual ACM Symposium on Theory of Computing, pages 212–219. ACM, 1996.
  * [11] C. A. R. Hoare.  An axiomatic basis for computer programming.  Communications of the ACM, 12(10):576–580, 1969.
  * [12] Y. Kakutani.  A Logic for Formal Verification of Quantum Programs.  Lecture Notes in Computer Science, pages 79–93, 2009.
  * [13] D. Kozen.  Semantics of probabilistic programs.  Journal of Computer and System Sciences, 22:328–350, 1981.
  * [14] D. Kozen.  A probabilistic PDL.  Journal of Computer and System Sciences, 30(2):162–178, 1985.
  * [15] Y. Li and D. Unruh.  Quantum relational Hoare logic with expectations.  arXiv preprint arXiv:1903.08357, 2019.
  * [16] A. McIver, C. Morgan, and C. C. Morgan.  Abstraction, refinement and proof for probabilistic systems.  Springer Science & Business Media, 2005.
  * [17] C. Morgan, A. McIver, and K. Seidel.  Probabilistic predicate transformers.  ACM Transactions on Programming Languages and Systems (TOPLAS), 18(3):325–353, 1996.
  * [18] M. Nielsen and I. Chuang.  Quantum computation and quantum information.  Cambridge university press, 2000.
  * [19] F. Olmedo, B. L. Kaminski, J.-P. Katoen, and C. Matheja.  Reasoning about recursive probabilistic programs.  In 2016 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–10. IEEE, 2016.
  * [20] L. H. Ramshaw.  Formalizing the analysis of algorithms.  Technical report, Stanford University, 1979.
  * [21] P. W. Shor.  Algorithms for quantum computation: discrete logarithms and factoring.  In Proceedings of the 35th Annual Symposium on Foundations of Computer Science, pages 124–134. IEEE Computer Society, 1994.
  * [22] D. Unruh.  Quantum Hoare logic with ghost variables.  In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–13. IEEE, 2019.
  * [23] J. von Neumann.  States, Effects and Operations: Fundamental Notions of Quantum Theory.  Princeton University Press, 1955.
  * [24] G. Winskel.  The Formal Semantics of Programming Languages - An Introduction.  The MIT Press, 1993.
  * [25] M. Ying.  Floyd–Hoare logic for quantum programs.  ACM Transactions on Programming Languages and Systems, 33(6):1–49, 2012.
  * [26] M. Ying.  Foundations of Quantum Programming.  Morgan Kaufmann, 2016.
  * [27] M. Ying, L. Zhou, and Y. Li.  Reasoning about parallel quantum programs.  arXiv preprint arXiv:1810.11334, 2018.
  * [28] L. Zhou, N. Yu, and M. Ying.  An applied quantum Hoare logic.  In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 1149–1162, 2019.