Martin Bodin

Philippa Gardner

Thomas Jensen

Alan Schmitt

Skeletal Semantics and Their Interpretations *

Keywords: CCS Concepts:, Theory of computation → Program semantics; programming language, semantics, abstract interpretation

The development of mechanised language specification based on structured operational semantics, with applications to verified compilers and sound program analysis, requires huge effort. General theory and frameworks have been proposed to help with this effort. However, none of this work provides a systematic way of developing concrete and abstract semantics, connected together by a general consistency result. We introduce a skeletal semantics of a language, where each skeleton describes the complete semantic behaviour of a language construct. We define a general notion of interpretation, which provides a systematic and language-independent way of deriving semantic judgements from the skeletal semantics. We explore four generic interpretations: a simple well-formedness interpretation; a concrete interpretation; an abstract interpretation; and a constraint generator for flow-sensitive analysis. We prove general consistency results between interpretations, depending only on simple language-dependent lemmas. We illustrate our ideas using a simple While language.

INTRODUCTION

Plotkin's Structural Operational Semantics [START_REF] Plotkin | A Structural Approach to Operational Semantics[END_REF]] provides a methodology for formally describing a programming language using a collection of inference rules. It has been widely used to provide, for example, mechanised language specifications of substantial parts of ML [START_REF] Owens | A Sound Semantics for OCamllight[END_REF]], C [START_REF] Blazy | Mechanized semantics for the Clight subset of the C language[END_REF][START_REF] Norrish | C formalised in HOL[END_REF]] and JavaScript [START_REF] Bodin | A Trusted Mechanised JavaScript Specification[END_REF]]. These specifications have, in turn, been used to build verified compilers [START_REF] Kumar | CakeML: a verified implementation of ML[END_REF][START_REF] Leroy | Formal certification of a compiler back-end, or: programming a compiler with a proof assistant[END_REF]] and to develop sound program analysis [START_REF] Cachera | Extracting a data flow analyser in constructive logic[END_REF][START_REF] Jourdan | A Formally-Verified C Static Analyzer[END_REF][START_REF] Klein | Verified Bytecode Verifiers[END_REF]. Such language specifications and their applications require huge effort, stretching the fundamental theory and tools to their limits. Researchers have therefore spent considerable thought developing general theories and frameworks where some of this effort can be unified for a wide class of languages.

Abstract interpretation [START_REF] Cousot | Abstract Interpretation: A unified lattice model for static analysis of programs by construction of approximations of fixpoints[END_REF]] is a well-known general theory for analysing programs. It provides general definitions for describing when an abstract semantics is consistent (sound) with respect to a concrete semantics, and even suggests a methodology for how to construct consistent abstract semantics from concrete semantics [START_REF] Cousot | The Calculational Design of a Generic Abstract Interpreter[END_REF][START_REF] Midtgaard | A Calculational Approach to Control-Flow Analysis by Abstract Interpretation[END_REF][START_REF] Van Horn | Abstracting Abstract Machines: A Systematic Approach to Higher-order Program Analysis[END_REF]. We focus on abstract semantics arising from concrete operational semantics. A prominent example can be found in the Verasco project [START_REF] Jourdan | A Formally-Verified C Static Analyzer[END_REF]] which provides a Coq-certified static analyser based on abstract interpretation, specifically targeting Com-pCert's mechanised C specification. Schmidt [START_REF] Schmidt | Natural-semantics-based Abstract Interpretation (preliminary version)[END_REF][Schmidt , 1997a] ] has demonstrated how to build abstract derivations from concrete derivations arising from an operational semantics, illustrating a close connection between the abstract and concrete semantics. The concepts are general, but the work does not attempt to be systematic. Inspired by Schmidt, Bodin et al. [Bodin et al. 2015] have identified a general rule format that can be systematically instantiated to both concrete and abstract semantics, with a general consistency result. However, their general rule format is based on a non-standard style of operational semantics, called pretty-big-step operational semantics [START_REF] Charguéraud | Pretty-big-step Semantics[END_REF], introduced to provide a Coq-mechanised specification of JavaScript [START_REF] Bodin | A Trusted Mechanised JavaScript Specification[END_REF]. It does not provide a general systematic approach for constructing an abstract semantics from a standard operational semantics.

A general framework provides a unifying meta-language for writing operational inference rules, in order to develop general environments for analysis [START_REF] Harper | A Framework for Defining Logics[END_REF][START_REF] Jung | Iris from the Ground Up[END_REF][START_REF] Pfenning | System Description: Twelf -A Meta-Logical Framework for Deductive Systems[END_REF][START_REF] Roşu | An Overview of the K Semantic Framework[END_REF]. Much of the work on frameworks does not aim to describe abstract analysis. One notable exception is the Iris framework [START_REF] Jung | Iris from the Ground Up[END_REF]] for reasoning about concurrent programs. Iris provides a systematic method for building a concurrent program logic from concrete operational semantics, proving a general consistency result. It starts from a concrete operational semantics and generically builds the program logic. Consequently, the general consistency result relies on language-dependent lemmas which require an induction over the possibly complex constructs of the language. It does not work with abstract semantics in general, and the lemmas associated with the general consistency result are difficult to prove.

We introduce a new approach. We have developed a meta-language, which we call a skeletal semantics, from which it is possible to construct systematically both concrete and abstract semantics, and prove a general consistency result. Our skeletal semantics comprises:

• skeletons, where each skeleton describes the complete behaviour of one language construct; • generic interpretations, which systematically derive semantic judgements from the skeletons:

for example, a generic concrete interpretation built using the usual concrete judgements of an operational semantics, parameterised by an input state, command and output state, and a generic abstract interpretation built from more abstract judgements over abstract domains; • a general consistency result between interpretations, which depends on simple languagedependent lemmas.

Our definitions of skeletal semantics and interpretations have been mechanised in the Coq theorem prover, and the consistency result proved. Skeletal semantics can be used to describe languages specified using big-step operational semantics and languages specified using an English standard such as the ECMAScript standard. In this introductory paper, we focus on a simple While language as the illustrative example; the lambda calculus is given in the Coq artefact. Consider the usual if command of a While language, whose behaviour is typically defined in an operational semantics using two standard rules for the true and false case. Instead, in our skeletal semantics, the behaviour of the if command is given by one skeleton comprising: a semantic judgement, in this case parameterised by input state, expression and value, and instantiated via the interpretations with, for example, the usual concrete and abstract judgements for evaluating expressions; then a branch of two paths guarded by filters for determining the true and false case, followed by judgements for the appropriate subcommands. Our if skeleton thus describes the information given in the two normal if rules, collected together under one syntactic construct. Skeletons provide all the information necessary to give systematically both concrete and abstract interpretations. Intuitively, our generic concrete interpretation picks one path from each branching/merging of the skeleton, whereas our generic abstract interpretation merges all the appropriate paths. In fact, our interpretations span many different types of analysis. The paper contains a simple well-formedness interpretation for simple sorts, suggesting that we can give many forms of standard well-formedness result associated with states and types. We also give an interpretation building a constraint generator for flow-sensitive analysis. We discuss other forms of analyses in future work.

We have proved general consistency results between interpretations, which depend on simple language-dependent filter lemmas. These filter lemmas only describe properties of the filters of a language, which are functions on the language values. The complexity of proving these filter lemmas thus only depends on the complexity the filters, which are simple in comparison with the complexity of the whole language. We explore the instantiation of our consistency result for our While language, demonstrating the consistency of the abstract interpretation with respect to the concrete interpretation for a selection of domains, as well as the consistency between the constraint generation and the abstract interpretation.

In summary, we have come a long way to answering the challenge of developing a languageindependent framework for relating concrete and abstract semantics. The real test will come when we move from the simple languages explored in this paper to real-world languages such as OCaml and JavaScript, discussed in the future work.

Example: the While Language

We demonstrate our skeletal semantics in action using the simple conditional statement from the While language. Consider the usual concrete rules associated with the conditional statement in Figure 1, and the abstract rules in Figure 2, supposing that the Booleans are abstracted by the usual four-valued lattice given by true # , false # , ⊤ bool , ⊥ bool . These abstract rules are intuitively correct, but they are first built in an ad hoc way and then shown to be related to the concrete rules using a Galois connection. More generally, the systematic construction of abstract rules from concrete rules requires a deep understanding of how the analysed programming language evaluates expressions: in a case like a vanilla While language, this is quite straightforward; for a complex language such as JavaScript [START_REF] Bodin | A Trusted Mechanised JavaScript Specification[END_REF]ECMA 2018;[START_REF] Maffeis | An Operational Semantics for JavaScript[END_REF], the relationship between the concrete and abstract semantics can be difficult to get right.

We define the skeletal semantics in Section 2, which provides a general meta-theory for defining language semantics. Figure 3 shows the skeleton associated with the if construct, with generic subterms denoted by x t 1 , x t 2 , and x t 3 , input state x σ and output state x o . Judgements of the form H (-, x t i , -) identify the required subcomputations associated with the subterms x t 1 , x t 2 , x t 3 . The skeleton stitches these judgements together, using the input and output states, the internal symbolic variable x f 1 , and the branching which identifies paths through the skeleton using the filters isTrue and isFalse, resulting in the output state x o . Such a skeleton thus explicitly describes both the data

σ, e ⇓ true # σ, t 1 ⇓ x o σ, if e t 1 t 2 ⇓ x o σ, e ⇓ false # σ, t 2 ⇓ x o σ, if e t 1 t 2 ⇓ x o σ, e ⇓ ⊤ bool σ, t 1 ⇓ x o σ, t 2 ⇓ x o σ, if e t 1 t 2 ⇓ x o σ, e ⇓ ⊥ bool σ, if e t 1 t 2 ⇓ ⊥ Fig. 2. Usual abstract rules for the if construct If if x t 1 x t 2 x t 3       H x σ , x t 1 , x f 1 ; isTrue x f 1 ; H x σ , x t 2 , x o isFalse x f 1 ; H x σ , x t 3 , x o {x o }       Fig. 3. Skeleton for the if construct
flow and the control flow associated with a language construct, identifying the common pattern underlying the concrete and abstract rules. We provide a general definition of interpretation for our skeletal semantics in Section 3 and study four generic interpretations:

• A simple well-formedness interpretation (Section 3), which states that the stitching of the skeleton in Figure 3 respects the sorting of the basic constructs. • The concrete interpretation (Section 4), which intuitively picks one path from each branching of the skeleton, corresponding to the two rules of Figure 1. • The abstract interpretation (Section 5), whose complex definition (Figure 10) boils down to the intuitive description given by the rule of Figure 4: a rule with optional branches, considering all paths compatible with the return value of the expression e. This rule naturally subsumes the four rules of Figure 2. • A constraint generator for flow-sensitive static analysis (Section 7). Although these constraints are different in nature to the abstract semantics, they are expressed in our meta-theory using the same mechanism: that is, an interpretation of the skeletal semantics. This provides a strong connection between them. We also provide general definitions of consistency between interpretations (Section 3.2), with general consistency proofs based on filter lemmas (Section 3.3). The shared structure of our different interpretations greatly eases the proof process. We use our consistency definitions to show that the abstract interpretation is correct with respect to the concrete interpretation, and that any solution to the constraints given by our constraint generator must give rise to a correct abstract semantics.

Throughout the paper, we instantiate our definitions and results to the While language as a way of introducing our ideas and demonstrating how classic proof techniques based on an abstract interpretation of While can be captured with our approach (Section 6). We however emphasise that skeletons and interpretations, as well as their consistency proofs, are generic and can be applied to any programming language. To begin to illustrate this, we extend our While language with exceptions, input/output and a heap in Section 8.

