Andrei Paskevich

Continuation Passing as an Abstract Syntax for Deductive Verification

Continuation-passing style allows us to devise an extremely economical abstract syntax for a generic algorithmic language. This syntax is flexible enough to naturally express conditionals, loops, (higher-order) function calls, and exception handling. It is type-agnostic and state-agnostic, which means that we can combine it with a wide range of type and effect systems.

We argue that this syntax is also well suited for the purposes of deductive verification. Indeed, we show how it can be augmented in a natural way with specification annotations, ghost code, and side-effect discipline. We define the rules of verification condition generation for this syntax, and we show that the resulting formulas are nearly identical to what traditional approaches, like the weakest precondition calculus, produce for the equivalent algorithmic constructions.

To sum up, we propose a minimalistic yet versatile abstract syntax for annotated programs for which we can compute verification conditions without sacrificing their size, legibility, and amenability to automated proof, compared to more traditional methods. We believe that it makes it an excellent candidate for internal code representation in program verification tools.

Introduction

Suppose we want to develop a deductive verification tool for a simple imperative language. We start with the basic while core -assignment, sequence, conditionals, and while loops -and, for the purposes of specification -assertions and loop invariants, and also loop variants, to prove termination. Then we add functions and procedures with their preconditions and postconditions, and auxiliary parameters, to catch the previous states of the modified variables. Auxiliary variables are nice but still quite limited, and so we add ghost variables, ghost function parameters, and ghost function results. Then we get adventurous and implement exception handling, which we already had in a rudimentary state in the form of break, continue, and return statements. Before long, our language has the abstract syntax tree with two dozen cases, some of which, like function calls or pattern matching, have a lot of components and are quite complex to handle.

We are fully aware that some (most?) of this complexity is justified and inevitable. And yet, we cannot help looking at lambda calculus, a universal computation formalism with mere three syntax rules and a single evaluation rule, and feeling like we have lost some truth, or at least some beauty, in the maelstrom of technical details.

The present work attempts to recover some of this loss, and it comes of one simple intuition: In a structural language, a block of code has a single entry but multiple exits. The "multiple exits" part means not just that there may be multiple exit points inside a block, but, more importantly, that there may be multiple ways in which a code block may end, leading to different execution paths afterwards, and with different postconditions to verify on exit.

This does not seem to be a universal perception: after all, the foundational tool of deductive verification, the Hoare triple, comes with a single postcondition. The notion that a program expression can only end in a single way and has to satisfy this postcondition on exit is a mental habit that we have to overcome when we start dealing with break, continue, return, and exceptions, both in code and in specification. We recognize the same habit in the type systems of ML-like languages, where exception-raising instructions are given type ∀α.α, which is a formal way to say "whatever". The type system simply cannot express that the expression does not produce any value (nor that it raises an exception), and the best we can do is to say that the produced value can have any type at all. The usual way to explain this inadequacy is to say that exceptions are side effects, and the type system, with its noble lambda pedigree, cares not for such shenanigans. However, we firmly believe that it is much more useful to see exceptions not as a side effect but as a pure control structure, a sequence step towards a different code point. In fact, from the standpoint of specification and verification (as opposed to compilation and actual execution), there is not much reason to distinguish a "normal" and an "exceptional" way to leave a block of code -they are just different kinds of return.

From the same standpoint, and perhaps more radically, there is not much reason to distinguish function calls and function returns. Indeed, we describe them in a very similar manner: both are parametrized by data (received and returned), and both carry conditions (pre-and post-) to verify when the execution reaches the corresponding point.

Of course, an approach that treats exits as entries -and function returns as function callsexists since the early days of computer science: it is called continuation-passing style. In this setting, leaving a block of code is done by calling another one (its continuation), and the multiplicity of possible outcomes comes naturally, as we are free to call any particular continuation at our disposal. It is an extremely powerful notion, which has seen no end of theoretical and practical applications, to which this work wants to add another one: being a great abstract syntax for deductive verification of imperative structural programs.

Let us consider, as an example, a function that computes the factorial of a natural number, in the syntax which we are going to use throughout this paper:

1 factorial (n: int) { 0 ⩽ n } 2 (return: (m: int) { m = n! }) 3 = fact 1 n 4 / fact (r: int) (k: int) 5 { 0 ⩽ k ⩽ n ∧ r • k! = n! } 6 = if (k > 0) tt ff 7 / tt → fact (r * k) (k -1) 8 / ff → return r
Lines 1 and 2 introduce and specify a handler, which is our name for a subroutine. The handler is called factorial and it expects a single data parameter, an integer named n, with a precondition that requires n to be non-negative. It also expects a single continuation parameter, named return, which takes an integer argument m, and the precondition for return is that m is the factorial of n.

Lines 3-8 contain the implementation of factorial. It consists in defining a recursive handler fact, expecting two data parameters, r and k, in lines 4-8, and calling it with arguments 1 and n, respectively, in line 3. The slash symbol separates the call from the definition. The precondition of fact is given on line 5. The implementation of fact tests whether k is positive, using a globally defined handler if, which has the following specification: if (c: bool) (then: { c }) (else: { ¬c })

The if handler expects a single data parameter c along with two nullary continuation parameters, named then and else. The precondition of then is that c is true, and the precondition of else is that c is false. It is worth emphasizing that if is not part of the language, but just a handler, like factorial or fact, and its specification above is sufficient for verification.

Going back to fact, the actual handler arguments supplied to if are defined in the last two lines. Unlike the data argument (k > 0) which is evaluated eagerly, the handler arguments tt and ff are continuations, to be called by if depending on the value of the data argument. Whenever k is strictly positive, if executes tt, which makes a recursive call of fact. Otherwise, if k is zero or negative, if calls ff, which passes r to the return handler, leaving factorial. There is a small peculiarity in the way we define tt and ff: the right arrow instead of the equality sign means that these handlers are not given a complete specification, and their code must be verified separately at each invocation.

Note that fact never returns to the caller: to do that, it would need to receive a continuation parameter and call it, like if and factorial do. Instead, fact escapes by calling return at the end of computation. In this respect, fact behaves rather like a loop than a recursive function. Indeed, its continuation is determined statically, by its lexical context, rather than dynamically by its caller. Consequently, there is no distinct postcondition associated to fact: in our language, postconditions are preconditions of continuation parameters, and fact has none thereof.

To verify a handler definition, we can compute the weakest precondition for the handler's body and check that it holds for all values of handler's parameters that satisfy the handler's precondition. Let us see how this works on our example (here, we ignore termination and we write V 𝑁 -𝑀 to denote the weakest precondition for the expression written in lines 𝑁 to 𝑀):

V factorial = ∀n. 0 ⩽ n → V 3-8 V 3-8 = V 3 ∧ V fact V 3 = (0 ⩽ k ⩽ n ∧ r • k! = n!) [r ↦ → 1, k ↦ → n] = 0 ⩽ n ⩽ n ∧ 1 • n! = n! V fact = ∀r k. (0 ⩽ k ⩽ n ∧ r • k! = n!) → V 6-8 V 6-8 = (k > 0 → V 7 ) ∧ (¬(k > 0) → V 8 ) V 7 = (0 ⩽ k ⩽ n ∧ r • k! = n!) [r ↦ → r • k, k ↦ → k -1] = 0 ⩽ k -1 ⩽ n ∧ r • k • (k -1)! = n! V 8 = (m = n!) [m ↦ → r] = r = n!
The weakest precondition for an expression consists of the weakest precondition for the top-most handler call and the verification conditions for the attached handler definitions (V fact ). Calls without continuation parameters (V 3 , V 7 , V 8 ) require us to merely verify the instantiated precondition of the callee. Calls with continuation parameters (V 6-8 ) also require checking that the actual handler arguments satisfy the specification of the formal continuation parameters. In our example, this means that the preconditions of the two continuation parameters in the contract of if must imply, respectively, the weakest preconditions of the actual continuations defined in lines 7 and 8.

Outline. Below we present our language: its syntax, semantics, type system, and procedures for effect analysis, deductive verification, and ghost code handling. The features of the language are introduced incrementally. We start with the pure fragment without annotations in Section 2. Then we introduce mutable state in Section 3, in a way that ensures the alias safety of well-typed programs. In Section 4, we add pre-write annotations that describe the effect that a given computation has on the program state. These annotations allow us to translate programs with mutable state into equivalent pure programs using a fine-grained monadic encoding.

In Section 5, we equip our handlers with functional specifications and show how to compute verification conditions for partial and total correctness. In particular, we demonstrate that classical Dijkstra-style weakest preconditions and efficient weakest preconditions as described by Flanagan and Saxe [?]. can both be derived as equivalent forms of the same verification condition.

Finally, in Section 6, we introduce the notion of ghost data: program variables that do not affect the main computation and are added solely to facilitate specification and proof. We devise a procedure that eliminates ghost variables and the code that depends on them, while checking that this elimination does not change the program behaviour.

Even before the formal introduction of various specification annotations, we systematically use them in our examples in order to better describe the behaviour of annotated handlers. In all such cases we provide an informal explanation of the meaning and purpose of these annotations.

Pure fragment

The building blocks of our language are handler definitions and handler calls. Contrary to the usual practice of functional programming languages, we separate code and data on the syntactic level: data terms (which we call simply terms) occur inside code terms (which we call expressions) as arguments in handler calls, but an expression cannot reduce (evaluate) to a term.

Here is the formal grammar of our base fragment: Just as we distinguish expressions and terms, we distinguish the names we assign to them, and call them handlers and variables, respectively. Thus, in handler contracts (which at this point are just lists of formal parameters), variables serve as data parameters and handlers as continuation parameters.

From now on, we will call the former term parameters and the latter, handler parameters.

We introduce two kinds of handler definitions which behave in the same way during execution but are quite different from the verification standpoint. The first kind, called abbreviations, are verified independently at each invocation site, as if the handler definition were inlined in the code. The second kind, called definitions proper, are verified just once, when introduced, and any subsequent invocation of the handler is merely required to satisfy the preconditions in the contract. In other words, the contract in a handler definition must provide a complete specification of the handler's behaviour, sufficient to abstract over its implementation. This allows for recursive handler definitions, without the risk of introducing circular dependencies in verification conditions. Abbreviations, on the other hand, are not allowed to be recursive.

We use letters 𝑒 and 𝑑 for expressions, 𝑠 and 𝑡 for terms, 𝑥, 𝑦, 𝑧 for variables, 𝑓 , 𝑔, ℎ for handlers, 𝑎 and 𝑏 for arguments (which can be terms or handlers), 𝛾 and 𝛿 for definitions and abbreviations, 𝜚 and 𝜋 for contracts, 𝜏 and 𝜃 for term types. We use the underscore symbol (_) to denote a fresh "dummy" handler name, which is not supposed to be bound or used anywhere else in the program. In a contract, no variable or handler parameter can appear twice, just like no handler can be defined twice in a group of handler definitions.

In formal rules and definitions, we use two separator symbols, and , to represent, respectively, abstraction and application. A pair 𝜚 𝑒 is a nameless handler definition, an implementation hidden behind a contract. A pair 𝜚 ā or a triple ( 𝜚 𝑒) ā stand for an application of some unnamed handler, described by its contract and, possibly, its implementation, to a specific list of arguments. We denote empty sequences of annotations, arguments or definitions with the box symbol (□). Since empty definition groups are not allowed in our syntax, 𝑒 / □ is identified with 𝑒.

Before we proceed to further presentation and analysis of our language, we shall briefly discuss its data side. For our purposes, we do not need precise definitions of the syntax and semantics of terms and term types. Instead, we assume a typing relation Γ ⊢ 𝑠 : 𝜏 that associates type 𝜏 with term 𝑠 in typing context Γ, which provides types for the free variables in 𝑠. We also assume a type-preserving normalization operator 𝑠 Σ that reduces 𝑠 to a ground normal form in evaluation context Σ, which provides values for the free variables in 𝑠. Handlers cannot occur inside terms. We require that terms can be directly used inside logical formulas (preconditions, verification conditions) with the same meaning as in program code. As a consequence, terms must be total and pure, i.e., normalization can neither fail nor produce side effects; all partial or effectful computations are to be done by handlers. It is possible to restrict terms to variables and constants only, so that normalization is limited to variable instantiation, but in a practical implementation, it is convenient to admit some operations, too.

For concrete examples in our paper, we will use unbounded integers, Booleans, and polymorphic lists, together with a handful of basic operations on them:

term ::= variable | true | false | . . . | -1 | 0 | 1 | 2 | . . . | term + term | term -term | term * term | term = term | term < term | term > term | cons term term | nil | isCons term | . . . termType ::= typeVariable | bool | int | list termType | . . .
Typing and normalization rules for this fragment are as usual, and we do not write them here. We compute the free variables and free handlers in expressions and abstractions as follows:

