Typestates specification and verification in Frama-C

Sébastien Patte, Virgile Prevosto

► To cite this version:

Sébastien Patte, Virgile Prevosto. Typestates specification and verification in Frama-C. 2025 IEEE/ACM 13th International Conference on Formal Methods in Software Engineering FormalISE 2025, Apr 2025, Ottawa, Canada. pp.146-156, 10.1109/FormaliSE66629.2025.00021 . cea-05312386

HAL Id: cea-05312386

https://cea.hal.science/cea-05312386v1

Submitted on 13 Oct 2025

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

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

<figure><img src="image_1.png" /></figure>
Typestates Specification and Verification in Frama-C

Sébastien Patte

Université Paris-Saclay, CEA, List

Palaiseau, France

sebastien.patte@cea.fr

Virgile Prevosto

Université Paris-Saclay, CEA, List

Palaiseau, France

virgile.prevosto@cea.fr

*Abstract*—Critical software systems need strong safety and security guarantees, since a bug can have very bad consequences. Thus, we need powerful verification techniques, such as formal methods, to assess such systems. Frama-C is an Open-Source platform for formal analysis of C code. It comes with ACSL, a specification language based on function contracts. Recently, a Frama-C plug-in has been developed for stating and verifying Typestates properties. These properties restrict possible operations on objects of a given datatype, depending on their current state. This plug-in instruments the original program with ACSL annotations, in order to use the standard Frama-C analyzers. We propose a formalization for this instrumentation, in order to prove its correctness. To this end, we rely on the Skel meta-language, the Necrocoq tool, and the Coq proof assistant.

*Index Terms*—Frama-C, Formal Methods, Program Analysis, Verification, Typestates, ACSL, Skeletal Semantics, Skel, Coq

# I. INTRODUCTION

## A. Context

The C programming language, created in the 70s, is still widely used in critical systems because it is a mature low-level language, with a wide range of compilers for many CPU architectures, and also because most companies developing critical systems already have large codebases written in C. The C language gives developer much freedom, which is one of the reasons for its popularity, but makes it easy to write a bad program whose behavior is undefined by the C standard [1] (e.g., division by 0, buffer overflow, or invalid pointer dereference), leading to safety and security risks. This calls for powerful verification techniques, such as formal methods, to assess C programs. FRAMA-C [2], [3] is a framework dedicated to the verification of C programs, based on a set of plug-ins dedicated to various specification and verification tasks. FRAMA-C is accompanied by ACSL [4], a formal specification language dedicated to C. The main analysis plug-ins are able to check ACSL annotations, while other plug-ins generate annotations from dedicated specification languages for specific kinds of properties. In particular, a FRAMA-C plug-in has recently been developed for typestate properties verification. These properties restrict possible operations on objects of a given datatype, depending on its current state. This plug-in instruments the original program with ACSL annotations, in order to then use standard FRAMA-C analyzers.

## B. Contribution

In this paper, we propose a formalization for this instrumentation, for a small imperative language constituting a rep-

<figure><img src="image_2.png" /><figcaption>(a) Typestate automaton</figcaption></figure>

```
\def, (FILE) fd == C | R | W;
\trans, f=undef, (init), f==C;
\trans, f==C, (open_w), f==W;
\trans, f==C, (open_r), f==R;
\trans, f==q, (close), f==C;
\trans, f==R, (close), f==C;
```

<caption>(b) Equivalent specification using the plug-in's syntax</caption>

<caption>Fig. 1: Typestates specification example</caption>

resentative subset of C, in order to prove its correctness. More precisely, if the original code is a valid program and respects its typestate specification, then the instrumented code should be valid and produce identical results. Conversely, if the original code is invalid or non-compliant with its typestate specification, its instrumented version should be invalid. To this end, we use the SKEL meta-language and its associated NECRO COQ tool to build a mechanized formalization for the COQ proof assistant. The formalization and related COQ proofs are available at https://doi.org/10.5281/zenodo.14221425. Notably, we introduce in Section VI-B the state-extension property as a first step towards the correction proof.

## C. Outline

The rest of this paper is structured as follows. First, we give some background on typestate properties, FRAMA-C and SKEL in Section II. Subsequently, Section III presents the syntax of our source and target languages, while Section IV defines their semantics. Then, the instrumentation function is described in Section V. Details about the current proof effort are available in Section VI. Finally, we discuss related works in Section VII, and offer some concluding remarks together with perspectives for future work in Section VIII.

# II. BACKGROUND

## A. Typestates

Typestates [5] is a refinement of the concept of type, used to constrain the set of operations allowed on a datastructure, with respect to a particular context. A datastructure can be in different typestates during its lifetime. The typestate specification tells us which operation can be used, depending on the current datastructure typestate, and which typestate this datastructure has after the operation.

As shown by the example of Fig. 1a, a simple typestate specification can be easily represented as an automaton. In this
example, a file descriptor can be in 3 different states: closed (C), opened in read mode (R) or write mode (W). In addition, we also have an implicit `undef` typestate, for non-initialized variables, as well as an `init` API function that initialize an `undef` file, and leads to the initial typestate C.

When a file has typestate C, we can call either `open_r` or `open_w`, to go respectively in typestate R or W. Conversely, if the file has typestate R or W, then we can call `close`, to go back in typestate C.

## B. Frama-C and ACSL

FRAMA-C is a platform to formally analyze C code. The ACSL [4] specification language, used by FRAMA-C plug-ins, allows stating function contracts or assertions at specific program points. Recently, the TYPESTATES plug-in has been developed for typestate properties verification with FRAMA-C. It works by instrumenting the original code with standard ACSL annotations modeling the typestate transitions (see Section II-C). The plug-in handles typestate properties where API functions are assumed to be the only operations that can modify typestate objects<fnref n="1" />.

In the rest of this section, we provide a brief overview of ACSL, focusing on constructions used in the TYPESTATES instrumentation. A basic function contract has a **requires** clause (known as *precondition*) which must hold each time the function is called (in the *pre-state*), and an **ensures** clause (known as *post-condition*) which must hold when the called function returns (in the *post-state*).

A contract can also involve multiple behaviors. In this case, we have a global precondition, and a list of behaviors. Each behavior can have an **assumes** and **ensures** clause. For each call, the global precondition must hold in the pre-state, and if an **assumes** is true in the pre-state then its post-condition must hold in the post-state. We can also add a **complete behaviors** clause to verify that each call fires at least one behavior, and a **disjoint behaviors** clause, indicating that a single call cannot fire more than one behavior.

Finally, **ghost** code is a very specific kind of annotation. Namely, it is regular C code, except that it can only modify **ghost** variables and must not change the control flow of non-**ghost** code. On the other hand, **ghost** variables are visible in ACSL specifications.

## C. Instrumentation Example

In this section, we present a typestate instrumentation example based on the specification given in Fig. 1a. The plug-in uses global ACSL extensions to describe the automaton, as shown in Fig. 1b. The `\def` clause indicates which type must be equipped with typestates (here `FILE`), and its associated states (C, R, and W). Then, `\trans` clauses specify each possible transition. Namely, such a clause has three elements: the precondition, indicating the typestate of the object on which an operation must be applied, the name of the operation itself, enclosed in braces, and the post-condition, indicating

the typestate of the object after the operation. In both the pre- and post-conditions, the objects referred to must be pointers to `FILE`, i.e., the typestate type.

Let us now examine in more detail how the instrumentation made by the plug-in works on the `close` function, starting from the original program presented in Fig. 2. In this very simple example, we first initialize a new file with `init`. Then, we open it with `open_r`, and finally close it with `close`.

<figure><img src="image_3.png" /><figcaption>Fig. 2: Original program</figcaption></figure>

Fig. 3 outlines the program after typestate instrumentation. First, `fd` is an enumeration type representing the four typestates `undef`, `C`, `R`, and `W`. The `close` API function has a new ghost parameter `ts_f`, a contract, and a ghost instruction. `ts_f` is called a *tracker*, as it keeps track of the original variable typestate along the execution. The contract has one behavior for each transition, and allows verifying typestate properties at each call site using the tracker. Finally, the ghost statement updates the tracker according to the associated transitions. Other functions in the API are instrumented similarly.

Conversely, in the client code, i.e., the `main` function, we have a new tracker `ts_f`, associated to the `f` local variable, that is used at each API call. Following the `init` call, this tracker has the `C` typestate value. Thus, the `open_r` precondition holds, and `ts_f` now stores typestate `R`. Last, the tracker respects the `close` precondition, in particular the second behavior, named `ts_l` in Fig. 3.