The definitions and proofs of Sections 2 to 5 have been formalised in Coq; those of Sections 6 and 7 have been proven on paper. They are all available from the companion website1 . We also assume a countable set of sorts, ranged over by s. The sorts are separated into base sorts, for base terms, and program sorts, for terms built using constructors. Any base term belongs to a single base sort. The signature of a constructor c, written sig(c), is of the form (s 1 ..s n ) → s, where n is the arity of c, the s i for i = 1..n are sorts, and s is a program sort.

σ # , e ⇓ v # ⟦isTrue⟧ # v # =⇒ σ # , t 1 ⇓ σ # o ⟦isFalse⟧ # v # =⇒ σ # , t 2 ⇓ σ # o σ # , if e t 1 t 2 ⇓ σ # o Fig. 4.
Running Example. For the While language, the base sorts are ident for the program variables and lit for the literals. Program sorts are expr for expressions and stat for statements. The signature of constructors is given in Figure 5.

Let Γ be a mapping from term variables to sorts. Sorted terms are either base terms, term variables x t of sort Γ(x t ), or a term c(t 1 ..t n ) of sort s, where c has signature sig(c) = (s 1 ..s n ) → s and the terms t 1 ..t n have the appropriate sort. We write Sort Γ (t) for the sort of t. Let E be a mapping from term variables to terms such that ∀x t ∈ dom(E), Sort Γ (E(x t )) = Γ(x t ). We extend it to terms as E(c(t 1 ..t n )) = c(E(t 1 )..E(t n )) when defined. We write Sort (t) for Sort ∅ (t) and Tvar(t) for the set of term variables in t. We say t is closed if Tvar(t) = ∅. In that case, we write t : s for Sort (t) = s.

Lemma 2.1. Let t a term, E an environment mapping term variables to closed terms, and Γ a sorting environment such that Tvar(t) ⊆ dom(E), Tvar(t) ⊆ dom(Γ), and for any x t ∈ Tvar(t) we have Γ(x t ) = Sort (E(x t )). Then we have Sort Γ (t) = Sort (E(t)).

Skeletons

We assume a countable set of flow variables, ranged over by x f , which are used in the skeleton bodies to hold semantic values (states, intermediate values, . . . ). Among flow variables, we distinguish two of them: x σ holds the semantic state at the start of a skeleton, and x o is supposed to hold the semantic result at the end of a skeleton. We let skeletal variables, ranged over by x or y, be the

Lit(const (x t )) litInt (x t ) ? ▷ x f 1 ; intVal x f 1 ? ▷ x o Var(var (x t )) [read (x t , x σ ) ? ▷ x o ] Add x t 1 + x t 2 H x σ , x t 1 , x f 1 ; isInt x f 1 ? ▷ x f 1 ′ ; H x σ , x t 2 , x f 2 ; isInt x f 2 ? ▷ x f 2 ′ ; add x f 1 ′ , x f 2 ′ ? ▷ x f 3 ; intVal x f 3 ? ▷ x o Eq x t 1 = x t 2 H x σ , x t 1 , x f 1 ; isInt x f 1 ? ▷ x f 1 ′ ; H x σ , x t 2 , x f 2 ; isInt x f 2 ? ▷ x f 2 ′ ; eq x f 1 ′ , x f 2 ′ ? ▷ x f 3 ; boolVal x f 3 ? ▷ x o Neg(¬x t ) H x σ , x t , x f 1 ; isBool x f 1 ? ▷ x f 2 ; neg x f 2 ? ▷ x f 3 ; boolVal x f 3 ? ▷ x o Skip(skip) [id (x σ ) ? ▷ x o ] Asn x t 1 := x t 2 H x σ , x t 2 , x f 1 ; write x t 1 , x σ , x f 1 ? ▷ x o Seq x t 1 ; x t 2 H x σ , x t 1 , x f 1 ; H x f 1 , x t 2 , x o If if x t 1 x t 2 x t 3       H x σ , x t 1 , x f 1 ; isBool x f 1 ? ▷ x f 1 ′ ; isTrue x f 1 ′ ; H x σ , x t 2 , x o isFalse x f 1 ′ ; H x σ , x t 3 , x o {x o }       While while x t 1 x t 2         H x σ , x t 1 , x f 1 ; isBool x f 1 ? ▷ x f 1 ′ ; isTrue x f 1 ′ ; H x σ , x t 2 , x f 2 ; H x f 2 , while x t 1 x t 2 , x o isFalse x f 1 ′ ; id (x σ ) ? ▷ x o {x o }        
Fig. 6. Skeletal semantics for While union of term variables and flow variables. A skeleton has the shape Name(c(x t 1 ..x t n )) S, where Name is the skeleton name, c is a constructor, x t 1 ..x t n are term variables, and S is the skeleton body:

Skeleton Body S [] | B; S Bone B H x f 1 , t, x f 2 | F (x 1 ..x n ) ? ▷ (y 1 ..y m ) | (S 1 ..S n ) V
where H (-, -, -) is the (terminal) hook constructor and F ranges over the set of filter functions.

A skeleton body is a sequence of bones. A bone is either a hook judgement H (x f 1 , t, x f 2 ), built using the constructor H (-, -, -) from an input flow variable x f 1 , a term t to be hooked during interpretation, and an output flow variable x f 2 ; or a filter F (x 1 ..x n ) ? ▷ (y 1 ..y m ) which tests if the values bound to its input skeletal variables (x 1 ..x n ) satisfy a condition specified by F , and in that case outputs values to be bound to (y 1 ..y m ); or a set of branches (S 1 ..S n ) V which represent the different behavioural pathways, where V declares the skeletal variables that are shared and must be defined by all branches.

A filter with no output skeletal variables is simply written F (x 1 ..x n ). It then acts as a predicate.

Requirement 2.2. We require that there exists exactly one skeleton for any given constructor c.

Running Example. The skeletons of our While example are given in Figure 6. Requirement 2.2 is trivially satisfied.

Flow Sorts

We extend the sorts with flow sorts, that are the sorts of values in interpretations. In our running example, flow sorts are store for the variable store, val for values, int for integers, and bool for Booleans. We relate flow sorts to hooks and filters as follows.

f fsort(f ) litInt lit → int intVal int → val isInt val → int add (int, int) → int f fsort(f ) boolVal bool → val isBool val → bool isTrue bool → () isFalse bool → () f fsort(f ) eq (int, int) → bool neg bool → bool read
(ident, store) → val write (ident, store, val) → store id store → store In a hook H (x f 1 , t, x f 2 ), the flow variable x f 1 stands for an input state that fits with t, and x f 2 stands for a result. Given a program sort s, we define in(s) as its input flow sort and out(s) as its output flow sort. In our running example, the input flow sort of both expressions and statements is store. The output flow sort of expressions is val and the output flow sort of statements is store.

Similarly, a filter F (x 1 ..x n ) ? ▷ (y 1 ..y m ) is assigned a signature, written fsort(F ), of the form (s 1 ..s n ) → (s ′ 1 ..s ′ m ). We write () for the output sort of a filter if m = 0 and omit the enclosing parentheses when n or m is 1. Filter signatures for our running example are given in Figure 7.

We check the consistency of the hook and filters with the skeletons in our well-formedness interpretation, introduced in Section 3.1.

INTERPRETATIONS

An interpretation I specifies base terms and how to interpret the empty skeleton body, hooks, filters, and branches. It defines a set of interpretation states, ranged over by Σ in this section but with specific notations for each interpretation, and a set of interpretation results, ranged over by O in this section, as well as the following relations:

• ⟦[]⟧ I (Σ) ⇓ O defining the interpretation of the empty skeleton body;

• H (x f 1 , t, x f 2 ) I (Σ) ⇓ Σ ′ defining the interpretation of a hook; • ⟦F (x 1 ..x n ) ? ▷ (y 1 ..y m )⟧ I (Σ) ⇓ Σ ′
defining the interpretation of a filter, for each filter F ;

• n I V (O, Σ) ⇓ Σ ′
defining the merging of the interpretation of branches, where O is a partial function from [1..n] to interpretation results, and where V is the set of skeletal variables defined and shared by all branches.

Given a skeleton body S and the relations above, we define the remaining cases for the interpretation of S as follows.

⟦B⟧ I (Σ) ⇓ Σ ′ ⟦S⟧ I (Σ ′ ) ⇓ O =⇒ ⟦B; S⟧ I (Σ) ⇓ O ∀i ∈ dom (O) . ⟦S i ⟧ I (Σ) ⇓ O (i) n I V (O, Σ) ⇓ Σ ′ =⇒ ⟦(S 1 ..S n ) V ⟧ I V (Σ) ⇓ Σ ′
Interpretations enable us to define the meaning of skeletons by only specifying the parts that matter. Interpretations apply to any skeletons and are thus independent of the language. The rest of the paper presents different interpretation and their relations.

Well-Formedness Interpretation

The first interpretation we consider is a well-formedness interpretation, to verify that every skeleton is well formed. More precisely, we verify that every skeletal variable used has been first defined, that every variable defined in a skeleton is fresh (with an exception for branches, see below), and that the sorting of filters, hooks, and branches are consistent.

Intuitively, in the hook H (x f 1 , t, x f 2 ), flow variable x f 1 is used and flow variable x f 2 is defined. Similarly, in the filter F (x 1 ..x n ) ? ▷ (y 1 ..y m ), skeletal variables (x 1 ..x n ) are used and skeletal variables (y 1 ..y m ) are defined. The case for branches (S 1 ..S n ) V is a bit more involved. First, each branch S i must define the skeletal variables in V . Second, every variable defined in the whole set of branches must be distinct, with the exception of the variables in V as they have to be defined in every branch. And third, the only variables defined by the branches that may be used in the rest of the skeleton body are those in V .

Assuming for each base sort a set of base terms, pairwise disjoint, we define the well-formedness (WF) interpretation in Figure 8. Its interpretation states and result consist of a pair of a sorting environments Γ, mapping term variables to base and program sorts, and flow variables to flow sorts, and a set D of skeletal variables that have been defined at that point. In this interpretation, we write x : s to state that the kind of variable and sort match, namely term variables with base or program sorts, and flow variables with flow sorts.

The interpretation for the empty skeleton body is trivial, it simply returns its arguments. The interpretation of a hook H (x f 1 , t, x f 2 ) checks that x f 1 is in Γ, that every term variable of t is also in Γ, and that variable x f 2 is fresh (i.e., not in D). In addition, it checks that the sort for x f 1 is what t expects as input sort and that x f 2 is latter bound to an output sort of t.

The interpretation for a filter F (x 1 ..x n ) ? ▷ (y 1 ..y m ) is similar. It ensures that the input skeletal variables (x 1 ..x n ) are in Γ, that the number and kind of both input and output variables match the signature of F , that the output variables are fresh, that the sort of the input variable corresponds to the input signature of F , and it continues binding the output variables to the output signature of F .

Finally, the interpretation of the merging of branches checks that every branch is well formed, that the variables in V are exactly those shared by the branches (neither less nor more than those), and that the sorting environments returned by the branches all agree when restricted to V . In that case, the returned sorting environment is the concatenation of the input environment and the one shared by the branches. The n ≥ 2 constraint is to have a more concise way of stating that the variables shared by the branches are exactly those in V . It is not a restriction as an empty set of branches is useless, it prevents the skeleton from being interpreted as offering no pathway, and a singleton set of branches can be inlined.

Let t = c(t 1 ..t n ) be a closed term such that Sort (t) = s, where s is a program sort. There are two ways to assign an output sort to t: directly, as out(s), or using the WF interpretation of the skeleton for c to compute the associated sort x o . If both coincide, we say the skeleton is well formed.

Definition 3.1. A skeleton Name(c(x t 1 ..x t n )) S is well formed iff for any closed term t = c(t 1 ..t n ) such that Sort (t) = s, we have ⟦S⟧ wf (Γ, D) ⇓ (Γ ′ , D ′ ) and Γ ′ (x o ) = out(s), with the initial sorting environment Γ being x σ → in(s) + x t 1 → Sort (t 1 )..x t n → Sort (t n )
, and with D = dom(Γ).