FV(ℎ □) ≜ ∅ FV(𝑒 / ℎ 𝜚 → 𝑑) ≜ FV(𝑒) ∪ FV( 𝜚 𝑑) FV(ℎ ā 𝑠) ≜ FV(ℎ ā) ∪ FV(𝑠) FV(𝑒 / γ (ℎ 𝜚 = 𝑑)) ≜ FV(𝑒 / γ) ∪ FV( 𝜚 𝑑) FV(ℎ ā 𝑔) ≜ FV(ℎ ā) FV((𝑥 :𝜏) 𝜚 𝑒) ≜ FV( 𝜚 𝑒) \ {𝑥} FV(□ 𝑒) ≜ FV(𝑒) FV((𝑔:𝜋) 𝜚 𝑒) ≜ FV( 𝜚 𝑒) ∪ FV(𝜋 _ □) FH(ℎ □) ≜ { ℎ } FH(𝑒 / ℎ 𝜚 → 𝑑) ≜ (FH(𝑒) \ { ℎ }) ∪ FH( 𝜚 𝑑) FH(ℎ ā 𝑠) ≜ FH(ℎ ā) FH(𝑒 / γ (ℎ 𝜚 = 𝑑)) ≜ FH(𝑒 / (_ 𝜚 → 𝑑) / γ) \ { ℎ } FH(ℎ ā 𝑔) ≜ FH(ℎ ā) ∪ {𝑔} FH((𝑥 :𝜏) 𝜚 𝑒) ≜ FH( 𝜚 𝑒) FH(□ 𝑒) ≜ FH(𝑒) FH((𝑔:𝜋) 𝜚 𝑒) ≜ FH( 𝜚 𝑒) \ {𝑔}
We call an expression closed if it contains no free variables. The abstraction 𝜋 _ □ used in the last rule for FV allows us to compute the free variables in contract 𝜋 by creating an abstraction over a dummy handler applied to an empty list of arguments. The actual name of the handler does not matter as it does not affect the result. Though at this point there are no free occurrences of variables in contracts, this will change in the following sections when we add effect annotations and preconditions. We do not apply this trick for FH, as handlers do not, and will not, freely occur in contracts. Also noteworthy is the rule to compute the free handlers in an expression with a group of handler definitions. Since handler definitions can be recursive, the definition body, 𝑑, may contain handlers defined in γ. To account for this, we transform the definition ℎ 𝜚 = 𝑑 into an abbreviation _ 𝜚 → 𝑑 and move it under γ. Again, the name of the dummy handler does not matter here, as it is fresh and thus cannot occur in 𝑒. After computing the free handlers in the resulting expression, we remove ℎ from the set. This rule also applies when γ is empty: as we said before, 𝑒 / □ is just 𝑒.

Operational semantics. We define a small-step operational semantics of our language as follows. An evaluation step is presented as transition relation

Λ ⊢ 𝑒 • Σ -→ 𝑒 ′ • Σ ′ .
Here, Λ is a handler evaluation context that maps handlers to abstractions, and Σ, Σ ′ are variable evaluation contexts that map variables to normalized ground terms. Handler context Λ keeps track of handler definitions and abbreviations. Variable contexts Σ and Σ ′ store values of mutable variables (Section 3), in the state before and after the evaluation step, respectively.

Here are the evaluation rules for the current syntax:

Λ, ℎ ↦ → 𝜚 𝑑 ⊢ 𝑒 • Σ -→ 𝑒 ′ • Σ ′ Λ ⊢ 𝑒 / ℎ 𝜚 → 𝑑 • Σ -→ 𝑒 ′ / ℎ 𝜚 → 𝑑 • Σ ′ (E-Abbr) Λ, ℎ ↦ → 𝜚 𝑑 ⊢ 𝑒 / γ • Σ -→ 𝑒 ′ / γ • Σ ′ Λ ⊢ 𝑒 / γ (ℎ 𝜚 = 𝑑) • Σ -→ 𝑒 ′ / γ (ℎ 𝜚 = 𝑑) • Σ ′ (E-Defn) ℎ ↦ → 𝜚 𝑑 ∈ Λ Σ ⊢ ( 𝜚 𝑑) ā -→ * (□ 𝑒) □ Λ ⊢ ℎ ā • Σ -→ 𝑒 • Σ (E-Call) Σ ⊢ ((𝑥 :𝜏) 𝜚 𝑒) 𝑠 ā -→ ( 𝜚 𝑒) [𝑥 ↦ → 𝑠 Σ ] ā (E-AppT) Σ ⊢ ((𝑔:𝜋) 𝜚 𝑒) 𝑓 ā -→ ( 𝜚 𝑒) [𝑔 ↦ → 𝑓 ] ā (E-AppH)
Rules E-Abbr and E-Defn evaluate expressions under handler abbreviations and definitions, by converting those into abstractions, which are added to the handler context Λ. Rule E-Call applies when the called handler is introduced by an abstraction or a definition, and therefore is found in Λ. An auxiliary transition relation Σ ⊢ ( 𝜚 𝑒) ā -→ ( 𝜚 ′ 𝑒 ′ ) ā′ , which we use here, is essentially β-reduction: it replaces formal term and handler parameters with the actual arguments; the term arguments are normalized under Σ. We assume that substitution into abstractions and expressions, as performed by rules E-AppT and E-AppH, renames bound variables and handlers as needed to avoid illegal capture. A single E-Call step requires full parameter application: all binders in the contract must be lifted and all arguments must be substituted into the handler body.

Of course, these evaluation rules are not enough. Handler calls and definitions are mere control structures, and all actual work has to be done by predefined library handlers, such as if which we used in the example in the introduction.

The semantics of library handlers is axiomatized by evaluation rules like these:

𝑠 Σ = true Λ ⊢ if 𝑠 𝑓 𝑔 • Σ -→ 𝑓 • Σ 𝑠 Σ = false Λ ⊢ if 𝑠 𝑓 𝑔 • Σ -→ 𝑔 • Σ 𝑠 Σ = cons 𝑡 1 𝑡 2 Λ ⊢ unList 𝑠 𝑓 𝑔 • Σ -→ 𝑓 𝑡 1 𝑡 2 • Σ 𝑠 Σ = nil Λ ⊢ unList 𝑠 𝑓 𝑔 • Σ -→ 𝑔 • Σ 𝑡 Σ ≠ 0 𝑠 Σ div 𝑡 Σ = 𝑛 Λ ⊢ div 𝑠 𝑡 𝑓 • Σ -→ 𝑓 𝑛 • Σ 𝑡 Σ ≠ 0 𝑠 Σ mod 𝑡 Σ = 𝑛 Λ ⊢ mod 𝑠 𝑡 𝑓 • Σ -→ 𝑓 𝑛 • Σ
Note that just like the conditional, pattern matching does not need to be part of the core language syntax and can be delegated to a handler. Of course, if we were implementing a compiler, we would still have to implement the actual pattern matching functionality. But since we are interested in static analysis and verification, we only need the specification of the library handlers:

if (c: bool) (then: { c }) (else: { ¬c }) unList (l: list α) (onCons: (h: α) (t: list α) { l = cons h t }) (onNil: { l = nil }) div (a: int) (b: int) { b ≠ 0 } (return: (q: int) { ∃r. 0 ⩽ r < |b| ∧ a = b • q + r }) mod (a: int) (b: int) { b ≠ 0 } (return: (r: int) { 0 ⩽ r < |b| ∧ ∃q. a = b • q + r })
which can be readily expressed in our language and used for verification condition generation in the same way as for user-defined handlers.

Typing rules. While our language is compatible with various type systems, we endow it here with ML-style polymorphic rank-1 types, to benefit from effective Hindley-Milner type inference. We will however restrict polymorphism to data types; the arity of handlers is invariant. Here is the grammar of expression and handler types:

expressionType ::= ⊥ | termType → expressionType | expressionType → expressionType handlerType ::= ⟨ typeVariable * ⟩ expressionType
Expression types are also assigned to contracts and abstractions. Type ⊥ is that of expressions that expect no additional arguments and can be readily executed. This type is also given to nullary contracts and abstractions. Handler calls with an incomplete argument list have arrow types; so do the contracts and abstractions that have formal parameters. Handler types can be generalized in some of their type variables and carry the list of these type variables inside angled brackets before their base type. When a handler type is monomorphic, i.e., not generalized in any of its type variables, we

Γ ⊢ 𝑒 : ⊥ Γ ⊢ □ 𝑒 : ⊥ (T-Nullary) Γ ⊢ 𝜋 : 𝜁 Γ, 𝑔 : 𝜁 ⊢ 𝜚 𝑒 : 𝜉 Γ ⊢ (𝑔:𝜋) 𝜚 𝑒 : 𝜁 → 𝜉 (T-ParH)
Rule T-Call specializes handler types by instantiating their generalized type variables with arbitrary data types. When we pass a handler as an argument (rule T-AppH), we check that it can be specialized into the expected type 𝜁 by typechecking its call with an empty argument list.

Rule T-Defn handles mutually recursive definitions using the same technique as the corresponding rule for FH: each definition is converted into an abbreviation under a fresh dummy handler name and pushed inside the expression. Handlers introduced by a definition are generalized in type variables that are not fixed by the typing context.

Handlers introduced by an abbreviation (rule T-Abbr) are not generalized. While there is no fundamental reason why they should not be, this restriction simplifies some of our procedures in later sections. Moreover, abbreviations are expected to represent proper continuations, i.e., code that retrieves and processes the results of a given computation. In ML-like languages, such code is not generalized: when we write let x = 𝑒 1 in 𝑒 2 , the type of x is fixed in 𝑒 2 .

Rule T-Contract derives the type of a contract from the type of an abstraction over a call of a dummy handler with an empty argument list, similarly to how we defined FV for handler parameters.

Finally, the types of handler parameters (rule T-ParH) are not generalized, in agreement with the rules of prenex polymorphism. find_greater (n: int) (l: list int) Control structures. We conclude with another example showing how usual programming constructs -recursion, pattern matching, and exception handling -are expressed in our language. In Figure 1, we define two OCaml functions. Recursive function find_greater returns the first element in a singly-linked list that exceeds a given integer or raises the Not_found exception if none such is found. Function check_greater uses find_greater to test whether a list contains an element greater than a given integer, and catches the Not_found exception to return a negative result.

(return: (r: int) { r ∈ l ∧ r > n }) (not_found: { ∀x ∈ l. x ⩽ n }) = unList l on_cons not_found / on_cons (h: int) (t: list int) → if (h > n) tt ff / tt → return h / ff → find_greater n t return not_found check_greater (n: int) (l: list int) (return: (r: bool) { r ↔ ∃x ∈ l. x > n }) = find_greater n l found not_found / found (x: int) → return true / not_found → return false
In Figure 2, we translate these functions into our language and add functional specifications. We use the previously shown library handler unList to deconstruct a list value. Notice that we do not put any precondition in the contract of on_cons: the body of this abbreviation will be verified in the context of its usage. Exceptions are translated using additional handler parameters: find_greater receives one handler parameter named return for normal termination, and another, named not_found, for exceptional termination. The caller, check_greater, provides a continuation for both outcomes. If the OCaml version of check_greater did not catch and handle the exceptional outcome of find_greater, then its specification in our language would receive an additional handler parameter to reflect that check_greater can raise an exception, and this parameter would be passed verbatim to find_greater. discuss automated translation?

This example underlines an important feature of a continuation-based representation: it naturally admits multiple outcomes for a unit of computation and makes no distinction between normal and exceptional outcomes. Each possible outcome is shown in the handler's contract and characterized by its own specification, modeled as a precondition of the corresponding handler parameter. Furthermore, by using the same notion of a handler (i.e., continuation) to represent entries and exits, units of computation and their outcomes, we achieve a rather elegant economy of concepts: results are modeled as parameters, postconditions as preconditions, etc.

Mutable State

Our next extension consists in adding mutable variables. We shall restrict our language to alias-free programs, for which simple and efficient techniques of program verification, like weakest precondition calculus, can be effectively applied. We do not introduce a pointer type, but rather treat certain variables as references to mutable memory cells. For this, we extend the syntax of expressions and handler contracts as follows:

expression ::= . . . | expression / & variable = term argument ::= . . . | & variable annotation ::= . . . | & variable : termType
On the lexical level, references are represented with ordinary variables. In particular, they can be used inside terms and preconditions. On introduction and usage, we distinguish references with the ampersand symbol &. We denote references with letters 𝑝, 𝑞, 𝑟.

Let us extend the definitions of FV and FH for the new constructs:

FV(𝑒 / &𝑟 = 𝑠) ≜ (FV(𝑒) \ {𝑟 }) ∪ FV(𝑠) FH(𝑒 / &𝑟 = 𝑠) ≜ FH(𝑒) FV(ℎ ā &𝑟) ≜ FV(ℎ ā) ∪ {𝑟 } FH(ℎ ā &𝑟) ≜ FH(ℎ ā) FV((&𝑟 :𝜏) 𝜚 𝑒) ≜ FV( 𝜚 𝑒) \ {𝑟 } FH((&𝑟 :𝜏) 𝜚 𝑒) ≜ FH( 𝜚 𝑒)
In the syntax rules above, the added productions correspond, respectively, to reference allocation, passing reference as an argument, and declaring a formal reference parameter. We do not need special syntax for dereferencing, as references that occur inside terms as variables are dereferenced implicitly. As for assignment, this functionality is, once again, delegated to a library handler:

assign (&r: α) (v: α) (return: [r] { r = v })
Library handler assign takes a reference parameter r and a term parameter v of the same generic type α. The handler parameter return takes no parameters (that is, assign returns no result), and the precondition of return states that the value stored in r when assign returns is equal to v. This can only be ensured if assign changes the content of r, and, indeed, the pre-write annotation [r] attached to return means that reference r is potentially modified during the execution of assign before return is called. Pre-write annotations are part of the functional specification and will be formally introduced in Section 4.

To give a better intuition of the new constructs, let us see how dereferencing and allocation can be implemented as handlers:

access (&r: α) (return: (v: α) { v = r }) = return r alloc (v: α) (return: (&r: α) { r = v }) = return &q / &q = v
Handler access takes a reference parameter r and a handler parameter return. The latter expects a single term parameter whose value must be equal to the value of r at the moment when return is called. Application return r treats r as a term argument (note the absence of & in front of r), and therefore passes to return the current value stored in r, which satisfies the precondition of return.

Handler alloc takes a term parameter v and returns (via its handler parameter) a reference containing the value of v. The no-alias restriction ensures that the reference returned by alloc is fresh, and we do not need to specify this explicitly in the contract. The implementation of alloc allocates a fresh reference q initialized to v and returns it. This does not create a "dangling pointer", since there is no stack shrinking on return: rule E-Call replaces a call to alloc with its appropriately instantiated body, and however the actual return handler is evaluated, it always stays in the scope of the new reference.

Operational semantics. Here are the evaluation rules for expressions with references:

Σ ⊢ ((&𝑞:𝜏) 𝜚 𝑒) &𝑟 ā -→ ( 𝜚 𝑒) [𝑞 ↦ → 𝑟] ā (E-AppR) Λ ⊢ 𝑒 • Σ, 𝑟 ↦ → 𝑠 Σ -→ 𝑒 ′ • Σ ′ , 𝑟 ↦ → 𝑡 Λ ⊢ 𝑒 / &𝑟 = 𝑠 • Σ -→ 𝑒 ′ / &𝑟 = 𝑡 • Σ ′ (E-Alloc)
Rule E-AppR (which participates together with E-AppT and E-AppH in evaluating handler calls) instantiates a formal reference parameter 𝑞 with an actual reference argument 𝑟. Note that the latter is not normlalized under Σ unlike the term argument in E-AppT: normalization replaces references with their values in the variable context.

Rule E-Alloc evaluates the underlying expression 𝑒 in the extended variable context that binds the new reference to the normalized initialization term. The value of this reference in the post-state is stored inside the allocation clause. In other words, allocations play the role of the mutable store inside expressions. In this way, we can preserve the lexical scope relationship between references and handlers during evaluation, after allocation takes place.

The operational semantics of assign is defined as follows:

Σ = Σ 1 , 𝑟 ↦ → 𝑡, Σ 2 Σ ′ = Σ 1 , 𝑟 ↦ → 𝑠 Σ , Σ 2 Λ ⊢ assign &𝑟 𝑠 𝑓 • Σ -→ 𝑓 • Σ ′
For instance, (assign &q (q*q+q) k / ... / &q = 6) evaluates to (k / ... / &q = 42).

Typing rules. Reference parameters add a new kind of type for expressions:

expressionType ::= . . . | & termType → expressionType
The typing rules for the new constructs are as follows:

Γ ⊢ 𝑠 : 𝜏 Γ, &𝑟 : 𝜏 ⊢ 𝑒 : ⊥ Γ ⊢ 𝑒 / &𝑟 = 𝑠 : ⊥ (T-Alloc) Γ, &𝑞 : 𝜏 ⊢ 𝜚 𝑒 : 𝜉 Γ ⊢ (&𝑞:𝜏) 𝜚 𝑒 : &𝜏 → 𝜉 (T-ParR) Γ, Δ ′ ⊢ ℎ ā : &𝜏 → 𝜉 Δ ′ is Δ with all handler bindings removed Γ, &𝑟 : 𝜏, Δ ⊢ ℎ ā &𝑟 : 𝜉 (T-AppR)
In typing contexts, we distinguish references from ordinary variables using the & symbol. The rules for allocation and abstraction are straightforward; notice that just like handler definitions, reference allocations can only be put over ⊥-typed, that is, executable, expressions.

Rule T-AppR, which handles passing of reference arguments, requires the applicand to be typechecked in a restricted context, from which the reference argument and all handlers that come after it have been evicted. This is done to ensure that well-typed programs are alias-free. In our language, the only way to create an alias -a possibility to access the same memory location under two different names -is to give another name to a reference by passing it as a reference argument to an expression. Rule T-Call verifies that this expression does access this reference in any other way, neither directly, nor through a handler. To see how this restriction works, consider two typical cases of aliasing:

f &r &r / &r = 0 / f (&p: int) (&q: int) = . . . g &r / g (&p: int) = . . . / &r = 0
In the expression on the left, call (f &r &r) evaluates to the body of f, where both p and q are instantiated with r, creating an alias. In the expression on the right, call (g &r) evaluates to the body of g, where p is instantiated with r. This also creates an alias, since g is already in the scope of reference r and may access it directly.

Rule T-Call excludes both of these programs. Indeed, (f &r &r) cannot be type-checked, because the typing context for (f &r) does not contain a binding for &r. Call (g &r) cannot be type-checked either, because the typing context for g does not contain a binding for g itself.

As a small exercise, consider the following handler definitions:

alias1 (&x: int) (return: (&y: int)) = return &x alias2 (return: (&y: int)) (&x: int) = return &x Are these definitions accepted by our type system? Is application of these handlers alias-safe?

Effect Computation

The next element of specification we add to our language are the pre-write annotations that specify, for any given handler ℎ, which references, visible to ℎ, are potentially modified after ℎ is introduced and before it is executed. We consider that a handler is introduced when its parent handler is executed; this holds both for defined handlers and handler parameters. We extend the syntax of contracts:

contract ::= pre-write * annotation * pre-write ::= [ variable ]
We do not put the & symbol before the reference name, since non-mutable variables cannot appear in a pre-write annotation and thus there is no possible ambiguity. We assume that all references in the pre-write annotations in any given contract are distinct. The references listed as pre-writes in the contract of handler ℎ are said to be the formal pre-writes of ℎ.

References in pre-write annotations are considered to occur freely in the contract:

FV([𝑝] 𝜚 𝑒) ≜ FV( 𝜚 𝑒) ∪ { 𝑝} FH([𝑝] 𝜚 𝑒) ≜ FH( 𝜚 𝑒)
Being part of specification, pre-writes do not affect evaluation:

Σ ⊢ ([𝑝] 𝜚 𝑒) ā -→ ( 𝜚 𝑒) ā (E-Eff)
Typing rules are extended in a straightforward way:

&𝑝 : 𝜏 ∈ Γ Γ ⊢ 𝜚 𝑒 : 𝜉 Γ ⊢ [𝑝] 𝜚 𝑒 : 𝜉 (T-Eff)
Effect checking. The pre-write annotations in a program must be exhaustive in the sense that every actual write effect that may happen during evaluation is accounted for. We can effectively check that user-written annotations are exhaustive; for this, we compute an overapproximation of actual prewrites for each handler bound in our code, and we check that each reference in this overapproximation is listed as a formal pre-write for that handler. In the rest of this section, we describe this procedure and discuss the restrictions that it imposes on the programs we can write. An effect set or simply an effect is a set of pairs (𝑟, ℎ) such that reference 𝑟 is a potential pre-write for handler ℎ. We can compute the effect set of any given expression, abstraction or application. For example, if we consider a handler call assign &p 42 g, which writes 42 into reference p and then passes control to handler g, then p is a pre-write for g, and the effect of the call is the singleton set {(p, g)}. We denote effect sets with capital letter 𝐸.

In an abstraction [𝑝] 𝜚 𝑒, reference 𝑝 is considered as a potential pre-write for every handler occurring in 𝑒 and not bound by 𝜚. The corresponding effect set is denoted 𝑝 ⊗ 𝜚 𝑒 and is formally defined as the cartesian product { 𝑝 } × FH( 𝜚 𝑒).

When a reference is bound in an expression or an abstraction, it is evicted from the underlying effect set. We denote this operation 𝐸 ⊖ 𝑟 and define it as

{ (𝑞, 𝑔) ∈ 𝐸 | 𝑞 ≠ 𝑟 }.
Similarly, when a handler is bound in an expression or an abstraction, we forget the pre-writes computed for this handler, on condition that they are all duly listed in the handler's contract:

𝐸 ⊖ ℎ ≜ { (𝑞, 𝑔) ∈ 𝐸 | 𝑔 ≠ ℎ } if for each ( 𝑝, ℎ) in 𝐸, 𝑝 is a formal pre-write of ℎ, undefined otherwise.
For the sake of simplicity, we assume the contract of handler ℎ to be known from the context.

Operator E computes the effect set for a given expression, abstraction or application:

E (ℎ ā) ≜ E ( 𝜚 ℎ ā) E (𝑒 / γ (ℎ 𝜚 = 𝑑)) ≜ E (𝑒 / (_ 𝜚 → 𝑑) / γ) ⊖ ℎ E (𝑒 / &𝑟 = 𝑠) ≜ E (𝑒) ⊖ 𝑟 E (𝑒 / ℎ 𝜚 → 𝑑) ≜ (E (𝑒) ⊖ ℎ) ∪ E ( 𝜚 𝑑) E ([𝑝] 𝜚 𝑒) ≜ E ( 𝜚 𝑒) ∪ ( 𝑝 ⊗ 𝜚 𝑒) E ([𝑝] 𝜚 ā) ≜ E ( 𝜚 ā) E ((𝑥 :𝜏) 𝜚 𝑒) ≜ E ( 𝜚 𝑒) E ((𝑥 :𝜏) 𝜚 𝑠 ā) ≜ E ( 𝜚 ā) E ((&𝑞:𝜏) 𝜚 𝑒) ≜ E ( 𝜚 𝑒) ⊖ 𝑞 E ((&𝑞:𝜏) 𝜚 &𝑟 ā) ≜ E ( 𝜚[𝑞 ↦ → 𝑟] ā) E (( 𝑓 :𝜋) 𝜚 𝑒) ≜ E ( 𝜚 𝑒) ⊖ 𝑓 E (( 𝑓 :𝜋) 𝜚 ℎ ā) ≜ E ( 𝜚 ā) ∪ E (𝜋 ℎ 𝑥𝑞𝑔 𝜋 ) E (□ 𝑒) ≜ E (𝑒) E (□ □) ≜ ∅
In the first rule, 𝜚 ℎ stands for a specialized (that is, type-instantiated and with all binders refreshed) contract of ℎ. The fourth rule for applications, E (( 𝑓 :𝜋) 𝜚 ℎ ā), deals with handler parameters.

The code to which we pass handler ℎ may perform write operations before calling ℎ. These writes are listed as formal pre-writes in contract 𝜋 and they constitute actual potential pre-writes for ℎ. In order to compute the corresponding effect set, we form an abstraction 𝜋 ℎ 𝑥𝑞𝑔 𝜋 , where 𝑥𝑞𝑔 𝜋 denotes the list of all formal parameters of 𝜋, in the order of their appearance in the contract (we use this three-letter notation to remind of the three kinds of parameters a handler can have, namely, term, reference, and handler parameters). In other words, we create a virtual definition, where the actual handler argument ℎ is used to implement the formal handler parameter 𝑓 . The same rule will be applied to the handler parameters in 𝑥𝑞𝑔 𝜋 , which will effectively allow us to verify that the contracts of the handler parameters of ℎ are compatible with what is supplied by 𝜋.

Let us return to the call assign &p 42 g. The contract of assign, which we saw in Section 3, is

(&r: α) (v: α) (return: [r] { r = v }).
Ignoring the precondition of return, which is irrelevant here, the effect of the application is computed as follows:

E ((&r: α) (v: α) (return: [r]) &p 42 g) = E ((v: α) (return: [p]) 42 g) = E ((return: [p]) g) = E (□ □) ∪ E ([p] g) = ∅ ∪ E (□ g) ∪ (p ⊗ □ g) = E (g) ∪ {(p, g)} = E ( 𝜚 g □) ∪ {(p, g)} = {(p, g)}
We do not specify the contract of g, but since this handler takes no parameters (we assume the initial expression to be well-typed), the effect set E ( 𝜚 g □) cannot be anything but empty.

The effect E (𝑋) is undefined when an actual pre-write computed for a handler introduced in 𝑋 (this includes the handler parameters in virtual definitions) is not listed as a formal pre-write in the handler's contract. A program whose effect set is undefined is considered ill-specified and is rejected. In what follows, we assume that all programs we consider have a well-defined effect.

Effect inference. The effect-checking rules above can be used to infer pre-write annotations in user-written code that does not come with ones. Indeed, we can treat missing formal pre-writes as meta-variables designing sets of references, and the conditions of the 𝐸 ⊖ ℎ would supply constraints on those sets that must be satisfied for the program to be acceptable. While multiple solutions are generally possible (it is legal to declare a reference as a formal pre-write even if it is never modified), it is reasonable to look for minimal sufficient annotations by default.

