# Generic Hoare Logic for Order-Enriched Effects with Exceptions

Christoph Rauch, Sergey Goncharov, Lutz Schröder

<figure><img src="image_1.png" /></figure>

To cite this version:

Christoph Rauch, Sergey Goncharov, Lutz Schröder. Generic Hoare Logic for Order-Enriched Effects with Exceptions. 23rd International Workshop on Algebraic Development Techniques (WADT), Sep 2016, Gregynog, United Kingdom. pp.208-222, 10.1007/978-3-319-72044-9_14 . hal-01767479

HAL Id: hal-01767479

https://inria.hal.science/hal-01767479

Submitted on 16 Apr 2018

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Generic Hoare Logic for Order-Enriched Effects with Exceptions

Christoph Rauch, Sergey Goncharov, and Lutz Schröder

Friedrich-Alexander-Universität Erlangen-Nürnberg

**Abstract.** In programming semantics, monads are used to provide a generic encapsulation of side-effects. We introduce a monad-based meta-language that extends Moggi's *computational metalanguage* with native exceptions and iteration, interpreted over monads supporting a dcpo structure. We present a Hoare calculus with abnormal postconditions for this metalanguage and prove relative completeness using weakest liberal preconditions, extending earlier work on the exception-free case.

# 1 Introduction

The use of monads as a means of modelling side-effecting computations [10] is well-established in the design and semantics of programming languages. A broad range of computational effects is subsumed under this paradigm, e.g. store, non-determinism, exceptions, probabilities, and alternation.

In addition to just *modelling* side-effects, a matter of interest is how to *reason* generically about properties of side-effecting programs, one of the most important properties being functional correctness. Goncharov and Schröder [7] have developed a monad-based generic *Hoare calculus*, and proved relative completeness using weakest liberal preconditions. More precisely the calculus is parametrized by the choice of a *predicated monad*, i.e. a monad that supports iteration via a suitable dcpo enrichment of its Kleisli category (the associated category of side-effecting functions), and is moreover equipped with a suitable submonad of *innocent* computations for use in assertions. In fact, the object of truth values is generated from a predicated monad as the type of innocent computations of unit type (pre- and postconditions thus become *affirmative assertions* in the sense of Vickers [20], e.g. semi-decidable).

*Exception monads* $T_E X = T(X + E)$ (with $E$ an object of exceptions and $T$ a predicated base monad) are, in fact, predicated but include an operation that does not fit into the required scheme for basic operations, namely exception catching *catch*: $T A \rightarrow T(A + E)$. The framework covers only operations that are *algebraic* [15], which *catch* is not. We therefore extend the generic Hoare calculus with explicit support for exception handling via *abnormal postconditions* [9], which govern the behaviour of a computation for the case where it terminates with an exception. The calculus thus allows, e.g., for a meaningful specification of exception raising, for which the normal postcondition is just $\perp$. Our main result is that the calculus is, again, relatively complete; we prove this by means of a weakest liberal precondition calculus featuring abnormal postconditions.
*Related Work.* Schröder and Mossakowski [18] present a monad-based Hoare calculus with abnormal postconditions, interpreted over a program semantics where the *base category* of the monad, rather than only the Kleisli category, is enriched over a suitable category of domains; our setting thus allows for more instances, e.g. involving monads on the category of sets. Moreover the semantics of the Hoare logic of [18] differs from ours in that the object of truth values is assumed in the base category rather than extracted from the monad as in our setting. The calculus of [18] is proved sound but a relative completeness proof is currently missing. Relative completeness proofs in *most general formula* style have been given for specific effect combinations found in concrete programming languages with exceptions, namely fragments of Java [13,16] and Eiffel [12]. Our approach to generic weakest preconditions essentially follows our previous work on the exception-free case [7]. In work subsequent to [7], Hasuo [8] provides an alternative categorical analysis of monad-based weakest preconditions, notably relying on similar assumptions to ensure well-behavedness of weakest preconditions (see Remark 11 for a detailed comparison). In this setup, no syntactic Hoare calculus, and a fortiori no relative completeness result, is provided.

## 2 Preliminaries: Monads and Exceptions

A monad $T$ over a category $C$ with class $|C|$ of objects can be described as a Kleisli triple $(T, \eta, -^*)$ in which $T$ is an endomap over $|C|$ (we adopt the general convention to use blackboard characters for monads and the corresponding Roman letters for their functorial parts), $\eta$ – the unit of the monad – is a family of morphisms $(\eta_X : X \to TX)_{X \in |C|}$ and $-^*$ – the Kleisli lifting – is a map sending each $f : X \to TY$ to $f^* : TX \to TY$ so that the monad laws are satisfied:

$$ \eta^* = \mathrm{id}, \qquad f^* \circ \eta = f, \qquad (f^* \circ g)^* = f^* \circ g^* \qquad (1) $$

This is equivalent to the standard definition of a monad in terms of a functor $T$ with unit and multiplication; in particular, $Tf = (\eta f)^*$ for morphisms $f$. One may think of $TX$ as being a type of side-effecting computations delivering results in $X$; examples include non-termination ($TX = X + 1$), non-determinism ($TX = PX$), statefulness (e.g. the *partial state monad* is given by $TX = S \to (S \times X)$ for an object $S$ of states, where $\to$ takes partial function spaces), and exceptions ($TX = X + E$ for an object $E$ of exceptions).

Furthermore, a *strong monad* is a monad $T$ together with a family of morphisms $\tau : X \times TY \to T(X \times Y)$ natural in both $X$ and $Y$ satisfying a set of coherence axioms (cf. e.g. [11]). As originally noted by Moggi, strong monads support a *computational metalanguage* [11], incorporated into Haskell as the *do-notation* [21]: it features an operator *ret*, denoting the unit $\eta$, and the *do-binder*, which from $f : X \to TY$ and $g : X \times Y \to TZ$ builds $\mathrm{do} y \leftarrow f(x); g(x, y)$, in which $y$ is syntactically bound and whose meaning is $g^* \circ \tau \circ \langle \mathrm{id}, f \rangle : X \to TZ$. For a term $p$ in the computational metalanguage, $FV(p)$ denotes the set of free variables of $p$. The monad laws (1) can be rewritten in this style, and then form
part of a complete axiomatization:

$$
\begin{align*}
& \mathbf{do} \ x \leftarrow (\mathbf{do} \ y \leftarrow p; q); r = \mathbf{do} \ y \leftarrow p; x \leftarrow q; r \qquad y \notin \mathbf{FV}(r) \\
& \mathbf{do} \ x \leftarrow \mathbf{ret} \ a; p = p[a/x] \\
& \mathbf{do} \ x \leftarrow p; \mathbf{ret} \ x = p.
\end{align*}
$$