In the following we only consider well-formed skeletons. For instance, the skeletons for While are well formed.

Interpretation Consistency

We now define how to relate interpretations. Given interpretations I 1 and I 2 , we assume a relation OKst(Σ 1 , Σ 2 ) between the interpretation states, and a relation OKout(O 1 , O 2 ) between their results. Intuitively, consistency is the propagation of these relations along interpretations.

=⇒ ⟦[]⟧ wf (Γ, D) ⇓ (Γ, D) x f 1 ∈ dom (Γ) ⊆ D Tvar (t) ⊆ dom (Γ) Γ x f 1 = in (Sort Γ (t)) x f 2 D Γ ′ = Γ + x f 2 → out (Sort Γ (t)) D ′ = D ∪ x f 2 =⇒ H x f 1 , t, x f 2 wf (Γ, D) ⇓ (Γ ′ , D ′ ) (x 1 ..x n ) ⊆ dom (Γ) ⊆ D (x 1 ..x n ) : (Γ (x 1 ) ..Γ (x n )) y 1 ..y m are pairwise distinct (y 1 ..y m ) ∩ D = ∅ fsort (F ) = (Γ (x 1 ) ..Γ (x n )) → (s 1 ..s m ) (y 1 ..y m ) : (s 1 ..s m ) Γ ′ = Γ + (y 1 ..y m ) → (s 1 ..s m ) D ′ = D ∪ (y 1 ..y m ) =⇒ ⟦F (x 1 ..x n ) ? ▷ (y 1 ..y m )⟧ wf (Γ, D) ⇓ (Γ ′ , D ′ ) n ≥ 2 dom (Γ) ⊆ D ∀i ∈ [1..n].O (i) = (Γ i , D i ) ∀i ∈ [1..n].dom (Γ i ) ⊆ D i ∀ij.i j =⇒ (D i \ D) ∩ D j \ D = V ∀i ∈ [1..n].Γ + Γ i | V = Γ ′ D ′ = i ∈[1..n] D i =⇒ n wf V (O, (Γ, D)) ⇓ (Γ ′ , D ′ ) Fig. 8. WF Interpretation
We define two kinds of consistency: one about where interpretations are defined, i.e, whether they return a result, and one about their results.

Definition 3.2. Interpretation I 1 is existentially consistent with interpretation I 2 if for any S, Σ 1 , Σ 2 , and O 1 , such that OKst(Σ 1 , Σ 2 ) and ⟦S⟧ I 1 (Σ 1 ) ⇓ O 1 , there exists a O 2 such that ⟦S⟧ I 2 (Σ 2 ) ⇓ O 2 and OKout(O 1 , O 2 ). Definition 3.3. Interpretations I 1 and I 2 are universally consistent if for any S, Σ 1 , Σ 2 , O 1 , and O 2 , if OKst(Σ 1 , Σ 2 ), ⟦S⟧ I 1 (Σ 1 ) ⇓ O 1 and ⟦S⟧ I 2 (Σ 2 ) ⇓ O 2 , then OKout(O 1 , O 2 ).

Proving Consistency

Both consistency properties can be stated at the level of the building block of interpretations. Formally, we have the following two lemmas. Lemma 3.4. Let I 1 and I 2 be two interpretations, OKst a relation between their input states, and OKout a relation between their output states. If for any Σ 1 and Σ 2 such that OKst(Σ 1 , Σ 2 ) we have

(1) ⟦[]⟧ I 1 (Σ 1 ) ⇓ O 1 =⇒ ∃O 2 . ⟦[]⟧ I 2 (Σ 2 ) ⇓ O 2 ∧ OKout(O 1 , O 2 ) (2) H (x f 1 , t, x f 2 ) I 1 (Σ 1 ) ⇓ Σ ′ 1 =⇒ ∃Σ ′ 2 . H (x f 1 , t, x f 2 ) I 2 (Σ 2 ) ⇓ Σ ′ 2 ∧ OKst(Σ ′ 1 , Σ ′ 2 ) (3) ⟦F (x 1 ..x n ) ? ▷ (y 1 ..y m )⟧ I 1 (Σ 1 ) ⇓ Σ ′ 1 =⇒ ∃Σ ′ 2 . ⟦F (x 1 ..x n ) ? ▷ (y 1 ..y m )⟧ I 2 (Σ 2 ) ⇓ Σ ′ 2 ∧ OKst(Σ ′ 1 , Σ ′ 2 ) (4) dom(O 1 ) = dom(O 2 ) ⊆ {1..n} ∧ ∀i ∈ dom(O 1 ).OKout(O 1 (i), O 2 (i)) ∧ n I V (O 1 , Σ 1 ) ⇓ Σ ′ 1 =⇒ ∃Σ ′ 2 . n I V (O 2 , Σ 2 ) ⇓ Σ ′ 2 ∧ OKst(Σ ′ 1 , Σ ′ 2 ) then I 1 is existentially consistent with I 2 .
Lemma 3.5. Let I 1 and I 2 be two interpretations, and OKst a relation between their input states. If for any Σ 1 and Σ 2 such that OKst(Σ 1 , Σ 2 ) we have

(1) ⟦[]⟧ I 1 (Σ 1 ) ⇓ O 1 ∧ ⟦[]⟧ I 2 (Σ 2 ) ⇓ O 2 =⇒ OKout(O 1 , O 2 ) (2) H (x f 1 , t, x f 2 ) I 1 (Σ 1 ) ⇓ Σ ′ 1 ∧ H (x f 1 , t, x f 2 ) I 2 (Σ 2 ) ⇓ Σ ′ 2 =⇒ OKst(Σ ′ 1 , Σ ′ 2 ) (3) ⟦F (x 1 ..x n ) ? ▷ (y 1 ..y m )⟧ I 1 (Σ 1 ) ⇓ Σ ′ 1 ∧ ⟦F (x 1 ..x n ) ? ▷ (y 1 ..y m )⟧ I 2 (Σ 2 ) ⇓ Σ ′ 2 =⇒ OKst(Σ ′ 1 , Σ ′ 2 ) (4) dom(O 1 ) ⊆ {1..n} ∧ dom(O 2 ) ⊆ {1..n} ∧ ∀i ∈ dom(O 1 ) ∩ dom(O 2 ).OKout(O 1 (i), O 2 (i)) ∧ n I V (O 1 , Σ 1 ) ⇓ Σ ′ 1 ∧ n I V (O 2 , Σ 2 ) ⇓ Σ ′ 2 =⇒ OKst(Σ ′ 1 , Σ ′
2 ) then I 1 and I 2 are universally consistent.

CONCRETE INTERPRETATION

We now define an interpretation used to compute a big-step evaluation semantics in the form of a triple set: a set of triples (also called judgements) of the form (state, term, result). For each base sort we assume a set of base terms, pairwise disjoint, and for each flow sort a set of values. We write t : s to state that base term t has base sort s, and v : s to state that value v has flow sort s.

For each filter F (x 1 ..x n ) ? ▷ (y 1 ..y m ) such that fsort(F ) = (s 1 ..s n ) → (s ′ 1 ..s ′ m ), we assume an interpretation ⟦F ⟧ which is a relation between elements of (s 1 ..s n ) and elements of (s

′ 1 ..s ′ m ). We write ⟦F ⟧ (v 1 ..v n ) ⇓ (v ′ 1 ..v ′ m ) to state it relates (v 1 ..v n ) to (v ′ 1 ..v ′ m ).

The input state of a concrete interpretation is a pair comprising

• an environment Σ mapping term variables to closed terms and flow variables to values,

• a set T of triples of value, closed term, and value, representing already known judgements and used to give meaning to the sub-derivations H (x f 1 , t, x f 2 ). The interpretation result maps term variables to closed terms and flow variables to values.

We define the concrete interpretation in Figure 9. For the empty skeleton body, it simply returns its environment. For a hook H (x f 1 , t, x f 2 ), it looks up in the triple set a known computation for Σ(x f 1 ) and Σ(t) whose result is v, and it continues binding x f 2 to v. Note that if the language is non-deterministic, there may be several such values and one is picked. For a filter F , one uses its interpretation with the input (Σ(x 1 )..Σ(x n )). As filter interpretations are relations, there may be several results as well. Finally, to merge branches, the interpretation picks a branch that successfully returned a result and extends its environment accordingly.

Running Example. We instantiate the base sort ident with strings and lit with integers. We instantiate the flow sort int with integers, bool with Booleans, val with the disjoint union int + bool, and store with a partial function from strings to val. The concrete interpretation of the filters are the following partial functions: litInt is the identity on integers, intVal and boolVal inject their arguments in int + bool, read(id, st): applies st to id (since st is a partial function, it may not return a result), isInt(v): matches v in the disjoint union int + bool, returns v if it is in int, add(i 1 , i 2 ): returns the integer addition of i 1 and i 2 , eq(i 1 , i 2 ):

returns true if i 1 = i 2 , false otherwise, isBool(v): matches v in the disjoint union int + bool, returns v if it is in bool, write(id, st, v): returns the =⇒ ⟦[]⟧ (Σ,T ) ⇓ Σ Σ x f 1 , Σ (t) , v ∈ T Σ ′ = Σ + x f 2 → v =⇒ H x f 1 , t, x f 2 (Σ,T ) ⇓ (Σ ′ ,T ) ⟦F ⟧ (Σ (x 1 ) ..Σ (x n )) ⇓ (v 1 ..v m ) Σ ′ = Σ + y 1 → v 1 ..y m → v m =⇒ ⟦F (x 1 ..x n ) ? ▷ (y 1 ..y m )⟧ (Σ,T ) ⇓ (Σ ′ ,T ) O (i) = Σ i V ⊆ dom (Σ i ) Σ ′ = Σ + Σ i | V =⇒ n V (O, (Σ,T )) ⇓ (Σ ′ ,T )

Consistency of WF and Concrete Interpretations

Definition 4.1. We say a triple set T is well formed if all its elements are well formed, i.e., if (σ, t, v) ∈ T , then t = c(t 1 ..t n ) and there is a sort s such that Sort (t) = s, σ : in(s), and v : out(s).

We define OKst((Γ, D), (Σ,T )) as follows: T is well-formed, dom(Γ) = dom(Σ), and for any x ∈ dom(Γ) we have Σ(x) : Γ(x). We define OKout((Γ, D), Σ) as follows: dom(Γ) = dom(Σ) and for any x ∈ dom(Γ) we have Σ(x) : Γ(x).

Lemma 4.2. The well-formedness and concrete interpretations are universally consistent.

Concrete Derivations

The concrete interpretation describes how skeletons can be interpreted from a set of hooks. The immediate consequence H describes how skeletons can be assembled. It starts from a set of wellformed triples (that is, of Hoare triples) T , and derives a new set of judgements using the concrete interpretation. Intuitively, from the set of triples generated by derivations of depth at most n, it builds the set of triples generated by derivations of depth at most n + 1. It is defined as follows.

H (T ) =                        (σ, t, v) t = c (t 1 ..t n ) ∧ Sort (t) = s Name c x t 1 ..x t n S ∈ Rules σ : in (s) Σ = x σ → σ + x t 1 → t 1 ..x t n → t n ⟦S⟧ (Σ,T ) ⇓ Σ ′ Σ ′ (x o ) = v                        Lemma 4.3. The functional H is monotone.
Proof. This is immediate by inspecting the interpretation of skeletal bodies, as the only one where T is used is for hooks, and a bigger T does not remove results. □ Lemma 4.4. If T is a well-formed triple set, then H (T ) is a well-formed triple set.

We now show that the smallest fixpoint of H corresponds to the set of triples generated by any finite derivation, or in other words, an inductive definition of the concrete rules. Lemma 4.5. H is continuous: for any increasing sequence of triple sets (T i ), we have i H (T i ) = H ( i T i ).