```c
enum fd {undef = 0, C = 1, R = 2, W = 3};
/*@ requires *ts_f == W V *ts_f == R;
  behavior ts_0:
    assumes *ts_f == W;
    ensures *ts_f == C;
  behavior ts_1:
    assumes *ts_f == R;
    ensures *ts_f == C;
  complete behaviors;
  disjoint behaviors; */
int close(FILE *f) /*@ ghost (enum fd \ghost *ts_f)*/ {
  /* update f's internal data ... */
  /*@ ghost
    if (*ts_f == W) { *ts_f = C; }
    else if (*ts_f == R) { *ts_f = C; }; */
  return 0;
}

int main() {
  /*@ ghost enum fd ts_f; */
  FILE f;
  init(&f) /*@ ghost (&ts_f) */;
  open_r(&f) /*@ ghost (&ts_f) */;
  close(&f) /*@ ghost (&ts_f) */;
}
```

<caption>Fig. 3: Instrumented program</caption>

<footnote n="1">¹This hypothesis could be verified through the use of other FRAMA-C plug-ins, notably METACSL [6].</footnote>
## D. Skeletal Semantics

Skeletal Semantics [7] consist of SKEL, a meta-language to describe the semantics of programming languages, and NECRO [8], a set of tools to manipulate these descriptions.

From a single SKEL file, the NECRO library can derive: a COQ formalization, a debugger, a dependency graph, an OCAML interpreter, or an abstract interpreter. We are particularly interested in NECRO COQ, to generate a mechanized formalization of our semantics and prove typestate instrumentation correctness.

NECRO COQ [9] uses a deep embedding of SKEL, and provides translation from a SKEL file to the embedded COQ formalization. Three different SKEL interpretations are included in NECRO COQ: big-step inductive, big-step iterative, and small-step. Big-step inductive is the simplest interpretation mode, while big-step iterative allows strong induction on the derivation tree (useful to prove induction principles). On the other hand, small-step interpretation reasoning about co-inductive behaviors, like non-termination. These three interpretations are proven equivalent, and we can easily switch from one to another, even in the middle of a proof.

## E. Notations

In the following sections, we will use `::` for the list cons operator, as is usual in ML-like languages, and `++` for the list concatenation operator. We will also use the sequence notation $(x_i)_{i=0}^n$, which represent the list $x_1, \dots, x_n$.

Additionally, we use the set comprehension notation $\{x | p\}$, which denotes the set of elements $x$ satisfying predicate $p$. Regarding environments, we write $s \uplus [x \mapsto v]$ to add the $(x, v)$ new association into $s$. Furthermore, $[x_i \mapsto v_i]_{i=0}^n$ denotes the environment $\emptyset \uplus [x_1 \mapsto v_1] \uplus \dots \uplus [x_n \mapsto v_n]$.

# III. SYNTAX

## A. Source Language

Fig. 4 describes the source language syntax. This is a minimalistic imperative language restricted to the features that are the most problematic for typestate instrumentation, namely pointers and function calls<fnref n="2" />. We only consider three base types, namely **bool**, **int**, and **ts**, the type to which typestates are attached. Each type has a specific set of literal values, left abstract for **ts**, except that we assume a default value $ts_0$.

On the left-hand side of assignments, we allow variables with an arbitrary number of dereferencing symbols `*`, and name this construction a *lval*. Expressions can be literals, *lvals*, taking the address of a variable (`&`), or an arithmetic or boolean operator `op`. We consider function definitions with local variable declarations at the beginning of the block, and a unique **return**. We also assume distinct local variable names across the whole program.

API functions are not allowed to call other functions, since these calls could modify trackers in the instrumented version, as explained in Section V-D. This is a limitation for API functions, but we are mainly interested in how client-code

<figure><img src="image_4.png" /><figcaption>Fig. 4: Source language syntax</figcaption></figure>

uses API functions, not in verifying the API implementation itself.

Since our typing process is fairly standard for an imperative language, we will not detail it here. This process uses a variables' type environment, denoted as $\Gamma$, to check types adequacy at assignments and functions calls. However, this procedure differs from a standard one by forbidding the use of **ts** constants in client-code. That is, client-code cannot modify explicitly **ts** variables by assigning a new value, but must use API functions instead. Additionally, we won't consider functions returning a tracked object, but use an *init* function instead. Typing rejects functions with a return type based on **ts**. In the rest of the paper, we always manipulate well-typed programs.

<footnote n="2">²The TYPESTATES plug-in itself supports most C constructions.</footnote>
## B. Target Language

```
pop = {^, V, ⇒}
typ ::= ... | **enum** ident
expr ::= ... | ident (enum tag)
pred ::= \**true** | \**false**
| expr cop expr
| pred pop pred
enumdef ::= **enum** ident {ident, ..., ident};
stmt ::= ...
| **if** expr **then** stmts₁ **else** stmts₂
behavior ::= **behavior** x :
    **assumes** pred;
    **ensures** pred;
contract ::= /*@ requires pred;
    **behavior** * /
fundef ::= contract typ ident
    (decls) block
file ::= **enumdef** **fundef*** main
```

<caption>Fig. 5: Target language syntax</caption>

Fig. 5 outlines the target language syntax, which is an extension of the source language. Additional C-like constructions are considered: definition of enumerated types, with their tags, and conditional statements. We also add ACSL-like logical predicates and function contracts (see Section II-B). A predicate can use boolean literals, comparisons between C expressions, or a logical connector (`V,^,⇒`). In the context of typestate analysis, these behaviors are complete and disjoint, as explained in Section II-B. Indeed, the TYPESTATES plugin only supports deterministic typestate transitions, as trackers stores a unique typestate value. Finally, enumeration tags are assumed distinct from the program variable names.

## IV. SEMANTICS

We present in this section the semantics of both our source and target languages, as defined in SKEL. Both languages are equipped with a big-step semantics, detailed in Sections IV-C and IV-D respectively. Before that, we must introduce auxiliary functions. First, Section IV-A describes the environment of function definitions. Second, we define functions that manipulate the memory state of the program in Section IV-B.

### A. Functions Environment

A program is executed in a function environment. It is initially the reversed list of definitions given in the file of the language. Indeed, in order to ensure the termination of our

programs, and facilitate COQ proofs, we forbid recursion by restricting this environment, when evaluating a call to `x_f`, to the `fundef` that occurs after the definition of `x_f`. For that, we recursively search for `x_f` and return the definition as well as the tail of the list. More formally, with `x_f` (resp. `x_g`) the identifier introduced by the `fundef f` (resp. `g`), `getFundef` is defined as such:

$$ 
\begin{aligned}
\text{getFundef } x_f (f :: \bar{g}) &= (f, \bar{g}) \\
\frac{x_f \neq x_g}{\text{getFundef } x_f (g :: \bar{h})} &= \text{getFundef } x_f \bar{h}
\end{aligned}
$$

### B. Memory State

1) **Environments:** In our semantics, we manipulate two kinds of environments. First, `σ_v`: `ident` → `value` maps each variable name to its value. We consider two kinds of values: literals (booleans, integers, and `ts` values), and pointer values (`Ptr l`). A pointer value `l` is either `null`, or a variable name. Second, `σ ts`: `ident` → `ident` stores a typestate name for each variable whose type is `ts`.

In the source language's semantics, a memory state `σ` = `(σ_v, σ ts)` is a pair of two environments, as we need `σ` to explicitly check typestate transitions. In the target language, contracts handle this task, and the memory state is simply `σ_v`.

2) **Variables initialization:** We define here the two primitive functions initializing a new variable in `σ_v`. First, `bind_var` initializes a variable to a specific value, given as argument. Then, `init_var` uses `bind_var` with a default value, determined by the `init_val` function, depending on the type of the variable (`false`, `0`, `null`, or `ts0`).

We also use `init_vars` and `bind_vars`, that simply iterate `init_var` (resp. `bind_var`) over a list of declaration.