It is important to notice that the solution space is finite. Indeed, the typing rules require any reference listed as a formal pre-write of a handler to be present in the typing context of that handler; thus, there is only a finite number of references that can appear in the pre-write annotation of any handler in our code. The effect sets computed by the E operator are similarly bounded. Indeed, it is easy to see that for any expression or abstraction 𝑋, any handler that occurs in E (𝑋) must freely occur in 𝑋. The same is not necessarily true for references, since a pre-write may be introduced via the contract of a called handler, without occurring explicitly in the call. However, since this handler must be in the scope of the concerned reference, and 𝑋 must be in the scope of the handler, we can conclude that any reference in the effect set of 𝑋 must be visible in 𝑋. No hidden side effects. Our effect system is sufficiently precise to allow effective computation of verification conditions, as we will see in the coming sections. However, this precision comes at a price, as it further restricts the expressiveness of our language by forbidding programs to have hidden side effects.

Consider the code in Figure 3, OCaml version on the left, translation in our syntax on the right. In this example, we omit all functional specification. Function iter is an idiomatic second-order list iterator, and function sum uses it to compute the sum of a list of integers in a local reference r, whose value is then returned as the result.

Handler add on the right changes the value of r before returning control to the caller via ret_add. The effect of the body of add is, according to the contract of assign, the singleton {(r, ret_add)}. This effect does not escape from the definition of add, since ret_add is bound in the definition. Instead, it is compared to the list of formal pre-writes of ret_add in the contract of add; and r is correctly listed as one. This pre-write is the write effect of add when it returns via ret_add. As for the pre-writes of handlers add and out, they should reflect the writes that may be performed during execution of sum before add and out are called. The correct annotation in both cases is [r], since iter may call add several times (and thus modify r before the second call) before calling out.

Unfortunately, our effect system cannot accommodate this code -let us see why. Computing E (iter l add out) requires us, for the first handler parameter add, to compute the effect of the virtual definition E ((i: int) (ret_fn:) add i ret_fn). The effect of the body is {(r, ret_fn)}, according to the pre-write annotation of ret_add in the contract of add. However, r is not listed as a formal pre-write of ret_fn in the contract of fn, and thus the overall effect is undefined. Informally, we cannot pass add as an argument to iter, because add modifies the program state (as reflected in the non-empty pre-write list of ret_add), whereas iter expects a handler without side effects (as reflected in the empty pre-write list of ret_fn).

To make this code accepted, the potential side effects of handler parameter fn in the contract of iter must be listed as formal pre-writes of ret_fn. This requires the concerned references to be visible to iter. One way of doing it is to move the definition of iter inside the scope of r. This approach is similar to implicit inlining of effectful higher-order functions proposed by Filliâtre et al.

[?]. Another possibility is to pass r to iter as an argument. Here is what the specification of iter would look like in this case: iter (&q: int) (l: list int) (fn: [q] (i: int) (ret_fn: [q])) (return: [q]) Despite the fact that iter never touches the reference parameter q in its own code, its handler parameter fn might do so, as reflected in the pre-write of ret_fn. From that, by analysing the body of iter, we can correctly infer that q is potentially modified during the execution of iter before fn or return are called, and so q must appear in their pre-writes, too.

State Elimination. Pre-write annotations allow us to translate an alias-free program with side effects into an equivalent pure program. This is essentially a monadic transformation where the state is passed as an additional parameter from one handler to another. However, effect computation allows us to refine the encoding by only passing the relevant parts of the state. Indeed, the pre-write annotations of a handler ℎ indicate which references accessible to ℎ may have changed their value between the start of the parent of ℎ and the start of ℎ itself. It is (the current values of) these references that must be passed to ℎ as extra parameters. As for other accessible references, their last values can be accessed directly from the lexical context that was established at the start of the parent of ℎ, since those references have not been modified since.

Operator • , defined below, applies to expressions, contracts, and applications. It translates expressions into pure expressions and contracts into contracts without pre-writes or reference parameters. Applications are transformed into sequences of pure arguments followed by abbreviations; these abbreviations are appended to the translated handler call.

ℎ ā ≜ ℎ 𝜚 ℎ ā 𝑒 / γ (ℎ 𝜚 = 𝑑) ≜ 𝑒 / γ (ℎ 𝜚 = 𝑑 ) 𝑒 / &𝑟 = 𝑠 ≜ 𝑒 [𝑟 ↦ → 𝑠] 𝑒 / ℎ 𝜚 → 𝑑 ≜ 𝑒 / ℎ 𝜚 → 𝑑 [𝑝] 𝜚 ≜ ( 𝑝:𝜏 𝑝 ) 𝜚 [𝑝] 𝜚 ā ≜ 𝑝 𝜚 ā (𝑥 :𝜏) 𝜚 ≜ (𝑥 :𝜏) 𝜚 (𝑥 :𝜏) 𝜚 𝑠 ā ≜ 𝑠 𝜚 ā (&𝑞:𝜏) 𝜚 ≜ (𝑞:𝜏) 𝜚 (&𝑞:𝜏) 𝜚 &𝑟 ā ≜ 𝑟 𝜚[𝑞 ↦ → 𝑟] ā ( 𝑓 :𝜋) 𝜚 ≜ ( 𝑓 : 𝜋 ) 𝜚 ( 𝑓 :𝜋) 𝜚 ℎ ā ≜ 𝑓 𝜚 ā / 𝑓 𝜋 → ℎ 𝑥𝑞𝑔 𝜋 □ ≜ □ □ □ ≜ □
Once again, 𝜚 ℎ is a specialized contract of ℎ and 𝑥𝑞𝑔 𝜋 denotes the list of all formal parameters of 𝜋.

We write 𝜏 𝑝 to denote the type of reference 𝑝 in the original program.

Our transformation converts reference parameters and pre-written references into term parameters. To preserve the well-typedness of the transformed code, each actual handler argument is encapsulated in a local abbreviation whose contract is supplied by the corresponding formal handler parameter. Without this precaution, the actual handler argument might have a different arity from what is expected by the callee, due to different formal pre-writes.

Notice that converting pre-writes into term parameters inevitably creates collisions, as each prewrite annotation must be in the scope of the corresponding reference. This is exactly our intention: by the rules of lexical scoping, each occurrence of a given reference is now captured by the closest (innermost) binder, which allows it to be instantiated with a correct value during execution.

Of course, we must also update the specification and semantics of library handlers that manipulate the state. For example, here is the converted contract of assign:

assign (r: α) (v: α) {} (return (r: α) { r = v })
The operational semantics of this pure version is as follows: Λ ⊢ assign 𝑡 𝑠 𝑓 • ∅ -→ 𝑓 𝑠 ∅ • ∅. This rule can be obtained from the original one by applying • to both sides of the rule and then by replacing each former reference argument with its value in the corresponding variable context. The latter is replaced by an empty set (as state elimination removes all references from the program).

In Figure 4, we return to the example from Figure 3, with an added reference parameter for iter (as suggested at the end of Section 4), to ensure that the effects are specified correctly. On the left side of Figure 4, we show the stateful definitions of iter and sum, and on the right side, their stateless encoding. For simplicity, we omit the preconditions and inline the trivial abbreviations generated for handler arguments whose contract has exactly the same pre-writes as the corresponding formal handler parameter. Then the only added abbreviation is onNil in the translated definition of iter. Indeed, library handler unList does not modify the program state, and therefore its handler parameters onCons and onNil have no pre-writes. Handler return, on the other hand, does have a pre-write which becomes a term parameter in translation. Abbreviation onNil → return q allows us to pass return to unList with this term parameter properly instantiated with q. iter (&q: int) (l: list int) (fn: [q] (i: int) (ret_fn: [q])) (return: [q]) = unList l on_cons return / on_cons h t → fn h tail / tail [q] → iter q t fn return sum (l: list int) (return: (s: int)) = iter r l add out / add [r] (i: int) (ret_add: [r]) = assign &r (i + r) ret_add / out [r] → return r / &r = 0 iter (q: int) (l: list int) (fn: (q: int) (i: int) (ret_fn: (q: int))) (return: (q: int)) = unList l on_cons onNil / onNil → return q / on_cons h t → fn q h tail / tail q → iter q t fn return sum (l: list int) (return: (s: int)) = iter 0 l add out / add (r: int) (i: int) (ret_add: (r: int)) = assign r (i + r) ret_add / out (r: int) → return r

Functional Correctness

We equip handler contracts with functional specifications, called preconditions, that describe the expected program state at the beginning of the handler execution. As functional specifications often need to relate the current program state to previous ones, we also add auxiliary variables (or simply auxiliaries) that capture reference values at the start of a handler:

annotation ::= . . . | { formula } | variable = term
The non-terminal formula represents statements in a suitable logical language; we require that data terms can be used inside formulas, and handlers can not. We denote formulas with letters 𝜑 and 𝜓.

Here are the additional rules to compute the free variables and handlers in abstractions:

FV({𝜑} 𝜚 𝑒) ≜ FV( 𝜚 𝑒) ∪ FV(𝜑) FH({𝜑} 𝜚 𝑒) ≜ FH( 𝜚 𝑒) FV((𝑧 = 𝑠) 𝜚 𝑒) ≜ (FV( 𝜚 𝑒) \ { 𝑧 }) ∪ FV(𝑠) FH((𝑧 = 𝑠) 𝜚 𝑒) ≜ FH( 𝜚 𝑒)
Evaluation rules are extended as follows:

Σ ⊢ ({𝜑} 𝜚 𝑒) ā -→ ( 𝜚 𝑒) ā (E-Pre) Σ ⊢ ((𝑧 = 𝑠) 𝜚 𝑒) ā -→ ( 𝜚 𝑒) [𝑧 ↦ → 𝑠 Σ ] ā (E-Aux)
Assuming a predefined typing relation Γ ⊢ 𝜑 : bool for formulas, here are the new typing rules:

Γ ⊢ 𝜑 : bool Γ ⊢ 𝜚 𝑒 : 𝜉 Γ ⊢ {𝜑} 𝜚 𝑒 : 𝜉 (T-Pre) Γ ⊢ 𝑠 : 𝜏 Γ, 𝑧 : 𝜏 ⊢ 𝜚 𝑒 : 𝜉 Γ ⊢ (𝑧 = 𝑠) 𝜚 𝑒 : 𝜉 (T-Aux)
Effect computation and state elimination ignore preconditions and auxiliaries:

E ((𝑧 = 𝑠) 𝜚 𝑒) ≜ E ( 𝜚 𝑒) E ((𝑧 = 𝑠) 𝜚 ā) ≜ E ( 𝜚 ā) E ({𝜑} 𝜚 𝑒) ≜ E ( 𝜚 𝑒) E ({𝜑} 𝜚 ā) ≜ E ( 𝜚 ā) (𝑧 = 𝑠) 𝜚 ≜ (𝑧 = 𝑠) 𝜚 (𝑧 = 𝑠) 𝜚 ā ≜ 𝜚 ā {𝜑} 𝜚 ≜ {𝜑} 𝜚 {𝜑} 𝜚 ā ≜ 𝜚 ā
Verification conditions are produced in a restricted fragment of the first-order language with local predicate definitions. This fragment can be described by the following grammar:

vc ::= ⊤ | vc ∧ vc | formula | formula → vc | ∀ variable : termType . vc | vc / handler (variable : termType) * ≡ vc | handler term *
In this syntax, handlers act as second-order variables that denote locally defined predicates: verification conditions, parametrized by a number of first-order values. Predicate definitions are not recursive and are not type-generalized. Note that vc can not occur in the antecedent of an implication. Moreover, since handlers can not occur in a formula, all occurrences of locally defined predicates and, therefore, of vc are necessarily positive. We denote verification conditions with Φ and Ψ.

Operator V computes the verification condition for a given expression, abstraction or application:

V (ℎ ā) ≜ V ( 𝜚 ★ ℎ ā) V (𝑒 / γ (ℎ 𝜚 = 𝑑)) ≜ V (𝑒 / γ) ∧ V ( 𝜚 𝑑) V (𝑒 / &𝑟 = 𝑠) ≜ V (𝑒) [𝑟 ↦ → 𝑠] V (𝑒 / ℎ 𝜚 → 𝑑) ≜ V (𝑒) / ℎ 𝑝𝑥𝑞𝑧 𝜚 ≡ V (𝑑) V ([𝑝] 𝜚 𝑒) ≜ ∀𝑝 : 𝜏 𝑝 . V ( 𝜚 𝑒) V ([𝑝] 𝜚 ā) ≜ V ( 𝜚 ā) V ((𝑥 :𝜏) 𝜚 𝑒) ≜ ∀𝑥 : 𝜏 . V ( 𝜚 𝑒) V ((𝑥 :𝜏) 𝜚 𝑠 ā) ≜ V ( 𝜚 ā) [𝑥 ↦ → 𝑠] V ((&𝑞:𝜏) 𝜚 𝑒) ≜ ∀𝑞 : 𝜏 . V ( 𝜚 𝑒) V ((&𝑞:𝜏) 𝜚 &𝑟 ā) ≜ V ( 𝜚[𝑞 ↦ → 𝑟] ā) V (( 𝑓 :𝜋) 𝜚 𝑒) ≜ V ( 𝜚 𝑒) V (( 𝑓 :𝜋) 𝜚 ℎ ā) ≜ V ( 𝜚 ā) ∧ V (𝜋 ℎ 𝑥𝑞𝑔 𝜋 ) V ((𝑧 = 𝑠) 𝜚 𝑒) ≜ V ( 𝜚 𝑒) [𝑧 ↦ → 𝑠] V ((𝑧 = 𝑠) 𝜚 ā) ≜ V ( 𝜚 ā) [𝑧 ↦ → 𝑠] V ({𝜑} 𝜚 𝑒) ≜ 𝜑 → V ( 𝜚 𝑒) V ({𝜑} 𝜚 ā) ≜ 𝜑 ∧ V ( 𝜚 ā) V (□ 𝑒) ≜ V (𝑒) V (□ □) ≜ ⊤ 𝜚 ★ ℎ ≜ 𝜚 ℎ { ℎ 𝑝𝑥𝑞𝑧 𝜚 ℎ } if ℎ is an abbreviation, 𝜚 ℎ otherwise.
As before, 𝜚 ℎ is a specialized contract of handler ℎ, 𝜏 𝑝 is the type of reference 𝑝, and 𝑥𝑞𝑔 𝜋 are the formal parameters of contract 𝜋. Local predicate definitions hold verification conditions of handler abbreviations; they are parametrized by the pre-writes, term and reference parameters, and auxiliary variables of the handler's contract 𝜚, collectively denoted 𝑝𝑥𝑞𝑧 𝜚 (the missing type annotations for pre-writes and auxiliaries can be pulled from the typing context). Predicates defined in such a way are added, as an extra precondition, to the contract of the corresponding handler whenever it is executed. We thus prove the instantiated verification condition of the abbreviation body separately at each call site, whereas handler definitions are verified just once, for all possible entry states and parameters.