A monad T defines the Kleisli category $C_T$ of T, whose objects are those of C and $\operatorname{Hom}_{C_T}(A, B) = \operatorname{Hom}_C(A, TB)$ with composition defined using the Kleisli lifting of T; that is, morphisms $X \to Y$ in $C_T$ may be thought of side-effecting functions $X \to Y$, with side-effects specified by T.

We fix from now on an object *E* of exceptions and a base monad T on a category *C* which is distributive, i.e. the canonical distributivity morphism *X* × *Y* + *X* × *Z* → *X* × (*Y* + *Z*) is an isomorphism, with inverse called dist, and which has Kleisli exponentials [19,15], i.e. exponentials [2] of the form *TZ*^*. The latter condition means that there is a natural isomorphism λ : *Hom*<sub>*C*</sub>(*X*×*Y*, *TZ*) ∼= *Hom*<sub>*C*</sub>(*X*, *TZ*^*). We furthermore denote pairing and copairing morphisms by angle and square brackets, respectively.

The well-known *exception monad transformer* [4] adds exceptions as an effect to a given monad: the functor

$$
T_E = T(-+E)
$$

is turned into a strong monad $T_E$, called an *exception monad*, by putting

$$
- \eta^{T_E} = \eta^T \circ \mathrm{inl};
$$

$$
- f^* = [f, \eta^T \circ \mathrm{inr}]^* \text{ for } f : A \to T(B + E);
$$

$$
- \tau_{A,B}^{T_E} = T((\mathrm{id} + \pi_2) \circ \mathrm{dist}) \circ \tau_{A,B+E}.
$$

That is, a computation in $T_E$ performs a side effect specified by $\mathcal{T}$ and then either terminates normally or with an exception. The definition of binding in $T_E$ means that in the latter case, subsequent statements have no further effects (e.g. in case $\mathcal{T}$ features statefulness, the state is frozen) other than propagating the exception. On $T_E$, we have operations for raising and catching exceptions (i.e. exposing exceptions raised by a program in the output type),

$$
\text{raise}_X = \eta \operatorname{inr} : E \to T(X + E) = T_E X
$$

$$
\text{catch}_X = T \text{ inl} : T_E X = T(X + E) \to T((X + E) + E) = T_E(X + E).
$$

3 Order-Enrichment and Innocence

As indicated in the introduction, we require a certain amount of infrastructure
in the base monad T to support, on the one hand, loops, and on the other hand,
an internalized assertion language. To this end, we require a complete partial
order on programs, i.e. Kleisli morphisms, of a given type A → TB. We will then
use certain well-behaved programs as logical assertions. Formal definitions are as
follows [7].
**Definition 1 (Order-enriched monad).** The monad $\mathbb{T}$ is *order-enriched* if

- every hom-set $\text{Hom}_C(A, TB)$ carries a bounded-complete and directed-complete partial ordering $\sqsubseteq$ (i.e. joins exist for finite bounded subsets and for directed subsets, and consequently for all bounded subsets),

- for any $h \in \text{Hom}_C(A', A)$ and any $u \in \text{Hom}_C(B, TB')$, the maps

$$f \mapsto f \circ h, \quad f \mapsto u^* \circ f, \quad f \mapsto \tau \circ \langle \text{id}, f \rangle$$

preserve all existing joins (including the empty join $\perp$),

- Kleisli star is Scott-continuous.

The ordering $\sqsubseteq$ is to be thought of as the usual information ordering; in particular, non-termination is below termination. Note that we do not include continuity of copairing in the above definition; in fact this follows from preservation of joins (Lemma 6).

We identify a class of *innocent* computations suitable for use within assertions of the Hoare logic. Intuitively, such a computation may read but should not modify the state, as required already in earlier work on monad-based program logics [17]. Instead of assuming a type of truth values in the base category, we will identify truth with termination, so that truth values are just innocent computations of unit type. Formally, the conditions for innocence are as follows [7].

**Definition 2 (Innocence).** A monad is *commutative* if it satisfies

$$\text{do } x \leftarrow p; y \leftarrow q; \text{ret } \langle x, y \rangle = \text{do } y \leftarrow p; x \leftarrow q; \text{ret } \langle x, y \rangle$$

for all $p, q$, and fresh $x, y$, in the computational metalanguage (Section 2). An order-enriched monad is *innocent* if it is commutative and satisfies *copyability*

$$\text{do } x \leftarrow p; y \leftarrow p; \text{ret } \langle x, y \rangle = \text{do } x \leftarrow p; \text{ret } \langle x, x \rangle$$

(for all $p$ and fresh $x, y$) and *weak discardability*

$$\text{do } x \leftarrow p; \text{ret} \star \sqsubseteq \text{ret} \star. \qquad (2)$$

Notice that the notion of weak discardability uses the ordering of the monad. It allows for non-termination; e.g. if $p = \perp$ is the everywhere diverging program, then the left hand side of (2) is also $\perp$ so that the inequality is satisfied. (Contrastingly, previous approaches [17] used *discardability* $\text{do } x \leftarrow p; \text{ret} \star = \text{ret} \star$, which implies termination.) On the other hand, weakly discardable computations cannot raise exceptions, as these fail to be below $\text{ret} \star$. Intuitively, the only side-effects an innocent computation may exhibit are possible non-termination and read operations on implicit states encapsulated in the base monad.

A key property of innocent monads $\mathbb{P}$ is that they support a logic on the base category, which we will later use as the underlying logic of the assertions of our Hoare calculus. Specifically, $P1$ is a *distributive lattice object in C*, i.e. $\text{Hom}(-, P1)$ factors through distributive lattices, in fact even through *frames* [7],
which are complete lattices in which finite meets distribute over all joins (with morphisms preserving finite meets and all joins). Consequently, P1 supports a form of geometric logic [20]. Notably, finite meets in P1 are given by sequential composition. In case C = Set, P1 is in fact a Heyting algebra, and thus supports full intuitionistic logic.

Computationally relevant monads, e.g. stateful ones, often fail to be innocent but will typically contain a useful innocent submonad. Formally:

**Definition 3 (Predicated monad).** A *predicated monad* $(\mathbb{T}, \mathbb{P})$ consists of an order-enriched monad $\mathbb{T}$ and an innocent order-enriched submonad $\mathbb{P}$ of $\mathbb{T}$ whose inclusion into $\mathbb{T}$ is Scott-continuous.