$$ 
\begin{aligned}
\sigma'_{v} = \sigma_{v} \uplus [x \mapsto v] \\
\frac{\text{bind_var } \tau x v (\sigma_{v}, \sigma_{ts}) = (\sigma'_{v}, \sigma_{ts})}{\text{init_val } \tau = \begin{cases} \text{false} & \tau = \text{bool} \\ 0 & \tau = \text{int} \lor \tau = (\text{enum}_-) \\ \text{null} & \tau = (\ast_-) \\ ts_{0} & \tau = \text{ts} \end{cases}} \\
\frac{\text{init_val } \tau = v \quad \text{bind_var } \tau v \sigma = \sigma'}{\text{init_var } \tau x \sigma = \sigma'}
\end{aligned}
$$

3) **Update and Lookup:** We use 2 other primitive functions to update and lookup in `σ_v`. First, `write` updates the value of a variable already present in `σ_v`. Second, `read` retrieves the value attached to a variable in `σ_v`.

Similarly, we use 2 primitive functions for `σ ts`: `set_ts` assigns a typestate value to a variable name, while we read a variable's typestate value with `get_ts`.
4) *Clear variables from state*: At the end of a function evaluation, we need to clear formals and local variables from the memory state, in order to prevent local address leaking.

The function *clear* takes a declaration list $\overline{d}$, and removes all the corresponding variables from the state. Additionally, this function clears pointers locations: if a pointer references one of the $\overline{d}$ variables, it is replaced with the null pointer.

$$ \sigma'_{ts} = \frac{\{[x \mapsto y] \in \sigma_{ts} \mid \forall \tau, (\tau x) \notin \overline{d}\}}{\text{clear } \overline{d} \sigma_{ts} = \sigma'_{ts}} $$

$$ \sigma'_{v} = \frac{\{[x \mapsto \text{clear } \overline{d} v] \mid (\tau x) \notin \overline{d} \wedge [x \mapsto v] \in \sigma_{v}\}}{\text{clear } \overline{d} \sigma_{v} = \sigma'_{v}} $$

$$ \frac{\forall x, v \neq \text{Ptr } x}{\text{clear } \overline{d} v = v} $$

$$ \frac{v = \text{Ptr } x}{\text{clear } \overline{d} v = v} \quad \forall \tau, (\tau x) \notin \overline{d} $$

$$ \frac{v = \text{Ptr } x}{\text{clear } \overline{d} v = \text{Ptr null}} \quad \exists \tau, (\tau x) \in \overline{d} $$

$$ \frac{\text{clear } \overline{d} \sigma_v = \sigma'_v \quad \text{clear } \overline{d} \sigma_{ts} = \sigma'_{ts}}{\text{clear } \overline{d} (\sigma_v, \sigma_{ts}) = (\sigma'_v, \sigma'_{ts})} $$

### C. Source Language

We now present the semantics of our source language. As said, expressions are evaluated in memory state $\sigma = (\sigma_v, \sigma_{ts})$ and statements modify $\sigma$ and their function environment.

1) *Lvals*: There are two ways to evaluate a *lval*: in left-mode ($\vdash_{lv}$), or right-mode ($\vdash_{rv}$). Left-mode returns its location, i.e., the associated variable name. Conversely, right-mode gives back the value associated to this location, and its current typestate name if it exists. Because of dereference, both modes are mutually recursive. Namely, the location of a dereference $*lv$ is $x$ when $lv$ evaluates to *Ptr $x$* in right-mode. Conversely, to compute the value of a *lval* with $\vdash_{rv}$, we first retrieve its location with $\vdash_{lv}$, then read its value in $\sigma$.

$$ \sigma \vdash_{lv} x \rightsquigarrow x \qquad \frac{\sigma \vdash_{rv} lv \rightsquigarrow \text{Ptr } x}{\sigma \vdash_{lv} *lv \rightsquigarrow x} $$

$$ \frac{\sigma \vdash_{lv} lv \rightsquigarrow x \quad \text{read } x \sigma = (\_, v)}{\sigma \vdash_{rv} lv \rightsquigarrow (v, \text{get\_ts } x \sigma)} $$

2) *Expressions*: For an *lval*, we just get its value, as well as the optional typestate name $y_{ts}$, via $\vdash_{rv}$. Other expressions, that cannot have type *ts*, do not have a typestate attached to them. The evaluation & $x$ gives a pointer *Ptr $x$*. We omit rules for the other cases, since they are quite classical:

constants are already values, and for binary operators we evaluate the two operands before applying the operator.

$$ \frac{\sigma \vdash_{rv} lv \rightsquigarrow (v, y_{ts})}{\sigma \vdash_{e} lv \rightsquigarrow (v, y_{ts})} \qquad \sigma \vdash_{e} \& x \rightsquigarrow \text{Ptr } x $$

3) *Statements*: For assignments, we first evaluate the left value to a location, the right expression to a value, and write the value at this location. The right expression evaluation can also give a typestate name: in this case, we update the typestate name at the left location. Evaluation of a function call is handled by the $\vdash_{call}$ rule (defined in Section IV-C4), which gives back the new state and returned value.

$$ \frac{\sigma_1 \vdash_{lv} lv \rightsquigarrow x \qquad \sigma_1 \vdash_{e} e \rightsquigarrow v \qquad \text{write } x \sigma_1 v = \sigma_2}{\sigma_1, \bar{g} \vdash_{s} lv := e \rightsquigarrow \sigma_2} $$

$$ \frac{\sigma_1 \vdash_{lv} lv \rightsquigarrow x \quad \sigma_1 \vdash_{e} e \rightsquigarrow (v, y_{ts})}{\text{write } x \sigma_1 v = \sigma_2 \quad \text{set\_ts } x y_{ts} \sigma_2 = \sigma_3} \qquad \sigma_1, \bar{g} \vdash_{s} lv := e \rightsquigarrow \sigma_3 $$

$$ \frac{\sigma_1, \bar{g} \vdash_{call} x_f(\bar{e}) \rightsquigarrow (\sigma_2, \_)}{\sigma_1, \bar{g} \vdash_{s} x_f(\bar{e}) \rightsquigarrow \sigma_2} $$

$$ \frac{\sigma_1 \vdash_{lv} lv \rightsquigarrow x \qquad \sigma_1, \bar{g} \vdash_{call} x_f(\bar{e}) \rightsquigarrow (\sigma_2, v) \qquad \text{write } x \sigma_2 v = \sigma_3}{\sigma_1, \bar{g} \vdash_{s} lv := x_f(\bar{e}) \rightsquigarrow \sigma_3} $$

$$ \frac{\forall i \in [1..n] : \sigma_{i-1}, \bar{g} \vdash_{s} s_i \rightsquigarrow \sigma_i}{\sigma_0, \bar{g} \vdash_{stmts} (s_i)_{i=1}^n \rightsquigarrow \sigma_n} $$

4) *Function Call*: When calling a function $f$, we first get its definition and the list $\bar{h}$ of functions that $f$ is allowed to call, with *getFundef*. Subsequently, we evaluate call arguments, and initialize formal parameters with these arguments' values, using *bind_vars*. Next, we evaluate the called block using $\vdash_{block}$, which is described in the next two sections, in the restricted function environment $\bar{h}$. Finally, at the end of the call, we clear formals from post-state and block return value.

