Reﬁning Exceptions in Four-Valued Logic ?
Susumu NISHIMURA
Dept. of Mathematics, Graduate School of Science, Kyoto University
Sakyo-ku, Kyoto 606-8502, JAPANsusumu@math.kyoto-u.ac.jp
December 25, 2009

Abstract. This paper discusses reﬁnement of programs that may raise and catch
exceptions. We show that exceptions are expressed by a class of predicate transformers built on Arieli and Avron’s four-valued logic and develop a reﬁnement
framework for the four-valued predicate transformers. The resulting framework
enjoys several reﬁnement laws that are useful for stepwise reﬁnement of programs
involving exception handling and partial predicates. We demonstrate some typical usages of the reﬁnement laws in the proposed framework by a few examples
of program transformation.

1

Introduction

Program reﬁnement has been intensively studied in the framework of reﬁnement calculus [BvW98, Mor94]. Reﬁnement calculus identiﬁes each program with a predicate
transformer and formally justiﬁes reﬁnement of programs by means of the so-called
reﬁnement relation that is induced from the logical entailment. Although reﬁnement
calculus is successfully applied to a certain extension of Dijkstra’s guarded commandlanguage [Dij76], fundamental difﬁculties arise when we try to extend the languagewith exceptions.
First, since exceptional termination is not discriminated from non-termination in thepredicate transformer semantics, a construct that catches exceptions would also catch
non-termination, which is counter-intuitive from the operational point of view. Second,
exceptions are not only raised explicitly by a command but also implicitly by a failure ofcomputation (e.g., division by zero). In this paper, we argue the latter type of exceptions
that are raised by partial predicates, whose truth value may not be deﬁned. Partiality
poses a foundational issue in developing the theory of reﬁnement based on the classicallogic, in which partiality is ruled out. For example, in Dijkstra’s predicate transformer
semantics, the weakest pre-condition of the conditional statement if p then S else T is
speciﬁed by a formula (p ⇒ S(ϕ)) ∧ (¬p ⇒ T (ϕ)) for any post-condition ϕ, but thisformula is nonsensical in the classical logic when p is undeﬁned.
King and Morgan [KM95] proposed a solution to the ﬁrst problem by developing
an extension to the traditional predicate transformer semantics for a language in which? This is a full version of the paper to appear in the post-proceedings of 19th International

Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2009), LNCS.

exceptions are explicitly raised by the command exit and are caught by the exception
block construct try S catch T 1 . They speciﬁed the input of each predicate transformer
by a pair of post-conditions hϕn , ϕe i, rather than by a single post-condition, where they
write wp(S, ϕn , ϕe ) for the weakest pre-condition that guarantees the program S either
to normally terminate establishing ϕn or to exceptionally terminate establishing ϕe . The
weakest pre-conditions for exit and the exception block are given as below:
wp(exit, ϕn , ϕe ) = ϕe ,wp(try S catch T, ϕn , ϕe ) = wp(S, ϕn , wp(T, ϕn , ϕe )).

The intuition behind these speciﬁcations are explained as follows. The exit command
immediately causes an exceptional termination. Thus, the command is guaranteed toterminate (exceptionally) establishing the pre-condition ϕe . The exception block try S
catch T executes S and terminates normally, if no exception is raised; If an exception
is ever raised, the raised exception is caught and then processed by T to resume normal
execution. Therefore, for the exception block to terminate establishing the pair hϕn , ϕe iof post-conditions, S is either to normally terminate establishing ϕn or to exceptionallyterminate establishing wp(T, ϕn , ϕe ), which guarantees T to terminate establishing thepair of conditions hϕn , ϕe i.
In this paper, we propose a reﬁnement calculus for a language that may raise andcatch exceptions, where exceptions can be raised not only by the exit command explicitly but also by the evaluation of partial predicates implicitly. For this, we develop ourtheory of program reﬁnement in a predicate transformer semantics based on Arieli andAvron’s four-valued logic [AA96, AA98].
The four-valued predicate transformer semantics can be easily derived from Kingand Morgan’s, in the following way. First, we identify each statement S by a predicate
transformer that maps a pair of (classical) predicates hϕn , ϕe i to another pair of predicates hϕ0n , ϕe i, where ϕ0n is the weakest pre-condition computed by King and Morgan’s
predicate transformer wp. This deﬁnition is intended to guarantee the program S either to normally terminate establishing ϕn or to exceptionally terminate establishing ϕe ,whenever the preceding statement normally terminates establishing ϕ0n or exceptionallyterminates establishing ϕe . Notice that the condition ϕe for exceptional termination isleft unchanged by the transformer because no statement can cancel exceptional termination caused by the preceding statements.
Next, let us designate a classical predicate by a total function from the set of states
to {0, 1}, where 0 and 1 designates the two classical truth values (i.e., false and true,
respectively). Then we identify each pair of predicates hϕn , ϕe i by a single four-valued
predicate ϕ such that ϕ(σ) = hϕn (σ), ϕe (σ)i for every state σ. The range of the fourvalued predicate is {h1, 0i, h0, 1i, h0, 0i, h1, 1i}, which we designate by t, f, ⊥, and >,respectively. This structure with four truth values gives rise to the so called Belnap’s
four-valued logic [Bel77], which has been studied by Ginsberg in the generalized setting of bilattices [Gin88] and was further examined by Fitting [Fit94]. Arieli and Avron[AA96, AA98] introduced the notion of logical bilattices and developed the corresponding proof system.
The four-valued logic provides a ﬁrm logical basis for reﬁning exceptions, as theoriginal reﬁnement calculus does for reﬁning the guarded command language. The
1 This extends the exception block construct proposed in [KM95] with exception handling.

constructs for exceptions and others as well are concisely speciﬁed by the formulas offour-valued logic. The conditional control via partial predicates can be translated into apredicate transformer, where the undeﬁnedness of partial predicates is denoted by thetruth value ⊥. The reﬁnement relation is induced from the logical entailment (in thesense of four-valued logic), i.e., S v T iff S(ϕ) entails T (ϕ) for any post-condition ϕ.
We emphasize that we use the four-valued logic in two different ways. In the predicate transformer semantics, it is used for discriminating the possible termination behaviors (either, both, or none of normal termination and exceptional termination), while
in modelling partial predicates, it is used as a many-valued logic that allows undeﬁnedness. Although a three-valued logic would be sufﬁcient for the latter purpose, we stickto the four-valued logic in developing the theory of reﬁnement in order to achieve asmooth translation of conditional controls via partial predicates into four-valued predicate transformers. For a more neat characterization of partial predicates that adheres tothe operational intuition, we also consider partial predicates in a three-valued sublogic,
whose truth values are conﬁned to f, t, and ⊥. In later sections we exploit the propertiesof partial predicates in this three-valued sublogic.
Related work. It seems that there has been no attempt to formulate a predicate transformer semantics that gives a unifying account for both exceptions and partial predicates. The exception mechanism was formulated in terms of predicate transformers
in King and Morgan’s reﬁnement calculus [KM95], which was further elaborated in[Wat02]. Partial predicates are out of their concern, however. (If partial predicates are
ignored at all, the reﬁnement calculus of theirs and that of ours are essentially the same.)
Partial predicates in program logic have been intensively studied in the context of
three-valued logic. For instance, the VDM speciﬁcation language deals with undeﬁnedness in a logic called LPF [Jon86, JM94]; Bono et al. [BK06] formulated a Hoare
logic with a third truth value denoting ‘crash’ of execution. Many other variants ofthree-valued logic have been proposed for the sake of a better treatment of partiality[Owe93, JM94, MB99]. The three-valued logic, however, is not suitable for describing a
predicate transformer semantics for exceptions, because the underlying predicate logic
must be able to discriminate the four different status of termination. Hähnle [Häh05]
discussed that partiality should be dealt by underspeciﬁcation, rather than by a value
representing undeﬁnedness in a many-valued logic. His argument is, however, about
predicates in speciﬁcation statements and does not consider exception catching.
Huisman and Jacobs [HJ00] extended Hoare logic to deal with abrupt (exceptional)
termination in Java programming language. They also formulated the mechanism ofcatching exceptions in their program logic by representing several different modes of
exceptional termination by different forms of Hoare triple. In contrast to theirs, ours
simply supports a single mode of exceptional termination. This does not imply ours areless expressive than theirs. Ours can simulate different modes of exceptional termination by introducing a special variable indicating the mode of termination.
Outline. The rest of the paper is organized as follows. Section 2 introduces the notionof bilattices and the four-valued logic. Section 3 speciﬁes a set of program statements
as four-valued predicate transformers and we identify the class of predicate transformers. The statements involve exit, exceptions blocks, and conditional controls via partial