**Example 4.** In the *nondeterministic state monad* $TX = S \to \mathcal{P}(S \times X)$, a program is weakly discardable iff it (possibly reads but) does not change the state. Such a program is copyable iff it is deterministic; all copyable and weakly discardable programs in $\mathbb{T}$ commute. We thus obtain an innocent submonad $\mathbb{P}$ of $\mathbb{T}$ given by $PX = S \to X$, the *partial reader monad*. Taking $\mathbb{T}$ to be either the partial state monad (Section 2) or the nondeterministic state monad and $\mathbb{P}$ the partial reader monad, we thus obtain a predicated monad $(\mathbb{T}, \mathbb{P})$.

**Lemma 5.** Let $(\mathbb{T}, \mathbb{P})$ be a *predicated monad*. Then the *exception monad* $\mathbb{T}_E$ is also order-enriched, and $(\mathbb{T}_E, \mathbb{P})$ is a *predicated monad*.

From now on, we fix a *predicated monad* $(\mathbb{T}, \mathbb{P})$.

# 4 A Computational Metalanguage

We proceed to define the syntax of a monad-based metalanguage that extends Moggi's computational metalanguage (Section 2) with native support for iteration and innocence. We introduce a system of *value types A* and *computation types C* by the grammar

$$A ::= W \mid 1 \mid A \times A \mid A + A \quad C ::= A \mid \Omega \mid T_E A \mid PA \mid A \to \Omega$$

with W ranging over a set $\mathcal{W}$ of basic types (denoting objects of $C$). While the type constructor $T_E$ represents side-effecting computations possibly raising exceptions in $E$, the type constructor $P$ represents innocent computations. The type $\Omega$ of truth values is just a synonym for P1. Additionally, we fix a signature $\Sigma$ of typed function symbols $f: A \to C$.

The term language is defined by means of the set of typing rules for terms in context shown in Figure 1; contexts $\Gamma$ consist of assignments $x: A$ of value types $A$ to variables $x$. We have the usual term formation rules for products, coproducts, sequential composition of computations, application of functions from the signature $\Sigma$, and most notably for exception raising and handling. Additionally, we incorporate rules for innocent computations saying essentially that $P$ is a submonad of $T_E$, i.e. closed under unit and binding, and each $PA$ has a least element $\perp$ ($\perp$ could of course be defined as a nonterminating loop but
for our purposes it is technically more convenient to make it a first-class citizen). Our loop construct is tuned to sum types:

$$ \text{init } x \leftarrow p \text{ intercase } c \text{ of } \text{inl } y \mapsto q; \text{inr } z \mapsto r $$

initializes the loop variable *x* with the result of *p* and then proceeds to execute *q* repeatedly, binding the result to *x*, as long as *c*: *B* + *C* remains in the left hand summand. Once *c* ends up in the right hand summand, the loop terminates and *r* is executed once, with the result bound to *x*. Note that the construct at hand allows passing *values* through the loop; boolean loop conditions as in standard while loops arise as special cases of our sum-type-based loop conditions, as the type 2 of Booleans is the sum type 1 + 1.

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
\frac{x: A \text{ in } \Gamma}{\Gamma \vdash x: A} & \frac{f: A \to C \in \Sigma}{\Gamma \vdash f(t): C} & \frac{\Gamma \vdash t: A}{\Gamma \vdash \star: 1} & \frac{\Gamma \vdash \perp: PA}{\Gamma \vdash \perp: PA} \\[1.5em]
\frac{\Gamma \vdash t: A \times B}{\Gamma \vdash \pi_1 t: A} & \frac{\Gamma \vdash t: A \times B}{\Gamma \vdash \pi_2 t: B} & \frac{\Gamma \vdash t: A}{\Gamma \vdash \text{inl } t: A+B} & \frac{\Gamma \vdash t: B}{\Gamma \vdash \text{inr } t: A+B} \\[1.5em]
\frac{\Gamma \vdash t: A}{\Gamma \vdash \langle t, u \rangle: A \times B} & \frac{\Gamma \vdash c: A+B}{\Gamma \vdash \text{case } c \text{ of inl } a \mapsto t; \text{inr } b \mapsto u: C} & \frac{\Gamma, a: A \vdash t: C}{\Gamma, b: B \vdash u: C} & \\[1.5em]
\frac{\Gamma \vdash p: MA}{\Gamma \vdash \text{do } x \leftarrow p; q: MB} & M \in \{T_E, P\} & \frac{\Gamma \vdash p: A}{\Gamma \vdash \text{ret } p: PA} & (A \text{ value type}) \\[1.5em]
\frac{\Gamma, x: A \vdash c: B+C}{\Gamma \vdash \text{init } x \leftarrow p \text{ intercase } c \text{ of inl } y \mapsto q; \text{inr } z \mapsto r: T_E A} & \frac{\Gamma \vdash p: T_E A}{\Gamma \vdash \text{raise } e: T_E A} & \frac{\Gamma \vdash p: T_E A}{\Gamma \vdash \text{catch } p: T_E(A+E)} & \\[1.5em]
\frac{\Gamma \vdash p: PA}{\Gamma \vdash p: T_E A} & \frac{\Gamma \vdash e: E}{\Gamma \vdash \text{raise } e: T_E A} & \frac{\Gamma \vdash p: T_E A}{\Gamma \vdash \text{catch } p: T_E(A+E)} &
\end{array}
$$

<caption>**Fig. 1.** Term formation rules for the simple imperative metalanguage with exceptions.</caption>

In addition to the metalanguage of programs, we can now use the fact that $P1 = \Omega$ serves as an object of truth values in geometric logic to develop rules for an assertion language. These rules, given in Figure 2 and understood as extending those of Figure 1, are identical to those for the exception-free case [7], essentially because innocent computations do not raise exceptions. The logic combines a very restricted set of propositional connectives with least and greatest fixpoint constructors over dedicated predicate variables. It is designed to accommodate weakest preconditions, i.e. is strong enough to guarantee relative completeness of the Hoare calculus.
<figure><img src="image_3.png" /><figcaption>Fig. 2. Assertion language.</figcaption></figure>

## 5 Semantics

The types $C$ of our metalanguage are interpreted over the predicated (exception) monad $(\mathbb{T}_E, \mathbb{P})$ as $C$-objects $[[C]]$ in the expected way, given an assignment of $C$-objects $[[W]]$ to basic types $W$, with $+$ and $\times$ interpreted as categorical sum and product, $P$ and $T_E$ as the corresponding object maps of $\mathbb{T}_E$ and $\mathbb{P}$, 1 as the terminal object, and $A \to \Omega$ as the Kleisli exponential ($[[P1]]$$^{[A]}$).