In what follows, we always simplify the occurrences of ⊤ in verification conditions.

It is important to notice that in the rules for application, we substitute reference arguments early, directly in the contract, but we instantiate term parameters and auxiliary variables late, in the computed verification condition. The reason for the former is that reference parameters of a handler can appear as formal pre-writes of its subsequent handler parameters: for instance, the reference parameter of assign is a pre-write of its handler parameter. These pre-writes will get bound when we verify the virtual definitions for those handler parameters; see the rules for V (( 𝑓 :𝜋) 𝜚 ℎ ā) and V ([𝑝] 𝜚 𝑒). We must therefore instantiate reference parameters early, in order to bind correct variables in ℎ 𝑥𝑞𝑔 𝜋 . On the other hand, term parameters and auxiliaries must not be instantiated early. Indeed, the terms we substitute into them may contain references, but these occurrences represent dereferenced values at the start of the handler call. If we substitute such a term into the contract, it may pass under a pre-write annotation which will turn into a universal quantifier over the reference variable, making it refer to some later value. To make this more clear, let us consider some examples.

Example: Increment. The handler defined below increments a given reference by 1.

incr (&p: int) (o = p) (out: [p] { p = 1 + o }) = assign &p (p + 1) out

Let us compute the verification condition of the corresponding abstraction.

V ((&p:int) (o = p) (out: [p] { p = 1 + o }) assign &p (p + 1) out) = ∀ p:int . V ((o = p) (out: [p] { p = 1 + o }) assign &p (p + 1) out) = ∀ p:int . V ((out: [p] { p = 1 + o }) assign &p (p + 1) out) [o ↦ → p] = ∀ p:int . V (□ assign &p (p + 1) out) [o ↦ → p] = ∀ p:int . V (assign &p (p + 1) out) [o ↦ → p] = ∀ p:int . V ((&r:int) (v:int) (return: [r] { r = v }) &p (p + 1) out) [o ↦ → p] = ∀ p:int . V (((v:int) (return: [r] { r = v })) [r ↦ → p] (p + 1) out) [o ↦ → p] = ∀ p:int . V ((v:int) (return: [p] { p = v }) (p + 1) out) [o ↦ → p] = ∀ p:int . V ((return: [p] { p = v }) out) [v ↦ → p + 1] [o ↦ → p] = ∀ p:int . (V (□ □) ∧ V ([p] { p = v } out)) [v ↦ → p + 1] [o ↦ → p] = ∀ p:int . (⊤ ∧ ∀ p:int . V ({ p = v } out)) [v ↦ → p + 1] [o ↦ → p] = ∀ p:int . (∀ p:int . p = v → V (□ out)) [v ↦ → p + 1] [o ↦ → p] = ∀ p:int . (∀ p:int . p = v → V (out)) [v ↦ → p + 1] [o ↦ → p] = ∀ p:int . (∀ p:int . p = v → V ([p] { p = 1 + o } □)) [v ↦ → p + 1] [o ↦ → p] = ∀ p:int . (∀ p:int . p = v → V ({ p = 1 + o } □)) [v ↦ → p + 1] [o ↦ → p] = ∀ p:int . (∀ p:int . p = v → p = 1 + o ∧ V (□ □)) [v ↦ → p + 1] [o ↦ → p] = ∀ p:int . (∀ q:int . q = v → q = 1 + o ∧ ⊤) [v ↦ → p + 1] [o ↦ → p] = ∀ p:int . ∀ q:int . q = p + 1 → q = 1 + p
The topmost universal quantifier binds the reference parameter of incr. The underlying formula is the verification condition of the definition body, that is, of the assign call. Since assign does not have preconditions, we only need to verify that the postcondition of assign (i.e., the precondition of its formal handler parameter return) implies the precondition of out. Since the handler parameter of assign has a formal pre-write -the modified reference p which replaced the formal reference parameter r -the implication must be universally quantified over p. In other words, the postcondition of incr must hold for every value of p that satisfies the postcondition of assign.

Example: Russian Peasant Multiplication. The code in Figures 5 and6, written first in OCaml and then in our language, implements the classical Russian peasant multiplication algorithm. For simplicity, we define the algorithm on natural numbers and use Euclidean division and remainder operators in terms. This code produces the following verification condition:

∀ a : nat . ∀ b : nat . a • b + 0 = a • b ∧ ∀ p : nat . ∀ q : nat . ∀ r : nat . p • q + r = a • b → (q > 0 → next) ∧ (q ≯ 0 → last) / last ≡ r = a • b / next ≡ (q mod 2 = 1 → write_r) ∧ (q mod 2 ≠ 1 → write_p r) / write_r ≡ ∀ v : nat . v = r + p → write_p v / write_p (r : nat) ≡ ∀ v : nat . v = p + p → write_q v r / write_q (p : nat) (r : nat) ≡ ∀ v : nat . v = q div 2 → p • v + r = a • b
Notice that the first conjunct a • b + 0 = a • b generated by the initial call to loop corresponds exactly to the initialisation of a loop invariant. Similarly, the assertion p • v + r = a • b coming from the second, let product (a: nat) (b: nat) : nat = let p,q,r = ref a, ref b, ref 0 in while !q > 0 do if !q mod 2 = 1 then r := !r + !p; p := !p + !p; q := !q div 2 done; !r recursive, call to loop, corresponds to the preservation of the invariant after a single iteration. In a traditional functional language, encoding loops as tail-recursive functions is slightly more difficult, since one also has to provide (and then prove) a postcondition. In our translation, when the loop condition becomes false, we simply call the after-the-loop continuation return r.

c: nat) { c = a • b }) = loop / loop [p] [q] [r] { p • q + r = a • b } = if (q > 0) next last / last → return r / next → if (q mod 2 = 1)
Termination proof. Assuming that library handlers always terminate (meaning that they either halt or return to the caller by executing one of their handler parameters), the only potential source of divergence in our language are recursive handler definitions. Indeed, without those, any program can be translated into a stateless one, as shown in Section 4, and then into a typed lambda-term, which are known to be strongly normalizing [?].

We can prove that a given recursive definition cannot loop on itself forever by associating a certain measure to the handler entry state and by showing that each recursive call makes this measure decrease with respect to some well-founded ordering.

Let us select some type 𝜃 and a well-founded relation ≺ on it. If we want to prove a recursive definition group γ to be well-founded, we place into the contract of each handler ℎ in γ a distinctive variant auxiliary (or simply variant) ( ûℎ = 𝑠 ℎ ) of type 𝜃. We only recognize variant auxiliaries in the contracts of handlers introduced through definitions (but not in abbreviations or handler parameters), and we allow at most one variant in a contract. Now we extend the V rule for handler calls as follows:

𝜚 ★ ℎ ≜                      𝜚 ℎ { ℎ 𝑝𝑥𝑞𝑧 𝜚 ℎ } if ℎ is an abbreviation, 𝜚 ℎ { û ≺ v } if û is a variant auxiliary in 𝜚 ℎ ,
v appears in the current typing context, v is a variant auxiliary of handler 𝑔, and 𝑔 is ℎ or defined in the same group as ℎ, 𝜚 ℎ otherwise.

The condition " v appears in the current typing context" verifies that handler ℎ is used -i.e., called directly or passed as a handler argument -inside the definition of handler 𝑔, which can be either ℎ itself or its sibling from the same definition group. In other words, we only add the extra precondition for recursive calls (passing a handler argument is treated as a call in a virtual definition), when both handlers have a variant auxiliary. Apart from this added precondition, variants are treated in exactly the same way as ordinary auxiliary variables with respect to typing, evaluation, etc. It is possible to use different types and orderings for variants in different definition groups, but inside a single group, all variants must be of the same type and must be compared via the same well-founded relation.

To prove termination of product, we add a variant (û = q) to the contract of loop. Notice that product itself is not recursively defined and therefore does not need a variant. This results in the following verification condition:

∀ a : nat . ∀ b : nat . a • b + 0 = a • b ∧ ∀ p : nat . ∀ q : nat . ∀ r : nat . p • q + r = a • b → (q > 0 → next) ∧ (q ≯ 0 → last) / last ≡ r = a • b / next ≡ (q mod 2 = 1 → write_r) ∧ (q mod 2 ≠ 1 → write_p r) / write_r ≡ ∀ v : nat . v = r + p → write_p v / write_p (r : nat) ≡ ∀ v : nat . v = p + p → write_q v r / write_q (p : nat) (r : nat) ≡ ∀ v : nat . v = q div 2 → p • v + r = a • b ∧ v < q
Notice that the extra precondition only appears when loop is used in its own definition, but not when it is called from product at the beginning. The standard ordering < is well-founded on N; if we used integers, we would have to add a precondition to loop requiring q to be non-negative -and similarly for product and b -and use the ordering relation 𝑢 < 𝑣 ∧ 𝑣 ⩾ 0 which is well-founded on Z. The relation 0 ⩽ 𝑢 < 𝑣 would work in this example, too, but is much less useful in the general case, where we often need to admit a negative number of the left-hand side.

Elimination of predicate definitions. If we want to use automated theorem provers to discharge verification conditions, we have to translate them into a format understood by those provers: usually, some variation of the first-order language. Assuming that user-written preconditions in our code are already first-order1, local predicate definitions are the only feature of verification conditions that may require translation. One method to eliminate predicate definitions is simply to inline them (remember that they cannot be recursive). By doing this, we obtain a logical formula that is very close to what is produced by the classical Dijkstra-style weakest precondition calculus. For example, below is the verification condition for product (without variant), obtained in this fashion. In addition to predicate inlining, we also simplify occurrences of (∀𝑥. 𝑥 = 𝑠 → Φ) to Φ[𝑥 ↦ → 𝑠], when term 𝑠 does not contain 𝑥:

∀ a : nat . ∀ b : nat . a • b + 0 = a • b ∧ ∀ p : nat . ∀ q : nat . ∀ r : nat . p • q + r = a • b → (q > 0 → (q mod 2 = 1 → (p + p) • (q div 2) + (r + p) = a • b) ∧ (q mod 2 ≠ 1 → (p + p) • (q div 2) + r = a • b)) ∧ (q ≯ 0 → r = a • b)
A well-known inconvenience of this method is that whenever some code fragment is reachable via two different code paths -which in our language is expressed by an abbreviation that is called from two different points in the underlying expression -its weakest precondition will appear twice in the verification condition. An example of this in the code of product is the write_p handler, called once from next and once from write_r. By chaining such constructions, we can easily come up with examples that demonstrate exponential growth of verification conditions compared to the size 1In our examples, we do not distinguish between bool-typed terms and formulas, but this is rather easy to handle. of the original program. Indeed, a simple sequence of conditional statements suffices to produce an oversized verification condition.

A different method of verification condition generation was proposed by Flanagan and Saxe [?]. It consists in computing a single formula that describes all code paths leading to a given sequence point, and avoids the combinatorial explosion in a large number of cases, including all While programs that do not use exceptions. The trade-off here is the increased complexity of the resulting formula. Leino demonstrated that verification conditions produced by this method can be obtained by interweaving application of classical procedures for the strict and liberal weakest precondition computation [?].

Below we show that these "compact" verification conditions can be also obtained directly from our verification conditions by a chain of truth-preserving transformations. Moreover, at any point of this process we can resort to inlining, meaning that we can freely mix the classical and the compact approaches in the same verification condition, balancing its complexity against its size.