predicates. The logical connectives for partial predicates are also discussed. In Section 4, we investigate a set of reﬁnement laws that hold for these statements and logicalconnectives. In Section 5, we apply the reﬁnement laws to carry out some programtransformations. Finally, Section 6 concludes the paper.

2

The bilattice FOUR and the Four-Valued Logic

2.1

The bilattice FOUR of four truth values> (= h1, 1i)¡ @@¡(h0, 1i =) ft (= h1, 0i)@¡@ ¡⊥ (= h0, 0i)≤tFig. 1. The bilattice of four truth values≤k

6

Let TWO be the lattice of classical truth values of 0, 1 with the trivial order 0 < 1. The
bilattice FOUR is a structure obtained by a
product construction TWO ¯ TWO: it consists of four elements h1, 0i, h0, 1i, h0, 0i,and h1, 1i, which are alternatively written t,f, ⊥, and >, respectively. The bilattice has
two lattice structures simultaneously (see the double Hasse diagram of Figure 1), eachcharacterized by the partial orders ≤t and ≤k deﬁned below.2
hx1 , y1 i ≤t hx2 , y2 i iff x1 ≤ x2 and y2 ≤ y1 ,hx1 , y1 i ≤k hx2 , y2 i iff x1 ≤ x2 and y1 ≤ y2 .
The ≤t order (resp. ≤k order) induces the meet ∧ and join ∨ operators (resp. meet
⊗ and join ⊕ operators) The deﬁnitions are given below, where u and t stand for themeet and join in TWO, respectively.
hx1 , y1 i ∧ hx2 , y2 i = hx1 u x2 , y1 t y2 i,

hx1 , y1 i ∨ hx2 , y2 i = hx1 t x2 , y1 u y2 i,

hx1 , y1 i ⊗ hx2 , y2 i = hx1 u x2 , y1 u y2 i,

hx1 , y1 i ⊕ hx2 , y2 i = hx1 t x2 , y1 t y2 i.

In addition, negation ¬ is deﬁned by ¬hx, yi = hy, xi as an operator that inverts the≤t order but keeps the ≤k order.
In FOUR, the operations ∨ and ∧ are De Morgan dual of each other, i.e., ¬(x ∨y) = ¬x ∧ ¬y and ¬(x ∧ y) = ¬x ∨ ¬y, while ⊕ and ⊗ are De Morgan self-dual, i.e.,¬(x ⊕ y) = ¬x ⊕ ¬y and ¬(x ⊗ y) = ¬x ⊗ ¬y. The four values are related with each otherby means of ∨, ∧, ⊕, and ⊗, e.g., ⊥ ∨ f = ⊥, t ⊕ f = >, x ∨ ⊥ = x ⊗ t.
The bilattice FOUR is distributive, i.e., the four lattice operations ∧, ∨, ⊗, and ⊕distribute over each other, e.g., x ⊕ (y ∧ z) = (x ⊕ y) ∧ (x ⊕ z). A distributive bilattice isalso interlaced, that is, each of the four lattice operations is monotonic with respect toboth ≤t and ≤k , e.g., y ≤t z implies x ⊗ y ≤t x ⊗ z.
The bilattice structure can be made into a logical bilattice that provides suitable
notions of implications in four-valued logic [AA96]. With D = {t, >} being the set of
2 In the literature, ≤ is often regarded as the degree of truth and ≤ as the amount of infortkmation. Given a product hx, yi of classical truth values, x represents the amount of evidence
for an assertion, while y represents the amount of evidence against it. However, one should
refrain from sticking to this particular interpretation, when the four-valued logic is used fordiscriminating the possible termination behaviors in the predicate transformer semantics.

designated truth values, which are the values recognized as (at least) known to be true,
the bilattice FOUR is made into a logical bilattice with two implication connectives,
called weak implication ⊃ and strong implication →, which are deﬁned as below:½
t (x 6∈ D )x⊃y,x→y , (x ⊃ y) ∧ (¬y ⊃ ¬x).
y (otherwise) ,Using strong implication, we deﬁne the equivalence x ↔ y by (x→y) ∧ (y→x).
2.2

The four-valued predicate logic