Proof. We prove this result by double inclusion. The inclusion i H (T i ) ⊆ H ( i T i ) follows from the monotony of H . To show that H ( i T i ) ⊆ i H (T i ), we show that for all triple set T and (σ, t, o) ∈ H (T ), there exists a finite subset T ′ of T such that (σ, t, o) ∈ H (T ′ ). This result is immediate by induction over the structure of the skeleton S. Then, for each (σ, t, o) ∈ H ( i T i ), there exists a finite subset T ′ of i T i such that (σ, t, o) ∈ H (T ′ ). As T ′ is finite and (T i ) monotone, there exists n such that T ′ ⊆ T i . We conclude by monotonicity of H . □ Definition 4.6. The concrete semantics ⇓ is the smallest fixpoint of H .

Lemma 4.7. We have ⇓ = n H n (∅).

Proof. The set of triple sets ordered by inclusion is a CPO, and H is continuous on this CPO. We conclude by Kleene fixpoint theorem. □ Lemma 4.8. The concrete semantics ⇓ is well-formed.

Proof. Let (σ, t, v) ∈ ⇓. By Lemma 4.7, there exists a finite number n such that (σ, t, v) ∈ H n (∅). We prove by induction on n that (σ, t, v) has the expected properties. It is immediate for 0, and for n + 1 we simply apply lemma 4.4. □

ABSTRACT INTERPRETATION

This section describes how a set of skeletons defining a programming language can be re-interpreted over an abstract domain of properties to obtain an abstract interpretation of the language.

Abstract Domains

An abstract interpretation of a set of skeletons must define abstract domains for all the terms and flow sorts used in the skeleton bodies, ending with abstract semantic states and abstract results. Elements in the abstract domains represent sets of values in the corresponding concrete domain (they are related through the concretion function γ introduced below). The abstract interpretation framework is designed to be parametric in the choice of abstract domains for base values such as integers, Booleans, and program states. All we require is that each abstract domain for sort s is a partial order ⊑ with a least element, denoted ⊥ s , representing the empty set. For example, the lattice of intervals can be used as an abstract domains for integers, with ⊥ int being the empty interval. Similarly, a state that maps program variables to integer values can be abstracted as a mapping from variables to intervals, or as a polyhedron that defines linear relations between program variables.

Skeletal variables can also range over terms. For each program or base sort s, we define an abstract domain by imposing a flat partial order on the set of terms of that sort (i.e., we relate a term to itself and no other term) and by adding a ⊥ s element, smaller than all terms of that sort. Abstract base terms include every concrete base term, they may also include additional terms that denote sets of concrete base terms. To ease notation, we sometimes omit the sort in ⊥ in an equality. In this case, v # = ⊥ should be read

v # = ⊥ Sort (v # ) and, v # ⊥ should be read v # ⊥ Sort (v # ) .

Abstract Interpretation of Skeletons

In addition to the abstract domains, an abstract interpretation must specify its input and output states, and how the empty skeleton body, hooks, filters, and the merging of branches are interpreted.

=⇒ ⟦[]⟧ # f , Σ # ,T # ⇓ f , Σ # Σ #′ = Σ # + x f 2 → ⊥ out(Sort (Σ # (t ))) =⇒ H x f 1 , t, x f 2 # ⊥, Σ # ,T # ⇓ ⊥, Σ #′ ,T # Σ # x f 1 ⊑ σ # Σ # (t) ⊑ t # σ # , t # , ⊥ ∈ T # Σ #′ = Σ # + x f 2 → ⊥ out(Sort (Σ # (t ))) =⇒ H x f 1 , t, x f 2 # ⊤, Σ # ,T # ⇓ ⊥, Σ #′ ,T # Σ # x f 1 ⊑ σ # Σ # (t) ⊑ t # σ # , t # , v # ∈ T # v # ⊑ v #′ Σ #′ = Σ # + x f 2 → v #′ =⇒ H x f 1 , t, x f 2 # ⊤, Σ # ,T # ⇓ ⊤, Σ #′ ,T # fsort (F ) = s ′ 1 ..s ′ n → (s 1 ..s m ) Σ #′ = Σ # + y 1 → ⊥ s 1 ..y m → ⊥ s m =⇒ ⟦F (x 1 ..x n ) ? ▷ (y 1 ..y m )⟧ # ⊥, Σ # ,T # ⇓ ⊥, Σ #′ ,T # Σ # (x 1 ) ..Σ # (x n ) ⊑ v # 1 ..v # n ⟦F ⟧ # v # 1 ..v # n = ⊥ fsort (F ) = s ′ 1 ..s ′ n → (s 1 ..s m ) Σ #′ = Σ # + y 1 → ⊥ s 1 ..y m → ⊥ s m =⇒ ⟦F (x 1 ..x n ) ? ▷ (y 1 ..y m )⟧ # ⊤, Σ # ,T # ⇓ ⊥, Σ #′ ,T # Σ # (x 1 ) ..Σ # (x n ) ⊑ v # 1 ..v # n ⟦F ⟧ # v # 1 ..v # n ⊑ v #′ 1 ..v #′ m Σ #′ = Σ # + y 1 → v #′ 1 ..y m → v #′ m =⇒ ⟦F (x 1 ..x n ) ? ▷ (y 1 ..y m )⟧ # ⊤, Σ # ,T # ⇓ ⊤, Σ #′ ,T # n ≥ 1 ∀i ∈ [1..n].O (i) = ⊥, Σ # i ∀i ∈ [1..n].V ⊆ dom Σ # i ∀i, j ∈ [1..n]. Σ # i V = Σ # j V Σ #′ = Σ # + Σ # 1 V =⇒ n # V f , O, Σ # ,T # ⇓ ⊥, Σ #′ ,T # dom (O) = [1..n] E = Σ # i O (i) = ⊤, Σ # i ∅ ∀Σ # i ∈ E.V ⊆ dom Σ # i Σ # i ∈ E =⇒ Σ #′ = Σ # + Σ # i V =⇒ n # V ⊤, O, Σ # ,T # ⇓ ⊤, Σ #′ ,T # Fig. 10. Abstract Interpretation
For each filter symbol F of signature (s 1 ..s n ) → (s ′ 1 ..s ′ m ) we assume a total function ⟦F ⟧ # from the domain corresponding to (s 1 ..s n ) to the domain corresponding to (s ′ 1 ..s ′ m ). A filter interpretation may return ⊥ to state it is not defined for that input.