Consider a verification condition of the form Φ / ℎ (𝑥 1 : 𝜏 1 ) . . . (𝑥 𝑛 : 𝜏 𝑛 ) ≡ Φ ℎ . We assume that Φ contains no predicate definitions; if it does, we eliminate them first. Then the grammar of verification conditions ensures that each application of ℎ in Φ occurs at a positive position, under a number of conjunctions, implications, and universal quantifiers. We want to rearrange Φ in such a way that multiple applications of ℎ in it are merged into one. Once we obtain an equivalent verification condition Φ ′ / ℎ (𝑥 1 : 𝜏 1 ) . . . (𝑥 𝑛 : 𝜏 𝑛 ) ≡ Φ ℎ , where ℎ is only applied once inside Φ ′ , we can inline the predicate definition without increasing the size of Φ ′ .

Our first step is to abstract out the different arguments passed to ℎ in Φ. We pick 𝑛 fresh variables 𝑧 1 , . . . , 𝑧 𝑛 and consider the following verification condition:

∀𝑧 1 : 𝜏 𝑛 . . . . ∀𝑧 𝑛 : 𝜏 𝑛 . (Φ 0 / ℎ (𝑥 1 : 𝜏 𝑛 ) . . . (𝑥 𝑛 : 𝜏 𝑛 ) ≡ Φ ℎ ),
where formula Φ 0 is obtained from Φ by replacing each occurrence of ℎ 𝑠 1 . . . 𝑠 𝑛 with

(𝑧 1 = 𝑠 1 ∧ • • • ∧ 𝑧 𝑛 = 𝑠 𝑛 ) → ℎ 𝑧 1 . . . 𝑧 𝑛 .
It is obvious that the new verification condition is well-typed (as predicate definitions are not typegeneralized) and equivalent to the initial one. Indeed, the universal quantifiers over 𝑧 1 , . . . , 𝑧 𝑛 can be pushed down in Φ 0 , and ∀ z . ( z = s → ℎ z) is equivalent to ℎ s -since variables z are fresh, they cannot occur in terms s. Now we can move the occurrences of subformulas (𝜑 → ℎ z) up in Φ 0 , and merge them when two or more appear in the same conjunction. To this end, we apply to Φ 0 the following rewriting rules, starting from the lowermost subformulas:

(𝜑 1 → ℎ z) ∧ (𝜑 2 → ℎ z) =⇒ (𝜑 1 ∨ 𝜑 2 ) → ℎ z 𝜑 1 → (𝜑 2 → ℎ z) =⇒ (𝜑 1 ∧ 𝜑 2 ) → ℎ z 𝜑 1 → ((𝜑 2 → ℎ z) ∧ Ψ) =⇒ ((𝜑 1 ∧ 𝜑 2 ) → ℎ z) ∧ (𝜑 1 → Ψ) ∀ ȳ. (𝜑 → ℎ z) =⇒ (∃ ȳ. 𝜑) → ℎ z ∀ ȳ. ((𝜑 → ℎ z) ∧ Ψ) =⇒ ((∃ ȳ. 𝜑) → ℎ z) ∧ ∀ ȳ. Ψ
Here we assume that Ψ contains no occurrences of ℎ z and we treat conjunction modulo associativity and commutativity. In the last two rules, we use the fact that variables z are bound above the definition of ℎ, and thus variables ȳ cannot occur in formula ℎ z. Again, it is easy to see that each rewriting step produces an equivalent formula.

We stop when the formula under the definition of ℎ contains only one application of ℎ; at that point we can simply inline the definition. It is also perfectly possible to inline some of the applications of ℎ at the very beginning, directly in Φ, instead of merging them with the other applications. This selective handling allows us to consider some code paths separately from the others, e.g., because they require some special proof techniques.

Notice that this approach still does not eliminate the possibility of exponential growth: the third rewriting rule duplicates formula 𝜑 1 . more elaborate analysis of sources of explosion + correspondence to Flanagan and Saxe VCs.

Here is the first-order verification condition obtained by merging two applications of write_p in the original verification condition. All other predicate variables are applied only once, and thus their definitions can be inlined directly. As before, we simplify the trivial variable definitions.

∀ a : nat . ∀ b : nat . a • b + 0 = a • b ∧ ∀ p : nat . ∀ q : nat . ∀ r : nat . p • q + r = a • b → (q > 0 → ∀ z : nat . ((q mod 2 = 1 ∧ z = r + p) ∨ (q mod 2 ≠ 1 ∧ z = r)) → (p + p) • (q div 2) + z = a • b)) ∧ (q ≯ 0 → r = a • b)
Show how this also allows to infer postconditions: must lift all the way up, not just until the single occurrence

Ghost Code

In the practice of deductive verification, the term "ghost code" refers to the parts of our program that do not participate in the computation of the final result but help writing adequate specification and verifying the program correctness. In the last section, we saw two examples of ghost code: auxiliary variable o in the contract of incr and variant auxiliary û for the loop in product. Without the former, we are unable to write the postcondition of incr, and we need the latter to prove termination of loop -but none of these variables affects the actual computation. Indeed, we can erase them from our code, together with the preconditions that may depend on them, without changing the behaviour of the program in any meaningful way.

Ghost code is a versatile and powerful instrument. Local ghost variables and ghost function parameters allow us to better describe the progression of an algorithm; for example, when looking for a maximal element in an array, we may use a ghost variable to store the index of the current best candidate, eliminating the need in an existential quantifier in the loop invariant. Ghost fields in data structures can provide a mathematical model of the data, independent of the implementation details, so that the operations on the data structure can be specified in terms of the abstract model rather than concrete implementation. One can even write an entire ghost reimplementation of a program, to be executed in lockstep with the original code, so that the correctness proof of one version could be transferred to the other [?].

From the point of view of type-checking, evaluation, effect analysis or VC generation, ghost code and ghost data are treated in exactly the same way as non-ghost, or material, parts of our program. Moreover, we want to use the same data types and operations over material and ghost data, without introducing a parallel standard library for ghost integers, ghost references, ghost arrays, etc. We must however ensure that ghost code in our program does not affect the material computation, that it can be erased from the program without changing its flow or outcome. One can see ghost data as a sort of classified information that should never leak to the lower-security material code. One way to verify this non-interference property is to recognize ghost data at the type level and use the typing rules to track dependencies between values, so that the material computation is never contaminated by ghost data. Filliâtre et al. used this approach in their formal framework for ghost code in a functional language with polymorphic types and mutable state [?].

In this work, we explore a slightly different method. Assuming that every variable in our code is explicitly marked as material or ghost, we determine which parts of our program can be safely skipped, as they produce no material data for subsequent computation nor make a choice between different continuations. Then we "deghostify" our program: we erase all ghost parameters and ghost values, and all skippable expressions. If the resulting program is well-formed, we know that ghost data is never leaked in the material computation, and the original program is admissible. If, on the other hand, we are left with code where a handler expecting a material parameter is given a ghost argument, and this handler call can not be skipped -then we have found an interference and must reject the program.

This analysis crucially depends on the functional correctness of our program -in particular, on its termination proof. Indeed, if some part of code may diverge, it obviously can not be erased, as that would alter the set of possible behaviours (unless the divergence is the only possible behaviour). Consequently, in order to see what expressions are skippable, we must annotate our well-founded recursive definitions with variants and prove the termination.

Let us proceed to formal definitions. We identify each variable name as either material or ghost. This denomination is extended to data terms: a term is considered ghost if it contains occurrences of ghost variables, otherwise it is material. In our examples, we will distinguish ghost variables by starting them with a capital letter. In our formal rules, to indicate the status of a variable or term 𝑋, we write • 𝑋 and • 𝑋 to say "ghost 𝑋" and "material 𝑋", respectively. In absence of such an indicator, 𝑋 can be either material or ghost, unless its status is established elsewhere. Handlers and expressions are not considered ghost or material.

An expression in a program is called unrestrained if it contains a recursive definition without a variant or is itself the right-hand side of such a definition; otherwise it is restrained. Assuming that no handler in our code is introduced twice, we say that handler ℎ is escaping when it satisfies one of the three conditions:

• ℎ is a library handler whose evaluation may diverge or halt;

• ℎ is a handler parameter;

• ℎ is introduced via a definition ℎ 𝜚 = 𝑑 or an abbreviation ℎ 𝜚 → 𝑑, where 𝑑 is unrestrained or FH( 𝜚 𝑑) contains an escaping handler.

This definition is circular for recursively defined handlers, as they freely occur in their own bodies. We resolve the ambiguity by considering the minimal set of escaping handlers. Then the status of each handler in the program can be effectively determined by proceeding top-down (i.e., from right to left) and by computing the least fixed point when treating recursive definitions with variants. Identifying escaping handlers is important for code flow analysis, as they do not always return to the caller via one of their handler parameters. Instead, they may escape either by halting the program (imagine a library handler exit), or by entering a non-terminating computation, or by passing control to some other escaping handler. We consider that handler parameters, whose actual implementation is a priori unknown, may always escape. Alternatively, we could introduce escaping as a new effect annotation in contracts and distinguish between escaping and non-escaping handler parameters.

An expression 𝑒 is skippable up to handler ℎ whenever the following conditions are satisfied:

1. 𝑒 is inside the scope of ℎ;

2. ℎ does not have handler parameters and all term and reference parameters of ℎ are ghost;

3. all formal pre-writes of ℎ that appear in E (𝑒) are ghost; 4. 𝑒 is restrained;

5. every escaping handler in FH(𝑒) \ {ℎ} is introduced via a definition or an abbreviation whose right-hand side is skippable up to ℎ.

Any expression that is skippable to handler ℎ can be replaced with a call to ℎ when we erase ghost data from our program. Indeed, ℎ is accessible from that position and would not require arguments. The skipped expression does not modify material references accessible to ℎ and does not diverge, meaning that no observable effects are lost when we skip it. The last condition ensures that the target handler cannot be bypassed: every escaping handler in the skipped expression is either ℎ itself or can be replaced with ℎ. Here, we only need to consider escaping handlers, as the non-escaping ones must necessarily return to the caller via one of the handler parameters. An expression can be skippable up to multiple handlers. Indeed, if expression 𝑒 is skippable up to handler ℎ, and the body of ℎ is itself skippable up to handler 𝑔, then 𝑒 is also skippable up to 𝑔. In a practical implementation, we would obviously want to skip as far as we can.

Condition 5 above is circular on recursive definitions. If there are other escaping handlers in the definition body that are not introduced in the same definition group (this includes the formal handler parameters), the ambiguity is lifted. A recursive definition group that does not include any escaping handler from the outside of the group is obviously divergent, as the computation has no way to leave the confines of that group. Then it either has an unrestrained right-hand side, breaking the circularity by condition 4, or its "termination" is proved due to a contradiction in premises, meaning that these definitions are unreachable code. In the latter case, we can indeed replace the right-hand sides with any suitable handler, provided that conditions 1-3 are respected.

Operator • applies to expressions, contracts, and applications. It removes skippable subexpressions, ghost parameters, and preconditions from expressions and contracts. It converts applications into sequences of material arguments followed by abbreviations; these abbreviations are appended to the translated handler call. This operator is partial: it is undefined whenever ghost data is passed to material code. In this case, the original program is considered invalid and is rejected.

𝑒 ≜ ℎ □ if 𝑒 is skippable up to handler ℎ, ⌊𝑒⌋ otherwise. ⌊ℎ ā⌋ ≜ ℎ 𝜚 ℎ ā ⌊𝑒 / γ (ℎ 𝜚 = 𝑑)⌋ ≜ 𝑒 / γ (ℎ 𝜚 = 𝑑 ) ⌊𝑒 / &•𝑟 = •𝑠⌋ ≜ 𝑒 / &𝑟 = 𝑠 ⌊𝑒 / ℎ 𝜚 → 𝑑⌋ ≜ 𝑒 / ℎ 𝜚 → 𝑑 ⌊𝑒 / &•𝑟 = •𝑠⌋ is undefined ⌊𝑒 / &•𝑟 = 𝑠⌋ ≜ 𝑒 [• 𝑝] 𝜚 ≜ [𝑝] 𝜚 [• 𝑝] 𝜚 ā ≜ 𝜚 ā (•𝑥 :𝜏) 𝜚 ≜ (𝑥 :𝜏) 𝜚 (•𝑥 :𝜏) 𝜚 •𝑠 ā ≜ 𝑠 𝜚 ā (&•𝑞:𝜏) 𝜚 ≜ (&𝑞:𝜏) 𝜚 (&•𝑞:𝜏) 𝜚 &•𝑟 ā ≜ &𝑟 𝜚[𝑞 ↦ → 𝑟] ā ( 𝑓 :𝜋) 𝜚 ≜ ( 𝑓 : 𝜋 ) 𝜚 ( 𝑓 :𝜋) 𝜚 ℎ ā ≜ 𝑓 𝜚 ā / 𝑓 𝜋 → ℎ 𝑥𝑞𝑔 𝜋 (•𝑧 = •𝑠) 𝜚 ≜ (𝑧 = 𝑠) 𝜚 (•𝑧 = •𝑠) 𝜚 ā ≜ 𝜚 ā □ ≜ □ □ □ ≜ □ (•𝑧 = •𝑠) 𝜚 is undefined (•𝑥 :𝜏) 𝜚 •𝑠 ā is undefined (•𝑧 = •𝑠) 𝜚 ā is undefined (&•𝑞:𝜏) 𝜚 &•𝑟 ā is undefined [• 𝑝] 𝜚 ≜ 𝜚 [• 𝑝] 𝜚 ā ≜ 𝜚 ā (•𝑥 :𝜏) 𝜚 ≜ 𝜚 (•𝑥 :𝜏) 𝜚 𝑠 ā ≜ 𝜚 ā (&•𝑞:𝜏) 𝜚 ≜ 𝜚 (&•𝑞:𝜏) 𝜚 &•𝑟 ā ≜ 𝜚 ā (•𝑧 = 𝑠) 𝜚 ≜ 𝜚 (•𝑧 = 𝑠) 𝜚 ā ≜ 𝜚 ā {𝜑} 𝜚 ≜ 𝜚 {𝜑} 𝜚 ā ≜ 𝜚 ā (&•𝑞:𝜏) 𝜚 &•𝑟 ā ≜ 𝜚 ā if pre-write [𝑞]
does not occur anywhere in 𝜚, undefined otherwise.