We give a four-valued ﬁrst-order predicate logic, based on the Arieli and Avron’s fourvalued propositional system. (Extension to the predicate logic is straightforward, as
mentioned in [AA96].) We assume the set Value of program values (integers, etc.) andthe set Var of program variables. Let us deﬁne State to be the set of total functions from
Var to Value. Given σ ∈ State and X ∈ Var, σ(X) denotes the value that is assigned tothe program variable X in the state σ.
Four-valued predicates, denoted by p, q, etc., are total functions from State to thefour truth values in FOUR. The four-valued predicates form a bilattice, where the twopartial orders ≤t and ≤k and logical connectives ∧, ∨, ⊗, ⊕, ¬, ⊃, →, ↔ are accordingly deﬁned in the pointwise way. That is, for every state σ, p ≤t q (resp. p ≤k q)
holds iff p(σ) ≤t q(σ) (resp. p(σ) ≤k q(σ)), and also logical connectives are deﬁnedby (p ∨ q)(σ) , p(σ) ∨ q(σ), (¬p)(σ) , ¬p(σ), etc. In abuse of notations, we will also
denote a constant predicate by the constant itself. That is, we write t for a predicate psuch that p(σ) = t for every state σ; Similarly for f, ⊥, and >.
It is easy to verify that the bilattice of the four-valued predicates is distributive,
interlaced, bounded, and complete. (A bilattice is complete, if the two lattices inducedby the partial orders ≤t and ≤k are both complete.) The completeness indicates that
we may also deﬁne quantiﬁcation by means of the inﬁnite join or meet. Given a familyof predicates {p(i) | i ∈ Value}, we deﬁne the universal quantiﬁcation (resp. existential
WVquantiﬁcation) over i of predicate p(i) by ∀i.p(i) , i p(i) (resp. ∃i.p(i) , i p(i))
The above mentioned structure of logical bilattice induces a four-valued predicate logic [AA96], which has a Gentzen-style proof system for sequents of the form
p1 , · · · , pn ` q1 , · · · , qm (n, m ≥ 0). The sequent corresponds to the consequence relation p1 , · · · , pn |= q1 , · · · , qm , which means, for any state σ, if pi (σ) ∈ D for all i, thenq j (σ) ∈ D for some j. We say a predicate p is valid iff |= p holds (i.e., p(σ) ∈ D for
any state σ).
Notice that the four-valued logic is a non-classical logic. In particular it is paraconsistent and does not admit the law of the excluded middle, that is, we have neither` p ∨ ¬p nor p ∧ ¬p ` q. The connectives ⊃, →, and ↔ are a logical implication oran equivalence in the following sense: |= p ⊃ q iff p |= q; |= p→q iff p ≤t q; |= p ↔ q
iff p = q. Furthermore the logical equivalence ↔ is a congruence: |= p ↔ q implies|= Θ(p) ↔ Θ(q) for any formula scheme Θ. For further details of the proof system andlogical properties of the four-valued logic, see [AA96, AA98].
Throughout the paper, we follow the convention that the negation and quantiﬁcations bind most tightly, while implications do least tightly and associate to right. We do
not impose any particular precedence between ∨, ∧, ⊕, and ⊗.

Finally, let us introduce some notations that are related to states. A program expression e is a total function from State to Value. We write σ[X\v] for the state obtained
by updating the value assigned to the program variable X in the state σ by the value v.
Similarly, we write σ[X\e] for an update of variable X with the value of expression e,that is, σ[X\e(σ)]. Given a four-valued predicate p, we also write p[X\v] (resp. p[X\e])for the predicate q such that q(σ) = p(σ[X\v]) (resp. q(σ) = p(σ[X\e])) In particular,a predicate p[X\v] can be recognized as a predicate indexed by v ranging over Value.
In abuse of notations, we may often confuse a program variable X with an expression
e such that e(σ) = σ(X). More generally, we may confuse numerical expressions andpredicates with their pointwise extensions.
¡ For example, ¢when we write X + 1 ≥ Y , itdenotes a predicate q such that q(σ) = σ(X) + 1 > σ(Y ) , where + is the binary integer addition and ≥ is the binary predicate such that (v ≥ v0 ) = t if v is greater than orequal to v0 but (v ≥ v0 ) = f otherwise.

3

Predicate Transformers and Reﬁnement

3.1

The lattice of predicate transformers

As we have argued earlier, a predicate transformer should be a function that maps apair of predicates hϕn , ϕe i to another pair hϕ0n , ϕe i. We also require every predicate
transformer to be monotonic.
Deﬁnition 3.1. A pair of four-valued predicates p and p0 is called an exception matching pair if t ⊕ p = t ⊕ p0 holds.
A predicate transformer S over four-valued predicates is monotonic if S(ϕ) ≤k S(ϕ0 )holds for every exception matching pair ϕ and ϕ0 such that ϕ ≤k ϕ0 . S is exception stable
if ϕ and S(ϕ) are an exception matching pair, for every ϕ.
Let PTran be the set of predicate transformers of four-valued predicates that aremonotonic and exception stable. Then PTran is made into a bounded complete lattice
as follows.
Theorem 3.1. Let PTran be lattice induced by the partial order v by:
S v T iff S(ϕ) ≤k T (ϕ) for any ϕ,where the join ⊕ and meet ⊗ operators are a pointwise extension of the corresponding
logical connectives, i.e., (S ⊕ T )(ϕ) = S(ϕ) ⊕ T (ϕ) and (S ⊗ T )(ϕ) = S(ϕ) ⊗ T (ϕ).
Then PTran is a bounded complete lattice.
The class PTran of predicate transformers are also closed under function composition, where we write S; T to mean (S; T )(ϕ) = S(T (ϕ)) and intend a sequential execution of S followed by T . The meet S ⊗ T and join S ⊕ T in PTran, called demonic choice
and angelic choice, respectively, are intended a non-deterministic choice between S
and T : The demonic choice represents the least possible non-deterministic executionthat the two statements agree, while the angelic choice represents the greatest possible
one.
In order to verify that a reﬁnement relation S v T holds, we need to show S(ϕ) ≤k
T (ϕ) holds for every ϕ. There are several different ways to verify this.

¡skip(ϕ) , ϕ¢
X := e (ϕ) , (f ⊕ ϕ[X\e]) ⊗ (t ⊕ ϕ)(skip)(assignment)

abort(ϕ) , f ⊗ ϕ(non-termination)

magic(ϕ) , t ⊕ ϕ(miracle)exit(ϕ) , (t ⊕ ϕ) ⊗ ¬(t ⊕ ϕ)¡¡¢¢try S catch T , f ⊕ S (f ⊕ ϕ) ⊗ ¬(f ⊕ T (ϕ)) ⊗ (t ⊕ ϕ)
© ªp (ϕ) , ¬(p ⊃ >) ⊗ ϕ£ ¤p (ϕ) , (p ⊃ ⊥) ⊕ ϕ­ ®
p (ϕ) , ((p ⊃ ⊥) ⊕ ϕ) ⊗ ¬((p ⊃ >) ⊕ ϕ)(exit)(exception handling)(assertion)(assumption)(conditional exit)

Fig. 2. Four-valued predicate transformers for program statements

Proposition 3.1. For any S, T ∈ PTran and any four-valued predicate ϕ, S(ϕ) ≤k T (ϕ)
iff S(ϕ) ≤t T (ϕ) iff |= S(ϕ)→T (ϕ) iff S(ϕ) |= T (ϕ) iff S(ϕ) ` T (ϕ).
Thus we may verify S v T by checking the validity of S(ϕ)→T (ϕ) in the modelof bilattice, which will be effective for the propositional cases. In case quantiﬁers are
involved, we may resort to a formal proof deriving the sequent of the form S(ϕ) ` T (ϕ).
Further discussions on these alternative ways for validating reﬁnement laws are foundin Appendix A.
3.2

Predicate transformers for basic statements

Let us write hϕn , ϕe i for the pair of predicates that a four-valued predicate ϕ encodes as
we have argued in the introduction. When we deﬁne a predicate transformer in PTran,
we often need to operate on each component of the pair separately. This can be easily
expressed by the four-valued logic formulas. For example, given four-valued predicates
p and q, we can express the pair hpn , qe i by the formula (f ⊕ p) ⊗ (t ⊕ q).3 A simple
calculation veriﬁes this as follows:(f ⊕ p) ⊗ (t ⊕ q) = (h0, 1i ⊕ hpn , pe i) ⊗ (h1, 0i ⊕ hqn , qe i) = hpn , 1i ⊗ h1, qe i = hpn , qe i.
In a similar way, we can verify that (t ⊕ p) ⊗ ¬(t ⊕ p) calculates hpe , pe i and (f ⊕ p) ⊗¬(f ⊕ p) does hpn , pn i.
In Figure 2, we give the deﬁnitions of four-valued predicate transformers for a setof basic statements. (It is easy to verify that all of them are a member of PTran.)– skip is the idle statement. It is an identity function and hence is a neutral element
for the sequential composition, i.e., skip; S = S; skip = S.
3 There are different ways of expressing the same operation, e.g., (t ⊗ p) ⊕ (f ⊗ q).

– X := e is the assignment statement. Given a post-condition hϕn , ϕe i, it calculates
the weakest pre-condition ϕn [X\e] for normal termination and keeps the condition
ϕe for exceptional termination unchanged. Note that this assignment is total anddeterministic, that is, it always successfully assigns a unique value to the program
variable. We will discuss partial assignments in Section 5.2.
– abort and magic are extremal elements, that is, the least and greatest elements of
PTran, respectively. abort4 represents a statement that is not guaranteed to terminate normally. On the other hand, magic represents a miraculous statement that always terminates normally, establishing any required post-condition (even falsity).
They are a left-zero element of sequential composition, that is, abort; S = abortand magic; S = magic.
– exit is the statement that raises an exception. As we discussed earlier, it is characterized by a function that transforms every post-condition hϕn , ϕe i into hϕe , ϕe i.
Again exit is a left-zero element, i.e., exit; S = exit.
– try S catch T is the exception handling statement. The statement calculates theweakest post-condition for normal termination given by King and Morgan’s wpfunction and combines it with the condition for exceptional termination, using theformulas©
ª £ ¤ discussed­ ® above.
– p , p , and p , which are called assertion, assumption, and conditional exit,
respectively, are primitive forms of conditional controls, which decide how to continue the execution, depending on the value of the four-valued predicate p, whichis called a guard predicate. They are all equivalent to ©skip,
p has aª £if ¤the­ predicate®
designated truth value (i.e., either t or >); otherwise, p , p , p are equivalent
to abort, magic, exit, respectively.5
The basic statements above can be combined to form a more complicated statement.
A conditional statement if p then S else T , which may raise an exception when a partial
predicate p evaluates to ⊥, can be deﬁned as follows:
­
® £ ¤
£
¤
if p then S else T , p ∨ ¬p ; (( p ; S) ⊗ ( p ⊃ ⊥ ; T )).
­®
The partiality of predicate p is ﬁrst tested by the prepended p ∨ ¬p , which acts likeexit if p has the value ⊥ but like skip otherwise. Then, a demonic choice is made between the two branches, each prepended by an assumption statement. (The assumption
statement in the unselected branch becomes magic, which is dismissed by the outerdemonic choice.)
3.3

Logical connectives for partial predicatesIn the above deﬁnition of conditional statements, we interpret > as an indication of trueon the ground that > is a designated value in the four-valued logic, but this sometimes
4 The name ‘abort’ is historical and is not necessarily adequate in the context of this paper, but

we keep using it for compatibility.
5 Some programming languages provide a feature called ‘assertion’, which is used for excep-

tionally terminating the execution©whenª some critical violation of condition is detected. Notethe difference from the assertion p , which is non-terminating when the test on p is false.
The name ‘assertion’ is thus somewhat confusing but we keep using it for historical reason.

leads to a result that runs counter to the operational intuition. (For example, some of thelaws given in Section 5.1 do not hold for arbitrary four-valued guard predicates.)
In order to obtain a more precise modelling of partial predicates that adheres to theoperational intuition, let us consider consistent predicates [Fit94]: A four-valued predicate p is called consistent if p(σ) ∈ {t, f ⊥} for any σ. The class of consistent predicatesforms a three-valued sublogic, whose logical operators ∧ and ∨, a.k.a. strong Kleeneconnectives, are non-strict operators that avoid ⊥ whenever possible. (For instance, bothf ∧ ⊥ and ⊥ ∧ f are interpreted f rather than ⊥.) Non-strictness implies that the strong
Kleene connectives cannot be implemented in real programming languages.
We can deﬁne logical operators that are found in practical programming languages
in the three-valued sublogic as follows. Following [Fit94], let us write p : q for ((p ⊗t) ⊕ ¬(p ⊗t)) ⊗ q. This derived formula p : q has ⊥ if p has f or ⊥; otherwise, it has thevalue of q.
We can deﬁne a ‘sequential’ disjunction ~∨ and conjunction ~∧ for any pair of consistent predicates p and q, as follows.
p~∧q , p ∧ (p : q)p~∨q , p ∨ (¬p : q)

These operators are strict and evaluated sequentially from left to right: it becomes ⊥ assoon as the left subformula p evaluates to ⊥.
We can also deﬁne the weak Kleene connectives ∨w and ∧w as the consensus of thecorresponding two sequential connectives of opposite directions.
p ∧w q , (p~∧q) ⊗ (q~∧ p)

p ∨w q , (p~∨q) ⊗ (q~∨ p)

In contrast to the strong Kleene connectives, the value of these connectives is deﬁned
only if both of the subformulas are deﬁned.
The strong Kleene connectives ∧ and ∨, the sequential connectives ~∧ and ~∨, andalso the weak Kleene connectives ∧w and ∨w are all De Morgan dual for each.

4

Reﬁnement Laws for Statements

In the rest of this paper, we assume that guard predicates occurring in control statements are four-valued, unless explicitly stated otherwise. We will indicate wherever a
guard predicate is required to be consistent. We further assume that, unless it is explicitly stated otherwise, numerical predicates (which we mentioned in the last paragraphof Section 2.2) are classical, that is, p(σ) ∈ {t, f} for any σ. The class of classical predicates in the four-valued logic forms a classical sublogic, where the connectives ∨, ∧,and ¬ substitute for the classical connectives of disjunction, conjunction, and negation,
respectively, and implications ⊃ and → substitute for the material implication. We may
resort to the standard classical logical reasoning in this sublogic.
Let us ﬁrst examine some basic reﬁnement laws. From the distributivity of logical connectives, we can derive several distribution laws for demonic choice. The sequencing operator admits the left distribution law, i.e., (S1 ⊗ S2 ); T = (S1 ; T ) ⊗ (S2 ; T ).
(The right distribution law does not hold in general, though.) The exception handlingstatement also admits a distribution law try S1 ⊗ S2 catch T = (try S1 catch T ) ⊗(try S2 catch T ).

By the interlaced property of logical connectives, all the statements introduced in
the previous section are monotonic with respect to reﬁnement of its substatements. For
instance, S1 ⊗ T1 v S2 ⊗ T2 holds if S1 v S2 and T1 v T2 .
4.1

Reﬁnement of conditional controls

The statement skip and the three conditional control statements are ordered by v as
below.
© ª£ ¤© ª ­ ® £ ¤p v skip v p(4.1)
p v p v p
(4.2)
Further, the assertion (resp. the assumption) is monotonic (resp. anti-monotonic)
with respect to the ≤t order over guard predicates. That is, if p→q is valid (or equivalently, p |= q), we have:© ª © ª£ ¤ £ ¤
p v q
(4.3)
q v p
(4.4)
In contrast, the conditional exit has no such particular (anti-)monotonicity property.
Provided that p→q is valid, we have:© ª © ª© ª © ª£ ¤ © ª­ ®
p = p ; q = p ; q = p ; q(4.5)£ ¤ £ ¤© ª £ ¤£ ¤ £ ¤­ ®
p = p ; q = p ; q = p ; q(4.6)­ ® ­ ®© ª ­ ®£ ¤ ­ ®­ ®
p = p ; q = p ; q = p ; q(4.7)
The following laws indicate that successive conditional control statements of thesame kind can be substituted with a single control statement which combines the guard
formulas in the original statements by either ∧, ~∧, or ∧w .
© ª© ª © ª© ª ©
ª ©
ª ©
ª
p ; q = q ; p = p ∧ q = p~∧q = p ∧w q
(4.8)
£ ¤£ ¤ £ ¤£ ¤ £¤ £¤ £ w ¤
p ; q = q ; p = p ∧ q = p~∧q = p ∧ q(4.9)­ ®­ ® ­ ®­ ® ­® ­® ­ w ®
p ; q = q ; p = p ∧ q = p~∧q = p ∧ q(4.10)
Combining the laws (4.5) through (4.10), we can propagate a copy of a conditional
control statement£ ¤ ©pastª ­one® or£ more¤ © successiveª ­ ® £ ¤ control statements (of possibly different
kinds), e.g., p ; q ; r = p ; q ; r ; p .
The disjunction in the guard of an assertion or an assumption can be substituted
with an appropriate non-deterministic choice.
©
ª © ª © ª£¤ £ ¤ £ ¤p∨q = p ⊕ q(4.11)
p∨q = p ⊗ q(4.12)
From the fact that exactly one of the formulas p and p ⊃ ⊥ can have a designatedtruth value at once, we obtain the following laws.
£ ¤ £
¤
­ ®­
®
p ⊗ p ⊃ ⊥ = skip
(4.13)
p ; p ⊃ ⊥ = exit
(4.15)£ ¤£¤p ; p ⊃ ⊥ = magic(4.14)

­®
Recall that we have used p ∨ ¬p for testing partiality of the predicate p in thedeﬁnition of conditional branch statement in Section 3.2. We will later make use of thefollowing rules in order to exploit the implicit control structure indicated by sequential
and weak Kleene connectives occurring in the test predicate.
­
® ­
®­
®
(p~∧q) ∨ ¬(p~∧q) = p ∨ ¬p ; ¬p ∨ q ∨ ¬q
(4.16)
­
® ­
®­
®
~
~
(p∨q) ∨ ¬(p∨q) = p ∨ ¬p ; p ∨ q ∨ ¬q
(4.17)
­
® ­
® ­
®­
®
w
w
w
w
(p ∧ q) ∨ ¬(p ∧ q) = (p ∨ q) ∨ ¬(p ∨ q) = p ∨ ¬p ; q ∨ ¬q
(4.18)
When the predicate p is classical, the following laws hold.
©
ª © ª
£
¤ £ ¤
­
®
p ⊃ ⊥ = ¬p (4.19)
p ⊃ ⊥ = ¬p (4.20)
p ∨ ¬p = skip (4.21)
4.2

Reﬁnement of exceptions

The following reﬁnement laws hold for exception statements.
­ ®
exit; S = exit (4.22)
try S; p catch skip = try S catch skip (4.23)
An interesting subclass of PTran is the one that never raise exceptions. We would
say that a transformer S never raises exceptions under any program context, if ψn =
ψ0n holds whenever hψn , ϕe i = S(hϕn , ϕe i) and hψ0n , ϕ0e i = S(hϕn , ϕ0e i). This is formallyspeciﬁed in terms of four-valued logic as follows.
Deﬁnition 4.1. A predicate transformer S ∈ PTran is called non-exceptional, if S(ϕ) =S(ϕ0 ) holds whenever f ⊕ ϕ = f ⊕ ϕ0 .
­ ®It is easy to verify that all the statements introduced in Section 3, except for exit andp , are non-exceptional if so are their substatements.
For any non-exceptional statement S, the following laws hold.
try S catch T = S

5(4.24)

try S; exit catch T = S; T

(4.25)

Examples of Program Transformation by Stepwise Reﬁnement

We will apply the reﬁnement laws developed in the previous section to transformationof programs that involve exceptions and partial predicates.
5.1 Translating conjunctions and disjunctions into explicit controls
Programs often contain implicit controls by partial predicates. For example, a single
conditional statement if p~∧q then S else T contains several implicit information forcontrol: The predicate p~∧q evaluates from left to right; As soon as p evaluates to f, theelse clause is selected; exception is raised as soon as p evaluates to ⊥; q is examined
only if p evaluates to t.

We justify this operational intuition via reﬁnement by showing that the above conditional statement is equivalent to the nested conditional statement if p then (if q then S
else T ) else T . Let us ﬁrst give a few subsidiary reﬁnement laws.
£
¤ £
¤ £
¤ £
¤
p~∧q ⊃ ⊥ = p ∧ q ⊃ ⊥ = p ⊃ ⊥ ⊗ q ⊃ ⊥ .
(5.1)
£ ¤­
® £ ¤­ ®
p ; ¬p ∨ q = p ; q
if p is consistent (5.2)
­
®£
¤ ­
®£
¤­
®
p ∨ ¬p ; p ⊃ ⊥ = p ∨ ¬p ; p ⊃ ⊥ ; ¬p ∨ q ∨ ¬q
if p is consistent (5.3)
Then we can carry out the following derivation, provided p is consistent.
­
® ¡£
¤
£
¤ ¢
if p~∧q then S else T = (p~∧q) ∨ ¬(p~∧q) ; p~∧q ; S ⊗ p~∧q ⊃ ⊥ ; T­®­® ¡£ ¤ £ ¤
£
¤
£
¤ ¢
= p ∨ ¬p ; ¬p ∨ q ∨ ¬q ; p ; q ; S ⊗ p ⊃ ⊥ ; T ⊗ q ⊃ ⊥ ; T )— by (4.16), (4.9), (5.1), and distributivity­®£ ¤­® ¡£ ¤ £ ¤
£
¤
£
¤ ¢
= p ∨ ¬p ; p ; ¬p ∨ q ∨ ¬q ; p ; q ; S ⊗ p ⊃ ⊥ ; T ⊗ q ⊃ ⊥ ; T­®£¤­® ¡£ ¤ £ ¤
£
¤
£
¤ ¢
⊗ p ∨ ¬p ; p ⊃ ⊥ ; ¬p ∨ q ∨ ¬q ; p ; q ; S ⊗ p ⊃ ⊥ ; T ⊗ q ⊃ ⊥ ; T— by (4.13) and distributivity­® ³£ ¤ ­® ¡£ ¤
£
¤ ¢ £
¤
£
¤£
¤ ´
= p ∨ ¬p ; p ; q ∨ ¬q ; q ; S ⊗ q ⊃ ⊥ ; T ⊗ p ⊃ ⊥ ; T ⊗ p ⊃ ⊥ ; q ⊃ ⊥ ; T— by (5.2), (5.3), (4.6), (4.7), (4.9), (4.10), (4.14), and distributivity® ³£ ¤ ­® ¡£ ¤£¤ ¢ £¤ ´= p ∨ ¬p ; p ; q ∨ ¬q ; q ; S ⊗ q ⊃ ⊥ ; T ⊗ p ⊃ ⊥ ; T— by (4.9), (4.4)­= if p then (if q then S else T ) else T.
We can also derive a law for the sequential disjunction:
if p~∨q then S else T = if p then S else (if q then S else T ),where p is consistent. For the weak Kleene connectives, we have similar laws:­®
if p ∧w q then S else T = if p then (if q then S else T ) else q ∨ ¬q ; T and­®
if p ∨w q then S else T = if p then q ∨ ¬q ; S else (if q then S else T ),where p need not be consistent.
5.2 Reﬁning exception handlingLet us apply our reﬁnement laws to a larger program. In the development, we will
make use of the technique that propagates context information via the assertion statement [LvW97, Gro00]. Below we list several non-trivial laws for propagating context
information.
© ª©
ªp ; X := e v X := e; ∃v.(p[X\v] ∧ X = e[X\v])(5.4)© ª£ ¤ £ ¤©
ªp ; q v q ; p∧q(5.5)© ª­ ® ­ ®©
ªp ; q v q ; p∧q
(5.6)

© ª
©
ª
©
ª
p ; if q then S else T v if q then ( p ∧ q ; S) else ( p ∧ (q ⊃ ⊥) ; T ) (5.7)
© ª
© ª
©
ª
if q then (S; p ) else (T ; q ) v (if q then S else T ); p ∨ q
(5.8)
© ª
© ª
p ; try S catch T v try p ; S catch T
(5.9)
© ª
© ª
©
ª
try S; p catch (T ; q ) v (try S catch T ); p ∨ q ;(5.10)Let us consider the following program S0 that implements a numerical algorithm.
S0 , X := N; try repeat Y := X; X := (Y ×Y + N) ÷ (2 ×Y ) until X ≥ Y catch skip.
√
This program computes the integral value of N for non-negative integer N, based on
the Newton-Raphson method [PTVF07], and assigns the answer to the variable Y . In
the repeat · · · until loop, the integer division operator ÷ may raise an exception due
to division-by-zero, in which case, however, the exception is caught and the execution
normally terminates with a correct answer.
Since PTran is a bounded complete lattice, each loop statement is speciﬁed by theleast ﬁxpoint µ.F of a function F ∈ PTran→PTran that is monotonic w.r.t. reﬁnement
order v [BvW98]. The loop statement in S0 is given by the least ﬁxpoint of the function:

F (T ) , Y := X; X := (Y ×Y + N) ÷ (2 ×Y ); if X ≥ Y then skip else T.
In order to express the partial assignment X := (Y × Y + N) ÷ (2 × Y ), which may
raise
exception
due to division-by-zero, we interpret it by the compound statement­®
¬(Y = 0) ; X := (Y ×Y + N) ÷0 (2 ×Y ), where ÷0 is a total extension of ÷ such thatdivision by zero yields a ﬁxed constant value (say, 0) instead of being undeﬁned.
In the following derivation, we reﬁne the original program S0 , with the assumption
N ≥ 0, into a program that makes no uses of exceptional statements.
©
ª©
ªN ≥ 0 ; S0 v X := N; X = N ∧ N ≥ 0 ; try µ.F catch skip
— by (5.4)¡£¤©
ª
v X := N; (try ¬(X = 0) ; 0 < X ≤ N ; µ.F catch skip)⊗£¤©
ª¢(try ¬(X = 0) ⊃ ⊥ ; ¬(X = 0) ⊃ ⊥ ; µ.F catch skip)— by (5.9), (4.13), (4.3), (4.1), (4.6), and distributivity.
The left substatement of the demonic choice is reﬁned as follows. (We defer proofsof some lemmas to Appendix. Lemma B.1 indicates that 0 < X ≤ N is a loop invariant
and lemma B.2 says that the ﬁxpoint operator on PTran preserves non-exceptionality.)£¤©
ªtry ¬(X = 0) ; 0 < X ≤ N ; µ.F catch skip£¤©
ªv try ¬(X = 0) ; repeat 0 < X ≤ N ;Y := X; X := (Y ×Y + N) ÷0 (2 ×Y )until X ≥ Y catch skip
— by lemma B.1£¤©
ª= ¬(X = 0) ; repeat 0 < X ≤ N ;Y := X; X := (Y ×Y + N) ÷0 (2 ×Y )until X ≥ Y catch skip

— by (4.24) and non-exceptionality
from
£
¤
©
ª­
® lemma B.2= ¬(X = 0) ; repeat Y := X; ¬(Y = 0) ; ¬(Y = 0) ; X := (Y ×Y + N) ÷0 (2 ×Y )until X ≥ Y— by (5.4), (4.3), and (4.5)£¤= ¬(X = 0) ; repeat Y := X; X := (Y ×Y + N) ÷ (2 ×Y ) until X ≥ Y — by (4.1)

For the other substatement of the choice, we derive:£¤©
ªtry ¬(X = 0) ⊃ ⊥ ; ¬(X = 0) ⊃ ⊥ ; µ.F catch skip
¡£
¤
©
ª­
®
v try ¬(X = 0) ⊃ ⊥ ;Y := X; ¬(Y = 0) ⊃ ⊥ ; ¬(Y = 0) ;¢X := (Y ×Y + N) ÷0 (2 ×Y ); if X ≥ Y then skip else µ.F catch skip
— ﬁxpoint; by (5.4)£¤©
ª= try ¬(X = 0) ⊃ ⊥ ;Y := X; ¬(Y = 0) ⊃ ⊥ ; exit catch skip£¤v ¬(X = 0) ⊃ ⊥ ;Y := X

— by (4.6), (4.10), and (4.15)— by (4.25) and (4.1).

Therefore the derivation ends up with:
­
® £
¤
£
¤
S0 v X := N; ¬(X = 0) ∨ ¬¬(X = 0) ; ( ¬(X = 0) ; µ.F ⊗ ¬(X = 0) ⊃ ⊥ ;Y := X)— by (4.21)= X := N; if ¬(X = 0) then repeat Y := X; X := (Y ×Y + N) ÷ (2 ×Y ) until X ≥ Yelse Y := X.

6

Conclusion and Future Work

We proposed a reﬁnement calculus for reﬁning exceptions in programs. In order tomodel the normal termination as well as the exceptional termination in a single uniﬁed
platform, we developed a four-valued predicate transformer semantics, which is basedon Arieli and Avron’s four-valued logic [AA96]. The programming constructs for raising and catching exceptions can be concisely expressed by the formulas of four-valued
logic in this framework. In particular, we allow partial predicates in the conditional control statements in order to model exceptions that are raised implicitly when the predicate
in a conditional statement is undeﬁned. The four-valued logic provides a fruitful ﬁeld
for justifying reﬁnement of programs that involve both explicit and implicit controls by
exceptions.
This paper, with a few deviations, dealt with concrete program statements suchas assignment, (conditional) exit, etc. Future research will concern abstract statements
such as non-deterministic (possibly partial) assignment and general speciﬁcation statement (which allows the uses of partial pre- and post-conditions) and also the methodology for deriving concrete programs from these abstract statements.
Acknowledgment I thank anonymous reviewers for their suggestions and comments.
This work was supported by JSPS KAKENHI(20500011).

References[AA96]

Ofer Arieli and Arnon Avron. Reasoning with logical bilattices. Journal of Logic,
Language, and Information, 5(1):25–63, 1996.

[AA98][Bel77][BK06][BvW98][Dij76][Fit94][Gin88][Gro00][Häh05][HJ00][JM94][Jon86][KM95][LvW97][MB99][Mor94][Owe93][PTVF07][Wat02]Ofer Arieli and Arnon Avron. The value of four values. Artiﬁcial Intelligence,
102(1):97–141, 1998.
N. D. Belnap. A useful four-valued logic. In G. Epstein and J. M. Dunn, editors,
Modern Uses of Multiple-Valued Logic, pages 7–37. Reidel Publishing Company,
1977.
Viviana Bono and Manfred Kerber. Extending Hoare calculus to deal with crash.
Technical Report CSR-06-08, School of Computer Science, The University of Birmingham, 2006.
Ralph-Johan Back and Joakim von Wright. Reﬁnement Calculus: A Systematic Introduction. Springer-Verlag, 1998. Graduate Texts in Computer Science.
Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.
Melvin Fitting. Kleene’s three-valued logics and their children. Fundamenta Informaticae, 20(1/2/3):113–131, 1994.
Matthew L. Ginsberg. Multivalued logics: A uniform approach to reasoning in artiﬁcial intelligence. Computational Intelligence, 4:265–316, 1988.
Lindsay John Groves. Evolutionary Software Development in the Reﬁnement Calculus. PhD thesis, Victoria University of Wellington, 2000.
Reiner Hähnle. Many-valued logic, partiality, and abstraction in formal speciﬁcation
languages. Logic Journal of the IGPL, 13(4):415–433, 2005.
Marieke Huisman and Bart Jacobs. Java program veriﬁcation via a Hoare logic withabrupt termination. In Fundamental Approaches to Software Engineering (FASE
2000), volume 1783 of LNCS, pages 284–303, 2000.
Cliff B. Jones and C. A. Middelburg. A typed logic of partial functions reconstructedclassically. Acta Informatica, 31(5):399–430, 1994.
Cliff B. Jones. Systematic Software Development Using VDM. Prentice-Hall International Series in Computer Science. Prentice-Hall International, 1986.
Steve King and Carroll Morgan. Exits in the reﬁnement calculus. Formal Aspects ofComputing, 7(1):54–76, 1995.
Linas Laibinis and Joakim von Wright. Context handling in the reﬁnement calculus
framework. Technical Report 118, TUCS Technical Report, 1997.
Joseph M. Morris and Alexander Bunkenburg. E3: A logic for reasoning equationally in the presence of partiality. Science of Computer Programming, 34(2):141–158,
1999.
Carroll Morgan. Programming from speciﬁcations. Prentice-Hall International Series in Computer Science. Prentice-Hall International, 2nd edition, 1994.
Olaf Owe. Partial logics reconsidered: A conservative approach. Formal Aspects ofComputing, 5(3):208–223, 1993.
William H. Press, Saul A. Teukolsky, William T. Vetterling, and Brian P. Flannery.
Numerical Recipes: The Art of Scientiﬁc Computing. Cambridge University Press,
3rd edition, 2007.
Geoffrey Watson. Reﬁning exceptions using King and Morgan’s exit construct.
In 9th Asia-Paciﬁc Software Engineering Conference (APSEC 2002), pages 43–51.
IEEE Computer Society, 2002.

Appendix
A

Proving Reﬁnement Laws in Four-Valued Logic

As we have seen in Section 3.1, a reﬁnement relation S v T can be veriﬁed either byshowing the validity of S(ϕ)→T (ϕ) or by deriving the sequent of the form S(ϕ) ` T (ϕ)
by a formal proof. The set of inference rules of Arieli and Avron’s four-valued logic[AA96] is given in Figure 3 for reference purpose.
The former method can be applied to most of the reﬁnement laws given in this paper,
since they are propositional (i.e., the formula S(ϕ)→T (ϕ) is quantiﬁer-free). The taskof checking the validity for propositional formulas can be mechanized.
The latter method can be used for justifying reﬁnement relations
more© human© ªin©a ªªunderstandable way. For example, the following derivation proves p ; q v p ∧ q .
(The proof of the other direction of reﬁnement is similar.)
1. p, ¬>, q, ¬>, ϕ ` p
2. p, ¬>, q, ¬>, ϕ ` q
3. p, ¬>, q, ¬>, ϕ ` p ∧ q
4. p, ¬>, q, ¬>, ϕ ` ¬>5. p, ¬>, q, ¬>, ϕ ` ¬(p ∧ q ⊃ >)6. ¬(p ⊃ >), ¬(q ⊃ >), ϕ ` ¬(p ∧ q ⊃ >)7. ¬(p ⊃ >), ¬(q ⊃ >), ϕ ` ϕ
8. ¬(p ⊃ >), ¬(q ⊃ >), ϕ ` ¬(p ∧ q ⊃ >) ⊗ ϕ
9. ¬(p ⊃ >) ⊗ ¬(q ⊃ >) ⊗ ϕ ` ¬(p ∧ q ⊃ >) ⊗ ϕ

Initial sequent
Initial sequent
1, 2, [` ∧]Initial sequent3, 4, [` ¬ ⊃]5, [¬ ⊃`]
Initial sequent
6, 7, [` ⊗]8, [⊗ `]In the above, the derivation is shown in a linear format: Each line contains a sequentand indicates the set of premises and the inference rule that are used for deriving thesequent.
We may simplify the veriﬁcation task for a reﬁnement relation that is accompaniedwith a side condition by appealing to the logical equivalence. (Recall that the logical equivalence in four-valued logic is a congruence.) For example,
let us show the¡law (4.24).
Suppose S is non-exceptional. Then it holds that S f ⊕ ((f ⊕ ϕ) ⊗ ¬(f ⊕¢T (ϕ)) = S(ϕ), because we have:¡ ¡¢f ⊕ f ⊕ (f ⊕ ϕ) ⊗ ¬(f ⊕ T (ϕ))= (f ⊕ ϕ) ⊗ ¬(t ⊕ f ⊕ T (ϕ))— distributivity, De Morgan= f⊕ϕ— by t ⊕ f = >.

Hence the following equational reasoning proves the law.
¡¡¢¢f ⊕ S (f ⊕ ϕ) ⊗ ¬(f ⊕ T (ϕ)) ⊗ (t ⊕ ϕ)
= (f ⊕ S(ϕ)) ⊗ (t ⊕ ϕ)
= (f ⊕ S(ϕ)) ⊗ (t ⊕ S(ϕ))— by the above equation— S is exception stable= S(ϕ)— distributivity.

Γ, p, q ` ∆Γ, p ∧ q ` ∆Γ, ¬p ` ∆ Γ, ¬q ` ∆[¬∧ `]Γ, ¬(p ∧ q) ` ∆Γ, p ` ∆ Γ, q ` ∆[∨ `]Γ, p ∨ q ` ∆Γ, ¬p, ¬q ` ∆[¬∨ `]Γ, ¬(p ∨ q) ` ∆Γ, p, q ` ∆[⊗ `]Γ, p ⊗ q ` ∆Γ, ¬p, ¬q ` ∆[¬⊗ `]Γ, ¬(p ⊗ q) ` ∆Γ, p ` ∆Γ, q ` ∆[⊕ `]Γ, p ⊕ q ` ∆Γ, ¬p ` ∆Γ, ¬q ` ∆[¬⊕ `]Γ, ¬(p ⊕ q) ` ∆Γ, p ` ∆[¬¬ `]Γ, ¬¬p ` ∆Γ ` p, ∆ Γ, q ` ∆[⊃`]Γ, p ⊃ q ` ∆Γ, p, ¬q ` ∆[¬ ⊃`]Γ, ¬(p ⊃ q) ` ∆Γ, p(e) ` ∆[∀ `]Γ, ∀v.p(v) ` ∆Γ, ¬p(u) ` ∆[¬∀ `]Γ, ¬∀v.p(v) ` ∆Γ, p(u) ` ∆[∃ `]Γ, ∃v.p(v) ` ∆Γ, ¬p(e) ` ∆[¬∃ `]Γ, ¬∃v.p(v) ` ∆[∧ `][¬t `][f `]Γ, ¬t ` ∆Γ, f ` ∆[⊥ `][¬⊥ `]Γ, ⊥ ` ∆Γ, ¬⊥ ` ∆