$$ \begin{array}{l} \forall i \in [1..n] : \sigma_1 \vdash_{e} e_i \rightsquigarrow v_i \\ \text{getFundef } x_f \bar{g} = (f, \bar{h}) \qquad f = (\tau, x_f, (d_i)_{i=1}^n, b) \\ \text{bind\_vars } (d_i)_{i=1}^n (v_i)_{i=1}^n \sigma_1 = \sigma_2 \\ \sigma_2, \bar{h}, \vdash_{block} (x_f, b) \rightsquigarrow (\sigma_3, v) \\ \text{clear } (d_i)_{i=1}^n \sigma_3 = \sigma_4 \qquad \text{clear } (d_i)_{i=1}^n v = v' \\ \frac{\sigma_1, \bar{g} \vdash_{call} x_f((e_i)_{i=1}^n) \rightsquigarrow (\sigma_4, v')}{\sigma_1, \bar{g} \vdash_{call} x_f((e_i)_{i=1}^n) \rightsquigarrow (\sigma_4, v')} \end{array} $$
There are two possible cases when evaluating the body of a function: either we are calling an API function (i.e., with typestate transitions) or a normal one. To distinguish between a client function and an API one, we use the `[]` trans function, which selects typestate transitions associated to $x_f$.

$$ [[tr]_{x_f}^{trans} = [(pre, x_f, post) \in tr] $$

5) **API Block:** When calling an API function, we first initialize local variables with `init_vars`. Second, we evaluate statements, with an empty list of accessible functions, as explained in Section V-B. Then, we evaluate the return value, and clear local variables from state and return value. Finally, we check typestate transitions with $\vdash_{trans}$ (defined below), between pre-state $\sigma_1$ and post-state $\sigma_4$, in order to obtain the state $\sigma_5$ with updated typestates values.

$$ \frac{\sigma_1 \vdash_{block} (x_f, \bar{d}, \bar{s}, e) \rightsquigarrow (\sigma_5, v')}{\sigma_1 \vdash_{pre} (x_i, y_i)^n_{i=1}} \qquad \sigma_1 \vdash_{post} (x_i, y_i)^n_{i=1} \rightsquigarrow \sigma_n $$

While using $\vdash_{trans}$ on a transitions list, one and only one precondition needs to be actionable. This is checked with $\vdash_{pre}$. Then, we use $\vdash_{post}$ on the corresponding post-condition, in order to update the associated typestates values.

To check a typestate precondition, we need the specified parameter names to have a pointer value `Ptr z`, and check that the referenced variable `z` has the required typestate value with `get_ts`. To apply a post-condition, we also need a pointer value, and update the typestate value of the referenced variable with `set_ts`.

$$ \frac{\sigma_1 \vdash_{pre} (x_i, y_i)^n_{i=1}}{\sigma_1 \vdash_{post} (x_i, y_i)^n_{i=1}} \qquad \sigma_1 \vdash_{pre} pre \quad \sigma_2 \vdash_{post} post \rightsquigarrow \sigma_3 $$

6) **Client Block:** Local variable initialization differs slightly when evaluating a client block. While all variables are still initialized to a default value with `init_vars`, we also need

to associate new `ts` variables with the default `undef` typestate in $\sigma_{ts}$. In contrast to API blocks, statements are evaluated using a non-empty list of accessible functions because we want them to be able to call previously defined functions. Last, we evaluate the return value and clear locals as for API blocks.

$$ \frac{\sigma_1 \vdash_{cliV} (\tau, x) \rightsquigarrow \sigma_2}{\sigma_1 \vdash_{cliL} (\bar{d}, \bar{s}, e) \rightsquigarrow \sigma_2} $$

## D. Target Language

We now define the semantics of our target language. More precisely, we only introduce here the rules for the constructions that differ from the source language.

1) **Enumerations:** Enumeration definitions are global, and we use an environment $E: \text{ident} \mapsto \mathbb{N}$ to map enumeration tags to their index. Then, the value of tag $y$ is just $E(y)$.

2) **Predicates:** We obtain boolean values from predicates using standard evaluation rules. As with expressions in the previous section, we omit these rules due to space constraints.

3) **Instructions:** Compared to the source language, we have a new instruction, namely the conditional. As usual, its evaluation simply amounts to evaluating the conditional test and the corresponding branch.

$$ \frac{\sigma_1 \vdash_{e} e \rightsquigarrow \text{true}}{\sigma_1, \bar{g} \vdash_{s} \textbf{if e then } \bar{s}_1 \textbf{ else } \bar{s}_2 \rightsquigarrow \sigma_2} $$