As before, 𝜚 ℎ is a specialized contract of ℎ and 𝑥𝑞𝑔 𝜋 are the formal parameters of 𝜋. The first rule replaces a skippable expression with a call to an appropriate handler; if the expression can not be skipped, we analyse it piece by piece. The three rules for reference allocation demonstrate three fundamental cases in ghost code elimination: a material reference initialized with a material term is admitted, a material reference initialized with a ghost term is rejected, and, finally, a ghost reference is removed from the program regardless of how it is initialized.

We see these three cases again in the three groups of rules for contracts and applications. Material parameters and material arguments passed for them are admitted; and so are material pre-writes, as well as handler parameters and arguments. Ghost values supplied for material parameters or material auxiliary variables are rejected. Ghost pre-writes, parameters, and auxiliaries are removed; and so are preconditions which may depend on them.

One special case is passing a material reference argument for a ghost formal reference parameter. The called handler expects a ghost reference, and so whatever data it puts there should be considered ghost: we cannot let material code access this data. Thus, if anywhere in the called handler's contract, we see a pre-write into this reference parameter, we reject the program. Otherwise, if no modification is announced, we consider the application safe and simply remove the parameter and the argument. But what happens if the called handler modifies its ghost reference parameter and then escapes by calling some other handler in its context? This write effect would not appear anywhere in the contract: there we only find the pre-writes that are seen by the handler parameters.

The non-interference in this case is ensured by the alias safety. Indeed, neither the called handler nor the handlers in its context can be in the scope of the material reference that we pass as an argument. This means that if the called handler escapes, the subsequent computation loses access to the original material reference. On the other hand, if the called handler returns via one of the handler parameters, the write effect has to be accounted for in the contract, as hidden effects are not allowed. To sum up, we admit passing a material reference argument for a ghost reference parameter in exactly those cases where we can make a ghost copy of the original reference and pass the copy instead. examples Inference: add ghost annotations, allowing more handlers to be checkpoints and allowing more computations to be skipped (due to references becoming ghost). We do not aim for complete analysis, and various policies of convenience are possible. One similar to that of Why3 is as follows: -an allocated reference is marked ghost if its initialisation term is ghost -a parameter of a defined partial handler f is marked ghost if f ever receives a ghost argument in that position (either directly or via Impl) -all reference, term, and total handler parameters of a defined partial handler f are marked ghost, if f is ever passed as an argument in a call to a total handler that we will have to skip (due to a ghost argument passed for a non-ghost parameter, either directly or via Impl). -we never modify the signatures of handler parameters, library handlers or total defined handlers: these are expected to be correctly specified by the programmer.

Index

𝜚 𝑒, abstraction, 4 𝜚 ā, application, 4 𝑥 = 𝑠, auxiliary variable, 15 _, dummy handler, 4 ⊗, ⊖, effect operations, 11 E (𝑒), effect set, 11, 15 □, empty sequence, 4 evaluation,5,9,11,15 FH,free handlers,5,9,11,15 FV,free variables,5,9,11,

Λ ⊢ 𝑒 • Σ → 𝑒 ′ • Σ ′ ,
ℎ ↦ → 𝜚 𝑑 ∈ Λ Σ ⊢ ( 𝜚 𝑑) ā -→ * (□ 𝑒) □ Λ ⊢ ℎ ā • Σ -→ 𝑒 • Σ (E-Call) Λ, ℎ ↦ → 𝜚 𝑑 ⊢ 𝑒 / γ • Σ -→ 𝑒 ′ / γ • Σ ′ Λ ⊢ 𝑒 / γ (ℎ 𝜚 = 𝑑) • Σ -→ 𝑒 ′ / γ (ℎ 𝜚 = 𝑑) • Σ ′ (E-Defn) Λ, ℎ ↦ → 𝜚 𝑑 ⊢ 𝑒 • Σ -→ 𝑒 ′ • Σ ′ Λ ⊢ 𝑒 / ℎ 𝜚 → 𝑑 • Σ -→ 𝑒 ′ / ℎ 𝜚 → 𝑑 • Σ ′ (E-Abbr) Λ ⊢ 𝑒 • Σ, 𝑟 ↦ → 𝑠 Σ -→ 𝑒 ′ • Σ ′ , 𝑟 ↦ → 𝑡 Λ ⊢ 𝑒 / &𝑟 = 𝑠 • Σ -→ 𝑒 ′ / &𝑟 = 𝑡 • Σ ′ (E-

  abbreviation ::= handler contract → expression definition ::= handler contract = expression contract ::= annotation * annotation ::= variable : termType | handler : contract

  Figure 1: Simple OCaml program.

Figure 2 :

 2 Figure 2: The program from Fig. 1, translated.

Figure 3 :

 3 Figure 3: Illicit hidden side effects.

Figure 4 :

 4 Figure 4: Program with side effects (left) and its stateless encoding (right)

Figure 5 :

 5 Figure 5: Russian Peasant Multiplication in OCaml.

Figure 6 :

 6 Figure 6: Russian Peasant Multiplication, translated.

  Alloc) Σ ⊢ ([𝑝] 𝜚 𝑒) ā -→ ( 𝜚 𝑒) ā (E-Eff) Σ ⊢ ((𝑥 :𝜏) 𝜚 𝑒) 𝑠 ā -→ ( 𝜚 𝑒) [𝑥 ↦ → 𝑠 Σ ] ā (E-AppT) Σ ⊢ ((&𝑞:𝜏) 𝜚 𝑒) &𝑟 ā -→ ( 𝜚 𝑒) [𝑞 ↦ → 𝑟] ā (E-AppR) Σ ⊢ ((𝑔:𝜋) 𝜚 𝑒) 𝑓 ā -→ ( 𝜚 𝑒) [𝑔 ↦ → 𝑓 ] ā (E-AppH) Γ ⊢ 𝜑 : bool Γ ⊢ 𝜚 𝑒 : 𝜉 Γ ⊢ {𝜑} 𝜚 𝑒 : 𝜉 (T-Pre)Above, the "non-rule" T-AppR 0 , included for comparison with T-AppR, does not prevent aliases.

Figure 11 :

 11 Figure 11: Typing rules.

  15 •𝑥, •𝑠, ghost variable, term, 22 𝑒 , ⌊𝑒⌋, ghost code elimination, 23 ℎ 𝜚 → 𝑒, handler abbreviation, 4 ℎ ā, handler call, 4 ℎ 𝜚 = 𝑒, handler definition, 4 ℎ:𝜚, handler parameter, 4 •𝑥, •𝑠, material variable, term, 22 [𝑟], pre-write annotation, 11 {𝜑}, precondition, 15 &𝑟 = 𝑠, reference allocation, 9 &𝑟:𝜏, reference parameter, 9 &𝑟, reference variable, 9 𝜚 ℎ , specialized contract, 12 𝑒 , state elimination, 14, 15 𝑠 Σ , term normalization, 4 𝑥:𝜏, term parameter, 4 Γ ⊢ 𝑒 : 𝜉, typing, 4, 7, 10, 11, 15 V, verification condition, 16, 18 &𝑟:𝜏, 9 term, 𝑥:𝜏, 4 pre-write annotation, [𝑟], 11 precondition, {𝜑}, 15 reference allocation, &𝑟 = 𝑠, 9 reference variable, &𝑟, 9 restrained expression, 22 skippable expression, 22 specialized contract, 𝜚 ℎ , 12 state elimination, 𝑒 , 14, 15

	effect set, E (𝑒), 11, 15
	empty sequence, □, 4
	escaping handler, 22
	𝜋 ℎ 𝑥𝑞𝑔 𝜋 , virtual definition, 12 ⊥, void type, 7 abstraction, 𝜚 𝑒, 4 actual pre-write, 11 annotation, 4, 9, 11, 15 auxiliary variable, 𝑥 = 𝑠, 15 handler parameter, ℎ:𝜚, 4 pre-write, [𝑟], 11 precondition, {𝜑}, 15 reference parameter, &𝑟:𝜏, 9 term parameter, 𝑥:𝜏, 4 application, 𝜚 ā, 4 auxiliary variable, 𝑥 = 𝑠, 15 closed expression, 5 contract, 4, 9, 11, 15 specialized, 𝜚 ℎ , 12 ghost, •𝑠, 22 material, •𝑠, 22 term normalization, 𝑠 Σ , 4 type, 4, 7 substitution, 7 variable, 7 void, ⊥, 7 typing, Γ ⊢ 𝑒 : 𝜉, 4, 7, 10, 11, 15 typing context, 4, 7, 10 variable, 4 auxiliary, 𝑥 = 𝑠, 15 evaluation context, 5, 9 free, FV, 5, 9, 11, 15 ghost, •𝑥, 22 material, •𝑥, 22 reference, &𝑟, 9 variant auxiliary, 18 verification condition, 15 generation, V, 16, 18 virtual definition, 𝜋 ℎ 𝑥𝑞𝑔 𝜋 , 12 reference, term, 4 evaluation, Λ ⊢ 𝑒 • Σ → 𝑒 ′ • Σ ′ , 5, 9, 11, 15 evaluation context, 5, 9 expression, 4 closed, 5 restrained, 22 skippable, 22 formal pre-write, 11 formula, 15 free handlers, FH, 5, 9, 11, 15 free variables, FV, 5, 9, 11, 15 ghost term, •𝑠, 22 variable, •𝑥, 22 ghost code elimination, 𝑒 , ⌊𝑒⌋, 23 handler, 4 abbreviation, ℎ 𝜚 → 𝑒, 4 call, ℎ ā, 4 contract, 4, 9, 11, 15 definition, ℎ 𝜚 = 𝑒, 4 dummy, _, 4 escaping, 22 evaluation context, 5 free, FH, 5, 9, 11, 15 library, 6 library handler, 6 access, 9 alloc, 9 assign, 9-12, 14 div, 6 if, 6 mod, 6 unList, 6 material term, •𝑠, 22 variable, •𝑥, 22 parameter, 4, 9 handler, ℎ:𝜚, 4 void type, ⊥, 7
	dummy handler, _, 4
	effect operations, ⊗, ⊖, 11

omit the prefix. Library handlers are always fully generalized. For example, the type of unList is ⟨α⟩ list α → (α → list α → ⊥) → ⊥ → ⊥. We denote expression types with letters 𝜉 and 𝜁.Typing judgements Γ ⊢ 𝑋 : 𝜉, where 𝑋 is an expression, a contract or an abstraction, are made under typing context Γ, which binds variables to term types and handlers to handler types. The types of library handlers are always present in Γ. Here are the typing rules:ℎ : ⟨ ᾱ⟩ 𝜉 ∈ Γ Γ ⊢ ℎ □ : 𝜉 [ ᾱ ↦ → τ] (T-Call) Γ ⊢ ℎ ā : 𝜏 → 𝜉 Γ ⊢ 𝑠 : 𝜏 Γ ⊢ ℎ ā 𝑠 : 𝜉 (T-AppT) Γ ⊢ 𝜚 𝑑 : 𝜉 Γ, ℎ : 𝜉 ⊢ 𝑒 : ⊥ Γ ⊢ 𝑒 / ℎ 𝜚 → 𝑑 : ⊥ (T-Abbr) Γ ⊢ ℎ ā : 𝜁 → 𝜉 Γ ⊢ 𝑔 □ : 𝜁 Γ ⊢ ℎ ā 𝑔 : 𝜉 (T-AppH) Γ ⊢ 𝜚 : 𝜉 Γ, ℎ : ⟨ ᾱ⟩ 𝜉 ⊢ 𝑒 / (_ 𝜚 → 𝑑) / γ : ⊥ no type variable in ᾱ is free in Γ Γ ⊢ 𝑒 / γ (ℎ 𝜚 = 𝑑) : ⊥ (T-Defn) Γ, _ : ⊥ ⊢ 𝜋 _ □ : 𝜁 Γ ⊢ 𝜋 : 𝜁(T-Contract) Γ, 𝑥 : 𝜏 ⊢ 𝜚 𝑒 : 𝜉 Γ ⊢ (𝑥 :𝜏) 𝜚 𝑒 : 𝜏 → 𝜉 (T-ParT)