Γ ` p, ∆Γ ` q, ∆Γ ` p ∧ q, ∆Γ ` ¬p, ¬q, ∆[` ¬∧]Γ ` ¬(p ∧ q), ∆Γ ` p, q, ∆[` ∨]
Γ ` p ∨ q, ∆Γ ` ¬p, ∆ Γ ` ¬q, ∆[` ¬∨]Γ ` ¬(p ∨ q), ∆Γ ` p, ∆ Γ ` q, ∆[` ⊗]
Γ ` p ⊗ q, ∆Γ ` ¬p, ∆Γ ` ¬q, ∆[` ¬⊗]Γ ` ¬(p ⊗ q), ∆Γ ` p, q, ∆[` ⊕]
Γ ` p ⊕ q, ∆Γ ` ¬p, ¬q, ∆[` ¬⊕]Γ ` ¬(p ⊕ q), ∆Γ ` p, ∆[` ¬¬]Γ ` ¬¬p, ∆Γ, p ` q, ∆[`⊃]Γ ` p ⊃ q, ∆Γ ` p, ∆Γ ` ¬q, ∆[` ¬ ⊃]Γ ` ¬(p ⊃ q), ∆Γ ` p(u), ∆[` ∀]Γ ` ∀v.p(v), ∆Γ ` ¬p(e)[` ¬∀]Γ ` ¬∀v.p(v), ∆Γ ` p(e), ∆[` ∃]Γ ` ∃v.p(v), ∆Γ ` ¬p(u)[` ¬∃]Γ ` ¬∃v.p(v), ∆
[` ∧]