4) **Function Call:** The evaluation procedure for function calls is similar to client function calls in the source language. The only difference is the contract verification, with pre-state $\sigma_2$ and post-state $\sigma_3$, using $\vdash_{contract}$, defined below. Note that, in contrast to the source language, the target language only has one evaluation mode for functions, as we don't need to build and maintain an explicit typestate environment, since we use tracker variables and rely on annotations to track typestates.
$$
\begin{align*}
\forall i \in [1..n] : \sigma_1 \vdash_e e_i \rightsquigarrow v_i \\
\text{bind\_vars } (d_i)_{i=1}^n (v_i)_{i=1}^n \sigma_1 = \sigma_2 \\
\text{getFundef } x_f \bar{g} = (f, \bar{h}) \qquad f = (x_f, (d_i)_{i=1}^n, b, c) \\
\sigma_2, \bar{g} \vdash_{\text{block}} b \rightsquigarrow (\sigma_3, v) \qquad \sigma_2, \sigma_3 \vdash_{\text{contract}} c \\
\text{clear } (d_i)_{i=1}^n \sigma_3 = \sigma_4 \qquad \text{clear } (d_i)_{i=1}^n v = v' \\
\frac{}{\sigma_1, \bar{g} \vdash_{\text{call}} f((e_i)_{i=1}^n) \rightsquigarrow (\sigma_4, v')}
\end{align*}
$$

5) **Block**: A block evaluation is simpler in the target language than source language. We just have to initialize local variables to default values with `init_vars`, evaluate statements with `|$^s$, the return expression with `|$^e`, and finally clear local variables from state and return value.

$$
\begin{align*}
\text{init\_vars } \bar{d} \sigma_1 = \sigma_2 \\
\sigma_2, \bar{g} \vdash_s s \rightsquigarrow \sigma_3 \qquad \sigma_3 \vdash_e e \rightsquigarrow v \\
\text{clear } \bar{d} \sigma_3 = \sigma_4 \qquad \text{clear } \bar{d} v = v' \\
\frac{}{\sigma_1, \bar{g} \vdash_{\text{block}} (\bar{d}, s, e) \rightsquigarrow (\sigma_4, v')}
\end{align*}
$$

6) **Contract**: A valid contract needs that its global precondition reduces to true. If the contract has any behavior, one and only one of them must fire (i.e., **assumes** condition reducing to true), and its post-condition needs to reduce to true. When a contract violates any of the above conditions, it is considered as invalid, and the evaluation blocks.

$$
\begin{align*}
\sigma_{pre} \vdash_p p \rightsquigarrow \text{true} \\
\exists! (p_1, p_2) \in \overline{bh} : \left\{
\begin{array}{@{}l@{}}
\sigma_{pre} \vdash_p p_1 \rightsquigarrow \text{true} \\
\sigma_{post} \vdash_p p_2 \rightsquigarrow \text{true}
\end{array}
\right. \\
\frac{}{\sigma_{pre}, \sigma_{post} \vdash_{contract} (p, \overline{bh})}
\end{align*}
\[
\frac{}{\sigma_{pre}, \sigma_{post} \vdash_{contract} (p, \text{[]})}
\]
$$

V. INSTRUMENTATION

The instrumentation procedure takes a program written in the source language, with its typestate specification, and instruments it with annotations. This instrumentation behaves differently on API functions (mentioned in the typestate specification), and client-code (other functions and “main” block).

A new variable, the tracker, is generated for each variable declared in client-code with a type based on **ts**, to store its typestate value. In client-code, for each assignment on an original variable, the instrumentation inserts an equivalent assignment on its tracker. These trackers are then injected into calls from client-code. For that, we add formal parameters to function definitions.

For each API function, we derive a statement and a contract from its associated typestate transitions. The contract specifies both which tracker values we are permitted to call the function

with, and how these values should evolve when returning to caller. Similarly, the statement updates these trackers, using conditionals and assignments, and must respect the contract.

A. **Enum**

The `[]enum` function builds an enumeration type definition from the typestate specification. We use the typestate property name `xts` as enumeration type's name. The list of enumerated values is composed of the special `undef` typestate and all other typestates from the specification. This enumeration type represents typestate values, and is used as the trackers' type.

B. Trackers

During instrumentation, we use a trackers' environment $\gamma$: `ident \to decl`, which maps a variable name to its tracker's declaration (if any). Such declarations are generated from local variable declarations during client-code instrumentation (Section V-C), and formal parameters while instrumenting function definitions (Section V-F). In both cases, we use the `[]trackers` function, which takes a declaration list and generates a fresh declaration `fresh(x)` for each variable `x` having a type based on **ts**. Additionally, these tracker declarations are stored in the tracker environment given as second result.

$$
\begin{align*}
\llbracket \mathbf{ts} \rrbracket^{\text{ty}} &= \mathbf{enum} \ x_{\text{ts}} \\
\llbracket \tau^* \rrbracket^{\text{ty}} &= \llbracket \tau \rrbracket^* \\
\llbracket (\tau, x) \rrbracket^{\text{decl}} &= (\llbracket \tau \rrbracket^{\text{ty}}, \text{fresh}(x)) \\
\llbracket (\tau_i x_i)_{i=1}^n \rrbracket^{\text{trackers}} &= ((\tau_i x_i)_{i=1}^n \text{++} (\llbracket \tau_i x_i \rrbracket^{\text{decl}})_{i=1}^n), \\
[x_i \mapsto \llbracket \tau_i x_i \rrbracket^{\text{decl}}]_{i=1}^n
\end{align*}
$$

Once $\gamma$ has an entry for each variable with a type based on **ts**, the `[]`^arg function converts an expression into its tracker version, if any, with the help of $\gamma$. This expression contains a variable `x` since it must be either a `lval` or a `&` operator. Thus, `[]`^arg returns an expression with its name `x` replaced by the tracker version $\gamma(x)$ if it exists.

`[]`^args transforms an expression list by giving the list of corresponding trackers and ignoring untracked variables.

$$
\begin{align*}
\llbracket x \rrbracket_{\gamma}^{\text{arg}} &= \text{snd } \gamma(x) \\
\llbracket *lv \rrbracket_{\gamma}^{\text{arg}} &= \llbracket *lv \rrbracket_{\gamma}^{\text{arg}} \\
\llbracket &\&x \rrbracket_{\gamma}^{\text{arg}} &= \&\llbracket x \rrbracket_{\gamma}^{\text{arg}}
\end{align*}
$$

C. Client Code

Statements from client-code are instrumented by the `[]`^cli_st function. This function extends call arguments, including in call assignments, with the needed trackers.

For a simple assignment `lv := e`, we insert its tracker-version when the `[]`^arg function gives a tracker for both left and right expressions. This procedure is not needed for call assignments since we only consider functions whose return type is not based on **ts**.
$$
\begin{align*}
\llbracket \mathit{lv} := e \rrbracket_{\gamma}^{\mathit{cli\_st}} &= \mathit{lv} := e; \llbracket \mathit{lv} \rrbracket_{\gamma}^{\mathit{arg}} := \llbracket e \rrbracket_{\gamma}^{\mathit{arg}} \\
\llbracket x_f(\bar{e}) \rrbracket_{\gamma}^{\mathit{cli\_st}} &= x_f(\bar{e}, \llbracket \bar{e} \rrbracket_{\gamma}^{\mathit{args}}) \\
\llbracket \mathit{lv} := x_f(\bar{e}) \rrbracket_{\gamma}^{\mathit{cli\_st}} &= \mathit{lv} := x_f(\bar{e}, \llbracket \bar{e} \rrbracket_{\gamma}^{\mathit{args}}) \\
\llbracket (s_i)_{i=1}^n \rrbracket_{\gamma}^{\mathit{cli\_sts}} &= (\llbracket s_i \rrbracket_{\gamma}^{\mathit{cli\_st}})_{i=1}^n
\end{align*}
$$

We now describe the instrumentation of a whole function definition. Using the `[]`<sup>trackers</sup> function, the instrumentation of a client-function block duplicates local variable declarations with their potential tracker version. In addition, for every base typestate object, we add an assignment to initialize its tracker with `undef`. Finally, we instrument client statements with `[]`<sup>cli_sts</sup> using both old and local trackers $(\gamma_1 \uplus \gamma_2)$.

$$
\frac{
  \begin{align*}
  \llbracket (\mathbf{ts}, x) \rrbracket^{\mathit{initTr}} &= \llbracket x \rrbracket^{\mathit{arg}} := \mathit{undef} \\
  \llbracket (\tau_i, x_i)_{i=1}^n \rrbracket^{\mathit{initTrs}} &= (\llbracket (\tau_i, x_i) \rrbracket^{\mathit{initTr}})_{i=1}^n \\
  \llbracket \bar{d} \rrbracket^{\mathit{trackers}} &= (\bar{d}', \gamma_2) \qquad \gamma_3 = \gamma_1 \uplus \gamma_2 \\
  \llbracket \bar{d}, \bar{s}, e \rrbracket^{\mathit{cli\_block}}_{\gamma_1} &= (\bar{d}', \llbracket d \rrbracket^{\mathit{initTrs}} \text{++} \llbracket \bar{s} \rrbracket^{\mathit{cli\_sts}}_{\gamma_3}, e)
  \end{align*}
}{
  \llbracket \bar{d}, \bar{s}, e \rrbracket^{\mathit{cli\_sts}}_{\gamma_1} = (\bar{d}', \llbracket d \rrbracket^{\mathit{initTrs}} \text{++} \llbracket \bar{s} \rrbracket^{\mathit{cli\_sts}}_{\gamma_3}, e)
}
$$

### D. API block

The instrumentation procedure inserts a statement at the end of each API function, that updates trackers with respect to typestate transitions. This statement is composed of nested conditionals, which test each precondition and update the tracker with respect to the corresponding post-condition. We try preconditions sequentially, but only one can be true, otherwise the generated contract defined in Section V-E wouldn't be fulfilled according to our semantics.

Note that an API function should not modify trackers before this ghost block, since it should update trackers with respect to their pre-state values. This is ensured as we do not create tracker versions from original statements. In particular, calls are forbidden so we do not have to generate tracker arguments.

$$
\begin{align*}
\llbracket (x_i, y_i)_{i=1}^n \rrbracket_{\gamma}^{\mathit{pre}} &= \& \& (\ast \llbracket x_i \rrbracket_{\gamma}^{\mathit{arg}} == y_i) \\
\llbracket (x_i, y_i)_{i=1}^n \rrbracket_{\gamma}^{\mathit{post}} &= (\ast \llbracket x_i \rrbracket_{\gamma}^{\mathit{arg}} := y_i)_{i=1}^n \\
\llbracket (\mathit{pre}, x_f, \mathit{post}) :: \mathit{tr} \rrbracket_{\gamma}^{\mathit{ts\_st}} &= \mathbf{if} \llbracket \mathit{pre} \rrbracket_{\gamma}^{\mathit{pre}} \mathbf{then} \llbracket \mathit{post} \rrbracket_{\gamma}^{\mathit{post}} \\
&\quad \mathbf{else} \llbracket \mathit{tr} \rrbracket_{\gamma}^{\mathit{ts\_st}} \\
\llbracket \llbracket \llbracket \mathit{x_f}, \mathit{post} \rrbracket :: \mathit{tr} \rrbracket_{\gamma}^{\mathit{ts\_st}} &= \llbracket \mathit{post} \rrbracket_{\gamma}^{\mathit{post}} \\
\llbracket \bar{d}, \bar{s}, e \rrbracket_{\mathit{tr}, \gamma}^{\mathit{api\_block}} &= (\bar{d}, (\bar{s}; \llbracket \mathit{tr} \rrbracket_{\gamma}^{\mathit{ts\_st}}), e)
\end{align*}
$$

### E. Function Contract

For each API function, we generate a function contract from its typestate transitions with `[]`<sup>contract</sup>. To transform a transition into a behavior, we transform preconditions and post-conditions into predicates using the function `[]`<sup>cond</sup>. Such a predicate is a conjunction of comparisons, which verifies

tracker values for each formal parameter specified in the typestate transition.

The `[]`<sup>bh</sup> function transforms the whole transitions list into the behaviors list. Last, we build the global precondition, which is the disjunction of behaviors' preconditions.

$$
\begin{align*}
\llbracket (x_i : y_i)_{i=1}^n \rrbracket_{\gamma}^{\mathit{cond}} &= \bigwedge_{i=1}^n (\ast \llbracket x_i \rrbracket_{\gamma}^{\mathit{arg}} == y_i) \\
\llbracket (\mathit{pre}, x_f, \mathit{post}) :: \mathit{tr} \rrbracket_{\gamma}^{\mathit{bh}} &= (\llbracket \mathit{pre} \rrbracket_{\gamma}^{\mathit{cond}}, \llbracket \mathit{post} \rrbracket_{\gamma}^{\mathit{cond}}) \\
&\qquad :: \llbracket \mathit{tr} \rrbracket_{\gamma}^{\mathit{bh}} \\
\llbracket (p_i, -)_{i=1}^n \rrbracket^{\mathit{req}} &= \bigvee_{i=1}^n p_i \\
\llbracket \mathit{tr} \rrbracket^{\mathit{contract}} &= \llbracket \llbracket \mathit{tr} \rrbracket_{\gamma}^{\mathit{bh}}^{\mathit{req}}, \llbracket \mathit{tr} \rrbracket_{\gamma}^{\mathit{bh}} \rrbracket
\end{align*}
$$

### F. Function definition

In both API and client functions, we use `[]`<sup>trackers</sup> to generate a tracker version for every formal parameter with a type based on `ts`.

We select transitions related to the current function with `[]`<sup>tr</sup>. As in Section IV-C4, if there are no transitions, the function is a client function; otherwise, it is an API function.

All it takes to instrument a client function is to create an always true contract and use `[]`<sup>cli_block</sup> to instrument statements. In contrast, when the function is an API one, we generate its contract with `[]`<sup>contract</sup> and instrument its statements with `[]`<sup>api_block</sup>.

$$
\frac{
  \begin{align*}
  \llbracket \bar{d} \rrbracket^{\mathit{trackers}} &= (\bar{d}', \gamma) & \llbracket \mathit{tr}_{ts} \rrbracket^{\mathit{tr}}_{x_f} &= [] \\
  \llbracket (x_f, \bar{d}, b) \rrbracket^{\mathit{fun}} &= (x_f, \bar{d}', (\top, []), \llbracket b \rrbracket_{\gamma}^{\mathit{cli\_block}}) \\
  \llbracket \bar{d} \rrbracket^{\mathit{trackers}} &= (\bar{d}', \gamma) & \mathit{tr} &= \llbracket \mathit{tr}_{ts} \rrbracket^{\mathit{tr}}_{x_f} \neq [] \\
  \llbracket (x_f, \bar{d}, b) \rrbracket^{\mathit{fun}} &= (x_f, \bar{d}', \llbracket \mathit{tr} \rrbracket_{\gamma}^{\mathit{contract}}, \llbracket b \rrbracket_{\mathit{tr}, \gamma}^{\mathit{api\_block}})
  \end{align*}
}{
  \llbracket (x_f, \bar{d}, b) \rrbracket^{\mathit{fun}}
}
$$

## VI. PROOF

### A. Freshness

We say that a name $x$ is fresh from memory state $\sigma$ when it cannot be read from memory (i.e., read $x \sigma = \text{None}$). We want to show that any statement preserves names freshness, as described in Fig. 6. Indeed, this point is important to ensure auxiliary variables introduced by the instrumentation do not clash with the variables of the source program.

$$
\forall \sigma_1 \sigma_2 \bar{f} s, \text{ freshNames } \bar{f} \sigma_1 \implies \\
\sigma_1, \bar{f} \vdash s \rightsquigarrow \sigma_2 \implies \\
\text{freshNames } \bar{f} \sigma_2
$$

<caption>Fig. 6: Freshness Preservation Theorem</caption>
Consequently, an assignment cannot introduce any new name in the memory-state. However, the proof is more involving in the case of a function call, since the called function can initialize new variables both as formal parameters and local variables. Indeed, we have to show that each name introduced during call evaluation is properly cleared from state before evaluating next statements of the caller.

The evaluation of a function call leads to the evaluation of the called function block, i.e., a list of statements. Thus, the evaluation of a single statement can lead to the evaluation of a statement list. Fig. 7 presents a simple induction principle on statement list evaluation. The second induction case has an induction hypothesis on the statements tail. However, when the first statement is a call, it reduces to the called block evaluation, for which we miss an induction hypothesis.

$$ \forall P, (\forall \sigma, P \sigma [] \sigma) \implies \left( \begin{array}{l} \forall \bar{g} \sigma_1 \sigma_2 \sigma_3 s_0 \bar{s}, \\ \sigma_1, \bar{g} \vdash s_0 \rightsquigarrow \sigma_2 \implies \\ P \sigma_2 \bar{s} \sigma_3 \implies \\ P \sigma_1 (s_0 :: \bar{s}) \sigma_3 \end{array} \right) \implies \forall \bar{g} \sigma_1 \sigma_2 \bar{s}, \quad \sigma_1, \bar{g} \vdash \bar{s} \rightsquigarrow \sigma_2 \implies P \sigma_1 \bar{s} \sigma_2 $$

<caption>Fig. 7: Simple induction principle for statements evaluation</caption>

To fix this issue, we build a deep induction principle on statements' evaluation, that accounts for the called function block evaluation. We present in Fig. 8, this principle when the first statement is a function call. In this case, we first initialize formal parameters and local variables from $\sigma_1$ to $\sigma_3$. Then, we suppose the induction hypothesis to hold on the evaluation of called block instructions $s_f$, with accessible functions definitions $\bar{h}$ (which is smaller than $\bar{g}$). Subsequently, we clear both locals and formals from state, which leads us to $\sigma_6$. Finally, we assume the induction hypothesis to hold on the statements tail $\bar{s}$ with original functions $\bar{g}$. This deep induction principle has been stated and proved in COQ. While we focus here on client function calls, API functions calls are similar, and other cases are similar to the simple induction principle.

We can now use this deep induction principle to prove freshness preservation on a statements list evaluation. When proving this preservation for the functions list $\bar{g}$, we deduce freshness preservation of $\bar{h}$ between $\sigma_3$ and $\sigma_4$ from the first induction hypothesis. Then, we prove that formal parameters $\bar{d}_p$ and local variables $\bar{d}_l$ are the only new names between $\sigma_1$ and $\sigma_4$. We conclude that $\bar{g}$ is still fresh in $\sigma_6$ and $\sigma_7$, since we have cleared formal parameters $\bar{d}_p$ and local variables $\bar{d}_l$.

## B. State Extension

In this section, we present the state extension property, meant to relate two states: a source and an instrumented state. Namely, we evaluate simultaneously a source program and its instrumentation, and compare memory states, linking original variables with their optional trackers.

$$ \begin{array}{l} \forall P, (\forall \bar{g} \sigma, P \bar{g} \sigma [] \sigma) \implies \\ \dots \\ \left( \begin{array}{l} \forall \bar{g} x_f \bar{e} \bar{s} f \bar{h} \bar{d}_p \bar{d}_l \bar{s}_f e_f \sigma_1 \dots \sigma_7, \\ \text{getFundef } x_f \bar{g} = (f, \bar{h}) \implies \\ f = (\bar{d}_p, (\bar{d}_l, \bar{s}_f, e_f)) \implies \\ \sigma_1 \vdash_{args} (\bar{d}_p, \bar{e}) \rightsquigarrow \sigma_2 \implies \\ \sigma_2 \vdash_{cliL} \bar{d}_l \rightsquigarrow \sigma_3 \implies \\ P \bar{h} \sigma_3 \bar{s}_f \sigma_4 \implies \\ \text{clear } \bar{d}_l \sigma_4 = \sigma_5 \implies \\ \text{clear } \bar{d}_p \sigma_5 = \sigma_6 \implies \\ P \bar{g} \sigma_6 \bar{s} \sigma_7 \implies \\ P \bar{g} \sigma_1 (x_f(\bar{e}) :: \bar{s}) \sigma_7 \end{array} \right) \implies \\ \dots \\ \forall \sigma_1 \sigma_2 \bar{g} \bar{s}, \quad \sigma_1, \bar{g} \vdash \bar{s} \rightsquigarrow \sigma_2 \implies P \bar{g} \sigma_1 \bar{s} \sigma_2 \end{array} $$

<caption>Fig. 8: Deep induction principle for the call evaluation case</caption>

$$ \begin{array}{l} \text{state\_ext}(\Gamma, \gamma, \sigma_1, \sigma_2, x, \text{tr\_x}): \\ \forall v, \text{read } x \quad \sigma_1 = v \implies \\ \quad \text{read } x \quad \sigma_2 = v \quad \wedge \\ \quad (x \notin \gamma \implies \Gamma \vdash x : \tau \quad \wedge \quad \text{ts} \not\vdash \tau) \quad \wedge \\ \quad (x \in \gamma \implies \text{var\_ext}(\Gamma, \gamma, \sigma_1, \sigma_2, x, \gamma(x))) \end{array} $$

<caption>Fig. 9: State Extension</caption>

We define this property as `state_ext(\gamma, \sigma_1, \sigma_2)` in Fig. 9. We say that $\sigma_2$ is an extension of $\sigma_1$, when each variable $x$ from $\sigma_1$, has the same value in $\sigma_2$. If this variable has no tracker in $\gamma$, the `ts` type is not included into the variable's type. When $x$ has an associated tracker in $\gamma$, then it must also have a variable extension in $\sigma_2$.

The variable extension property, defined in Fig. 10, has two cases: base tracker (`ts_ext`) and pointer tracker (`ptr_ext`).

$$ \begin{array}{l} \text{var\_ext}(\Gamma, \gamma, \sigma_1, \sigma_2, x_1, \text{tr\_x}_1) := \\ \quad | \text{ts\_ext} v y_{ts} v_{ts}: \\ \qquad \Gamma \vdash x_1 : \mathbf{ts} \quad \wedge \quad \sigma_1 \vdash x_1 \rightsquigarrow (v, y_{ts}) \\ \qquad E(y_{ts}) = v_{ts} \quad \wedge \quad \sigma_2 \vdash \text{tr\_x}_1 \rightsquigarrow v_{ts} \\ \quad | \text{ptr\_ext} \tau x_2 \text{tr\_x}_2: \\ \qquad \Gamma \vdash x_1 : *\tau \quad \wedge \quad \sigma_1 \vdash x_1 \rightsquigarrow \text{Ptr } x_2 \\ \qquad \gamma(x_2) = \text{tr\_x}_2 \quad \wedge \quad \sigma_2 \vdash \text{tr\_x}_1 \rightsquigarrow \text{Ptr } \text{tr\_x}_2 \end{array} $$

<caption>Fig. 10: Variable Extension</caption>
In the base tracker case, the variable $x_1$ has type `ts`, and an associated typestate value $y_{ts}$ which is equivalent to the evaluation of its tracker $tr\_x_1$ in $\sigma_2$. In the pointer case, the variable `x` has a pointer type $*\tau$, its evaluation gives a pointer to $x_2$, and its tracker evaluation gives a pointer to $tr\_x_2$ which is the tracker of $x_2$. Note that this *variable extension property* implies that `ts` is included in the variable's type, which is impossible when `x` has no tracker.

In other words, values are unchanged for all classic variables, and every `ts` object has a tracker representing the same typestate as in $\sigma_{ts}$. This *state extension property* thus makes the link between the original program and its instrumentation. We want to prove that this property is preserved by a statement evaluation. Proof effort is still ongoing for this preservation property, but, again, the deep induction principle of Fig. 8 should help us with function calls.

## VII. RELATED WORK

Despite the fact that the original concept of typestates [5] was designed for languages without objects, recent works focused on Object-Oriented languages. Some of them use static analysis to try to determine program points which violates typestate specification [10]–[13]. Others rely on runtime monitoring guided by static analysis, known as *Hybrid typestates analysis* [14], [15].

We can also mention some works which developed programming languages with a built-in notion of typestate, like the *Plaid* [16] or *Obsidian* [17] languages. These languages come with a type system that prevent programmers from causing typestate errors. They are based on the concept of *Typestate-oriented programming* [18]–[20], which is derived from object-oriented programming: the methods of an object are typestate transitions and each instance of the object is tracked. The *TYPESTATES* plug-in verifies typestate properties with the help of the ACSL language. Unlike the *Typestate-oriented programming* paradigm, our plug-in allows for a typestate transition to involve more than one parameter. Furthermore, these approaches do not seem to feature a mechanized formalization similar to our SKEL development.

Typestate verification can also be implemented as a library in pre-existing languages. This is the case, for example, of the C++ [21] library *COCONUT* [22], and the RUST [23] library *TYPESTATE* [24]. This last library relies on RUST's type and macros system, to verify typestate properties, and supports non-deterministic transitions. Again, in both cases, a transition cannot include more than one object.

We used the meta-language SKEL for our formalization, but other semantic tools could have been used instead. For example, LEM [25] and OTT [26] languages, provide *LATEX*, *COQ*, *ISABELLE/HOL*, and *OCAML* generators. These languages are heavier and more complex than SKEL. Their *COQ* generators directly builds *COQ* definitions and inductives, and relies on a specific *COQ* library, whereas the SKEL language has a deep embedding in *COQ* and is thus more flexible.

The K framework allows writing operational semantics through rewrite rules. The KPROVER [27], [28] deductive

verification tool allows verifying reachability properties on a specific program. The K framework sees any semantics as a logical theory, where rewrite rules are axioms. However, we cannot prove semantics meta-properties with KPROVER.

DEDUKTI [29], [30], is a logical framework which allows interoperability between different formal proof tools (COQ, Isabelle/HOL [31], Lean [32], PVS [33] ...). KAMELO [34] allows translating any semantics from K into DEDUKTI. However, verification of proofs from KPROVER, and ability to check meta-properties from a K semantics into DEDUKTI are long-term goals of this work.

## VIII. CONCLUSION AND PERSPECTIVES

We have presented in this paper a formalization of the typestate instrumentation for a small C-like language, using the SKEL environment. This formalization was designed to verify the actual instrumentation procedure, performed by the FRAMA-C TYPESTATES plug-in. We have also detailed the current proof effort. In particular, our main objective is the *state extension property* and correctness of the instrumentation.

Furthermore, we want to increase the expressiveness of the specification language. First, we want to specify terminal typestates: every object should be in a terminal typestate at the end of its scope. This could be done easily by generating assertions during instrumentation. In a longer run, refined transitions' guards should be investigated.

Additionally, we would like the instrumentation to duplicate API functions with a *tracker-version*, instead of extending parameters with trackers. That way, original API functions are left unchanged. The *tracker-version* of an API function takes necessary tracker parameters, the function contract which verifies transitions, and the conditional which effectively updates trackers. This new version allows API functions to call others since the *tracker-function* does not depend on the original function implementation.

Finally, our languages are currently a tiny subset of C and ACSL. A longer term perspective is to extend the formalization of the instrumentation to the full languages. This would make it possible to unify mechanized formalizations that have been similarly proposed for other FRAMA-C plug-ins in the past, each on its own C fragment ([35]–[37]). However, this would require as a preliminary step a complete formalization of the semantics of both C and ACSL. While the former exists (see e.g. Krebbers' PhD [38]), the latter is still incomplete (Gauthier et al. [39] provide a first step, but this does not include all the necessary ingredients for TYPESTATES).

## ACKNOWLEDGEMENT

The authors wish to thank the anonymous reviewers for their insightful comments on a first version of this paper. This work has been partially done within the SECUREVAL project, funded by the "France 2030" government investment plan managed by the French National Research Agency, under the reference "ANR-22-PECY-0005", and the SecOPERA project, that has received support from the European Union's Horizon Europe research and innovation programme under grant agreement N° 101070599.
REFERENCES

[1] “ISO/IEC 9899:2018: Programming languages — C,” Standard, 2018. [Online]. Available: https://www.open-std.org/JTC1/SC22/WG14/www/docs/n2310.pdf

[2] P. Baudin, F. Bobot, D. Bühler, L. Correnson, F. Kirchner, N. Kosmatov, A. Maroneze, V. Perrelle, V. Prevosto, J. Signoles, and N. Williams, “The dogged pursuit of bug-free C programs: the Frama-C software analysis platform,” Commun. ACM, vol. 64, no. 8, p. 56–68, jul 2021. [Online]. Available: https://doi.org/10.1145/3470569

[3] N. Kosmatov, V. Prevosto, and J. Signoles, Eds., Guide to Software Verification with Frama-C: Core Components, Usages, and Applications, ser. Computer Science Foundations and Applied Logic. Springer Cham, 2024. [Online]. Available: https://doi.org/10.1007/978-3-031-55608-1

[4] P. Baudin, P. Cuoq, J.-C. Filliàtre, C. Marché, B. Monate, Y. Moy, and V. Prevosto, ACSL: ANSI/ISO C Specification Language. Version 1.20, Nov. 2024. [Online]. Available: https://frama-c.com/download/acsl.pdf

[5] R. E. Strom and S. Yemini, “Typestate: A programming language concept for enhancing software reliability,” IEEE Trans. Soft. Eng., vol. 12, no. 1, pp. 157–171, 1986. [Online]. Available: https://doi.org/10.1109/TSE.1986.6312929

[6] V. Robles, N. Kosmatov, V. Prevosto, L. Rilling, and P. Le Gall, “Methodology for specification and verification of high-level requirements with MetAcsl,” in IEEE/ACM 9th Inter. Conf. on Formal Methods in Soft. Eng. (FormaliSE), S. Bliudze, S. Gnesi, N. Plat, and L. Semini, Eds., 2021, pp. 54–67. [Online]. Available: https://doi.org/10.1109/FORMALISE52586.2021.00012

[7] M. Bodin, P. Gardner, T. Jensen, and A. Schmitt, “Skeletal Semantics and their Interpretations,” Proc. of the ACM on Prog. Lang., vol. 44, pp. 1–31, 2019. [Online]. Available: https://inria.hal.science/hal-01881863

[8] L. Noizet and A. Schmitt, “Stating and Handling Semantics with Skel and Necro,” Inria Rennes - Bretagne Atlantique, Research Report RR-9449, Jan. 2022. [Online]. Available: https://doi.org/10.1017/S0956796809990293

[9] Noizet, Louis and Schmitt, Alan, “Formalisation de Sémantiques Squelettiques,” in JFLA , Gruissan, France, Jan. 2020, pp. 1–14. [Online]. Available: https://inria.hal.science/hal-02512485

[10] N. E. Beckman and A. V. Nori, “Probabilistic, modular and scalable inference of typestate specifications,” SIGPLAN Not., vol. 46, no. 6, p. 211–221, jun 2011. [Online]. Available: https://doi.org/10.1145/1993316.1993524

[11] N. A. Naeem and O. Lhotak, “Typestate-like analysis of multiple interacting objects,” p. 347–366, 2008. [Online]. Available: https://doi.org/10.1145/1449764.1449792

[12] A. Arslanagić, P. Subotić, and J. A. Pérez, “Scalable typestate analysis for low-latency environments,” in Integrated Formal Methods, M. H. ter Beek and R. Monahan, Eds. Cham: Springer, 2022, pp. 322–340. [Online]. Available: https://doi.org/10.1007/978-3-031-07727-2_18

[13] R. DeLine and M. Fähndrich, “Typestates for objects,” in ECOOP 2004 - Object-Oriented Prog., ser. LNCS, M. Odersky, Ed., vol. 3086. Springer, 2004, pp. 465–490. [Online]. Available: https://doi.org/10.1007/978-3-540-24851-4_21

[14] E. Bodden and L. Hendren, “The Clara framework for hybrid typestate analysis,” Int. J. Soft. Tools Technol. Transf., vol. 14, no. 3, pp. 307–326, 2012. [Online]. Available: https://doi.org/10.1007/s10009-010-0183-5

[15] R. Wolff, R. Garcia, É. Tanter, and J. Aldrich, “Gradual typestate,” in ECOOP 2011 - Object-Oriented Prog., ser. LNCS, M. Mezini, Ed., vol. 6813. Springer, 2011, pp. 459–483. [Online]. Available: https://doi.org/10.1007/978-3-642-22655-7_22

[16] J. Aldrich, R. Bocchino, R. Garcia, M. Hahnenberg, M. Mohr, K. Naden, D. Saini, S. Stork, J. Sunshine, E. Tanter, and R. Wolff, “Plaid: A permission-based programming language,” in Proc. of the ACM Inter. Conf. Comp. on Object Oriented Prog. Sys. Lang. and App. Comp., ser. OOPSLA ’11, New York, NY, USA, 2011, p. 183–184. [Online]. Available: https://doi.org/10.1145/2048147.2048197

[17] M. Coblenz, R. Oei, T. Etzel, P. Koronkevich, M. Baker, Y. Bloem, B. A. Myers, J. Sunshine, and J. Aldrich, “Obsidian: Typestate and assets for safer blockchain programming,” ACM Trans. Prog. Lang. Syst., vol. 42, no. 3, nov 2020. [Online]. Available: https://doi.org/10.1145/3417516

[18] J. Aldrich, J. Sunshine, D. Saini, and Z. Sparks, “Typestate-oriented programming,” in Proc. of the 24th ACM SIGPLAN Conf. Comp. on Object Oriented Prog. Sys. Lang. and App., New York, NY, USA, 2009, p. 1015–1022. [Online]. Available: https://doi.org/10.1145/1639950.1640073

[19] R. Garcia, E. Tanter, R. Wolff, and J. Aldrich, “Foundations of typestate-oriented programming,” ACM Trans. Prog. Lang. Syst., vol. 36, no. 4, oct 2014. [Online]. Available: https://doi.org/10.1145/2629609

[20] L. Padovani, “Deadlock-free typestate-oriented programming,” CoRR, 2018. [Online]. Available: http://arxiv.org/abs/1803.10670

[21] “ISO/IEC 14882:2020: Programming languages — C++,” Standard, 2020. [Online]. Available: https://www.iso.org/standard/79358.html

[22] A. H. Alsubhi and O. Dardha, Coconut: Typestates for C++. [Online]. Available: http://www.dcs.gla.ac.uk/~ornela/publications/AD22.pdf

[23] N. D. Matsakis and F. S. Klock, II, “The rust language,” in Proc. of the 2014 ACM SIGAda annual conference on High integrity lang. technology, HILT, 2014, pp. 103–104. [Online]. Available: https://doi.org/10.1145/2663171.2663188

[24] J. Duarte and A. Ravara, “Retrofitting typestates into rust,” in 25th Brazilian Symp. on Prog. Lang., ser. SBLP’21, 2021, p. 83–91. [Online]. Available: https://doi.org/10.1145/3475061.3475082

[25] D. P. Mulligan, S. Owens, K. E. Gray, T. Ridge, and P. Sewell, “Lem: Reusable engineering of real-world semantics,” SIGPLAN Not., vol. 49, no. 9, p. 175–188, aug 2014. [Online]. Available: https://doi.org/10.1145/2692915.2628143

[26] P. Sewell, F. Zappa-Nardelli, S. Owens, G. Peskine, T. Ridge, S. Sarkar, and R. Strniša, “Ott: Effective tool support for the working semanticist,” Journal of Fun. Prog., vol. 20, no. 1, p. 71–122, 2010. [Online]. Available: https://hal-cea.archives-ouvertes.fr/cea-01809013

[27] A. Stefănescu, D. Park, S. Yuwen, Y. Li, and G. Roșu, “Semantics-based program verifiers for all languages,” SIGPLAN Not., vol. 51, no. 10, p. 74–91, Oct. 2016. [Online]. Available: https://doi.org/10.1145/3475061.3475082

[28] K framework. Accessed 2024-10-28. [Online]. Available: https://kfframework.org/

[29] A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek, C. Dubois, F. Gilbert, P. Halmagrand, O. Hermant and R. Saillard, “Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system,” in TYPES: Types for Proofs and Programs , Novi SAd, Serbia, May 2016. [Online]. Available: https://minesparis-psl.hal.science/hal-01441751

[30] Dedukti - a logical framework. Accessed 2024-10-28. [Online]. Available: https://deducteam.github.io/

[31] T. Nipkow, M. Wenzel, and L. C. Paulson, Isabelle/HOL: a proof assistant for higher-order logic. Springer, 2002. [Online]. Available: https://doi.org/10.1007/3-540-45949-9

[32] L. De Moura, S. Kong, J. Avigad, F. Van Doorn, and J. von Raumer, “The lean theorem prover (system description),” in CADE-25: 25th Inter. Conf. on Automated Deduction, Proc. Springer, 2015, pp. 378–388. [Online]. Available: https://doi.org/10.1007/978-3-319-21401-6_26

[33] S. Owre, J. M. Rushby, and N. Shankar, “Pvs: a prototype verification system,” in Inter. Conf. on Auto. Deduction. Springer, 1992, pp. 748–752. [Online]. Available: https://doi.org/10.1007/3-540-55602-8_217

[34] A. Ledein, V. Blot, and C. Dubois, “A semantics of K into dedukti,” in 28th Inter. Conf. on Types for Proofs and Programs (TYPES). Nantes, France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Jul. 2023. [Online]. Available: https://inria.hal.science/hal-03895834

[35] P. Herms, “Certification of a Tool Chain for Deductive Program Verification,” Theses, Université Paris Sud - Paris XI, Jan. 2013. [Online]. Available: https://tel.archives-ouvertes.fr/tel-00789543

[36] A. Blanchard, F. Louergue, and N. Kosmatov, “From concurrent programs to simulating sequential programs: Correctness of a transformation,” Elec. Proc. in Theoretical Computer Science, vol. 253, pp. 109–123, Aug. 2017. [Online]. Available: http://doi.org/10.4204/eptcs.253.9

[37] L. Blatter, N. Kosmatov, V. Prevosto, and P. L. Gall, “An Efficient VCGen-Based Modular Verification of Relational Properties,” in 11th Inter. Symp. on Leveraging App. of Formal Methods, Verification and Validation, ISoLA 2022, ser. LNCS, T. Margaria and B. Steffen, Eds., vol. 13701. Springer, 2022, pp. 498–516. [Online]. Available: https://doi.org/10.1007/978-3-031-19849-6_28

[38] R. Krebbers, “The C standard formalized in Coq,” Ph.D. dissertation, Radboud University Nijmegen, 2015. [Online]. Available: https://doi.org/10.1145/3022671.2984027

[39] L. Gauthier, V. Prevosto, and J. Signoles, “A semantics of structures, unions, and underspecified terms for formal specification,” in Proc. of the 2024 IEEE/ACM 12th Inter. Conf. on Formal Methods in Soft. Eng., ser. FormaliSE ’24, New York, NY, USA, 2024, pp. 100–110. [Online]. Available: 10.1145/3644033.3644380