The input state of an abstract interpretation is a triple (f , Σ # ,T # ) comprising a flag f , an abstract environment Σ # (mapping skeletal variables to abstract terms and values), and a set of abstract semantic triples T # that gives semantics to hooks. A flag is either ⊥ or ⊤ and it indicates whether it has been determined that the current skeleton does not apply (⊥) or that it may still apply (⊤). The output state of an abstract interpretation is a flag and an abstract environment where skeletal variables hold the result of the abstract interpretation. Figure 10 defines the abstract semantics.

The abstract interpretation of an empty list of hypotheses just returns the flag and environment from its input. There are three cases for the interpretation of a hook H (x f 1 , t, x f 2 ). If we have determined that the skeleton does not apply, we set x f 2 to ⊥ of the correct sort. In the two other cases, we need to have a triple (σ # , t # , v # ) from T # such that Σ # (x f 2 ) ⊑ σ # and Σ # (t) ⊑ t # . This loss of precision gives some flexibility for such a derivation. We then have two (non exclusive) cases: if v # = ⊥, then we know the skeleton does not apply, and set the flag to ⊥ and x f 2 to the appropriate ⊥. For the last case, we do not restrict what v # is (it may still be ⊥), and we bind in the resulting environment x f 2 to some v #′ that may be less precise than v # , again to gain flexibility.

The abstract interpretation of a filter F (x 1 ..x n ) ? ▷ (y 1 ..y m ) also has three cases. If we know the skeleton does not apply, we just bind the output variables (y 1 ..y m ) to the appropriate ⊥ depending on the signature of F . Otherwise, we apply the filter interpretation to an approximation of the arguments as given by the environment. If the result is ⊥, we know the skeleton does not apply and switch the flag to ⊥, as well as extend the environment with ⊥ of the correct sort. Otherwise, we keep the flag as ⊤ and extend the environment to an approximation of the result of the filter.

For the merging operator, we interpret every possible branch and collect their results in O. If all branching have the ⊥ flag (either because the ⊥ flag was set before their interpretation, which would then be propagated, or because they newly returned it), then the skeleton does not apply and we set the flag accordingly, extending the environment with mappings from the shared skeletal variables V to ⊥ of the correct sort. Otherwise, we collect all branches that have a ⊤ flag. They must all return abstract environments that agree on the shared variables (which is why the approximations in the filter and hook cases are useful, to ensure this is possible), and we extend the current environment with this common environment.

The key difference between the abstract and concrete interpretations is how the different results are merged in case of branching. The concrete semantics picks one of them, whereas the abstract semantics requires all branches that provided a result to agree. This is because the goal of the abstract semantics is to infer abstract semantic triples that are valid statements about all possible resulting states, i.e., about all possible concrete choices in case of branching.

Consistency of WF and Abstract Interpretations

We define OKst((Γ, D), (f , Σ # ,T # )) as follows: T # is well formed, dom(Γ) = dom(Σ # ), and for any x ∈ dom(Γ) we have Σ # (x) : Γ(x). We define OKout((Γ, D), (f , Σ # )) as follows: dom(Γ) = dom(Σ # ) and for any x ∈ dom(Γ) we have Σ # (x) : Γ(x).

Lemma 5.1. The well-formedness and abstract interpretations are universally consistent.

Abstract Derivations

We define the abstract immediate consequence operator from well-formed triple sets to triple sets in Figure 11. As in the concrete case, the immediate consequence describes how to assemble skeletons.

Lemma 5.2. The functional H # is monotonic.

Proof. This is immediate by inspecting the interpretation of skeletal bodies, as the only one where T # is used is for hooks, and a bigger T # does not remove results.

□

⟦litInt⟧ # = λ(n).[n, n] ⟦id⟧ # = λσ # . σ # ⟦intVal⟧ # = λi. (i, ⊥ bool ) ⟦boolVal⟧ # = λb. (⊥ int , b) ⟦isInt⟧ # = λ(i, b). i ⟦isBool⟧ # = λ(i, b). b ⟦add⟧ # = λ([l 1 , u 1 ], [l 2 , u 2 ]).[l 1 + l 2 , u 1 + u 2 ] ⟦eq⟧ # = λ(i 1 , i 2 ).          true # if i 1 = [n, n] = i 2 false # if i 1 ∩ i 2 = ∅ ⊤ bool otherwise ⟦neg⟧ # = λb.          false # if b = true # true # if b = false # b otherwise ⟦read⟧ # = λ σ # , x . σ # (x) ⟦write⟧ # = λ(x, σ # , v # ). σ # x ← v # ⟦isTrue⟧ # = λb. ⊥ if b ∈ ⊥ bool , false # () otherwise ⟦isFalse⟧ # = λb. ⊥ if b ∈ ⊥ bool , true # () otherwise
γ ([n, m]) = {i | n ≤ i ≤ m} γ (i, b) = γ (i) ∪ γ (b) γ (⊤ bool ) = {true, false} γ (⊥ bool ) = ∅ γ true # = {true} γ false # = {false} γ σ # = Σ ∀x.Σ (x) ∈ γ σ # (x)
The abstraction of the basic filters used in the definition of While is given in Figure 12. Notice that the abstract interpretation of the filters isInt and isBool return an abstract integer and an abstract Boolean, respectively, instead of a Boolean stating whether their argument can be an integer and a Boolean. This is correct because an abstract value that is only an integer has the shape (i, ⊥ bool ), and applying isBool to it returns ⊥ bool , indicating it contains no Boolean.

Lemma 5.12. The abstract filters are consistent with the concrete filters.

Lemma 5.13. The abstract semantics of While is correct.

DERIVING PROOF TECHNIQUES FROM AN ABSTRACT SEMANTICS

This section presents several proof techniques derived from an abstract semantics and instantiated in our While language.

Abstract Rules for Analysing While

Given the instantiation of the filters used in the abstract semantic of While, we can now derive an abstract interpretation of While programs. The result of an abstract interpretation of a program is a set of abstract triples that correctly describes the program behaviour. We shall present the analysis through a set of syntax-directed inference rules for inferring such triples. For a given term c(t 1 ..t n ), we take the corresponding skeleton Name(c(x t 1 ..x t n )) S in the semantics and apply the general abstract interpretation to the skeleton body S. This results in a series of conditions for a triple to be valid that will form the hypotheses of the inference rules.

Rule for addition. As a first example, we derive a rule for analysing arithmetic expressions such as

t 1 + t 2 . A triple (σ # , t 1 + t 2 , v # ) is valid if it belongs to a fixpoint T # of H # . Unfolding definitions, σ # , t 1 + t 2 , v # ∈ T # = H # T # ⇔ H x σ , x t 1 , x f 1 ; isInt x f 1 ? ▷ x f 1 ′ ; H x σ , x t 2 , x f 2 ; isInt x f 2 ? ▷ x f 2 ′ ; add x f 1 ′ , x f 2 ′ ? ▷ x f 3 ; intVal x f 3 ? ▷ x o # ⊤, Σ # 1 ,T # ⇓ f , Σ # o ∧ Σ # 1 = x σ → σ # + x t 1 → t 1 + x t 2 → t 2 ∧ v # = Σ # o (x o )
For simplicity, we here choose to ignore weakenings and the non-⊤-case for the flag f . In other words, we are ignoring the possibility of short-cutting the abstract interpretation of the rule if a ⊥ is found during the abstract execution.

σ # , t 1 + t 2 , v # ∈ H # T # ⇐ Σ # 1 (x σ ) , Σ # 1 x t 1 , v # 1 ∈ T # ∧ isInt x f 1 ? ▷ x f 1 ′ ; H x σ , x t 2 , x f 2 ; isInt x f 2 ? ▷ x f 2 ′ ; add x f 1 ′ , x f 2 ′ ? ▷ x f 3 ; intVal x f 3 ? ▷ x o # ⊤, Σ # 2 ,T # ⇓ ⊤, Σ # o ∧ Σ # 1 = x σ → σ # + x t 1 → t 1 + x t 2 → t 2 ∧ Σ # 2 = Σ # 1 + x f 1 → v # 1 ∧ v # = Σ # o (x o )
Interpreting the filter isInt makes us consider the integer projection of the abstract value v # 1 . We can thus rewrite the implication as follows.

σ # , t 1 + t 2 , v # ∈ H # T # ⇐ σ # , t 1 , v # 1 ∈ T # ∧ v # 1 = i # 1 , b # 1 ∧ H x σ , x t 2 , x f 2 ; isInt x f 2 ? ▷ x f 2 ′ ; add x f 1 ′ , x f 2 ′ ? ▷ x f 3 ; intVal x f 3 ? ▷ x o # ⊤, Σ # 2 ,T # ⇓ ⊤, Σ # o ∧ Σ # 2 = x σ → σ # + x t 1 → t 1 + x t 2 → t 2 + x f 1 → v # 1 + x f 1 ′ → i # 1 ∧ v # = Σ # o (x o )
We can continue unfolding the abstract interpretation of the rule. We eventually reach the following implication:

σ # , t 1 + t 2 , v # ∈ H # T # ⇐ σ # , t 1 , v # 1 ∈ T # ∧ σ # , t 2 , v # 2 ∈ T # ∧ v # 1 = i # 1 , b # 1 ∧ v # 2 = i # 2 , b # 2 ∧ v # = Σ # o (x o ) ∧ add x f 1 ′ , x f 2 ′ ? ▷ x f 3 ; intVal x f 3 ? ▷ x o # ⊤, Σ # 4 ,T # ⇓ ⊤, Σ # o ∧ Σ # 4 = x σ → σ # + x t 1 → t 1 + x t 2 → t 2 + x f 1 → v # 1 + x f 1 ′ → i # 1 + x f 2 → v # 2 + x f 2 ′ → i # 2 ⇐ σ # , t 1 , i # 1 , b # 1 ∈ T # ∧ σ # , t 2 , i # 2 , b # 2 ∈ T # ∧ ⟦add⟧ # i # 1 , i # 2 = i # ∧ v # = i # , ⊥ bool
By writing σ # ⊢ t : v # for (σ # , t, v # ) ∈ T # we get the familiar rule below.

σ # ⊢ t 1 : i # 1 , b # 1 σ # ⊢ t 2 : i # 2 , b # 2 ⟦add⟧ # i # 1 , i # 2 = i # σ # ⊢ t 1 + t 2 : i # , ⊥ bool
Rule for conditionals. In the case of the addition, the structure of the skeleton was linear. We have seen that we ignored some branches (the ones triggering ⊥), but these were not very important. We now show the example of conditionals, where branches are more visible. A triple (σ # , if t 1 t 2 t 3 , σ # o ) is valid if it belongs to a fixpoint T # of H # . Unfolding definitions, and passing through the linear part of the skeleton, we get:

σ # , if t 1 t 2 t 3 , σ # o ∈ H # T # ⇔ H x σ , x t 1 , x f 1 ; isBool x f 1 ? ▷ x f 1 ′ ; isTrue x f 1 ′ ; H x σ , x t 2 , x o isFalse x f 1 ′ ; H x σ , x t 3 , x o {x o } # ⊤, Σ # 1 ,T # ⇓ f , Σ # o ∧ Σ # 1 = x σ → σ # + x t 1 → t 1 + x t 2 → t 2 + x t 3 → t 3 ∧ σ # o = Σ # o (x o ) ⇐ σ # , t 1 , v # 1 ∈ T # ∧ v # 1 = i # 1 , b # 1 ∧ isTrue x f 1 ′ ; H x σ , x t 2 , x o isFalse x f 1 ′ ; H x σ , x t 3 , x o {x o } # ⊤, Σ # 2 ,T # ⇓ f , Σ # o ∧ Σ # 1 = x σ → σ # + x t 1 → t 1 + x t 2 → t 2 + x t 3 → t 3 + x f 1 → v # 1 + x f 1 ′ → b # 1
From this stage, we continue the analysis in each of the two subbranches to build a map O representing the outputs of both branches. We consider two cases, depending on the value of b # 1 . First, if b # 1 is ⊤ bool . We then have both isTrue and isFalse holding on b # 1 . By unfolding definitions and using weakening for the results of the two hooks, we get the following implication:

σ # , if t 1 t 2 t 3 , σ # o ∈ H # T # ⇐ σ # , t 1 , v # 1 ∈ T # ∧ σ # , t 2 , σ # 2 ∈ T # ∧ σ # , t 3 , σ # 3 ∈ T # ∧ v # 1 = i # 1 , ⊤ bool ∧ σ # 2 ⊑ σ # o ∧ σ # 3 ⊑ σ # o
Using the same notations as above we can simplify this rule as below.

σ # ⊢ t 1 : i # 1 , ⊤ bool σ # ⊢ t 2 : σ # 2 σ # 2 ⊑ σ # o σ # ⊢ t 3 : σ # 3 σ # 3 ⊑ σ # o σ # ⊢ if t 1 t 2 t 3 : σ # o
This rule is imprecise (we assume that we get ⊤ bool when evaluating the conditional's expression), but shows how our equivalent of concrete rules are merged in the abstract interpretation. We now consider a more precise version of the rule, for the case when the conditional expression evaluates to true # . The other cases false # and ⊥ bool are similar. In this case, the isTrue filter holds, but not isFalse: we can derive the judgement below when

Σ # (x f 1 ′ ) = true # . isFalse x f 1 ′ ; H x σ , x t 3 , x o # ⊤, Σ # ,T # ⇓ ⊥, Σ # o
Following the rules for abstract interpretation (see Figure 10), this removes the second branch from the E set, only leaving constraints from the first branch. We thus get the following implication, where we no longer need the weakening for the result of the hook.

σ # , if t 1 t 2 t 3 , σ # o ∈ H # T # ⇐ σ # , t 1 , v # 1 ∈ T # ∧ σ # , t 2 , σ # o ∈ T # ∧ v # 1 = i # 1 , true #
We can rewrite this implication as above into the rule

σ # ⊢ t 1 : i # 1 , true # σ # ⊢ t 2 : σ # 2 σ # ⊢ if t 1 t 2 t 3 : σ # 2 .
Rule for loops. The skeleton for loops is close to the one for conditionals. We can similarly derive abstract rules such as the ones below.

σ # ⊢ t 1 : i # 1 , ⊤ bool σ # ⊢ t 2 : σ # 2 σ # 2 ⊢ while t 1 t 2 : σ # 3 σ # 3 ⊑ σ # σ # ⊢ while t 1 t 2 : σ # σ # ⊢ t 1 : i # 1 , true # σ # ⊢ t 2 : σ # 2 σ # 2 ⊢ while t 1 t 2 : σ # 3 σ # ⊢ while t 1 t 2 : σ # 3 σ # ⊢ t 1 : i # 1 , false # σ # ⊢ while t 1 t 2 : σ #
We can also use the fact that any fixpoint of H # is considered valid. The following implication (which we can prove in a way similar to above) is valid for any well-formed set T # .

σ # , while t 1 t 2 , σ # o ∈ H # T # ⇐ σ # , t 1 , v # 1 ∈ T # ∧ v # 1 ⊑ i # 1 , ⊤ bool ∧ σ # , t 2 , σ # 2 ∈ T # ∧ σ # 2 , while t 1 t 2 , σ # 3 ∈ T # ∧ σ # 3 ⊑ σ # o ∧ σ # ⊑ σ # o
In particular, as the condition v # 1 ⊑ (i # 1 , ⊤ bool ) is vacuously true, we can weaken this implication as follows (forcing all intermediate states to be the same).

σ # , while t 1 t 2 , σ # ∈ H # T # ⇐ σ # , t 1 , v # 1 ∈ T # ∧ σ # , t 2 , σ # ∈ T # ∧ σ # , while t 1 t 2 , σ # ∈ T # This implication means that given any T # 0 , such that T # 0 ⊆ H # (T # 0 ), that associates t 1 in the state σ # with a result (that is that there exists v # such that (σ # , t 1 , v # ) ∈ T # 0 ), and such that (σ # , t 2 , σ # ) ∈ T # 0 , we can extend T # 0 into T # 1 = T # 0 ∪ (σ # , while t 1 t 2 , σ # ) . By monotonicity of H # , we get T # 0 ⊆ H # (T # 1
), and by the above implication, we get (σ # , while

t 1 t 2 , σ # ) ∈ H # (T # 1 ). Hence, T # 1 ⊆ H # (T # 1 )
, and every triple in T # 1 is correct in relation to ⇓. In other words, the following familiar rule is admissible.

σ # ⊢ t 1 : v # σ # ⊢ t 2 : σ # σ # ⊢ while t 1 t 2 : σ #

State Splitting

As another example of the use of the abstract interpretation, we show how to extend the abstract semantics to obtain more precise results. Our motivating example is t: while ¬(x = 0) x := x -1 for which we want to show that the triple (x → [0, ∞], t, x → 0) is correct (we simplify notation and write n for ([n, n], ⊥ bool ), and [n, m] for ([n, m], ⊥ bool )). Proving this is not possible as such. To see this, observe that in the rule for While, the same state is used to run the expression and the statement, hence the return value of the expression is not reflected in the state (it may only prevent a branch from being taken). Communicating information from an expression back to a state is a non-trivial problem which depends on the language considered, but we can help the abstract interpretation by splitting the state in three parts:

{(x → 0, t, x → 0), (x → [1, ∞], t, x → 0), (x → [0, ∞], t, x → 0)}.
Let T # be the set of triples (listed below) obtained from adding triples for every sub-expression of t. We can show that {(x → 0, t,

x → 0), (x → [1, ∞], t, x → 0)} ⊂ H # (T # ) (the second triple uses (x → [0, ∞], t, x →
0) to evaluate the recursive while term). However there is still one of the three triples that cannot be derived, viz.,

(x → [0, ∞], t, x → 0) ∈ H # (T # ).
To derive this third triple, we introduce a proof technique called state splitting to obtain a more precise abstract semantics. The core idea of the technique is that if the state σ # of a triple (σ # , t # , v # ) is covered by the states of some triples

(σ # 1 , t # , v # )..(σ # n , t # , v # ), in the sense that γ (σ # ) ⊆ γ (σ # 1 ) ∪ .. ∪ γ (σ # n ), then we may use (σ # , t # , v # ) in the input triple set T # of H # (T # ) without having to show that (σ # , t # , v #
) is in the resulting triple set H # (T # ) and still remain correct.

Formally, we first define a function Sp from triple sets to triple sets that adds such triples. The constraints on 1 x σ and 1 x o are generated when considering the program point 1, corresponding to the evaluation of ¬(x = 0) (corresponding to the skeleton Neg). As stated, the set of all generated constraints is large; it is provided in the supplementary material on the companion website.

=⇒ ⟦[]⟧ c (N, pp, C) ⇓ C HPP t 0 (pp, N, t) = pp ′ x f 1 ∈ D N (C) C ′ = C ∪ pp x f 1 ⊑ pp ′ x σ , pp ′ x o ⊑ pp x f 2 D N (C ′ ) = D N (C) ∪ x f 2 =⇒ H x f 1 , t, x f 2 c (N, pp, C) ⇓ (N, pp, C ′ ) {x 1 ..x n } ⊆ D N (C) ⟦F ⟧ c pp x 1 ..pp x n , pp y 1 ..pp y m = C f C ′ = C ∪ C f D N (C ′ ) = D N (C) ∪ {y 1 ..y m } =⇒ ⟦F (x 1 ..x n ) ? ▷ (y 1 ..y m )⟧ c (N, pp, C) ⇓ (N, pp, C ′ ) i ≥ 1 ∀i ∈ [1..n].O (i) = C i ∀i ∈ [1..n].V ⊆ D N (C i ) C ′ = C ∪ i ∈[1..n] C i D N (C ′ ) = D N (C) ∪ V =⇒ n c V (O, (N, pp, C)) ⇓ (N, pp, C ′ )
f fsort(f ) in in → (val, in) alloc (heap, val) → (heap, loc) locVal loc → val isLoc val → loc get (loc, heap) → val set (loc, heap, val) → heap out (out, val) → out f fsort(f ) mkSt (in,

EXTENDING WHILE WITH EXCEPTIONS, INPUT/OUTPUT, AND A HEAP

To further illustrate the use of skeletal semantics, we extend our While language with exceptions, input/output, and a heap. We first need to define new flow sorts: in for input streams, out for output streams, heap for heaps, loc for locations in the heap, state for the combination of the streams with a store and a heap, valState for the further combination with a value, and excState for a state extended to signal whether an exception was raised. We still have two program sorts (expr and stat), but their input flow sorts are state, and their output flow sorts are now valState for expressions and excState for statements. Figure 14 lists the additional constructors of our language. The additional filters are defined in Figure 15, the rules for expressions in Figure 16, and the rules for statements in Figure 17. To help reading the rules, flow variables have names related to their sorts: σ for state, w for valState, v for val, n for int, i for in, and so on.

Instantiation of concrete interpretation. We instantiate the in and out sorts with list of values, denoted by L. We instantiate locations as integers. A heap is a pair of an integer (the next free location) and a map from integers to values. We instantiate the state sort as a tuple of in, out, store, and heap, the valState sort as a pair of val and state, and the excState sort as a pair of a Boolean and state. The val sort is extended to include a case for locations, as well as the intVal, boolVal, isInt, and isBool filters. The locVal filter injects a location in the val type, and the isLoc filter applies if the val argument is a location, which it then returns. The in filter applies if the input list is not empty, it returns its head and its tail. The alloc filters applied to ((n, m), v) returns the heap (n + 1, m + n → v). The get filter applies if the location is in the heap, and it returns the Lit(const corresponding value. The set filter applies if the location is in the heap, and it return the heap updated with the given value. The out filter always apply and adds the given value to the output list. The mkOK filter (resp. the mkExc filter) always applies and builds a pair of true (resp. false) and the given state. The isOK filter (resp. the isExc filter) applies if the Boolean is true (resp. is false), it then return the state component of the tuple. Other filters build or deconstruct tuples.

(x t )) litInt (x t ) ? ▷ x f n ; intVal x f n ? ▷ x f v ; mkValSt x f v , x σ ? ▷ x o Var(var (x t )) splitSt (x σ ) ? ▷ x f i , x f o , x f s , x f h ; read x t , x f s ? ▷ x f v ; mkSt x f i , x f o , x f s , x f h ? ▷ x f σ ; mkValSt x f v , x f σ ? ▷ x o In(in) splitSt (x σ ) ? ▷ x f i , x f o , x f s , x f h ; in x f i ? ▷ x f v , x f i ′ ; mkSt x f i ′ , x f o , x f s , x f h ? ▷ x f σ ; mkValSt x f v , x f σ ? ▷ x o Alloc(ref (x t ))           H x σ , x t , x f w ; getValSt x f w ? ▷ x f v , x f σ ; splitSt x f σ ? ▷ x f i , x f o , x f s , x f h ; alloc x f h , x f v ? ▷ x f h ′ , x f l ; locVal x f l ? ▷ x f v ′ ; mkSt x f i , x f o , x f s , x f h ′ ? ▷ x f σ ′ ; mkValSt x f v ′ , x f σ ′ ? ▷ x o           Acc(!x t )        H x σ , x t , x f w ; getValSt x f w ? ▷ x f v , x f σ ; isLoc x f v ? ▷ x f l ; splitSt x f σ ? ▷ x f i , x f o , x f s , x f h ; get x f l , x f h ? ▷ x f v ′ ; mkSt x f i , x f o , x f s , x f h ? ▷ x f σ ′ ; mkValSt x f v ′ , x f σ ′ ? ▷ x o        Add x t 1 + x t 2           H x σ , x t 1 , x f w 1 ; getValSt x f w 1 ? ▷ x f v 1 , x f σ 1 ; isInt x f v 1 ? ▷ x f n 1 ; H x f σ 1 , x t 2 , x f w 2 ; getValSt x f w 2 ? ▷ x f v 2 , x f σ 2 ; isInt x f v 2 ? ▷ x f n 2 ; add x f n 1 , x f n 2 ? ▷ x f n ; intVal x f n ? ▷ x f v ; mkValSt x f v , x f σ 2 ? ▷ x o           Eq x t 1 = x t 2           H x σ , x t 1 , x f w 1 ; getValSt x f w 1 ? ▷ x f v 1 , x f σ 1 ; isInt x f v 1 ? ▷ x f n 1 ; H x f σ 1 , x t 2 , x f w 2 ; getValSt x f w 2 ? ▷ x f v 2 , x f σ 2 ; isInt x f v 2 ? ▷ x f n 2 ; eq x f n 1 , x f n 2 ? ▷ x f b ; boolVal x f b ? ▷ x f v ; mkValSt x f v , x f σ 2 ? ▷ x o           Neg(¬x t ) H x σ , x t , x f w ; getValSt x f w ? ▷ x f v , x f σ ; isBool x f v ? ▷ x f b ; neg x f b ? ▷ x f b ′ ; boolVal x f b ′ ? ▷ x f v ′ ; mkValSt x f v ′ , x f σ ? ▷ x o
Instantiation of abstract interpretation. To illustrate the flexibility of our approach, we choose a coarse abstraction for the in and out sorts (they are either ⊥ or a single abstract value), and a precise abstraction of heaps: abstract heaps are modelled similar to concrete heap as a pair (n, m # ) of an integer and a mapping from integers to abstract values. Locations are abstracted as sets of integers. Tuples are abstracted as tuples of the abstraction of their components. The tuple-manipulating abstract filters are straightforward, so we only detail the other ones in Figure 18.

Lemma 8.1. The abstract filters are consistent with the concrete filters. Lemma 8.2. The abstract semantics of Extended While is correct.

Skip(skip) [mkOK (x σ ) ? ▷ x o ] Throw(throw) [mkExc (x σ ) ? ▷ x o ] Asn x t 1 := x t 2        H x σ , x t 2 , x f w ; getValSt x f w ? ▷ x f v , x f σ ; splitSt x f σ ? ▷ x f i , x f o , x f s , x f h ; write x t 1 , x f s , x f v ? ▷ x f s ′ ; mkSt x f i , x f o , x f s ′ , x f h ? ▷ x f σ ′ ; mkOK x f σ ′ ? ▷ x o        Set x t 1 ← x t 2              H x σ , x t 1 , x f w 1 ; getValSt x f w 1 ? ▷ x f v 1 , x f σ ; isLoc x f v 1 ? ▷ x f l H x f σ , x t 2 , x f w 2 ; getValSt x f w 2 ? ▷ x f v 2 , x f σ ′ ; splitSt x f σ ′ ? ▷ x f i , x f o , x f s , x f h ; set x f l , x f h , x f v 2 ? ▷ x f h ′ ; mkSt x f i , x f o , x f s , x f h ′ ? ▷ x f σ ′′ ; mkOK x f σ ′′ ? ▷ x o              Out out x t 1        H x σ , x t 1 , x f w ; getValSt x f w ? ▷ x f v , x f σ ; splitSt x f σ ? ▷ x f i , x f o , x f s , x f h ; out x f o , x f v ? ▷ x f o ′ ; mkSt x f i , x f o ′ , x f s , x f h ? ▷ x f σ ′ ; mkOK x f σ ′ ? ▷ x o        Seq x t 1 ; x t 2       H x σ , x t 1 , x f e ; isOK x f e ? ▷ x f σ ; H x f σ , x t 2 , x o isExc x f e ? ▷ x f σ ′ ; mkExc x f σ ′ ? ▷ x o {x o }       Try try x t 1 catch x t 2       H x σ , x t 1 , x f e ; isOK x f e ? ▷ x f σ ; mkOK x f σ ? ▷ x o isExc x f e ? ▷ x f σ ′ ; H x f σ ′ , x t 2 , x o {x o }       If if x t 1 x t 2 x t 3         H x σ , x t 1 , x f w ; getValSt x f w ? ▷ x f v , x f σ ; isBool x f v ? ▷ x f b ; isTrue x f b ; H x f σ , x t 2 , x o isFalse x f b ; H x f σ , x t 3 , x o {x o }         While while x t 1 x t 2              H x σ , x t 1 , x f w ; getValSt x f w ? ▷ x f v , x f σ ; isBool x f v ? ▷ x f b ; isTrue x f b ; H x f σ , x t 2 , x f e ; isOK x f e ? ▷ x f σ ′ ; H x f σ ′ , while x t 1 x t 2 , x o isExc x f e ? ▷ x f σ ′′ ; mkExc x f σ ′′ ? ▷ x o {x o } isFalse x f b ; mkOK x f σ ? ▷ x o {x o }             

RELATED WORK

Ott [START_REF] Sewell | Ott: Effective Tool Support for the Working Semanticist[END_REF]] is a formalism for describing language semantics and type systems. Ott proposes a meta-language with a humanly readable syntax for writing semantic definitions as inference rules, and has facilities for translating these definitions into executable interpreters and specifications in proof assistants such as Coq and HOL. Lem [START_REF] Mulligan | Lem: Reusable Engineering of Real-world Semantics[END_REF]] offers a core functional language extended with logical features from proof assistants for writing semantic [START_REF] Turi | Towards a Mathematical Operational Semantics[END_REF] propose a generic way of defining small step operational semantics, presented in a category theoretic framework. More recently, Churchill emphet al. [START_REF] Churchill | Reusable Components of Semantic Specifications[END_REF] addresses the issue of the reusability of operational semantics. Their approach is based on structures called fundamental constructs, or funcons, which only specify the changed parts of the state for a given construct. For instance, the funcon for if does not mention environments, but only the Boolean part of the value which is needed. Funcons can then be combined to build a programming language. There is a connection between these funcons and our rules as they are both meant to capture the whole behaviour of a given language construct. One difference is that funcons have a certain degree of sort polymorphism, menaning that e.g., conditional statements and conditional expressions can be treated by the same "if"-funcon. Skeletal semantics would treat each sort separately but would re-use the filters, so as to avoid increasing the proof effort required. To the extent of our knowledge, the work on funcons has been focused on building extendable concrete semantics, and has never been used to build an abstract semantics.

γ v # = L ∀v ∈ L.v ∈ γ v # γ a # , b # , c # = {(a, b, c)|a ∈ γ (a) ∧ b ∈ γ (b) ∧ c ∈ γ (c)} γ l # = l # γ n, m # = (n, m) dom (m) = dom m # ∀i ∈ dom (m) .m[i] ∈ γ m # [i] in # v # = v # , v # isOK # b # , s # = s # if true # ⊑ b # ⊥ state otherwise out # v # 1 , v # 2 = v # 1 ⊔ v # 2 isExc # b # , s # = s # if false # ⊑ b # ⊥ state otherwise locVal # l # = ⊥ int , ⊥ bool , l # isval # n # , b # , l # = l # get # l # , n, m # = l ∈l # m # [l] alloc # n, m # , v # = n + 1, m # + n → v # set # l # , n, m # , v # = n, m ′# where m ′# [l] = m # [l] ⊔ v # if l ∈ l # m ′# [l] = m # [l] otherwise
Views [START_REF] Dinsdale-Young | Views: Compositional Reasoning for Concurrent Programs[END_REF]] has a concrete operational semantics for control flow, but is parameterised on the state model and basic commands. It proposes a program logic for this language, which is parameterised on the actions of the basic commands. They prove a general soundness result stating that it suffices to check soundness for each basic command. This corresponds in our framework to the fact that only simple properties on filters need to be checked. Similarly, Keidel et al. [START_REF] Keidel | Compositional Soundness Proofs of Abstract Interpreters[END_REF] very recently proposed to capture the similarity between a concrete an abstract interpreter using a shared interpreter parameterised by arrows that could be instantiated to concrete and abstract versions, thus reducing the proof effort needed.

Iris [START_REF] Jung | Iris from the Ground Up[END_REF]] is a concurrent separation logic framework. It is parameterised by a smallstep reduction relation and it proposes a logic to reason about resources. This logic is parameterised by a representation of resources in the form of an algebraic structure called a "camera". Cameras come with local properties about resources that users have to check. These local constraints yield the soundness of the Iris logic. To be used in practice, Iris requires its users to provides lemmas about weakest preconditions for each language construct. These lemmas are easy to find and prove in simple examples (such as a vanilla While), but they require a deep understanding about how one reasons about the considered language. Such lemmas can be much complex to express (let alone prove) in complex languages such as JavaScript [START_REF] Gardner | Towards a Program Logic for JavaScript[END_REF]. We believe that our framework guides the proof effort by local reasoning: at each step, the abstract interpretation naturally considers every applicable branch.

The K framework [START_REF] Roşu | An Overview of the K Semantic Framework[END_REF] proposes a formalism for writing operational semantics and for constructing program verifiers directly on top of the semantic definitions, as opposed to using an intermediate representation and/or a verification generator linked to a specific program logic. The semantic rules are given as rewriting rules over terms of semantic state. The K framework has been used to write semantic definitions of several real-world languages, including C, Java, and JavaScript. The program verifiers are based on matching logic [START_REF] Roşu | Matching Logic[END_REF]], a formalism for reasoning about patterns and the set of terms that they match. A language-independent set of proof rules defines a Reachability Logic which can reason about the set of reachable states of a program. This has been instantiated to obtain program verifiers reasoning about data structures of heap-manipulating programs in C, Java, and JavaScript [Ştefănescu et al. 2016].