[` t]

Γ ` t, ∆[` ¬f][` >][` ¬>]Γ ` ¬f, ∆Γ ` >, ∆Γ ` ¬>, ∆Fig. 3. The inference rules [AA96]

When quantiﬁers are involved in the formula, we need to resort to a formal proof.
For example, the law (5.4) in Section 5.2© ª©
ªp ; X := e v X := e; ∃v.(p[X\v] ∧ X = e[X\v])

is formally proved as below, where we write p0 for ¬(∃v.(p[X\v] ∧ X = e[X\v] ⊃ >)and indicate the use of equality axiom Γ ` e = e, ∆ by [Equal].
1. p, ¬> ` p
Initial sequent
2. p, ¬> ` e = e
Axiom [Equal]
3. p, ¬> ` p[X\X] ∧ e = e[X\X]
1, 2, rule [` ∧]4. p, ¬> ` ∃v.(p[X\v] ∧ e = e[X\v])
3, rule [` ∃]5. p, ¬> ` ¬>Initial sequent
6. p, ¬> ` ¬(∃v.(p[X\v] ∧ e = e[X\v]) ⊃ >)4, 5, rule [` ¬ ⊃]7. ¬(p ⊃ >) ` ¬(∃v.(p[X\v] ∧ e = e[X\v]) ⊃ >)6, rule [¬ ⊃`]8. ¬(p ⊃ >), ϕ[X\e] ` ¬(∃v.(p[X\v] ∧ e = e[X\v]) ⊃ >)7, weakening
9. ¬(p ⊃ >), ϕ[X\e] ` ϕ[X\e]Initial sequent
10. ¬(p ⊃ >), ϕ[X\e] ` ¬(∃v.(p[X\v] ∧ e = e[X\v]) ⊃ >) ⊗ ϕ[X\e]8, 9, rule [` ⊗]11. ¬(p ⊃ >), f ` (p0 ⊗ ϕ)[X\e]Axiom [f `]12. ¬(p ⊃ >), f ⊕ ϕ[X\e] ` (p0 ⊗ ϕ)[X\e]10, 11, rule [⊕ `]13. ¬(p ⊃ >), f ⊕ ϕ[X\e], t ⊕ ϕ ` f, (p0 ⊗ ϕ)[X\e]12, weakening
14. ¬(p ⊃ >), f ⊕ ϕ[X\e], t ⊕ ϕ ` f ⊕ (p0 ⊗ ϕ)[X\e]13, rule [` ⊕]15. ¬(p ⊃ >), f ⊕ ϕ[X\e], t ⊕ ϕ ` t, (p0 ⊗ ϕ)
Axiom [` t]
16. ¬(p ⊃ >), f ⊕ ϕ[X\e], t ⊕ ϕ ` t¡⊕ (p0 ⊗ ϕ)15,
rule [` ⊕]¢ ¡¢17. ¬(p ⊃ >), f ⊕ ϕ[X\e], t ⊕ ϕ ` f ⊕ (p0¡⊗ ϕ)[X\e] ⊗ t ⊕¢(p0¡⊗ ϕ)
14,
16,
rule [` ⊗]¢18. ¬(p ⊃ >) ⊗ (f ⊕ ϕ[X\e]) ⊗ (t ⊕ ϕ) ` f ⊕ (p0 ⊗ ϕ)[X\e] ⊗ t ⊕ (p0 ⊗ ϕ) 17, rule [⊗ `]B

Supplementary Laws for the Development in Section 5.2

Lemma B.1.
©
ª
0 < X ≤ N ; repeat Y := X; X := (Y ×Y + N) ÷ (2 ×Y ) until X ≥ Y©
ªv repeat 0 < X ≤ N ;Y := X; X := (Y ×Y + N) ÷0 (2 ×Y ) until X ≥ Y
Proof. Let us deﬁne F as in Section 5.2 and F 0 as follows.
©
ª
F 0 (T ) , 0 < X ≤ N ;Y := X; X := (Y ×Y + N) ÷0 (2 ×Y ); if X ≥ Y then skip else T.
©
ª
It is enough to show by transﬁnite induction that 0 < X ≤ N ; F α (abort) v µ.F 0
for any ordinal α.
In case α being a non-limit ordinal, suppose α = β + 1 for some ordinal β.
©
ª
0 < X ≤ N ; F β+1 (abort)©
ª= 0 < X ≤ N ;Y := X; X := (Y ×Y + N) ÷ (2 ×Y ); if X ≥ Y then skip else F β (abort)
©
ª
©
ª­
®
v 0 < X ≤ N ;Y := X; 0 < Y ≤ N ∧Y = X ; ¬(Y = 0) ; X := (Y ×Y + N) ÷0 (2 ×Y );if X ≥ Y then skip else F β (abort)— by (5.4) and (4.3)

©
ª
©
ª
= 0 < X ≤ N ;Y := X; 0 < Y ≤ N ∧Y = X ; X := (Y ×Y + N) ÷0 (2 ×Y );if X ≥ Y then skip else F β (abort) — by (4.5), since 0 < Y ≤ N→¬(Y = 0)ªv 0 < X ≤ N ;Y := X; X := (Y ×Y + N) ÷0 (2 ×Y );©
ª
if X ≥ Y then 0 < Y ≤ N ∧ X = (Y ×Y + N) ÷0 (2 ×Y ) ; skip©
ªelse 0 < Y ≤ N ∧ X = (Y ×Y + N) ÷0 (2 ×Y ) ; F β (abort)©

— by (5.4), (5.7), and (4.3)ª
v 0 < X ≤ N ;Y := X; ¬(Y = 0) ; X := (Y ×Y + N) ÷0 (2 ×Y );©
ª
if X ≥ Y then skip else 0 < X ≤ N ; F β (abort)©

ª©

— by (4.1) and (4.3) with an elementary number theoretical argumentªv 0 < X ≤ N ;Y := X; X := (Y ×Y + N) ÷0 (2 ×Y ); if X ≥ Y then skip else µ.F 0— by induction hypothesis©

= µ.F 0— ﬁxpoint.

If α is a limit ordinal, we have:©
ª©
ªL
0 < X ≤ N ; F α (abort) = 0 < X ≤ N ; β<α F β (abort)¡©
ª¢L= β<α 0 < X ≤ N ; F β (abort) — by distributivityv

Lβ<α µ.F
00— by induction hypothesis= µ.F .

tu
Lemma B.2. Suppose F ∈ PTran→PTran is a monotonic function. Then, µ.F is nonexceptional, if F (S) is so for every non-exceptional S.
Proof. We show F α (abort) is non-exceptional for any ordinal α by transﬁnite induction. Suppose α is a non-limit ordinal such that α = β + 1. By induction hypothesis, F β (abort) is non-exceptional. Therefore F α (abort) = F (F β (abort)) is nonexceptional. In case α is a limit ordinal, by induction hypothesis, F β (abort) is nonexceptional for any
β < α. This implies,Lfor any ϕ and ϕ0 such that f ⊕ ϕ = f ⊕ ϕ0 ,LαF (abort)(ϕ) = β<α F β (abort)(ϕ) = β<α F β (abort)(ϕ0 ) = F α (abort)(ϕ0 ). Therefore the limit F α (abort) is also non-exceptional.