Σ ⊢ ((𝑧 = 𝑠) 𝜚 𝑒) ā -→ ( 𝜚 𝑒) [𝑧 ↦ → 𝑠 Σ ] ā (E-Aux) Σ ⊢ ({𝜑} 𝜚 𝑒) ā -→ ( 𝜚 𝑒) ā (E-Pre)Figure10: Operational semantics.ℎ : ⟨ ᾱ⟩ 𝜉 ∈ Γ Γ ⊢ ℎ □ : 𝜉 [ ᾱ ↦ → τ] (T-Call) Γ ⊢ ℎ ā : 𝜏 → 𝜉 Γ ⊢ 𝑠 : 𝜏 Γ ⊢ ℎ ā 𝑠 : 𝜉 (T-AppT) Γ ⊢ ℎ ā : &𝜏 → 𝜉 &𝑟 : 𝜏 ∈ Γ Γ ⊢ ℎ ā &𝑟 : 𝜉 (T-AppR 0 ) Γ ⊢ ℎ ā : 𝜁 → 𝜉 Γ ⊢ 𝑔 □ : 𝜁 Γ ⊢ ℎ ā 𝑔 : 𝜉 (T-AppH) Γ, Δ ′ ⊢ ℎ ā : &𝜏 → 𝜉 Δ ′ is Δ with all handler bindings removed Γ, &𝑟 : 𝜏, Δ ⊢ ℎ ā &𝑟 : 𝜉 (T-AppR) Γ ⊢ 𝜚 : 𝜉 Γ, ℎ : ⟨ ᾱ⟩ 𝜉 ⊢ 𝑒 / (_ 𝜚 → 𝑑) / γ : ⊥ no type variable in ᾱ is free in Γ Γ ⊢ 𝑒 / γ (ℎ 𝜚 = 𝑑) : ⊥ (T-Defn) Γ ⊢ 𝜚 𝑑 : 𝜉 Γ, ℎ : 𝜉 ⊢ 𝑒 : ⊥ Γ ⊢ 𝑒 / ℎ 𝜚 → 𝑑 : ⊥ (T-Abbr) Γ ⊢ 𝑠 : 𝜏 Γ, &𝑟 : 𝜏 ⊢ 𝑒 : ⊥ Γ ⊢ 𝑒 / &𝑟 = 𝑠 : ⊥ (T-Alloc) Γ, _ : ⊥ ⊢ 𝜋 _ □ : 𝜁 Γ ⊢ 𝜋 : 𝜁 (T-Contract) Γ ⊢ 𝑒 : ⊥ Γ ⊢ □ 𝑒 : ⊥ (T-NullSpec) Γ, 𝑥 : 𝜏 ⊢ 𝜚 𝑒 : 𝜉 Γ ⊢ (𝑥 :𝜏) 𝜚 𝑒 : 𝜏 → 𝜉 (T-ParT) &𝑝 : 𝜏 ∈ Γ Γ ⊢ 𝜚 𝑒 : 𝜉 Γ ⊢ [𝑝]𝜚 𝑒 : 𝜉 (T-Eff) Γ, &𝑞 : 𝜏 ⊢ 𝜚 𝑒 : 𝜉 Γ ⊢ (&𝑞:𝜏) 𝜚 𝑒 : &𝜏 → 𝜉 (T-ParR) Γ ⊢ 𝑠 : 𝜏 Γ, 𝑧 : 𝜏 ⊢ 𝜚 𝑒 : 𝜉 Γ ⊢ (𝑧 = 𝑠) 𝜚 𝑒 : 𝜉 (T-Aux) Γ ⊢ 𝜋 : 𝜁 Γ, 𝑔 : 𝜁 ⊢ 𝜚 𝑒 : 𝜉 Γ ⊢ (𝑔:𝜋) 𝜚 𝑒 : 𝜁 → 𝜉 (T-ParH)

Contract 𝜚 ℎ is a specialized (type-instantiated and with all bound variables refreshed) contract of ℎ and 𝑥𝑞𝑔 𝜋 stands for the list of all parameters of 𝜋 in the order of their appearance in the contract.

v appears in the current typing context, v is a variant auxiliary of handler 𝑔, and 𝑔 is ℎ or defined in the same group as ℎ, 𝜚 ℎ otherwise.

Contract 𝜚 ℎ is a specialized (type-instantiated and with all bound variables refreshed) contract of ℎ, 𝑝𝑥𝑞𝑧 𝜚 stands for the list of pre-writes, term and reference parameters, and auxiliary variables of 𝜚, 𝑥𝑞𝑔 𝜋 stands for the list of all parameters of 𝜋 in the order of their appearance in the contract, and 𝜏 𝑝 is the type of reference 𝑝. Relation ≺ is well-founded and used for all handlers in the group of ℎ and 𝑔.

Contract 𝜚 ℎ is a specialized (type-instantiated and with all bound variables refreshed) contract of ℎ, 𝑥𝑞𝑔 𝜋 stands for the list of all parameters of 𝜋 in the order of their appearance in the contract, and 𝜏 𝑝 is the type of reference 𝑝.

does not occur anywhere in 𝜚, undefined otherwise. Notation •𝑋 means that variable or term 𝑋 is material and •𝑋 means that variable or term 𝑋 is ghost. Contract 𝜚 ℎ is a specialized (type-instantiated and with all bound variables refreshed) contract of ℎ, and 𝑥𝑞𝑔 𝜋 stands for the list of all parameters of 𝜋 in the order of their appearance in the contract.


Samuel Vitorio Lima

Victor Travassos Sarinho
email: vsarinho@uefs.br

A Memory Game Proposal for Facial Expressions Recognition in Health Therapies

Keywords: Health game, Facial expressions, RFID

The recognition of facial expressions has an important role in the communication and interaction between human beings. Researches attest that it is possible to exercise the recognition skills and production of facial expressions with the aid of computational support tools. This article presents Trimemória, a game whose objective to produce a therapeutic playful environment for children with difficulty in recognizing facial expressions. Trimemória seeks to apply classic dynamics of memory games with sensors, in an attempt to increase the integration of the real world with the virtual interactions provided by the game.

Introduction

The recognition of facial expressions is an intrinsic ability of human beings [START_REF] Eckman | Manual for the facial action coding systems, consulting psych[END_REF], representing a important role in the communication and interaction between humans. However, some children can show some difficulties at the task of facial expressions recognition [START_REF] Baron-Cohen | Does the autistic child have a "theory of mind[END_REF], such as Autism Spectrum Disorder (ASD) carriers.

The ASD is classified in the group of neurodevelopmental disorders [START_REF] Klin | Autismo e síndrome de asperger: uma visão geral[END_REF], which result in significant losses in the communication, the interpersonal relationships, the imaginative ability and movement [START_REF] Lô | Representação emocional de crianças autistas frente a um programa de intervenção motora aquática[END_REF]. The ASD does not have cure, but psychological approaches can be useful for the improvement of behavior of individual ASD carrier, given a life improvement and not allowing a worse condition [START_REF] Pradi | Ferramentas de computaçao visual para apoio ao treinamento de expressoes faciais por autistas: Uma revisao de literatura[END_REF].

Searches attest that it is possible to exercise the recognition abilities and production of facial expressions of ASD carriers, through the support of visual computing tools capable of reinforce the connection between mental state and facial expression [START_REF] Gordon | Training facial expression production in children on the autism spectrum[END_REF][START_REF] Tanaka | Using computerized games to teach face recognition skills to children with autism spectrum disorder: the let's face it! program[END_REF][START_REF] Deriso | Exploring the facial expression perception-production link using real-time automated facial expression recognition[END_REF]. In this sense, this article presents the development of a therapeutic support game for children, in special who carries ASD, called Trimemória. It is a game that extends the popular memory game with facial elements for expression recognition, together with Radio Frequency IDentification (RFID) resources to produce a real and virtual playful therapeutic ambient for the child audience.

Related Work

The RFID technology is used in the automated identification of people and objects. It is a sensor which extends the integration between real and virtual world in the smart environment [START_REF] Bohn | The smart jigsaw puzzle assistant: Using rfid technology for building augmented real-world games[END_REF]. As a result, RFID allows computer programs or cell phones to track changes in the physical world and reflect them in the virtual world [START_REF] Bohn | The smart jigsaw puzzle assistant: Using rfid technology for building augmented real-world games[END_REF].

Some developed initiatives has been applied with the use of RFID technology to the support of educational activities for children with ASD. As an example, in the United Kingdom (U.K.), teachers use the Pictures Exchange Communication System (PECS) for communication support with children who carries ASD. Based in the PECS, Herring et al. [START_REF] Herring | Designing a virtual teacher for nonverbal children with autism: Pedagogical affordances and the influence of teacher voice[END_REF] developed a virtual teacher for the child interaction that recognizes images with embedded RFID tags, giving as a result a certain autonomy to children interact and learn with it.

Another example of RFID as a support tool was created by Sula and Spaho [START_REF] Sula | Using assistive technologies in autism care centers to support children develop communication and language skills. a case study: Albania[END_REF], where cards with RFID tags were used to support assistive education activities, such as images learning, identify equals object, coo-work, emotional categories, and lastly math. The main use of RFID in this system was performed by parents that can index some objects. When the child takes an indexed card and goes through the sensor, he will hear the word in the native language with the proposal to repeat it [START_REF] Sula | Using assistive technologies in autism care centers to support children develop communication and language skills. a case study: Albania[END_REF].

Methodology

Trimemória uses distinct memory cards with at least three images of the same creature with different facial expressions to be find by the player (Fig. 1). The idea is to allow distinct expressions identification in the same creature, expanding intervention possibilities during therapeutic sessions. To associate a virtual environment to the game, each Trimemória card has a built-in RFID tag that will be read by a integrated RFID service. The idea is to detect which creature the child found and generate an associated stimulus for it.

For each detected RFID tag, an information is sent to a MQTT broker that transfers the detection to connected clients. The action of sending the RFID tag is done by an RFID service supported by an RFID device, and each connected client represents an application that generates a virtual stimulus to the player for each received information.

Another point is the RFID service assembly with a low cost and open hardware micro-controller able to read RFID sensors. For this, a NodeMCU Lolin 1.0 was used to: collect the data of an RFID sensor; manage the connection with the WiFi service; manage the connection with the provided broker; and send RFID tags detected by the protocol MQTT's topic. The MQTT server/broker is responsible for managing the messages of the topics, which contains the IDs of the detected RFID tags by the connected RFID service. After receiving a message, the MQTT server sends the message to all clients connected with the topic, in this case the outPut topic of the Trimemória game. A TCP server was also developed to be activated when the RFID service turns on. It is responsible to collect available WiFi information from an external dispositive (smartphone for example) that will be used by the RFID service to connect with the MQTT broker. After the confirmation that the internet information is available to be used, the RFID service turns off the TCP server and connects itself with the chosen WiFi, and consequently with the respective active MQTT broker (Fig. 3).

A HTML server was also created to act as a client to the MQTT broker (Fig. 3). It was development through available JavaScript frameworks able to: interpret the developed MQTT client code (Node.js); manage the information from HTTP requisitions and provide an API REST (CORS and Express.js); perform the connection with the MQTT broker(MQTT.js); and create dynamic views for the game (Vue.js). As a result, when the MQTT broker sends a new information to the MQTT client to API REST, this information will appear in a connect client interface managed by Vue.js.

Results and Discussion

For the initial RFID service prototype (Fig. 4), that was built using a low cost open hardware (U$ 4.23 as total cost), it is able to execute two main processes for the game operation. The first is responsible to establish a communication to receive the necessary settings to control the communication with the MQTT broker. The second is responsible to control the communication with the MQTT broker, by sending detected tag IDs from the RFID device. In both, the game presented a good server performance and a fast device response, without compromise the game play as a whole. For the game cards with associated tag IDs, they will be detected by the RFID device when the player selects one. The RFID service sends a message via MQTT broker to the HTML server, that is received by the HTML client due to a continuous verification of the HTML server status (Fig. 3). As a final result, for each received tag ID by the MQTT broker, the associated images and sounds of the detected emotion is displayed to the player (Fig. 4).

Conclusions and Future Work

This paper presented Trimemória, a game that creates a mixed reality in a memory game, which can be used in health therapies to assist the patient in the recognition of facial expressions. For that, RFID, MQTT and HTML services were developed to provide: hardware devices, for player interaction on a physical level; software services, for the card detection together with internet communication; and client apps, able to present multimedia content associated with detected facial expression.

Regarding the use of open hardware, this paper confirms that its use is viable for the creation of an initial low-cost prototype of the proposed game, despite the different types of developed and configured services for its proper functioning. As an example, the creation of an extra TCP application to establish the communication between the RFID service and the MQTT broker shows that it is necessary to automate and simplify the activation and the synchronization process of the proposed hardware/software resources for the game.

As future work, it is intended to create an approach for the direct communication between RFID and the virtual game interface, eliminating the use of different services applied in the developed prototype. Other game dynamics, such as the competitors identification in a match and the return of game awards points, will be develop in the future. To finish, the application of the game in therapies with ASD carriers, along with the assessment of gains and losses obtained with its use, will also be carried out in a near future.

Fig. 1 .

 1 Fig. 1. Some designed creatures with respective emotions for the Trimemória game.

Fig. 2 .

 2 Fig. 2. Prototyping the RFID service for the Trimemória game.

Fig. 3 .

 3 Fig. 3. RFID, MQTT and HTML services for the Trimemória game.

Fig. 4 .

 4 Fig. 4. RFID service prototype, game cards with RFID tags, and an HTML client example.