The K framework has goals similar to ours: derive verifiers from operational semantics, correct by construction. A key difference is that the semantics of the K specification tool is complex and not clearly documented [START_REF] Li | IsaK: A Complete Semantics of K[END_REF]. In this work, we have focused on crystallising a general yet simple rule format. Our format enables a general definition of when a semantics is well-defined and provides a generic correctness theorem for the derived program verifiers that can be machine-checked in the Coq proof assistant.

Schmidt initiated the abstract interpretation of big-step operational semantics [START_REF] Schmidt | Natural-semantics-based Abstract Interpretation (preliminary version)[END_REF]] by showing how to abstract derivation trees (using co-induction to harness infinite derivations) and derived classical data flow and control flow analyses as abstract interpretations. Other systematic derivations of static analyses have taken small-step operational semantics as starting point. Schmidt [Schmidt 1997b] discusses the general principles for such an approach and compares small-step and big-step operational semantics as foundations for abstract interpretation. Cousot [START_REF] Cousot | The Calculational Design of a Generic Abstract Interpreter[END_REF] shows how to derive static analyses for an imperative language defined by a compositional transition semantics using the principles of abstract interpretation. [START_REF] Midtgaard | A Calculational Approach to Control-Flow Analysis by Abstract Interpretation[END_REF] use a similar approach for calculating control-flow analyses for functional languages from operational semantics in the form of abstract machines. Van Horn andMight [Van Horn andMight 2010, 2011] show how a series of analyses for higher-order functional languages can be derived from operational semantics formulated as abstract machines. The atomic operations of the machines are given an abstract interpretation and it is shown that the "abstract abstract machines" can simulate all the transitions of the concrete abstract machine. The abstract machines used by Van Horn and Might can be expressed in our rule format: the atomic operations correspond to our filters and the simulation result corresponds to our consistency result for concrete and abstract interpretations. The two works differ slightly in scope in that we are interested in a general semantic rule format and its meta-theory whereas Van Horn and Might are concerned with giving a systematic derivation of advanced analyses for higher-order languages with state.