As usual, contexts are then interpreted as the product of the interpretations of the types of their variables, and a term in context $\Gamma \vdash p : C$ as a morphism $[[\Gamma]] \to [[C]]$. The term constructors for product and sum types are interpreted using the structure of $C$ as a distributive category in the usual way, and the interpretation of the term constructors for the monadic structure (ret and do) is as in the computational metalanguage [11], instantiated for the exception monad $\mathbb{T}_E$, respectively its submonad $\mathbb{P}$ for innocent computations; $\Gamma \vdash \bot : PA$ is interpreted as the bottom element of $\text{Hom}([\Gamma], [[PA]])$. The operations catch and raise are interpreted as the corresponding morphisms for $\mathbb{T}_E$ (Section 2); e.g. $[[\Gamma \vdash \text{catch } p : T_E(A + E)]] = \text{catch} \circ [[p]]$.

The interpretation of our coproduct-based loop construct `itcase` follows the treatment of a previous Boolean loop construct [7]. Let $?: A + B \to PA$ be the operator defined by

$$ c? = \text{case } c \text{ of inl } y \mapsto \text{ret } y; \text{ inr } z \mapsto \bot, $$

and let $c \mapsto \bar{c}$ denote the symmetry isomorphism $A + B \to B + A$, i.e. $\bar{c} = \text{case } c \text{ of inl } y \mapsto \text{inr } y; \text{ inr } z \mapsto \text{inl } z$ for $c : A + B$. We adopt the convention to write $c?$ instead of (`do` $c?$; `ret` $\star$) whenever the return type `P1` is expected.

**Lemma 6.** Assume terms $\Gamma, y : A \vdash p : T_E C; \Gamma, z : B \vdash q : T_E C; \text{ and } \Gamma \vdash c : A + B$. Then the join (`do` $y \leftarrow c?$; $p$) $\sqcup$ (`do` $z \leftarrow \bar{c}?$; $q$) exists and equals case c of inl $y \mapsto p; \text{inr } z \mapsto q$.

Consequently, `case` is Scott-continuous in both program arguments. By Kleene's fixpoint theorem, we can thus define an interpretation for the special case
init. $x \leftarrow \text{ret } x$ itercase $c$ of $\text{inl } y \mapsto q$; $\text{inr } z \mapsto r$ as the least fixed point of the map

$$f \mapsto (\text{case } c \text{ of inl } y \mapsto (\text{do } x \leftarrow q; f); \text{inr } z \mapsto r).$$

The full itcase construct is then interpreted as

$$\llbracket \Gamma \vdash \text{init } x \leftarrow p \text{ itercase } c \text{ of inl } y \mapsto q; \text{inr } z \mapsto r : T_E A \rrbracket = \\ \llbracket \Gamma \vdash \text{do } x \leftarrow p; (\text{init } x \leftarrow \text{ret } x \text{ itercase } c \text{ of inl } y \mapsto q; \text{inr } z \mapsto r) : T_E A \rrbracket. \quad (3)$$