Inspired by Schmidt, Bodin et al. [Bodin et al. 2015] identify a rule format that can be systematically instantiated to both concrete and abstract semantics, with a generic consistency result. Our work generalises their approach. Their rule format is based on a non-standard style of operational semantics, called pretty-big-step operational semantics [START_REF] Charguéraud | Pretty-big-step Semantics[END_REF]], which cuts up standard big-step rules into many fine-grained rules. In our work, one skeleton describes the behaviour of one language construct. Our skeletal semantics captures many forms of traditional operational semantics, such as the traditional big-step semantics studied in this paper.

CONCLUSIONS AND FUTURE WORK

We have introduced a new meta-language for capturing the behaviour of programming languages, called skeletal semantics. A skeleton provides a simple way of describing the complete behaviour of a language construct in a single definition. We have given a language-independent, generic definition of interpretation of a skeletal semantics, systematically deriving semantic judgements from the skeletons. We have explored four such interpretations: a well-formedness interpretation; a concrete interpretation; an abstract interpretation; and a constraint generator for flow-sensitive analysis. A key advantage of skeletal semantics is that we are able to establish general, language-independent consistency results, which can then be instantiated to specific programming language by proving simple language-dependent filter lemmas.

In this paper, we have focused on proving the fundamental properties of skeletal semantics, using the simple While language and its extensions as illustrative examples. We have demonstrated that we can capture many language constructs including higher-order and object-oriented features. In future, we would like to explore how our formalism scales to real-world languages such as OCaml and JavaScript. For instance, the specification of JavaScript [ECMA 2018] is written in a style where the whole behaviour of each language construct is described in a single definition. It should be comparatively straightforward to provide a specification of JavaScript using a skeletal semantics.

A distinguishing feature of skeletal semantics is that interpretations can be used to characterise several styles of semantics, independently of the language considered. In this paper, we have focused on big-step semantics. In future, we plan to capture other forms of semantics such as small-step operational semantics, semantics for describing concurrent, distributed and interactive computation, and abstract machines, using an approach similar to [START_REF] Uustalu | Coinductive Big-Step Semantics for Concurrency[END_REF]].

We have interesting proof techniques that are worth further exploration. For example, we have demonstrated how to add an abstract rule for state splitting. The proof technique used to validate this abstract rule, namely that abstract interpretation is a greatest fixpoint, is not specific to state splitting. We thus want to explore other abstract rules validated by this greatest fixpoint. In particular, we conjecture that we can use this approach to obtain a frame rule for skeletal semantics, paving the way for the integration of separation logic as an abstract interpretation. It is also possible to generate better (more precise) constraints than those given in Section 7, as well as constraints for other analyses such as control flow analysis. Based on the skeletal semantics for the λ calculus, we have reproduced the constraint generation for 0-CFA [START_REF] Palsberg | Closure Analysis in Constraint Form[END_REF]]. We are currently studying how more advanced control flow analyses for other languages can be expressed in our framework.

Finally, we have mechanised in Coq the definitions of skeletal semantics and interpretations, and have proved the general consistency results. We have formalised the well-formedness, concrete and abstract interpretations, verifying that the abstract interpretation for the While language is correct. We have also mechanised a skeletal semantics for the λ calculus. We are currently studying how to leverage this Coq mechanisation to build a certificate checker for abstract analysis.

Fig. 7 .

 7 Fig. 7. Filter sorts

Fig. 9 .

 9 Fig. 9. Concrete Interpretation

Fig. 12 .

 12 Fig. 12. Abstract interpretation of filters

Fig. 13 .

 13 Fig. 13. Constraint Generation

Fig. 14 .

 14 Fig. 14. Additional Constructors for While

Fig. 15 .

 15 Fig. 15. Additional filters

Fig. 16 .

 16 Fig. 16. Skeletal semantics for extended While (Expressions)

Fig. 17 .

 17 Fig. 17. Skeletal semantics for While2 (Statements)

Fig. 18 .

 18 Fig. 18. Abstract Interpretation of Extended While

  σ, e ⇓ true σ, t 1 ⇓ x o σ, if e t 1 t 2 ⇓ x o σ, e ⇓ false σ, t 2 ⇓ x o σ, if e t 1 t 2 ⇓ x o Fig. 1. Usual concrete rules for the if construct

  The abstract interpretation of the if construct: intuitive description.

	c	Signature	c	Signature
	const	lit → expr	skip	stat
	var	ident → expr	:=	(ident × expr) → stat
	+	(expr × expr) → expr	;	(stat × stat) → stat
	=	(expr × expr) → expr	if	(expr × stat × stat) → stat
	¬	expr → expr	while	(expr × stat) → stat
		Fig. 5. Constructors for While
	2 SKELETAL SEMANTICS
	2.1 Terms
	Terms t of a skeletal semantics are built using base terms, term variables, and constructors. Base
	terms are left unspecified and correspond to the basic blocks of the syntax, such as literals or
	program identifiers. They are instantiated by interpretations. We assume a countable set of term
	variables, ranged over by x t , and a finite set of constructors, ranged over by c. A term is thus a base
	term, a term variable, or a constructor applied to terms.

  out, store, heap) → state splitSt state → (in, out, store, heap)

	mkValSt	(val, state) → valState
	getValSt	valState → (val, state)
	mkOK	state → excState
	mkExc	state → excState
	isOK	excState → state
	isExc	excState → state

Proc. ACM Program. Lang., Vol. 3, No. POPL, Article 44. Publication date: January 2019.

http://skeletons.inria.fr Proc. ACM Program. Lang., Vol. 3, No. POPL, Article 44. Publication date: January

See the Figure10of[Schmidt 1997a] for an example of such representation.Proc. ACM Program. Lang., Vol.

3, No. POPL, Article 44. Publication date: January 2019.

We impose the technical restriction that any hook used in a skeleton can be matched to a program point of the program (closed term) t 0 under consideration. Thus constraint-based analysis of code-generating code is not considered here.Proc. ACM Program. Lang., Vol. 3, No. POPL, Article

Publication date: January 2019.

* This research has been partially supported by the ANR projects AJACS ANR-14-CE28-0008 and CISC ANR-17-CE25-0014-01. Bodin and Gardner were partially supported by the EPSRC programme grant 'REMS: Rigorous Engineering of Mainstream Systems', EP/K008528/1.

Skeletal Semantics and Their Interpretations 44:15 An abstract semantics ⇓ # is a set of facts of the form (σ # , t # , v # ) stating that from state σ # term t # evaluates to v # . A correct abstract semantics is one where such triples correspond to triples in the concrete semantics (see Section 5.5). The more facts an abstract semantics contains, the more useful it is, as it provides more information about the behaviour of terms. Hence, we choose as abstract semantics the one with most facts, i.e., the greatest fixpoint of H # . This choice provides a proof technique: since the greatest fixpoint the union of all sets such that T # ⊆ H # (T # ), to prove that a fact is correct, one can propose a candidate set T # containing this fact, and then show that T # ⊆ H # (T # ). This amounts to proving that the facts T # constitute an invariant of the semantics. If we were to translate such invariants into a derivation, the resulting derivation may be infinite. 2 We could also define the abstract semantics ⇓ # as the smallest fixpoint of H # . This would be sound but, having fewer facts, we would then miss valuable abstract results. More precisely, if a triple (σ # , t, v # ) belongs to the smallest fixpoint of H # , then (as abstract triple sets form a CPO ordered by inclusion and H # is continuous on this CPO), there exists a finite number n such that (σ # , t, v # ) ∈ H # n (∅). In other words, there exists a finite abstract derivation yielding the triple (σ # , t, v # ). This implies that for all concrete state σ ∈ γ (σ # ), the program t terminates. We would thus have lost all facts for which the abstract semantics cannot prove termination. Defining the abstract semantics as the greatest fixpoint of H # solves this issue.

Definition 5.4. The abstract semantics ⇓ # is the largest fixpoint of H # as a function from wellformed triple sets to well-formed triple sets. This restriction is well-defined by Lemma 5.3. Lemma 5.5. ⇓ # is well formed.

Proof. As ⇓ # is the largest fixpoint of H # , it is the union of all well-formed triple sets

has the requested properties. □

Consistency of Concrete and Abstract Interpretations

We assume a concretion function γ for the abstract domain, from abstract terms to sets of concrete terms, and from abstract values to sets of concrete values. We impose several constraints on γ . First, γ must be compatible with ⊑:

Second, for any abstract term t # of sort s, the set γ (t # ) must only contain terms of sort s. In addition, γ (c(t

Conversely, for any concrete term t, we have γ (t) = {t }, as abstract base terms are extensions of concrete base terms. Lemma 5.6. Let Σ be a mapping from term variables to concrete terms, and Σ # be a mapping from term variables to abstract terms. If Tvar(t) ⊆ dom(Σ), Tvar(t) ⊆ dom(Σ # ), and ∀x t ∈ Tvar(t), Σ(x t ) ∈ γ (Σ # (x t )), then Σ(t) ∈ γ (Σ # (t)).

Proof. By induction on the structure of t. If it is a base term, then the result holds by hypothesis on base terms, if it is a term variable, then the result is immediate, and otherwise we prove the property by induction on the subterms. □

Regarding values, we have similar restrictions: for any abstract value v # of sort s, the concrete values in γ (v # ) all have sort s. We also require the abstract interpretation of filters to be consistent with the concrete one:

In particular, if the concrete filter relates its input to an output, the abstract filter cannot return ⊥.

Definition 5.7. Let T a concrete triple set and T # an abstract triple set. We say they are consistent if for any (σ, t, v) ∈ T and (σ

), and T and T # are well formed and consistent. We define OKout(Σ, (f , Σ # )) as follows: f = ⊤, dom(Σ) = dom(Σ # ), and for any x ∈ dom(Σ), we have Σ(x) ∈ γ (Σ # (x)).

Lemma 5.8. The concrete and abstract interpretations are universally consistent.

Lemma 5.9. Let T and T # well formed and consistent triple sets, then H (T ) and H # (T # ) are well formed and consistent triple sets.

We finally show that the abstract semantics is correct relative to the concrete semantics. In a nutshell, for any triple in the concrete semantics ⇓ (the smallest fixpoint of H ) and any triple in the abstract semantics ⇓ # (the largest fixpoint of H # ), if the input states and terms are related, then the output values are related. Formally, we have the following.

Definition 5.10. An abstract triple set T # is correct if it is well-formed and consistent with ⇓. Theorem 5.11. ⇓ # is correct.

Proof. We prove by induction on k that H k (∅) and ⇓ # are well formed and consistent. The check that ⇓ # is well formed is simply Lemma 5.5.

The result is immediate for k = 0 since ∅ is well formed, and there is nothing else to check. Let k = n + 1, by induction we have H n (∅) and ⇓ # are well formed and consistent. By Lemma 4.4 we have H n+1 (∅) and H # (⇓ # ) = ⇓ # are well formed and consistent, as required.

To conclude, we apply Lemma 4.7. □

Note that in the previous theorem we only use the fact that ⇓ # is a fixpoint: it does not have to be the greatest fixpoint.

Example: Interval analysis of While

To give a concrete example of an abstract interpretation we design a value analysis of the language While in the style of Schmidt's Abstract Interpretation of Natural Semantics [START_REF] Schmidt | Natural-semantics-based Abstract Interpretation (preliminary version)[END_REF]]. We have the following flow sorts in the semantic definition (cf. Figure 7): int, bool, val, and store.

We describe an analysis in which integers are approximated by intervals, ordered by inclusion. Writing [n, m] for the interval of integers between n and m (with the convention that [n, m] = ∅ if m < n), we can define the abstract domains for each of the flow sort as follows:

Definition 6.1. Let T # an abstract triple set. We define the state splitting function Sp(T # ) as:

For any T # , T # ⊆ Sp(T # ), and Sp is monotonic. Lemma 6.3. Let T # a well-formed triple set, then Sp(T # ) is well formed.

□

We next show that the functional Sp(H # (Sp(•))) has the same consistency property as H # (•).

Lemma 6.4. Let T and T # be well formed and consistent triple sets, then H (T ) and Sp(H # (Sp(T # ))) are well formed and consistent triple sets.

We finally state that the proof technique is correct. Lemma 6.5. Let T # a well-formed abstract triple set. If T # ⊆ H # (Sp(T # )), then Sp(T # ) is correct.

We turn back to our example. Consider the following triple set.

Note that this proof technique does not depend on the programming language considered. The difficulty is transferred to the choice of how to split the state, but as long as the splitting is correct (the added triple is covered by the existing ones), the resulting technique is sound.

CONSTRAINT GENERATION

As a final interpretation, we show how the abstract interpretation can be used to construct an actual program analyser. We define the analyser as an interpretation that generates data flow constraints to analyse a given program [START_REF] Nielson | Principles of Program Analysis[END_REF]]. 3 Constraint-based program analysis is a well-known technique for defining analyses. We show how this technique can be lifted and defined entirely as an interpretation, by generating constraints over all the flow variables used in a semantic definition.

We first need to formalise (and extend) the standard notion of program point. We take a program point pp to be a list of integers denoting a position in a term. Program points form a monoid with concatenation operator • and neutral element ϵ. We define a subterm operator t@pp as follows.

We assume a function PP that for a given term t 0 states the set of program points for which constraints will be generated. It typically consists of the set of executable subterms of t 0 . We require the program points of PP(t 0 ) to be executable: if pp ∈ PP(t 0 ), then t 0 @pp = c(t 1 ..t n ). Requirement 2.2 enforces the existence of a skeleton for this term.

We next define a partial operator HPP t 0 that associates program points to the terms occurring in the hooks of a skeleton. Formally, if HPP t 0 (pp, N, t) = pp ′ , then (1) skeleton N is applicable: pp ∈ PP(t 0 ), t 0 @pp = c(t 1 ..t n ), and N is of the form N(c(x t 1 ..x t n )) S, (2) a hook H (_, t, _) occurs in S, and (3) the resulting program point is part of the set of explored program points: pp ′ ∈ PP(t 0 ) and t 0 @pp ′ = (x

Constraints are either of the form

where x and x ′ are variables and s a sort. We generate variable names in constraints of the form pp x. The constraint generation function Gen that takes a program t 0 and returns the set of constraints generated by t 0 is defined as

For each skeleton N we define a function D N that maps sets of constraints to sets of skeletal variables. This is not necessary for the constraint generation but is used to prove consistency between constraints and the abstract semantics.

The constraint generation interpretation of skeletons ⟦S⟧ c is given in Figure 13. The rule for hooks generates constraints for connecting the input state pp ′ x σ with the flow variable holding the input state in the hook pp x f 1 , and the resulting output state of the hook with the output of the hook. Each filter comes with a constraint generation function ⟦F ⟧ c specific to the analysis of that filter. We require that the constraints generated for that filter agree with the abstract semantics: if S is a solution to the constraints ⟦F ⟧ c (pp x 1 ..pp x n , pp y 1 ..pp y m ), then following holds: ⟦F ⟧ # (S(pp x 1 )..S(pp x n )) ⊑ (S(pp y 1 )..S(pp y m )). For analysing a set of branches, we generate constraints for each branch and return the union of these constraint sets.

Correctness. A solution S of a set of constraints C is a mapping from the variables in C to abstract values and terms such that every constraint in C holds. Lemma 7.1. Let t 0 be a term and S be a solution of Gen(t 0 ). Let T # be defined as follows:

Discussion. The constraints we generate are path-insensitive: they do not capture the fact that when a filter does not hold, the rest of the skeleton does not matter. Constraints can be pathsensitive by letting the state of the interpretation be a pair consisting of a set Stop of constraint sets representing pathways in the skeleton that are stopped, similar to the ⊥ flag in the abstract interpretation, and another set Run of constraint sets representing all the running paths. When a filter is encountered, the Run sets are added to Stop with the additional constraint that the filter returns ⊥. The usual constraints for the filter are added to each set in Run. In a nutshell, we duplicate constraints for each filter: once when it does not hold, and once when it may hold. At the end of Example. Consider t 0 = while ¬(x = 0) x := x -1. Its executable subterms are

Note that the subterm x appears both as program points 1•1•1 and 2•2•1 of t 0 . For the different filters we generate symbolic constraints that will reuse abstract filters: ⟦isBool⟧ c (x, y) = {[y = isBool(x)]}. A mapping S is then a solution of such a symbolic constraint if S(y) = ⟦isBool⟧ # (S(x)).

The definition of Gen(t 0 ) generates a large number of constraints. We focus on a selection of them: those generated by the initial program point ϵ. The associated skeleton is While while x t 1 x t 2 H x σ , x t 1 , x f 1 ; isBool x f 1 ? ▷ x f 1 ′ ; . . . .

The constraint generation then produces the constraints

[ϵ x σ : store] , ϵ x t 1 = ¬ (x = 0) , [ϵ x o : store] , ϵ x t 2 = x := x -1 .

as well as the constraints given by H (x σ , x t 1 , x f 1 ); isBool(x f 1 ) ? ▷ x f 1 ′ ; . . . c (N, pp, ∅). The hook case links the variable ϵ x σ to the input of x t 1 , which here represents ¬(x = 0): HPP t 0 (ϵ, While, x t 1 ) = 1 and we thus generate the two constraints