*Semantics of assertions.* Contexts $\Gamma$ for assertions may contain propositional variables $X: A \to \Omega$, giving rise to factors ($\llbracket P1 \rrbracket$$^{[A]}$ in the interpretation of $\Gamma$. Assertions $\Gamma \vdash \phi : \Omega$ are then interpreted as morphisms $\llbracket \Gamma \rrbracket \to \llbracket P1 \rrbracket$. Logical conjunction and disjunction are interpreted as meets and joins in $\Omega = P1$, respectively (which exist because $P1$ is a distributive lattice object). For lambda abstraction and evaluation of predicates, we inductively define

$$\frac{\llbracket \Gamma, x : A \vdash t : \Omega \rrbracket = f}{\llbracket \Gamma \vdash \lambda x. t : A \to \Omega \rrbracket = \lambda f} \qquad \frac{\llbracket \Gamma \vdash t : A \rrbracket = f}{\llbracket \Gamma \vdash s(t) : A \to \Omega \rrbracket = g} \qquad \frac{\llbracket \Gamma \vdash s : A \to \Omega \rrbracket = g}{\llbracket \Gamma \vdash t : A \rrbracket = f}$$

where $\epsilon$ is the usual evaluation morphism. Fixpoints $\Gamma \vdash \eta X. \phi$ with $\eta \in \{\mu, \nu\}$ are interpreted using the fact that the hom-sets $\text{Hom}(\llbracket \Gamma \rrbracket \times \llbracket A \rrbracket, \llbracket \Omega \rrbracket)$ are complete lattices. In detail, the interpretation of $\Gamma, X: A \to \Omega \vdash \phi : \Omega$ is a morphism $g: \llbracket \Gamma \rrbracket \times (\llbracket P1 \rrbracket)^{[A]} \to (\llbracket P1 \rrbracket)^{[A]}$. We thus define an endomorphism $F$ on $\text{Hom}(\llbracket \Gamma \rrbracket \times \llbracket A \rrbracket, \llbracket \Omega \rrbracket)$ by taking $F(h)$ to be

$$\llbracket \Gamma \rrbracket \times \llbracket A \rrbracket \xrightarrow{\langle \text{id}, \lambda h \circ \pi_1 \rangle} \llbracket \Gamma \rrbracket \times \llbracket A \rrbracket \times (P1)^{[A]} \xrightarrow{\langle g \circ \langle \pi_1, \pi_3 \rangle, \pi_2 \rangle} (P1)^{[A]} \times \llbracket A \rrbracket \xrightarrow{\epsilon} \llbracket \Omega \rrbracket.$$

We then take $\llbracket \Gamma \vdash \eta X. \phi \rrbracket$ to be $\lambda \eta F$; the required fixpoints exist by the Knaster-Tarski theorem as all assertions are monotone in their variables.

**Definition 7.** A judgment $\Gamma \vdash \phi \sqsubseteq \psi$ is valid over $\mathbb{P}$ if $\llbracket \phi \rrbracket \sqsubseteq \llbracket \psi \rrbracket$.

# 6 Hoare Calculus

In the exception-free case, a semantics of Hoare triples over order-enriched monads [7] is defined by taking $\{\phi\} x \leftarrow p \{\psi\}$ (with $p: T_E A$ and assertions $\phi, \psi$, where $\psi$ may depend on $x: A$) to abbreviate the equation

$$\text{do } \phi; x \leftarrow p; \psi; \text{ret } x = \text{do } \phi; p.$$

As indicated previously, this setup is insufficient for the verification of exception-raising programs; e.g. nothing useful can be said about raise beyond $\{\top\}$ raise $e \{\bot\}$. We thus need an additional postcondition for abnormal termination [9,18]: Intuitively, a *Hoare quadruple*

$$\{\phi\} x \leftarrow p \{\psi \mid \epsilon\}$$
with abnormal postcondition $\varepsilon: E \to \Omega$ says that if $p$ is executed in a prestate satisfying $\phi$ and terminates normally with result $x$, then the poststate and $x$ satisfy the normal postcondition $\psi$, and if $p$ terminates with an exception $e$ then the poststate satisfies $\varepsilon(e)$. Using the previous definition of Hoare triple, we formally interpret $\{\phi\} x \leftarrow p \{\psi \mid \varepsilon\}$ by letting it abbreviate

$$ \{\phi\} y \leftarrow \mathit{catch} p \{\mathit{case} y \mathit{of} \mathit{inl} x \mapsto \psi; \mathit{inr} e \mapsto \varepsilon(e)\}. $$

We write $\mathbb{T}, \mathbb{P} \models \{\phi\} x \leftarrow p \{\psi \mid \varepsilon\}$ if the above equality holds in $(\mathbb{T}, \mathbb{P})$ (under the given interpretation of the basic programs, elided in the notation).

The inference rules for our calculus are shown in Figure 3. The inequalities in (wk) refer to the notion of validity introduced above (Definition 7); inequality $\varepsilon \sqsubseteq \varepsilon'$ of abnormal postconditions is understood pointwise. We assume a set $\Delta$ of valid axioms for basic programs, and then write $\Delta \vdash_P \{\phi\} x \leftarrow p \{\psi \mid \varepsilon\}$ if a Hoare quadruple $\{\phi\} x \leftarrow p \{\psi \mid \varepsilon\}$ is derivable from axioms in $\Delta$ and inequalities of assertions valid over $\mathbb{P}$.

The rules (basic), (ret), (do) and (wk) are derived straightforwardly from the rules for the exception-free case [7]; rule ($\perp$) is clear. We spend some time on discussing the remaining new rules:

**Rules for exceptions** are taken from [18]. The (raise) rule is self-explanatory. The (catch) rule is based on the fact that catch $p: T_E(A + E)$ renormalizes the computation $p$ and returns an exception possibly raised by $p$ in the right-hand summand of the normal result.

**Case rule.** The precondition of a case statement is a disjunction of the preconditions for the two alternatives, with access to the value of the branching condition $c$ within the two summands provided by the $c$? construct introduced in Section 5. Soundness of the rule is proved by Lemma 6.

**Iterated case rule.** The full `itcase` construction, as defined in (3), is actually a sequential composition of two programs. For simplicity, we treat only the special case $p = \mathit{ret} x$ in the Hoare calculus, which we abbreviate as

$$ \mathit{itcase} c \mathit{of} \mathit{inl} a \mapsto q; \mathit{inr} b \mapsto r := \mathit{init} x \leftarrow \mathit{ret} x \mathit{itcase} c \mathit{of} \mathit{inl} a \mapsto q; \mathit{inr} b \mapsto r. $$

In contrast to the case of **while** loops [7], we cannot expect that after the loop, the value of the test term $c$ contains a right injection, as $c$ could be affected by the program $r$, which is executed after the loop terminates. The intuition behind the formulation of the (itcase) rule is the following: The assertion $\psi$ plays the role of the loop invariant. In every iteration, the loop body $q$, which depends on $a$, is executed with the value of $a$ extracted from $c$, and possibly changes the value of $c$. As a postcondition of $q$, we thus require that either the loop continues and the invariant $\psi$ still holds for the next iteration, i.e. `do a \leftarrow c?; \psi` holds, or the loop terminates and the precondition of $r$ holds, with $b$ replaced by the value contained in $c$. As the loop terminates with an execution of $r$, the postcondition of the loop obtained in the conclusion of the rule is then just that of $r$.
<figure><img src="image_4.png" /><figcaption>Fig. 3. Hoare calculus for order-enriched effects with exceptions.</figcaption></figure>

**Theorem 8 (Soundness).** *The Hoare calculus for order-enriched effects with exceptions is sound, i.e.*

$$ \Delta \vdash_P \{\phi\} x \leftarrow p \{\psi\} \quad \text{implies} \quad T_E, P \vdash \{\phi\} x \leftarrow p \{\psi\}. $$

The main idea in Cook's original proof of relative completeness of ordinary Hoare logic is a calculus of weakest liberal preconditions or shorter weakest preconditions [5], that is (adapted to our setting), for every program $p$, postcondition $\psi$ and abnormal postcondition $\varepsilon$, a precondition $wp(x \leftarrow p, \psi | \varepsilon)$ such that

$$ \{wp(x \leftarrow p, \psi | \varepsilon)\} x \leftarrow p \{\psi | \varepsilon\} \qquad (4) $$

is a valid Hoare quadruple and $\phi \sqsubseteq wp(x \leftarrow p, \psi | \varepsilon)$ whenever $\{\phi\} x \leftarrow p \{\psi | \varepsilon\}$. If we can prove that all quadruples (4) are derivable in the calculus then relative completeness follows by soundness and (wk).

Semantically, we construct weakest preconditions in the obvious way by

$$ \mathit{wp}(x \leftarrow p, \psi | \varepsilon) = \mathop{\sqcup}\{\phi \mid \{\phi\} x \leftarrow p \{\psi | \varepsilon\}\} $$

The join exists because every $\mathit{Hom}(X, \Omega)$ is a complete lattice. The definition of a weakest precondition $wp(x \leftarrow p, \psi)$ for $T$ is recovered by taking $E = 0$. By the continuity requirements for order-enriched monads, we have

**Lemma 9.** *For all programs $p$ and postconditions $\psi \mid \varepsilon$, $wp(x \leftarrow p, \psi \mid \varepsilon)$ is a weakest precondition.*
It remains to show that weakest preconditions are definable in our assertion language under the assumption that the weakest preconditions of all signature symbols exist. To this end we give an inductive definition of syntactic weakest preconditions $wp_s(x \leftarrow p, \psi | \varepsilon)$, extending the corresponding calculus for the exception-free case [7], and prove that the definition of $wp_s$ is sound w.r.t. $wp$. This requires a suitable restriction imposed on the underlying predicated monad, which we first recall for the exception-free case:

**Definition 10 (Sequential Compatibility [7]).** We call a predicated monad $(\mathbb{T}, \mathbb{P})$ sequentially compatible if for all programs $p, q$ and assertions $\psi$, we have

$$wp(x \leftarrow (do y \leftarrow p; q), \psi) \sqsubseteq wp(y \leftarrow p, wp(x \leftarrow q, \psi)). \quad (5)$$

**Remark 11.** The inequality converse to (5) holds automatically, and therefore for sequentially compatible predicated monads

$$wp(x \leftarrow (do y \leftarrow p; q), \psi) = wp(y \leftarrow p, wp(x \leftarrow q, \psi)).$$

An equivalent formulation, called the interpolation property, is used by Bloom and Ésik [3]; it can be reformulated in our terms as follows: for every valid Hoare triple $\{\phi\} x \leftarrow (do y \leftarrow p; q) \{\psi\}$ there exists $\xi$ such that $\{\phi\} y \leftarrow p \{\xi\}$ and $\{\xi\} x \leftarrow q \{\psi\}$ (w.l.o.g. we can take $\xi$ to be $wp(x \leftarrow q, \psi)$).

Given $\phi : X \to \Omega$, we can form $\phi^\circ(p) = wp(x \leftarrow p, \phi(x))$, which yields an operator $(-)^\circ : \text{Hom}(X, \Omega) \to \text{Hom}(\text{TX}, \Omega)$. A predicated monad $(\mathbb{T}, \mathbb{P})$ is sequentially compatible iff the right of the following two conditions is satisfied (the left one is satisfied automatically) for all $\phi : Y \to \Omega, f : X \to TY$:

$$\phi^\circ \circ \eta = \phi, \qquad \phi^\circ \circ f^* = (\phi^\circ \circ f)^\circ. \qquad (6)$$

It follows that $(-)^\circ$ is natural in the domain of its argument, for $\phi^\circ \circ (Tf) = \phi^\circ \circ (\eta \circ f)^* = (\phi^\circ \circ \eta \circ f)^\circ = (\phi \circ f)^\circ$, and therefore, by the Yoneda lemma, $(-)^\circ$ is uniquely induced by a map $\square : T\Omega \to \Omega$. The axioms (6) then amount to saying that $(\square, \Omega)$ is a $\mathbb{T}$-algebra. This relates sequential compatibility, introduced in [7], to later work by Hasuo [8] who called such an algebra a *modality*, under the running assumption that $\mathbb{T} = \mathbb{P}$, which we do not assume in general.

The inductive definition of syntactic weakest preconditions is given in Figure 4. Sequential compatibility of $(\mathbb{T}, \mathbb{P})$ generalizes to $(\mathbb{T}_E, \mathbb{P})$:

**Lemma 12.** Given a sequentially compatible monad $(\mathbb{T}, \mathbb{P})$, we have

$$wp(x \leftarrow (do y \leftarrow p; q), \psi | \varepsilon) \sqsubseteq wp(y \leftarrow p, wp(x \leftarrow q, \psi | \varepsilon) | \varepsilon).$$

To understand the definition of $wp_s$ for catch, first note that catch itself never terminates abnormally; by unfolding the definitions of Hoare quadruples and catch, we thus have that $\{\phi\} y \leftarrow \text{catch } p \{\psi | \varepsilon\}$ is equivalent to the Hoare triple $\{\phi\} y \leftarrow \text{catch } p \{\psi\}$. We can now eliminate catch by decomposing $\psi$ into a case
$$ \mathbf{wp}_s(x \leftarrow f(t), \psi | \varepsilon) = \mathbf{wp}(x \leftarrow f(z), \psi | \varepsilon)[t/z] \qquad (7) $$

$$ \mathbf{wp}_s(x \leftarrow \mathrm{ret} t, \psi | \varepsilon) = \psi[t/x] \qquad (8) $$

$$ \mathbf{wp}_s(x \leftarrow \perp, \psi | \varepsilon) = \top \qquad (9) $$

$$ \mathbf{wp}_s(y \leftarrow (\mathbf{do} x \leftarrow p; q), \psi | \varepsilon) = \mathbf{wp}_s(x \leftarrow p, \mathbf{wp}_s(y \leftarrow q, \psi | \varepsilon) | \varepsilon) \qquad (10) $$

$$ \begin{aligned} \mathbf{wp}_s(x \leftarrow (\mathbf{case} c \ \mathbf{of} \ \mathbf{inl} \ a \mapsto q; \ \mathbf{inr} \ b \mapsto r), \psi | \varepsilon) = & \\ & \mathbf{do} \ a \leftarrow c?; \mathbf{wp}_s(x \leftarrow q, \psi | \varepsilon) \lor \mathbf{do} \ a \leftarrow \bar{c}?; \mathbf{wp}_s(x \leftarrow r, \psi | \varepsilon) \end{aligned} \qquad (11) $$

$$ \begin{aligned} \mathbf{wp}_s(x \leftarrow (\mathbf{init} \ x \leftarrow \mathbf{ret} \ x \ \mathbf{itercase} \ c \ \mathbf{of} \ \mathbf{inl} \ a \mapsto q; \ \mathbf{inr} \ b \mapsto r), \psi | \varepsilon) = & \\ & (\nu X. \lambda x. \mathbf{do} \ a \leftarrow c?; \mathbf{wp}_s(x \leftarrow q, X(x) | \varepsilon) \lor \\ & \mathbf{do} \ b \leftarrow \bar{c}?; \mathbf{wp}_s(x \leftarrow r, \psi | \varepsilon))(x) \end{aligned} \qquad (12) $$

$$ \mathbf{wp}_s(x \leftarrow \mathbf{raise} e, \psi | \varepsilon) = \varepsilon(e) \qquad (13) $$

$$ \mathbf{wp}_s(y \leftarrow \mathbf{catch} p, \psi | \varepsilon) = \mathbf{wp}_s(x \leftarrow p, \psi[\mathbf{inl} x/y] | \lambda e. \psi[\mathbf{inr} e/y]) \qquad (14) $$

<caption>**Fig. 4.** Syntactic definition of weakest preconditions.</caption>

construction and applying the definition of Hoare quadruple:

$$ \begin{aligned} \{\phi\} & y \leftarrow \mathbf{catch} p \{\psi\} \\ & \Leftrightarrow \{\phi\} y \leftarrow \mathbf{catch} p \{\mathbf{case} y \ \mathbf{of} \ \mathbf{inl} \ x \mapsto \psi[\mathbf{inl} x/y]; \ \mathbf{inr} \ e \mapsto \psi[\mathbf{inr} e/y]\} \end{aligned} \qquad (15) $$

$$ \Leftrightarrow \{\phi\} x \leftarrow p \{\psi[\mathbf{inl} x/y] | \lambda e. \psi[\mathbf{inr} e/y]\}, \qquad (16) $$

immediately leading to the definition of $\mathbf{wp}_s(y \leftarrow \mathbf{catch} p, \psi | \varepsilon)$ shown in Figure 4.

For basic programs $f \in \Sigma$, we need to assume that weakest preconditions $\mathbf{wp}(x \leftarrow f(z), \psi)$ for every $\psi$ are expressible in the assertion language, and then include $\{\mathbf{wp}(x \leftarrow f(z), \psi)\} x \leftarrow f(z) \{\psi | \varepsilon\}$ as an axiom in $\Delta$.

**Lemma 13.** Given a sequentially compatible predicated monad, we have for all programs $p$ and postconditions $\psi$

$$ \Delta \vdash_P \{\mathbf{wp}(x \leftarrow p, \psi | \varepsilon)\} x \leftarrow p \{\psi | \varepsilon\}. $$

*Proof (Sketch).* The proof is via induction over $p$. We carry out the interesting cases of the inductive step in detail:

**Case $p = \mathbf{catch} q$.** Just note that the rule (catch) essentially connects (15) and (16) in the above chain of equivalences explaining $\mathbf{wp}_s$ for catch, decorated with an (irrelevant) abnormal postcondition.

**Case $p = \mathbf{itercase} c \ \mathbf{of} \ \mathbf{inl} \ a \mapsto q; \ \mathbf{inr} \ b \mapsto r$.** Let $\xi$ denote the right-hand side of (12). By the induction hypothesis, $\{\mathbf{wp}_s(x \leftarrow q, \xi | \varepsilon)\} x \leftarrow q \{\xi | \varepsilon\}$ is derivable. This quadruple is equivalent to

$$ \{\mathbf{wp}_s(x \leftarrow q, \xi | \varepsilon)\} x \leftarrow q \left\{ \begin{array}{l} \mathbf{do} \ a \leftarrow c?; \mathbf{wp}_s(x \leftarrow q, \xi | \varepsilon) \lor \\ \mathbf{do} \ b \leftarrow \bar{c}?; \mathbf{wp}_s(x \leftarrow r, \psi | \varepsilon) \end{array} \right\}. $$
We also have {$wp_s(x \leftarrow r, \psi | \varepsilon)$} $x \leftarrow r$ {$\psi | \varepsilon$} by induction. The required quadruple is obtained directly by applying (**itcase**) to the previous two quadruples. □

By Lemma 13 and soundness, $wp_s(x \leftarrow p, \psi | \varepsilon) \sqsubseteq wp(x \leftarrow p, \psi | \varepsilon)$ for all $p, \psi, \varepsilon$. Conversely, we have

**Lemma 14.** For all $p, \psi, \varepsilon$, $wp(x \leftarrow p, \psi | \varepsilon) \sqsubseteq wp_s(x \leftarrow p, \psi | \varepsilon)$.

*Proof (Sketch).* Induction over $p$. Again, we only detail the interesting cases:

*Case p = itercase c of inl a $\mapsto$ q; inr b $\mapsto$ r.* Let $\xi$ denote the right-hand side of (12). Following [7], we need to prove that $\phi_0 := wp(x \leftarrow p, \psi | \varepsilon)$ is a postfixed point of the functional defining $\xi$.

By the definition of weakest preconditions, this amounts to showing that every $\phi$ satisfying {$\phi$} $x \leftarrow p$ {$\psi | \varepsilon$} is smaller than the functional evaluated at $\phi_0$, i.e.

$$ \phi_0 \sqsubseteq \mathbf{do} a \leftarrow c?; \mathbf{wp}_s(x \leftarrow q, \phi_0 | \varepsilon) \lor \mathbf{do} a \leftarrow \bar{c}?; \mathbf{wp}_s(x \leftarrow r, \psi | \varepsilon). $$

Therefore, by case distinction, we need to show that

$$ c? \land \phi_0 \sqsubseteq \mathbf{do} a \leftarrow c?; \mathbf{wp}_s(x \leftarrow q, \phi_0 | \varepsilon) $$

$$ \bar{c}? \land \phi_0 \sqsubseteq \mathbf{do} b \leftarrow \bar{c}?; \mathbf{wp}_s(x \leftarrow r, \psi | \varepsilon). $$

– *Continuation branch.* Unrolling the first iteration of the loop, we see that {$c? \land \phi$} $x \leftarrow (\mathbf{do} a \leftarrow c?; x \leftarrow q; p)$ {$\psi | \varepsilon$} holds and thus

$$ c? \land \phi \sqsubseteq \mathbf{wp}(x \leftarrow (\mathbf{do} a \leftarrow c?; x \leftarrow q; p), \psi | \varepsilon) $$

$$ \sqsubseteq \mathbf{do} a \leftarrow c?; \mathbf{wp}(\mathbf{do} x \leftarrow q; p, \psi | \varepsilon). $$

By sequential compatibility, $wp(x \leftarrow (\mathbf{do} x \leftarrow q; p), \psi | \varepsilon) \sqsubseteq wp(x \leftarrow q, wp(x \leftarrow p, \psi | \varepsilon))$ and by induction $c? \land \phi \sqsubseteq \mathbf{do} a \leftarrow c?; \mathbf{wp}_s(x \leftarrow q, \psi_0 | \varepsilon)$.

– *Termination branch.* By definition of (**itcase**), {$\phi$} $x \leftarrow p$ {$\psi | \varepsilon$} decomposes sequentially into

$$ \{\phi\} x \leftarrow p[\mathrm{ret} x/r] \{\bar{c}? \land \phi\} \text{ and } \{\bar{c}? \land \phi\} x \leftarrow (\mathbf{do} b \leftarrow \bar{c}?; r) \{\psi | \varepsilon\}. $$

From the latter quadruple, we have $\bar{c}? \land \phi \sqsubseteq wp(x \leftarrow (\mathbf{do} b \leftarrow \bar{c}?; r), \psi | \varepsilon)$. Again, $\bar{c}? \land \phi \sqsubseteq \mathbf{do} b \leftarrow \bar{c}?; \mathbf{wp}_s(x \leftarrow r, \psi | \varepsilon)$ by sequential compatibility and by induction.

*Case p = catch q.* As seen in the derivation of the syntactic weakest precondition for *catch*, the Hoare quadruple in question is equivalent to

$$ \{\phi\} x \leftarrow q \{\psi[\mathrm{inl} x/y] | \lambda e. \psi[\mathrm{inr} e/y]\} $$

Thus, $\phi \sqsubseteq wp(x \leftarrow q, \psi[\mathrm{inl} x/y] | \lambda e. \psi[\mathrm{inr} e/y])$ which is smaller than $wp_s(x \leftarrow p, \psi | \varepsilon)$ by induction.
Case $p = \mathbf{raise} e$. Since $\mathbf{catch}(\mathbf{raise} e) = \mathbf{ret} \mathbf{in} \mathbf{re}$,

do $\phi$; $y \leftarrow \mathbf{catch}(\mathbf{raise} e)$; (case $y$ of inl $x \mapsto \psi$; inr $e \mapsto \varepsilon(e)$); $\mathbf{ret} y = \mathbf{do} \phi$; $\mathbf{ret} \mathbf{in} \mathbf{re}$
$\Leftrightarrow$ do $\phi$; $\varepsilon(e)$; $\mathbf{ret} \mathbf{in} \mathbf{re} = \mathbf{do} \phi$; $\mathbf{ret} \mathbf{in} \mathbf{re}$.

So, $\phi \sqcap \varepsilon(e) = \phi$, and therefore $\phi \sqsubseteq \varepsilon(e) = \mathbf{wp}_s(x \leftarrow \mathbf{raise} e, \psi | \varepsilon)$. $\square$

<figure><img src="image_5.png" /></figure>

We are now ready to prove our main result:

**Theorem 15 (Relative completeness).** Let $(\mathbb{T}_E, \mathbb{P})$ be a sequentially compatible predicated monad and let the weakest preconditions for basic programs be expressible in the assertion language. Then

$\mathbb{T}_E, \mathbb{P} \models \{\phi\} x \leftarrow p \{\psi | \varepsilon\} \text{ implies } \Delta_{\Sigma} \vdash_{\mathbb{P}} \{\phi\} x \leftarrow p \{\psi | \varepsilon\},$

where $\Delta_{\Sigma}$ are axioms for the basic programs in the signature $\Sigma$.

*Proof.* By Lemma 13 and Lemma 14, we can express the weakest precondition $\mathbf{wp}(x \leftarrow p, \psi | \varepsilon)$ in the assertion language, and

$$ \Delta_{\Sigma} \vdash_{\mathbb{P}} \{\mathbf{wp}(x \leftarrow p, \psi | \varepsilon)\} x \leftarrow p \{\psi | \varepsilon\}. $$

By the definition of $\mathbf{wp}(x \leftarrow p, \psi | \varepsilon)$, we thus have $\phi \sqsubseteq \mathbf{wp}(x \leftarrow p, \psi | \varepsilon)$, so we can use $(\mathbf{wk})$ to derive the required quadruple. $\square$

<figure><img src="image_6.png" /></figure>

# 7 Conclusion and Further Work

We have extended a previous monad-based generic Hoare calculus [7] to cover computations raising exceptions, modelled in terms of the exception monad transformer [4]. To this end, we have added abnormal postconditions [9] to the system, which govern poststates reached by the program in case it terminates with an exception. Our framework is based on order-enriched monads, which provide the requisite semantic infrastructure to support loops while avoiding the assumption that the underlying category of data types is enriched over complete partial orders; consequently, our generic logic applies also to monads that live on categories with less structure, in particular the category of sets. Moreover, we equip the underlying monad with the choice of a submonad of innocent computations causing only restricted side-effects; this choice induces an object of truth values, in the shape of the type of innocent computations of unit type, that supports a form of geometric logic in which we phrase our assertion language.

We have proved soundness and relative completeness, the latter by giving a calculus of weakest (liberal) preconditions, which turn out to be expressible in spite of the fact that the assertion language is quite weak. Here, a key role is played by fixpoint constructs in the assertion language.

Exceptions can be regarded as a very simple case of uninterpreted operations; in future research, we will explore the possibility of extending the framework to cover more general uninterpreted operations, such as process-algebraic action prefixing. Moreover, we will investigate a more general setup where loops are interpreted by axiomatic iteration in the spirit of complete Elgot monads [1,6], thus in particular covering also coinductive resumption monads [14].
References

1. Adámek, J., Milius, S., Velebil, J.: Equational properties of iterative monads. Information and Computation 208(12), 1306–1348 (2010)

2. Barr, M., Wells, C. (eds.): Category theory for computing science, 2nd ed. Prentice Hall International (UK) Ltd., Hertfordshire, UK, UK (1995)

3. Bloom, S.L., Ésik, Z.: Iteration theories: the equational logic of iterative processes. Springer-Verlag New York, Inc. (1993)

4. Cenciarelli, P., Moggi, E.: A syntactic approach to modularity in denotational semantics. In: Category Theory and Computer Science, CTCS 1993 (1993)

5. Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (Aug 1975)

6. Goncharov, S., Rauch, C., Schröder, L.: Unguarded recursion on coinductive re-
sumptions. In: Mathematical Foundations of Programming Semantics, MFPS 2015.
ENTCS (2015)

7. Goncharov, S., Schröder, L.: A relatively complete Hoare logic for order-enriched effects. In: Logic in Computer Science, LICS 2013. pp. 273–282. IEEE (2013)

8. Hasuo, I.: Generic weakest precondition semantics from monads enriched with order.
Theoretical Computer Science 604, 2 – 29 (2015)

9. Huisman, M., Jacobs, B.: Java program verification via a Hoare logic with abrupt termination. In: Fundamental Approaches to Software Engineering, FASE 2000. LNCS, vol. 1783, pp. 284–303. Springer (2000)

10. Moggi, E.: A modular approach to denotational semantics. In: Category Theory and Computer Science, CTCS 1991. LNCS, vol. 530, pp. 138–139. Springer (1991)

11. Moggi, E.: Notions of computation and monads. Inf. Comput. 93, 55–92 (1991)

12. Nordio, M., Calcagno, C., Müller, P., Meyer, B.: A sound and complete program logic for Eiffel. In: Objects, Components, Models and Patterns, TOOLS EUROPE 2009. Lect. Notes Business Inf. Proc., vol. 33, pp. 195–214. Springer (2009)

13. von Oheimb, D.: Hoare logic for Java in Isabelle/HOL. Concurrency and Computa-
tion: Practice and Experience 13, 1173–1214 (2001)

14. Piróg, M., Gibbons, J.: The coinductive resumption monad. In: Mathematical Foundations of Programming Semantics, MFPS 2014. ENTCS, vol. 308, pp. 273–288 (2014)

15. Plotkin, G., Power, J.: Algebraic operations and generic effects. Appl. Cat. Struct. 11, 69–94 (2003)

16. Poetzsch-Heffter, A., Rauch, N.: Soundness and relative completeness of a program-
ming logic for a sequential Java subset. Tech. rep., TU Kaiserlautern (2004)

17. Schröder, L., Mossakowski, T.: Monad-independent Hoare logic in HasCASL. In: Fundamental Aspects of Software Engineering, FASE 2003. LNCS, vol. 2621, pp. 261–277 (2003)

18. Schröder, L., Mossakowski, T.: Generic exception handling and the Java monad. In: Algebraic Methodology and Software Technology, AMAST 2004. LNCS, vol. 3116, pp. 443–459. Springer (2004)

19. Simpson, A.K.: Recursive types in Kleisli categories. Tech. rep., MFPS Tutorial, April 2007 (1992)

20. Vickers, S.: Topology via Logic. Cambridge University Press (1989)

21. Wadler, P.: How to declare an imperative. ACM Comput. Surveys 29, 240–263 (1997)