Franc ¸ois Pessaux
email: francois.pessaux@ensta.fr

Damien Doligez
email: damien.doligez@inria.fr

Compiling Programs and Proofs: FoCaLiZe Internals

Keywords: Formal Method, Compilation, Dependency Analysis, FoCaLiZe, Coq ˚Corresponding

Designing a tool to ease the development of high-level security or safety systems must consider to facilitate not only design and coding but also formal demonstrations of correctness and compliance to standards. This entails some requirements on the tool as these demonstrations ask to link together computational and logical aspects of the development. These requirements are briefly considered and a solution is proposed: functions, statements and proofs are handled in a unique language, offering inheritance and parametrized modules. The FoCaLiZe environment implements this language, which remains simple enough to be used in a usual engineering process. The code generation produces an executable functional code (in OCaml) and a checkable term of a logical Type Theory (verified by Coq), close enough to truly ease traceability. It ensures that OCaml and Coq produced codes are error-free and provides compact generated code.

The main contribution of this paper is a detailed presentation of the compilation scheme, which is supported by an original treatment of the dependencies induced by the combination of computational and logical constructs. As the whole source code is translated to a logical term verified by Coq, we get a strong assurance in the correctness of the generated code, hence avoiding the need to prove correctness of the compiler itself.

Introduction

Formal methods have demonstrated their usefulness in software engineering, at least for high safety or security systems. But formal methods have not totally spread upon the software industry: while it is widely recognized that they decrease debugging time by a large amount, they also have the reputation of increasing development time. A way to encourage the use of formal methods is to provide a dedicated development environment, which integrates formal methods all along the development process. An ideal development environment should at least address together specification, design, programming, and proving in a unified language to ease the formal development process. It should also provide checkable verifications/proofs to ease the assessment process, and obviously it should generate runnable code. There already are environments offering some of these features. One can cite Z [START_REF] Spivey | An introduction to Z and formal specifications[END_REF], Maude [2], Dafny [START_REF] Leino | An automatic program verifier for functional correctness[END_REF][START_REF] Leino | Specification and verification of object-oriented software[END_REF], Why3 [5,[START_REF] Bobot | Why3: Shepherd your herd of provers[END_REF][START_REF] Filliâtre | Why3 -Where Programs Meet Provers[END_REF] and B [START_REF][END_REF], largely used in transports.

Theorem provers also provide such environments as they allow declaring specifications and functions and relating them, even by extracting functions from proofs. One can cite Isabelle [START_REF] Team | The Isabelle/Isar reference manual[END_REF][START_REF] Paulson | The foundation of a generic theorem prover[END_REF][START_REF] Nipkow | Isabelle/HOL -A Proof Assistant for Higher-Order Logic[END_REF], Nuprl [START_REF] Constable | Writing programs that construct proofs[END_REF], PVS [START_REF] Owre | PVS: an experience report[END_REF][START_REF] Owre | Writing PVS proof strategies[END_REF] and Coq [START_REF] Team | The Coq proof assistant reference manual[END_REF]. For example, CompCert [START_REF] Blazy | Formal verification of a memory model for C-like imperative languages[END_REF][START_REF] Blazy | Formal verification of a C compiler front-end[END_REF][START_REF] Leroy | Formal certification of a compiler back-end, or: programming a compiler with a proof assistant[END_REF] is developed with Coq and the resulting compiler is obtained using extraction.

All these tools still require some real expertise and not all developers are really acquainted with them [START_REF] Etienne | Improving predictability, efficiency and trust of model-based proof activity[END_REF]. Of course, there is no hope of using formal methods without some knowledge of logics but one cannot expect that most developers know more than first-order logic. Thus an ideal environment should allow writing code, properties and their proofs in a FOL style, possibly with features easing programming (inheritance, parametrization, etc.). Paradoxically, it should also allow to link external code and to state some properties as axioms, for example contracts on external code or physical characteristics. It is clearly unsafe from a logical point of view, must be documented and submitted to a severe review process. But it is unavoidable in real life developments.

The FoCaLiZe [START_REF] Focalize | [END_REF] environment is an attempt to bring a common answer to two aspects of formal methods integration. The first one addresses developers needs, specially when a high level of safety is required. The second one is directly linked to the safety and security assessment process, as required by regulation authorities before commissioning. FoCaLiZe developments contain at the same level logical properties, programming features (pure functional, i.e. without imperative constructs) and mechanized proofs. The compiler emits both executable code and checked proofs together with automatic documentation facilities and ensures strong links between these outputs to increase confidence and to ease assessment. This is achieved by a common trunk of compilation until the concrete computational and logical syntaxes are emitted. Since some safety standards [21,[START_REF]Common Criteria for Information Technology Security Evaluation, Norme ISO/IEC[END_REF] require source code and proof code review by assessors before commissioning, links between source code, object code, properties and proofs must remain very visible at the syntax level. An important point is that logical and computational parts of a program depend on each other. First, these dependencies must be controlled to avoid logical inconsistencies and production of code depending on proofs. Second, dependencies may serve to increase code sharing. Managing these two points is the cornerstone of the compilation process and is the main subject of the paper. They guarantee that the OCaml and Coq emitted codes contain no errors (i.e. any error detected by the target compilers is due to a bug of the FoCaLiZe compiler).

FoCaLiZe has already been used to develop a library of mathematical algebraic structures up to multivariate polynomial rings, a library of security policies [START_REF] Habib | Formal definition and comparison of access control models[END_REF] and to certify airport security regulation [START_REF] Delahaye | Certifying Airport Security Regulations using the Focal Environment[END_REF].

The remaining of this paper is organized as follows. Section 2 recalls our requirements on the design of the language and explains the choices underlying it. Section 3 gives a first approach of the dependency analysis. Section 4 introduces the syntactic elements of the language and some preliminary definitions (4.1), then presents the formalization of the normalization (4.5) and the typechecking (4.6) of species. Section 5 explores various code generation models and justifies the adopted one, which aims at maximizing code sharing and traceability between source and generated code and proofs. Then is sketched the compilation process, which deeply relies on λ-lifting techniques. This demonstrates the need for a more complex dependency calculus. Section 6 addresses the complete dependency calculus. The code generation is formalized in 7. Section 8 discusses some other possible choices and why we did not adopt them. Finally, a comparison with related works is done in Section 9.

Although definitions are given in a as formal as possible language, the paper intentionally contains no theorem to keep it shorter. The focus is put on a precise description of all the aspects of the compilation process, to ease some reuse in other projects. The study of dependencies was first presented in [START_REF] Prevosto | Conception et implantation du langage FoC pour le développement de logiciels certifiés[END_REF]. We give here a completely revised and extended presentation.

Analyzing the design of FoCaLiZe

FoCaLiZe is a "laboratory language" designed to study how to help the development of high integrity software from the double sight of developers and assessors. It is also conceived to be suitable for extensions, experiments, in order to test and progress toward constructs and analyses to make "formal development" easier. This section presents some design choices we considered and the adopted solutions.

The idea is to keep the language simple, pretty close to programming languages usually practiced by engineers, providing commonly used flavors like inheritance, modularity but also allowing to deal with formal properties and proofs. Logical aspects of the language are tried to be kept simple, with human-readable proofs (not only checkable by a machine), making possible interfaces with theorem provers to help the user in carrying on her/his proofs.

Choice of the Semantical Framework

High level security/safety standards such as EN-61508, CC2 [21,[START_REF]Common Criteria for Information Technology Security Evaluation, Norme ISO/IEC[END_REF] ask specifications to be as much as possible formally stated, that is, expressed in a logical language. And the assessment process requires a -as formal as possible -proof that these specification (or design) requirements are satisfied by the implementation.

If the semantics of the specification and programming languages differ too much, errors can arise when mapping logical concepts onto programming ones or vice-versa. These inconveniences can be avoided by choosing a single semantical framework for code, specifications and proofs. This choice is influenced by the one of the programming style which constrains a lot the logical style.

Targeting an imperative language usually leads to the use of Hoare logic style (separation logic, B logic. . . ) to express properties. But proofs cannot freely unfold functions and procedures due to the possible side-effects. This is a real drawback.

Targeting a functional language can ease the choice if the needed side-effects (at least inputs-outputs) can be easily isolated into dedicated modules and separately handled. Then, in any first-order or higher-order logic, due to their referential transparency, functions (of the pure part) can be consistently unfolded when making proofs and thus, can be used without restriction to express properties and proofs. Properties of functions making side-effects can be separately demonstrated and rendered as contracts. For example, ERLANG and SCADE adopt this functional approach, however without logical counterpart. Note that the LAFOSEC study [START_REF] Lafosec | Sécurité et langages fonctionnels[END_REF], ordered by the French National Security Agency (ANSSI), recommends the use of functional languages to develop high-level cyber-security tools.

Since static strong typing is known to ease error detection, we choose to target a strongly typed functional language for the generation of computational aspects. Now the kernel of any strongly typed functional language is a typed λ-calculus, which is a sub-language of any Type Theory, the correspondence between computations and logics being given by the Curry-Howard isomorphism. It relates programming types with types of the theory. Thus, we target a Type Theory as logical language. We choose OCaml (to get an executable program) and Coq (to check consistency of the global development).

Incremental Specification and Development

We now discuss the features to be offered to the user within the retained semantical framework. To illustrate coming discussions, we gradually introduce our running example. It is a "monitor" which inputs a value and outputs a validity flag indicating the position of the value with regards to two thresholds, and this value or a default one in case of problem. It is a simplification of a generic voter developed in FoCaLiZe for critical software [START_REF] Ayrault | Development of a generic voter under focal[END_REF].

Notation. Technical words denoting features and concepts have their first occurrence written in italic while keywords are written in bold.

To serve incremental development and reusability, FoCaLiZe allows inheritance, i.e. the ability of introducing, at any stage of the development, properties, functions and proofs. The rule of visibility is kept simple (no tags private, friend, member, etc.): all inherited elements are visible. Multiple inheritance is available and the choice of the last mentioned element is done in case of name conflict.

The formalized parts of specifications are rendered into (roughly speaking) firstorder statements, called here properties (property), which will receive proofs (proof of). Declarations (signature) introduce names and types of functions. Definitions (let) give functions bodies. Theorems (theorem) are methods embedding a property and its proof at once. Now, only the name of a function is needed to express a (specification) property on it and its body must be known only when unfolded in certain proofs. Thus declarations and definitions may be given separately. And a given function may receive different definitions, enhancing reusability (but function types, which are a true part of functions specification, must be kept). However, because definitions can be unfolded in proofs, each effective definition must be known at compile-time. This static resolution of methods is sometimes called early-binding and the proof management must consider this point (studied further).

Structured data types and pattern-matching are known to ease the management of complex algorithms. We choose a type language à la ML (product and union types, pattern-matching) with a slight different handling of polymorphism (see Section 2.3). We are now ready for a first example.

species Data = let id = "default" ; signature fromInt : int -> Self ; end ;; species OrdData = inherit Data ; signature lt : Self -> Self -> bool ; signature eq : Self -> Self -> bool ; let gt (x, y) = ˜˜(lt (x, y)) && ˜˜(eq (x, y)) ; property ltNotGt : all x y : Self, lt (x, y) -> ˜gt (x, y) ; end ;;

The component Data (introduced by species) simply defines an "identifier" id and declares a function fromInt converting an integer to a value of the type Self which denotes a not yet known internal representation of Data. The species OrdData inherits from Data, it declares two functions (lt and eq), defines a derived function gt and states a property ltNotGt which uses both declared and defined names. Note the use of ˜˜, the "not" operator on booleans, in contrast to ˜which applies to logical formulae.

Species are components of a modular development. They do not collect only types, declarations and definitions but also related properties and proofs. Inside a species, the manipulated data-types have a double role: a programming one used in type verification and a logical one used with the chosen Type Theory, as studied in the following. To simplify the model, all the data-types introduced in a species are grouped (by the way of product and union types) into a single data-type called the representation (rep). It can be just a type variable, whose name (Self) serves in declarations, and be instantiated by inheritance (but not redefined) to allow typing of definitions. It gives to species a flavor of Algebraic Data Type, a notion which has proved its usefulness in several formal frameworks (see [2], CASE tools). The species TheInt defines the representation (as an int, which is a type of FoCaLiZe standard library) and methods already declared in OrdData, then proves the property by unfolding gt and using a property found in the standard library (this proof, which could be done in OrdData, will be used later).

Parameterization

Parameterization is a more general way to use components material as exempli-fied by functors. Two kinds of parameters are often considered, the component ones and the value ones (e.g. integers modulo n). We adopt this feature with the notion of parametrized species. It has however to be adapted to reflect the link between a parametrized component and its parameters at the logical level. This is one of the roles of the dependencies of a Dependent Type Theory, hence it reinforces our choice of the target logical language. The species IsIn below owns one collection parameter V (roughly speaking a component parameter) which provides the methods present in any component having at least those of OrdData. The species also owns two entity parameters minv and maxv whose type is the underlying rep of V. Calling a method of a collection parameter is done using the "bang notation": V!gt stands for the method (property) gt of the collection parameter V. The main question on the design of the modularity mechanism is about the representation of the component parameter: should its definition be exposed or encapsulated? There are two conflicting answers:

type statut_t = | In_range | Too_low | Too_high ;; species IsIn (V is OrdData, minv in V, maxv in V) = rep = (V *
• Inheritance requires exposure as total encapsulation can make the development task tedious (permanent use of "getters" and "setters"). • A component "seeing" the data representation of its parameters can manipulate it without using the provided functions, hence breaking invariants, structural assumptions and theorems brought by parameters. Hence parameterization asks for abstraction. The abstraction of types, as it is usually done via module interfaces, is not sufficient since properties can still reveal the exact definition of the representation. Thus the compiler also has to forbid properties revealing it by a dependency analysis (c.f. Sections 3, 6).

Our solution is to introduce two notions of components, clearly identified at the syntax level by different names (not by attributes drown in code) with very different semantics:

• Species, which expose their representation, and which can be only used along inheritance during design and refinement. • Collections, built from species by encapsulation of the representation, used as effective species parameters during the integration process.

To avoid link-time errors, any call to an effective species parameter imposes that all the functions exported by this parameter are already defined. To preserve consistency, all exported properties must have received proofs. Thus collections must be obtained by encapsulation of the so-called complete species, i.e. those which only contain definitions and theorems. The encapsulation builds an interface hiding the representation and only exposing the declarations of the functions and the properties of this complete species. The compiler must guarantee that all the corresponding definitions and theorems have been checked. The interface is then the only way to access them. The species TheInt, being complete, is submitted to encapsulation (implement ) to create the collection IntC. IntC is used as the effective argument of IsIn's parameter V. Its method fromInt is used to provide effective values for the minv and max parameters. The species IsIn (IntC, IntC!fromInt (5), IntC !fromInt [START_REF] Paulson | The foundation of a generic theorem prover[END_REF]) is then abstracted to create the collection In 5 10. Idem for In 1 8.

Parameterization Versus Polymorphism

Polymorphic method types are forbidden to prevent inconsistency coming from redefinition of methods along inheritance like in: where AsInt inherits from Poly and redefines id with the type int Ñ int. AsBool uses Poly assuming its id has type bool Ñ bool. Both types are correct instances of the scheme @α.α Ñ α. AsInt inheriting from Poly, it can be used to create a collection CInt. This collection then should be usable as an effective parameter of AsBool to create Err. However, in this latter Err!elt evaluates in true + 1 which is ill-typed. Forbidding polymorphic methods is not a real restriction and is even wanted. A polymorphic method taking an argument of type α cannot rely on any property on this type (it can be any effective type). Conversely, let S be a species having a collection parameter C. Any method of S can rely on the properties and the functions of C. Now C can be instantiated by any effective collection issued from a complete species, in which the representation has been defined and these properties have received proofs. Hence parameterization is a way to retrieve a kind of "polymorphism with proved properties".

For instance, a basic species implementing finite sequences of elements with a mem function and a theorem taking benefit from a property of its elements could be written as:

species FSeq (E is OrdData) = rep = list (E) ; let rec mem (e, l : Self) = match l with | [] -> false | h :: q -> E!eq (h, e) || mem (e, q) ; theorem mem_eq_compatible : all l : Self, all e1 e2 : E, E!eq (e1, e2) -> mem (e1, l) -> mem (e2, l) proof = ... ; end ;;

Properties and Proofs

We choose a usual first-order syntax to express properties, however built upon names of types, functions and other properties known in the logical context defined by the species construction. Our experience shows that this simple language is sufficient to express most requirements. It is indeed a sub-language of a dependent type theory, providing only certain forms of dependencies.

Proof writing is based on natural deduction as it is reminiscent of mathematical reasoning and is accessible to a non-specialist without too much effort. Then, the proof is conceived as a hierarchical decomposition into intermediate steps [START_REF] Lamport | How to write a proof[END_REF] unfolding definitions, introducing sub-goals and assumptions in the context until reaching a leaf, that is, a sub-goal which can be automatically handled by a prover. When all the leaves have received proofs, the compiler has to translate the whole tree to the target logical language and to build the context needed for checking this proof.

Solving leaves in FoCaLiZe is done by the prover Zenon [29]. It is a first-order automated theorem prover, based on the Tableaux method, developed by D. Doligez. Zenon can translate its proofs into Coq proofs, to be inserted in the appropriate context computed by the compiler.

We illustrate the decomposition with the following example. A list of steps is always ended by a qed step, whose goal is just the parent goal. Proofs done in a given species are shared by all the species inheriting from this one. As early-binding allows redefinition of functions, proofs using an "old" definition are no longer valid. They must be detected by the compiler as soon as the redefinition is done, reverted to the property status and must be done again. This link between proofs and definitions is an example of dependencies between elements of the user development. Sections 3,4.4 and 6 study them.

Specification requirements such as the safety/security ones need to be proved early in the development cycle, assuming that some functional properties will be satisfied. This helps an early detection of specification errors [START_REF] Ayrault | Development life-cycle of critical software under focal[END_REF]. Thus, FoCaLiZe allows to do proofs using properties not yet proved. The compiler guarantees that they will be proved later in a derived complete species. This is a way to do the proofs just in time and to maximize proof sharing [START_REF] Prevosto | Making proofs in a hierarchy of mathematical structures[END_REF].

Requirements and Choices on the Compilation Process

The target languages and the language features being chosen, it remains to conceive the compilation process.

Code generation has to translate the user code to a source code of the target computational language (called here simply computational code) and to a term of the target logical language (called here logical code). Computational code does not contain properties and proofs. In the logical code, data types and properties have to be translated to types of the Type Theory while definitions and proofs are translated to terms. Moreover, the user code, the computational and logical codes are to be scrutinized along the assessment process, as imposed by some safety and security standards. So the design of the compilation must ensure a good traceability between these three files. It has also to maximize code sharing between different parts of a development, to decrease the amount of code review.

The target languages' compilers typecheck the emitted codes. But on one hand these checks arrive too late. On the other hand, these errors found by the target compilers should be "de-compiled" to be conveyed to the developer. This is not an easy task. The best solution is that the target codes produced by the compiler contain no errors. We choose to include a typing pass during the compilation to early detect computational and logical typing errors and to emit comprehensive diagnostics. This is achieved by a common trunk of compilation for both target languages, the differentiation between them being done only in the very last pass of code generation, at concrete syntax emission. Logical aspects (methods, proofs, and logical dependencies "artifacts") which contribute to Coq code are simply discarded when producing OCaml code. The choice of not relying on an extraction mechanism is discussed in Section 8.

The management of inheritance and early-binding could rely on the internal mechanisms of a functional language providing these features [START_REF] Hardin | Les objets des mathématiques[END_REF] but most of Type Theories do not have them. Thus, an ad hoc translation into the logical target would be needed. But this choice would lead to two different compilation schemes, jeopardizing traceability. Moreover, preserving logical consistency requires a strict control of redefinitions. Therefore we decide to resolve inheritance and early-binding before code generation.

Dependencies in User Code

In this section we introduce a first notion of dependencies, one of the cornerstones of the compilation process. This notion is extended along the study of the code generation model in Section 5.2 then completed into the sections 4.4 and 6, which give a formal presentation of it. A first description of dependencies was done in [START_REF] Prevosto | Algorithms and proof inheritance in the Foc language[END_REF].

In a Dependent Type Theory, terms and types may depend on terms or types. S. Boulmé [START_REF] Boulmé | Spécification d'un environnement dédié à la programmation certifiée de bibliothèques de calcul formel[END_REF] formalized the semantics of an early version of the language in Coq and identified two kinds of dependencies between methods. Either typing a method m may need to know the term corresponding to a method n. We call such a dependency a def-dependency of m on n. Or, typing m may only need to know the type of n. We call this kind of dependency a decl-dependency of m on n.

S. Boulmé also shown that def-dependencies, combined with other features, may introduce inconsistencies. Some of them can be avoided by syntactical restrictions: function bodies cannot contain property names nor keywords for proofs. Thus a function cannot def-depend on a proof. There remain only two possibilities. First, proofs with a by definition of m step (which unfolds the definition of m) def-depend on m. If m is redefined, these proofs must be invalidated. Second, functions and proofs can safely def-depend on the representation. But properties must not def-depend on it as explained by the following example.

The collection Bad encapsulates the complete species Wrong, its interface contains the statement of the theorem theo. When translated into logical code, this statement should be well-typed but typing x + 1 in theo requires to know that Self is indeed (unifies with) int. The encapsulation of the representation, turning Self into an abstract type, prevents it. Thus, the species Wrong must be rejected by the compiler as typing theo would reveal the concrete type rep (a very bad point for security purposes, see [START_REF] Lafosec | Sécurité et langages fonctionnels[END_REF]). Note that function calls do not create def-dependencies and that encapsulation of collections prevents any def-dependency on methods of collection parameters. Thus, the analysis of def-dependencies must ensure that proofs remain consistent despite redefinitions and that properties have no def-dependencies on the representation (in other words, interfaces of collections should not reveal encapsulated information).

The different forms of decl-dependencies are the following. A function m decldepends on a function p if m calls p, a property m decl-depends on a function p if the typing of m in the logical theory requires p's type, a proof decl-depends on p if it contains a step by property p or an expression whose typing needs p and, recursively, m decl-depends on any method upon which p decl-depends and so on. Def-dependencies are also decl-dependencies. The method p can come either from the species itself or from a collection parameter. The following example gives another motivation for decl-dependencies analysis. In S, even is at once declared and defined, so its type can be inferred by the typechecker, using the type of odd. Thus, even decl-depends on odd but odd does not depend on even. In T, defining odd creates a decl-dependency of odd on even and an implicit recursion between them. To keep the logical consistency, such an implicit recursion must be rejected. Recursion between entities must be declared (keyword rec). The compiler has to detect and forbid any cycle in dependencies through the inheritance hierarchy.

Dependencies and Normalization

A well-formed species must not have several methods of the same name and must not change the types of methods along inheritance. The normal form of a species is obtained by regrouping its explicitly given methods and its inherited ones, removing the inherit clauses. Computing this normal form is resolving the inheritance, however without unfolding methods (see Section 4.5). This inheritance resolution phase is important since it is required to check the consistency of the dependencies brought by inherited methods (c.f. Section 3). Species typechecking, verification, normalization, computation of abstractions were first described by V. Prevosto [START_REF] Prevosto | Conception et implantation du langage FoC pour le développement de logiciels certifiés[END_REF]. We resume this presentation, adding clarifications and extensions. It serves as a basis for a complete study of dependencies and for the code generation model.

Syntax

In the following, we shortly introduce the syntax of the language, intentionally skipping constructs that do not add any specific points to the code generation model.

Definition 4.1. Types τ :" a | C | Self | prop | τ Ñ τ | α
Įn addition to types à la ML, Self denotes the representation of the current species (defined or not), C the abstracted representation of a collection parameter and prop the type of logical statements. Basic type constructors are denoted by a. In the following, we identify the syntax of the types with the type algebra. literal denotes the usual constants, ident represents basic lowercase identifiers, used to name methods, functions/properties bound variables, and upper-ident stands for uppercase identifiers used to name species and collections. Note that partial applications of functions should be named. The syntax forbids to nest a proposition into an expression. script describes a hierarchical sequence of proof goals (i.e. logical expressions) with their related proof hints (combination of assumptions and facts). A bullet is a syntactic element representing the nesting level and the name of a step. The assumed keyword represents an admitted proof (c.f. discussion in Section 8); assume serves to introduce typed variables as assumptions in the context of the proof. :" upper-ident | upper-ident p p psarg `q q q prm :"

upper-ident is upper-ident | upper-ident is upper-ident p p pupper-ident ˚q q q | ident in upper-ident field :" inherit se `| rep " τ | signature ident: τ | logical let ident " p | let rrecs ident " e pand ident = eq | property ident : p | proof of ident : = proof | theorem ident : p proof = proof s
:" species upper-ident p p pprm ˚q q q = f ield c :" collection upper-ident = implement se Note.

A logical let definition names a function taking expressions only (not logical expressions) as arguments and returning a logical formula, moreover it can be only applied to all its arguments. It serves as a "macro" as shown by the definition of reflexive: logical let reflexive (r)=all x:Self, r (x, x ) allows to state the properties reflexive (leq), reflexive (geq), . . . No quantification is available over names introduced by logical let, which types are functions to prop (not a logical term). Thus, such definitions bring no higher-order logic features and their applications receive the same treatment as expressions of type prop. So they are not further considered and, as any logical method, they generate no code in OCaml.

Definition 4.6. Names of a Field

Let φ be a field, the set of bound names introduced by φ, written N pφq, is defined by:

N plet m = eq " N psignature m: τ q " N plogical let m = pq " tmu N plet rec m 1 = e 1 and ... m n = e n q " tm 1 ; . . . ; m n u N prepq " N prep = τ q " trepu N pproperty m : pq " N ptheorem m : p proof = proof q " tmu N pproof of m = proof q " tmu
The difference between a field and a method appears with a let rec field which possibly introduces several methods. Note the constant name rep denoting the representation.

Preliminary Definitions Definition 4.7. Defined Names of a Field

Let φ be a field, the set of defined names introduced by φ, written Dpφq, is defined by: Dpsignature m: τ q " Dprepq " Dpproperty m : pq " H Otherwise, Dpφq " N pφq The complete typechecking process of a species S is the construction of a normal form. It first computes the flat form of S, then typechecks its fields and finally ensures its well-formedness. This global process can be refined into 8 consecutive steps detailed in the next sections:

1. Typechecking parameters; 2. Typechecking the inherit clause; 3. Typechecking the fresh methods of the species; 4. Appending inherited methods and methods defined in the species; 5. Flattening the species (resolve inheritance and early-binding to determine which are the effective methods present in the species, collapsing proof of fields with their related logical properties); 6. Ensuring that methods do not have a polymorphic ML-type; 7. Computing the def and decl-dependencies; 8. Ensuring that the obtained species is well-formed.

Definition 4.8. Species in Flat Form

A species S is said in flat form if all the following conditions are satisfied:

• It contains no inherit clause.

• It contains no proof of field (i.e. all of them have been combined with a related property to lead to a theorem, see definition 4.26). Įn such a species, inheritance and selection among available methods (early-binding) have been resolved (c.f. 4.5). This implies that its fields do not introduce several times a same name: @i, j, i " j ñ N pφ i q X N pφ j q " H.

Definition 4.9. Normal Form of a Species

A species S is said in normal form if all the following conditions are satisfied:

• It is in flat form;

• Its fields are well-typed and not polymorphic (however, they can contain "type variables" quantified at the species level); • It is well-formed, i.e. a field only depends on names introduced in previous fields (c.f. 4.25). In other words, fields are ordered (by the compiler) according to their dependencies which cannot be circular (except between explicitly let recbound methods).

4.3.

Type of Fields, Species and Collections

We denote by Φ the field φ annotated by its (inferred) ML-type τ . The type of a species is defined only for a species in normal form. Definition 4.10. Type of Species

ts :" t Ý Ñ Φ u | pC is t Ý Ñ Φ uq ts | pC in τ q ts
The type of a species, ts, is represented by the type of its parameters (C's), followed by the list of the typed fields ({ Ý Ñ Φ }) contained in the normal form of the species. We call atomic species type a type without parameters, i.e. of the form t Ý Ñ Φ u.

Notation. In the rest of this paper, we use a covering arrow to denote a finite ordered sequence of items: Ý Ñ ' stands for a sequence of "'" of the form ' 1 ; . . . ; ' n . When collection and entity parameters (c.f. 2.3) are not distinguished, we shorten C is t or C in τ by the notation C 't. For brevity, cascading parameters pC 1 't 1 qppC 2 ' t 2 qppC 3 ' t 3 qtsqq are shortened by a comma-separated notation: The type of a collection, tc, is the list of the names and types of the methods present in the normal form of its underlying complete species. Definition 4.12. Typechecking Environments • Γ S : pS Þ Ñ tsq or pC Þ Ñ tcq maps a species name S onto its species type and a collection name C onto its collection type.

pC 1 ' t 1 , C 2 ' t 2 , C 3 ' t 3 qts.
• Γ e : px Þ Ñ @ Ý Ñ α .τ q maps an identifier or a method x onto its type-scheme. 4.3.1.

Core Expressions Typechecking

The typechecking of expressions is based on a slightly modified Hindley-Milner algorithm [START_REF] Damas | Principal type-schemes for functional programs[END_REF][START_REF] Milner | A theory of type polymorphism in programming[END_REF][START_REF] Tofte | Operational semantics and polymorphic type inference[END_REF]. As usual, the typing rules rely on two usual functions, Gen and ď. The inference algorithm and fields fusion (c.f. Section 4.26) rely on a slight modification of the most general unifier of two types Mgu.

In the coming definitions, all the rules are given to provide a self-contained presentation, but those not differing from a usual type system à la ML are written in smaller fonts. Definition 4.13. Free Type Variable, Type Generalization and Type Scheme Instantiation

• The set FV of free type variables in a type or a type scheme is defined by : FV pCq " FV pSelfq " FV ppropq " H FV pαq " tαu FV pτ1 Ñ τ2q

" FV pτ1q Y FV pτ2q FV p@α1 . . . αn.τ q " FV pτ qztα1 . . . αnu

• The set of of free type variables in a typing environment is defined by : FV pΓeq "

ď xPDompΓe q FV pΓepxqq
• The type generalization creates a type scheme from a type τ by universally quantifying the unconstrained variables in the environment Γ e . It is defined as usual by:

Genpτ, Γeq " @α1 . . . αn.τ with tα1 . . . αnu " FV pτ qzFV pΓeq

• τ 1 is an instance of the type scheme σ " @α 1 . . . α k .τ (and we write σ ď τ 1 ) if there exists a substitution ϕ from type variables to types such as Dompϕq " tα 1 . . . α k u and τ 1 " ϕpτ q.

We modify the usual notion of most general unifier [START_REF] Robinson | A machine-oriented logic based on the resolution principle[END_REF] in order to keep the representation visible for some steps of the unification process and hide it when types need to be explicited by the compiler (when building interfaces of collections for example).

We first introduce an auxiliary function, Mgpτ 1 , τ 2 q to determine if τ 1 and τ 2 are unifiable under the hypothesis that the representation of the species is either τ rep if defined or Self otherwise. Trying to unify two types may require to know what Self is equivalent to (i.e. what definition is assigned to the representation) as shown in the following definition:

[MGID] τ rep $ Mgpτ, τ q " τ, id if τ " τ rep [MGSELFL] τ rep $ MgpSelf, τ rep q " Self, id [MGSELFR] τ rep $ Mgpτ rep , Selfq " Self, id [MGVARL] τrep $ Mgpα, τ q " τ, rα Ð τ s with α R FV pτ q [MGVARR] τrep $ Mgpτ, αq " τ, rα Ð τ s with α R FV pτ q [MGARR] τrep $ Mgpτ1, τ 1
1 q " τ 2 1 , θ1 τrep $ Mgpθ1pτ2q, θ1pτ 1
2 qq " τ 2 2 , θ2 τrep $ Mgpτ1 Ñ τ2, τ 1 1 Ñ τ 1 2 q " τ 2 1 Ñ τ 2 2 , θ2 ˝θ1
Note that no type apart τ rep is unifiable with Self. The rules [MGSELFL] and [MGSELFR] return the type Self although they could return τ rep . This choice allows to keep the representation hidden. As usual, the cases not handled by the rules fail.

Definition 4.14. Most General Unifier and Unification

Mgupτ 1 , τ 2 q, the most general unifier of τ 1 and τ 2 , is defined by using Mg as follows. If the computation Γ e prepq $ Mgpτ 1 , τ 2 q returns τ 3 , θ, then Mgupτ 1 , τ 2 q " θpτ 3 q. Definition 4.15. Typechecking Rules for Expressions Typechecking computational expressions follows the usual rules with only the call to (species or collection) methods added.

Γ e pmq " @ Ý Ñ α .τ 1 @ Ý Ñ α .τ 1 ďτ Γ S , Γ e $ Self!m : τ [SELFM] Γ S pCq " x Ý ÝÝÝ Ñ m i : τ i y m : τ P Ý ÝÝÝ Ñ m i : τ i Γ S , Γ e $ C!m : τ [COLLM]
Logical expressions are expected to have the type representing logical properties prop, which differs from the type of boolean values bool. Since logical expressions fully embed computational ones, a conversion from bool to prop is allowed by the rule [REGEXPR] where the inferred bool is turned into prop as illustrated by the following figure. As stated in Section 3, def-dependencies of properties and theorems on Self are forbidden by clearing the representation in the typechecking environment (Γ e ' prep : Selfq). The proof of a theorem is typechecked by checking all the expressions located in the proof tree although no type is issued. This ensures that all its sub-goals (which are expressions) are well-typed. No "logical typing", i.e. verification of the correctness of the proof is done at this stage.

Γ S , Γ e ' prep : Selfq $ p : prop proof is well-typed Γ S , Γ e $ theorem m : p proof = proof : theorem m : p proof = proof
The last rule typechecks the list of fields of a species. Each field is typechecked in the environment extended with the bindings issued by the previous typechecked fields.

Γ S , Γ e $ φ : Φ Φ " Ý ÝÝÝ Ñ m i : τ i Γ 1 e " Γ e ' pm i : Genpτ i , Γ e q | m i : τ i P Φq Γ S , Γ 1 e $ Ý Ñ ψ : Ý Ñ Ψ Γ S , Γ e $ φ; Ý Ñ ψ : Φ; Ý Ñ Ψ Definition 4.

Body of a Method

Let S be a species in flat form and m P N pSq a method name. The body of m, written B S pmq, is defined as follows:

B S pmq " K if m R DpSq B S prep = τ q " τ B S plet m = eq
" e B S plet rec m 1 : τ 1 = e 1 and ... m : τ = e and ... m n : τ n = e n q " e i B S ptheorem m : p proof = proof q " proof Definition 4.18. Logical Type of a Method Let S be a species in flat form, with fields well-typed according to rules of Section 4.3.1 and not polymorphic. We define the type T S pmq of a method m P N pSq by embedding computational types into logical ones thanks to the Curry-Howard isomorphism. Hence, logical types are logical statements (i.e. abstract syntax of p's).

T S plet m : τ = eq " T S psignature m: τ q " τ T S plet rec m 1 : τ 1 = e 1 and ... m : τ = e and ... m n : τ n = e n q " τ T S prep : τ q " τ T S pproperty m : pq " T S ptheorem m : p proof =...q " p Note that if the representation is not defined, the typing rules of 4.3.1 naturally give it the type Self. Note also that the type of a proof of field is not addressed. Such fields are assumed to have been merged with a property in order to become a theorem as later described in the definition 4.26.

Notion of Dependencies: First Stage

The rules of 4.3.1 described the typing rules for species fields. In order to obtain the type of a species, the normal form of the species must be computed.

To introduce well-formed species and their normalization, a first notion of dependencies is needed : dependencies of methods on Self and on methods of the species, decl-dependencies of expressions, def-dependencies of a proof and dependencies obtained by transitive closure. This notion of dependencies will be extended in the Section 6.

Definition 4.19. Dependencies of Methods on Self

• A method m decl-depends on the representation if its type or the type of a subexpression of its body is Self. • A method m def-depends on the representation if typechecking m uses the rules

[MGSELFL] or [MGSELFR] in the unification process. Ą decl-dependency means that some parts of the method require the existence of a representation, whatever is its effective definition. A def-dependency means that the particular definition of rep is required to typecheck the method (changing the effective type of rep would cause typechecking to fail).

Technically, the detection of dependencies on the representation is done at two points of the analysis: once during typechecking and once during typed fields fusion (c.f. definition 4.26).

Definition 4.20. Syntactic Decl-Dependencies of an Expression

Let e be an expression, the set e is defined by:

x " H pIf x is a variableq C!m " H pIf C " Selfq Self!m " tmu fun x 1 , . . . , x n Ñ e
" e e pe 1 , . . . , e n q " e Y e 1 Y . . . Y e n let x 1 " e 1 in e 2 " e 1 Y e 2 let rec x 1 " e 1 and . . . and x n " e n in e n`1 "

Ť i"1...n`1 e i p 1 _ p 2 " p 1 ^p2 " p 1 ñ p 2 " p 1 Y p 2 " p " all x : τ, p " ex x : τ, p " p ˛
e collects all the decl-dependencies of e on the methods of the current species by a syntactical walk along the Abstract Syntax Tree of e. As stated in Section 3, this is collecting the names of methods of the species called in e. Let S be a species in flat form and m P N pSq. We define the decl-dependencies ( m S ) and the def-dependencies ( m S ) of a method m on the methods of S by cases on the form of m.

• If m is a signature or is rep, m S " m S " H. • If m is a let, m S " B S pmq and m S " H. • If m is a let rec, m S " p Ť n B S pnq | n 8 mq z t n | n 8 m u and m S " H. • If m is a property, m S " T S pmq and m S " H. • If m is a theorem, m S " B S pmq Y T S pmq and m S " B S pmq .
Įf a field is a let rec m1 =..., all the m i have the same set of decl-dependencies, obtained by removing the names m i from the union of the decl-dependencies of the m i 's bodies. Note that these rules do not consider dependencies on the representation which were already addressed in the definition 4.19.

m 1 ă decl S m 2 ô D a, b such as a 8 m 1 ^b 8 m 2 ^Dt p i u i"1...n such as $ & % a " p 1 p n " b @j ă n, p j P p j`1 S Y p j`1 S m 1 ă def S m 2 ô Dt p i u i"1...n such as $ & % p 1 8 m 1 p n 8 m 2 @j ă n, p j P p j`1 S Įn
other words, a and m 1 are in a same field (i.e. let-rec bound), so are b and m 2 , and there exists a dependency path between m 1 and m 2 , hence between a and b.

To

check if m 1 ă decl S m 2 (resp. m 1 ă def S m 2 )
, one builds the decl-dependencies (resp. def-dependencies) graph of all the methods of S, and searches a path from m 1 to m 2 . These graphs are also used to properly order λ-liftings when building method generators and collection generators as described further.

Normalization Definition 4.25. Well-Formed Species

A species S is said well-formed if @m P N pSq, pm ă decl S mq.

In a well-formed species no field has a circular dependency on itself by transitivity. The following examples show several errors detected by the analysis of wellformedness.

First, 8 can reveal a latent dependency between a let rec bound name m1 having no direct dependency on a name m3. Indeed, m1 depends on m2 which depends on m3. where m3 depends on m1 and m1 depends on m3 via m2, mutually defined with m1. Hence, m3 depends on itself although it was not defined as recursive.

In the definition of ă decl S , the conditions a 8 m 1 and b 8 m 2 are important since decl-dependencies of names introduced by a mutual let rec method exclude these names. In the figure below, omitting the condition m 1 8 a would prevent detecting the transitive dependency of m 1 on p 4 (hence on m 2 ). which is not well-formed. Indeed, taking p 1 " m1, we have m1 8 m1, taking p 2 " m2, we have m2 8 m2. Then we have m1 P m2 B and m2 P m1 B hence m1 ă decl B m1.

Definition 4.26. Typed Fields Fusion

Let Φ 1 and Φ 2 be two typed fields such as N pΦ 1 q X N pΦ 2 q " H. The fusion of two typed fields, Φ 1 Φ 2 , is defined by case. Note that is not symmetric.

signature m : τ 1 signature m : τ 2 = signature m : Mgupτ 1 , τ 2 q signature m : τ 1 let m : τ 2 = e 2 = let m : Mgupτ 1 , τ 2 q = e 2
signature m : τ 1 let rec m : τ 2 = e 2 and n i :

ρ i = en i = let rec m : Mgupτ 1 , τ 2 q = e 2
and n i :

ρ i = en i let m : τ 1 = e 1 signature m : τ 2 = let m : Mgupτ 1 , τ 2 q = e 1 let m : τ 1 = e 1 let m : τ 2 = e 2 = let m : Mgupτ 1 , τ 2 q = e 2 let m : τ 1 = e 1 let rec m : τ 2 = e 2
and n i :

ρ i = en i = let rec m : Mgupτ 1 , τ 2 q = e 2
and n i : ρ i = en i let rec m : τ 1 = e 1 and n i :

ρ i = en i signature m : τ 2 = let rec m : Mgupτ 1 , τ 2 q = e 1
and n i : ρ i = en i let rec m : τ 1 = e 1 and n i :

ρ i = en i let m : τ 2 = e 2 = let rec m : Mgupτ 1 , τ 2 q = e 2
and n i :

ρ i = en i let rec m i : τ i = em i and n i : ρ i = en i let rec m i : σ i = em 1 i and o i : π i = eo i = let rec m i : Mgupτ i , σ i q " em 1 i and n i : ρ i = en i and o i : π i = eo i property m : p 1 property m : p 2 = property m : p 2 if p 1 α " p 2 property m : p 1 theorem m : p 2 = pr = theorem m : p 2 = pr if p 1 α " p 2 theorem m : p 1 = pr property m : p 1 = theorem m : p 1 = pr if p 1 α " p 2 theorem m : p 1 = pr 1 theorem m : p 2 = pr 2 = theorem m : p 2 = pr 2 if p 1 α " p 2 property m : p proof of m = pr = theorem m : p = pr theorem m : p = pr 1 proof of m = pr 2 = theorem m : p = pr 2 α
" is the usual syntactical identity modulo α-conversion between expressions.

Because the fusion relies on α " and Mgu which can fail, this function is partial. Moreover, because fields are not polymorphic, a successful application of Mgu means that the type of a field has not been modified by redefinitions.

As introduced in 4.19, dependencies on the representation are checked again during the fusion process which uses Mgu, possibly unifying Self with other types, adding decl and/or def-dependencies on the representation.

As inheritance allows re-definitions, a proof can be invalidated because the definitions it relies on have been changed. In such a case, the theorem owning the proof has to be reverted into a property. Detection of changes in a method, i.e. of conflicts between its different definitions is the starting point of proof invalidation (c.f. definition 4.29).

Definition 4.27. Conflict Between Fields

Let Φ 1 and Φ 2 be two typed fields sharing a same name m. We say that Φ 1 conflicts with Φ 2 in one of the following cases:

Φ 1 is let m : τ = e 1 and Φ 2 is let m : τ = e 2 Φ 1 is theorem m : p proof = proof 1 and Φ 2 is theorem m : p proof = proof 2 Φ 1 is let m : τ = e 1
and Φ 2 is let rec m : τ = e 2 and . . . Φ 1 is let rec m : τ = e 1 and . . .

and Φ 2 is let m : τ = e 2
No conflict exist between theorem and property (resp. let vs signature) since property and signature only show types, through which no def-dependency is possible.

Redefinitions can invalidate proofs, which must be erased if they have def-dependencies on the redefined method. Def-dependencies on the representation can arise in any kind of methods but since methods must keep their type along redefinitions, the representation cannot be changed, hence cannot require erasure.

E N pHq " H E N pm ; lq " Epmq ; E N YN pmq plq if m X N " H E N pm ; lq " m ; E N plq if m X N " H Įn
the second case of this definition, if m def-depends on names present in N , then m is erased first, and then all the proofs having a def-dependency on m in the remaining context are erased.

We now present the normalization algorithm NF which is used after the typechecking of all the fields. Let us consider S a species defined by: species S Ý ÝÝÝ Ñ pC ' tq = inherit S 1 , . . . , S n " φ 1 . . . φ m end The call to NF to normalize S is done under the hypotheses that the S i are in normal form, the types of parameters methods are known in the environment and the fields of S are typed. The input, W 1 , of NF is a list containing all the typed fields Ý Ý Ñ Φ Si of the inherited species S i in normal form, in the same order as specified in the inherit clause, and ended by the fields directly defined in the species S. This ordering of W 1 is an invariant of the algorithm.

W 1 " Ý Ý Ñ Φ S1 @ . . . @ Ý Ý Ñ Φ Sn @rΦ 1 . . . Φ m s
W 1 can contain several occurrences of a same name in different fields because of multiple inheritance and methods redefinition. The algorithm returns a list W 2 of typed fields such that each name of W 1 appears only once in W 2 (i.e. resolution of inheritance). W 2 represents the list of fields already processed by the algorithm and (possibly temporary) accepted as members of the normalized species. Hence, at any moment, they are "older" according to the inheritance order than the currently processed Φ.

To do that, the algorithm recursively extracts the first field, Φ, of W 1 and appends it to W 2 , if no field of W 2 shares a name with Φ. Otherwise, Φ is fusioned with the first field, Ψ i0 , of W 2 which shares a name with it. The result of fusion is re-inserted as the head of W 1 to look for other possible conflicts with the fields of W 2 following Ψ i0 . The field Ψ i0 is removed from W 2 and, in case of conflict between Ψ i0 and Φ, erasing is propagated in the remainder of W 2 . Doing that, all the theorems recorded in W 2 which def-depend on a name of Φ are reverted into properties. Definition 4.30. Normalization Algorithm

NF pW 1 q = W 2 Ð H While W 1 " H do Φ Ð hdpW 1 q and X Ð tlpW 1 q If N pΦq X N pW 2 q " H then W 1 Ð X and W 2 Ð W 2 @rΦs

Else

Assume that W 2 is of the form rΨ 1 ; . . . ; Ψ m s Let i 0 be the smallest index such as for i P r1 : ms, N pΦq X N pΨ i q " H W 1 Ð pΨ i0 Φq ::

X If Φ conflicts with Ψ i0 then W 2 Ð rΨ 1 ; . . . ; Ψ i0´1 s @ E N pΨi 0 q pΨ i0`1 , . . . , Ψ m q Else W 2 Ð rΨ 1 ; . . . ; Ψ i0´1 s @ rΨ i0`1 ; . . . , Ψ m s 4.6.

Typechecking Species and Collections Definition 4.31. Sub-species Relation

Let S 1 and S 2 be two species in normal form. S 1 is a sub-species of S 2 , written S 1 ď S 2 , if:

N pS 2 q Ă N pS 1 q ^@x P N pS 2 q, T S1 pxq " T S2 pxq By construction, if S 1 inherits from S 2 , then S 1 ď S 2 . This intuitively means that S 1 has at least all the methods of S 2 , with the same types. This relation is used to check that the instantiation of a collection parameter of interface P by a collection of interface C is sound, that is C has at least the methods required by P .

Let ts be a species type and C a collection parameter name. We define Apts, Cq the abstraction operation turning an atomic species type (i.e. without parameters) ts into a collection type by replacing the occurrences of Self by C in the types of the methods of ts.

Apt Ý Ñ Φ u, Cq " xm i : τ i rSelf Ð Csy @m i : τ i P t Ý Ñ Φ u
The abstraction operation allows hiding the structure of the representation when creating a collection from a species. Follow the rules for the typechecking of a species expression se, which issues a species type. We use the "overloaded" operator ' standing for the extension of an environment Γ e with the bindings coming from the names bound in a typed field Φ. Definition 4.33. Rules of Typechecking Species Expressions

Γ S , Γ e $ se 1 : t Ý Ñ Φ 1 u . . . Γ S , Γ e $ se i : t Ý Ñ Φ i u Γ 1 e " Ý Ñ Φ 1 ' . . . ' Ý Ñ Φ i Γ S , Γ 1 e $ Ý Ñ φ : Ý Ñ Φ Ý Ñ Φ 2 " NF p Ý Ñ Φ 1 @ . . . @ Ý Ñ Φ i , Ý Ñ Φ q @m : τ P Φ 2 , τ is not polymorphic Ý Ñ Φ 2 is well-formed Γ S , Γ e $ species S = inherit Ý Ñ se i ; Ý Ñ φ : t Ý Ñ Φ 2 u [NO-PRM] Γ S , Γ e $ se : t Ý Ñ Φ u Γ S ' pC : Apt Ý Ñ Φ u, Cqq $ species Spprmsq = inherit Ý Ñ se i ; Ý Ñ φ : ts Γ S , Γ e $ species SpC is se, prmsq = inherit Ý Ñ se i ; Ý Ñ φ : pC is t Ý Ñ Φ uq ts [COLL-PRM] τ " C Γ S , Γ e ' px : τ q $ species Spprmsq = inherit Ý Ñ S i ; Ý Ñ φ : px in τ q ts Γ S , Γ e $ species Spx in C, prmsq = inherit Ý Ñ S i ; Ý Ñ φ : px in τ q ts [ENT-PRM] Γ S , Γ e $ se : px in τ q ts Γ S , Γ e $ e : τ Γ S , Γ e $ sep p peq q q : tsrx Ð es [ENT-INST] Γ S , Γ e $ se : pC 1 is t Ý Ñ Φ uq ts Γ S pC 2 q " tc 2 tc 2 ď Apt Ý Ñ Φ u, C 2 q Γ S , Γ e $ sep p pC 2 q q q : tsrC 1 Ð C 2 s [COLL-INST]
Γ S pSq " ts Γ S , Γ e $ S : ts rSPEC-IDENTs The rule [COLL-PRM] requires that se has an atomic type: there is no higher-order species. This verification is performed during the typechecking. This restriction also appears in [COLL-INST] since the effective argument C 2 of se has to be a collection name (enforced by the syntax of the language) and not an arbitrary species expression.

In the rule [ENT-INST], τ can only be a name of a collection denoting the representation of this collection. This is syntactically enforced by the grammar of species parameters (c.f. prm in the definition 4.5).

Proposition. The important property of a typechecked species is that its type does not show anymore inheritance: the species is in normal form, with all the methods brought by inheritance and kept according to the early-binding mechanism (the most recent method is always kept in case of redefinition).

Code Generation Model

In this section we outline the chosen code generation model and show the advantages of the dependencies analysis for this model. In Section 8 other possibilities, not adopted, for the code generation are discussed.

Our first choice is to encapsulate the species and collection translations into OCaml and Coq modules to take benefit from a name-space, modularity and later, abstraction by module signature. We use a flat module model where species methods lead to module fields.

Generating Code for only Collections

As explained before, FoCaLiZe design makes a neat distinction between the code writer (of species) and the code user (of collections). This entails that collections are the only mean given to developers to ultimately create computational and logical codes. Thus we may decide to emit target code only when a collection is created. This is indeed possible as FoCaLiZe provides only static object features. But this choice has a major drawback explained below.

Let S be a complete species defined by species S (C is S1). Let C1 created by C1 implement S(D1) and C2 created by C2 implement S(D2). Let m be a method of S. C1 and C2, compiled independently, have their own copy (m1 and m2) of m. m1 and m2 share the body of m up to their calls to methods of D1 and D2. Moreover let SE be a complete species inheriting from S and let C3 a collection created from SE. C3 contains a copy m3 of SE!m. If m is not redefined in SE then m1, m2 and m3 share the body of S!m, up to the calls of methods of S redefined in SE and the calls of parameters' methods. This sharing cannot be capitalized, due to the independence of the compilation of collections.

Thus compiling only collections leads to the duplication of the methods bodies in each created collection. It increases the size of the generated code. It prevents separate compilation since the code is only generated at the "end of the development", requiring the re-examination of all the species underlying each collection. At last, it duplicates code review.

Incremental Code Generation

Our goal is to maximize code sharing between all the collections issued from species created along a given inheritance chain. In these collections, methods having the same name can differ either because some ones have been redefined or because they call methods which have been redefined or provided by different effective collection parameters. In this last case, the changes are located only at these calls: the core of the algorithm remains the same.

On the example of Section 2.3, whatever are the collections created from IsIn, the core of the filter method always applies comparisons. The only differences are the used parameters method lt and the parameters values minv and maxv. In the same way, the statements and the proofs of the theorem lowMin only differ by the effective used method filter of the species and those of its parameters V, minv and maxv.

Method Generator

We decide to generate the code of a method as soon as the method is defined in order to share it all along the inheriting species and the derived collections. Let m be a method whose body contains a call to a method p. Suppose that p is only declared or provided by a collection parameter. Then we λ-lift the name p in the body of m. On the opposite, calls to methods on which m has a def-dependency are directly done. Hence, we use def-and decl-dependencies to determine if a name should be λ-lifted.

If the target language requires explicit types representation (as in Coq), the only declared reps (from the species itself or from its parameters) appearing in the type of the method are also λ-lifted (suffixed by T in the following figure). let gt (x, y) = ˜˜lt (x, y) && ˜˜eq (x, y) The function generated from a given method m by λ-lifting its decl-dependencies is called the method generator of m. It is emitted as soon as m is (re-)defined in a species S, and is shared by all the children of S in the inheritance tree to avoid code duplication. Thus, introducing the notion of method generators allows maximal sharing of the methods bodies. Then, the value of m in a given species will be obtained by applying its method generator to the effective values of its decl-dependencies.

let filter (x) : Self = if V!lt (x, minv) then (minv, Too_low) else if V!gt (x,

Collection Generator

If the species is not yet complete, its compilation produces only the set of method generators of the methods defined by this species. If the species is complete, it may be used to create collections and its compilation has a last step, which is the production of its collection generator. In the above figure, the shapes representing the methods vary in size. The initial size represent the body of the method. As long as the code sharing increases, the shapes get smaller still keeping their contour to remind the original method they implement. Thin arrows represent in some sense pointers to the code of the related method. The dark gray method m 3 is only declared. λ-lifted symbols are in pale gray to remind they indeed represent unknown (a kind of declared) methods.

Let m be a method of a complete species S, thus a method of all the collections C i created upon S. m may have decl-dependencies on a set M of methods of S and a set of decl-dependencies P on collection and entity parameters. Note that the values of the called methods of M by m are already known. Therefore the method generator g m of m can be applied to these values before any creation of one C i . Let us call m M the value of this application. It only remains in m M the λ-liftings of the names in P . Indeed the values of the different occurrences of m in the C i differ now only by the values of the called methods from P .

All the m M 's values of methods of S are grouped into a record while their abstractions are lifted outside the record as abstractions on the whole set of collection parameters methods (dashed rectangles in the figure). This is the definition of the collection generator of S. Doing this way, all the C i share the m M 's bodies.

The value m M itself is obtained by first searching the method generator of m in the inheritance tree of S to find its most recent version, say in the species S1. Suppose that the method m 1 of M was λ-lifted from the body of m because m 1 was an only declared method in S1. Now m 1 has received a definition at some place in the inheritance tree (S is complete) so its method generator g m 1 is known. To obtain the effective value of m 1 , it remains to eliminate the λ-liftings of g m 1 by applying them to the corresponding effective values. This process is well-founded as there is no circular dependencies. Now let CC be a collection obtained from S. The values of CC are obtained by applying the collection generator of S to the effective values of the collection parameters methods. Their search is as follows. Let p 1 be a method of P . It was λ-lifted from the body of m because provided by a collection parameter C of S1. C has been instantiated by a collection D to create the complete species S, through a chain of parameter instantiations along the inheritance tree, which at a node gives the effective value of p 1 . Note that lifting parameters at the record level instead doing it at each method level simplifies the generated code structure and increases its readability (a good point for assessment).

As a conclusion, providing material from the species parameters to create a collection is hence done once, at the point where the collection generator is called. The usage of the method generators ensures code sharing between all the species of a same inheritance tree. The usage of collection generators ensures code sharing between all the collections implementing a given species.

On the example of Section 2.3, the collection generator of the species IsIn (where some types are omitted) can be represented by: where gen xxx stands for the method generator of the method xxx and t xxx for the temporary application of its method generator to its required arguments (either already t yyy or λ-lifted collection / entity parameters material).

To now summarize, a species is compiled toward an OCaml and a Coq module made of the ordered sequence of method generators. Only declared or inherited methods do not lead to generated code. When a species has all its methods defined (complete species), this module also contains a record type definition and a collection generator returning, when applied, a value of this type.

To later create a collection, the collection generator is applied to the methods, types and values passed as effective arguments. As previously stated, a collection being opaque, it will be represented by a module with a constraint signature forcing to only export methods and an abstract type representing the collection's rep.

Dependency Calculus: Second Stage

As explained in this section, the notion of dependencies introduced in Section 4.4 is not sufficient to emit code that Coq can typecheck. We must now address the production of terms correctly typed at the logical level.

Dependencies on Methods of the Species

Let m be a well-typed method. Creating its method generator requires to know the types of the λ-lifted names. If m is a function of body e, only are needed the types of the methods appearing in the decl-dependencies e of e. Since these types are "MLlike" types, they cannot bring any other dependencies. Theorems bodies (i.e. proofs) can introduce def-dependencies, whose definitions must be well-typed in the logical target. Proofs may also introduce decl-dependencies on logical methods, whose types are logical statements: methods appearing in such types must also be well-typed in the logical target language. This is illustrated by the following example, which considers the theorem ltNotGt of Section 2.2.

Convention on generated code. : In the method generator of a method m, the methods n of the species on which m depends are always named abst n. They are either λ-lifted (decl-dependency) or bound by the := construct (def-dependency) to their effective generator. abst T corresponds to the dependency on the representation (which is a type). ltNotGt syntactically decl-depends on gt, lt, the representation and def-depends on gt. As stated in 5.2.1, def-dependencies are not λ-lifted and their corresponding definitions are directly used. Since the proof contains a def-dependency on gt, it means that the Coq term issued by the external prover contains eq (coming from the body of gt), assumed to be λ-lifted as abst eq. Now λ-lifting only methods found in the syntactic def-and decl-dependencies (e.g. forgetting transitive dependencies) would lead to a generated code looking like:

Theorem ltNotGt (abst_T : Set) (abst_lt := lt) (abst_gt := OrdData.gt abst_T abst_eq abst_lt) : forall x y : abst_T, Is_true (abst_lt x y) -> ˜Is_true (abst_gt x y). apply "Large Coq term generated by Zenon";

In this generated code, abst eq which is unbound represents eq. But, eq has a def-dependency on the representation: it should also be propagated to ltNotGt.

Thus only considering dependencies coming from the syntax is not sufficient. The same incompleteness of syntactic dependencies arises for collection parameters methods. Hence, omitted until now, a process of "completion" of these dependencies has to be applied before really λ-lifting them. This point is carried out by computing: 1. the visible universe of a method; 2. its minimal logical typing environment; 3. dependencies on the parameters methods (indeed, these methods are not defined until an effective collection instantiates the parameter: they will be λ-lifted as well -they are decl-dependencies).

The visible universe of a method m is the set of other methods of the species that are needed to ensure that the translation of the method generator of m will be well-typed by the two target languages. The minimal logical typing environment of a method m is obtained by picking the methods of the visible universe and abstracting them or not, i.e. determining if one just needs to keep their type (hence λ-lifting) or also their body (hence ":=-binding"). They are formally defined below.

The visible universe of a method m contains all the methods p on which m has a transitive def-dependency and the methods on which the p decl-depend. Definition 6.1. Visible Universe of a Method

The visible universe of a method m, | m | is defined as follows:

m 1 P m S m 1 P | m | m 1 ă def S m m 1 P | m | m 2 ă def S m m 1 P m 2 S m 1 P | m | m 2 P | m | m 1 P T S pm 2 q S m 1 P | m |
From the notion of visible universe, one defines the minimal logical typing ronment of a method m of a species S. It contains the other methods of S needed to have the method generator of m well-typed in the target languages.

• Methods not present in the visible universe are not required.

• Methods present in the visible universe on which m doesn't def-depend are required but only their type is needed. • Methods present in the visible universe on which m def-depends are required with both their type and body.

Definition 6.2. Minimal Logical Typing Environment of a Method

Let S be a species in normal form of type: Ý ÝÝÝ Ñ pC ' tq tn i : τ i " e i u. Let m be a method name P N pSq. The minimal typing environment of m is obtained by the \ operation defined by:

H \ m " H n R | m | tn i : τ i " e i u \ m " Σ tn : τ " e ; n i : τ i " e i u \ m " Σ n P | m | n ă def S m tn i : τ i " e i u \ m " Σ tn : τ " e ; n i : τ i " e i u \ m " tn : τ " e ; Σu n P | m | n ă def S m tn i : τ i " e i u \ m " Σ tn : τ " e ; n i : τ i " e i u \ m " tn : τ ; Σu 6.2.

Dependencies on Parameters Methods

We now compute the dependencies of an expression on parameters methods.

Definition 6.3. Dependencies of an Expression on a Species Parameter

Let C be a collection parameter of a species S in normal form. t e u S,C the set of direct dependencies of an expression e of S on methods of C is defined by:

t C u S,C pIf C is an entity parameterq " tCu t m u S,C pIf m is a variableq " H t C 1 !m u S,C " H pIf C 1 " Cq t C!m u S,C
" tmu t fun x 1 , . . . , x n Ñ e u S,C

" t e u S,C t e pe 1 , . . . , e n q u S,C

" Let C be a parameter of the species S. We now address computing the minimal set of methods of C required to typecheck the method generator of the method m of S. The rule [DEF] collects dependencies of a method m on C searching them in the set of transitive def-dependencies of m's body in S. The rule [UNIV] collects dependencies of a method m on C searching them in the types of the methods belonging to the visible universe of m. These first four rules can be used before the following rule [PRM].

t
Γ S pSq " p. . . , C p is ... , . . . , C p 1 is S 1 p. . . , C p , . . .qq Γ S pS 1 q " p. . . , C 1 k is I 1 k , . . .q o P rTypes t m u S,C p 1 _ o P rBodys t m u S,C p 1 pn : τ n q P rTypes t o u S 1 ,C 1 k pn : τ n rC 1 k Ð C p sq P rPrms t m u S,Cp
The rule [PRM] takes into account dependencies of a method on a previously introduced parameter, C p , used as argument to build the current parameter C p 1 . [PRM] returns a set of names with their type. The type τ n coming from the rule rTypes t o u S 1 ,C 1 k is the type computed during the typechecking and the rule [PRM] modifies it. We explain it with the following example. In Sprim, the type of K!equal in the dependency of prm reflex is its inferred one: K Ñ K Ñ bool. In the species S, the method prm reflex2 depends on Cpprim!prm reflex which, in turn, depends on equal, but which equal? It does not depend on the one of K since this parameter is the formal one of Sprim. It depends on equal coming from the effective collection used to instantiate K, i.e. Cp. Hence, the type of this equal is no more K Ñ K Ñ bool as above, but Cp Ñ Cp Ñ bool. A substitution is required to replace K by Cp. Indeed, rTypes t o u S 1 ,C 1 k computes the dependencies in S 1 , hence relatively to the parameters of S 1 . There is a dependency of prm_reflex in Sprim on K!equal. However, in S, the effective dependency is on the collection parameter Cp used to instantiate the formal parameter K of Sprim . This information is especially important because the code generation needs to emit typed identifiers to λ-lift dependencies.

Note that the methods n added as new dependencies of m by [PRM] only come from the type of o. Indeed C p being a collection parameter, only the types of its methods are visible. These types can be "ML-like" ones, which contain no method names. They can also be logical formulae and the only names appearing in them are those of computational methods (since properties cannot depend on properties) which have "ML-like" types. Hence there is no risk that (logically) typing such an n needs to transitively add other methods.

None of these rules take into account decl-dependencies that methods of parameters have inside their own species and that are visible through their types. This is the role of the rule [CLOSE] which is applied once the five previous ones have been applied. The following example shows that, using P!th0 to prove th1 (which only makes reference to P!f) however needs to add P!g in the logical typing context, which is done by [CLOSE]. although _p_P_g should also be λ-lifted to get a well-typed term like in the following (and correct) generated code: The following and last rule serves to build the complete set of dependencies D ùpon an initial set of dependencies D.

Γ S pSq " p. . . , C p is I p , . . .q o P DpS, C p qrms pn : τ n q P T Ip poq Ip pn : τ n rSelf Ð C p sq P D `pD, S, C p qrms CLOSE This rule does not consider def-dependencies because only types of parameters are visible (encapsulation of collections) and they have no def-dependencies. Moreover, for the same reasons given for [PRM], new dependencies brought by this rule cannot themselves require applying this rule again to make them logically typecheckable.

Code Generation

Code generation strongly relies on the computation of dependencies, done after the normalization of the species. Species lead to code only through their defined methods. For collections, the produced code comes from the aggregation of the methods of species, taking into account instantiations of parameters.

As stated in Section 2.6, the code generation model is the same for both the computational and the logical target languages. A common intermediate form is elaborated from which concrete syntaxes are finally emitted. Dependencies are indeed tagged to determine whether they come from only logical or also computational methods. The emission of computational code simply ignores logical methods, dependencies they induce and explicit polymorphism. We only present the logical code generation (Coq as target language) since the computational code (OCaml as target language) is just obtained by forgetting logical parts and minor syntactical adjustments.

Remember that a species is compiled into a module containing the generators of its methods. If the species is complete, this module also hosts a record type and the collection generator. A collection is also compiled into a module, containing a call to the collection generator of its underlying species, followed by the definitions of the methods coming from the application of the collection generators to the effective values of its parameters.

We present code generation for species and then, for collections. We adopt a topdown approach to first present the global shape of the code before refining details at each step. All along the code generation rules, we use the grayed typewriter font to denote code emitted in Coq syntax.

Species

The code emitted for a species S is a module (also named S) which possibly contains a record type definition (R), then the code (M) issued from the methods of S and possibly a collection generator (C).

Definition 7.1. Species Generation R " GenRecordpSq M " GenM ethsGenspSq Γ S pSq " p ÝÝÑ C ' tqt Ý Ñ Φ u C " if @m P N pΦq, m P DpΦq then GenCollGenpSq else H S ÝÑ Module S .R M C End S.
The procedures GenRecord, GenM ethsGens and GenCollGen are given in the following, according to the chosen top-down presentation.

As exposed in Section 5.2.2, the record contains all the applications already done of the method generators of the complete species being compiled. The record type exposes their types rf m k : τ k . Only the representations C i of the parameters followed by those of the methods of the parameters m j remain λ-lifted in this record type, as follows:

Record me as species (Ci T : Set) ( p Cj mj: τj ) : Type := mk record { rf T : Set ; rf m k : τ k ; } Note that the representation of the species (rf T : Set) is always the first field of the record since it cannot depend on any other method of the species.

Record Type Generation Definition 7.2. Lifting Parameters in the Record Type

Let m be a method of a species S. Let C be a parameter of S. We define : rRtypes t m u S,C " D `prTypes t m u S,C q rRtypes t m u S,C is computed from the rule [TYPE] completed by application of the rule [CLOSE] for this parameter C.

It is indeed the set of dependencies of m on the methods of C which have to be λ-lifted in the record type definition. Since the record type only shows the types of methods, the dependencies collected by the rule [BODY] are not needed. Moreover, def-dependencies do not appear in types, hence dependencies from the rules [DEF] and [UNIV] are also not relevant. Finally, the rule [PRM] is also not relevant since in the types present in the record, the methods of a parameter, even built by a species expression "application", are always abstracted relative to this parameter's name : the provided effective argument never appears. Let's consider the following example:

species Base = signature one : Self ; signature eq : Self -> Self -> bool ; property eq_spec: all x : Self, eq (x, x) ; end ;; species Sprim (K is Base) = let param_one = K!one ; theorem prm_refl: all z : K, K!eq (z, z) proof = by property K!eq_spec ; end ;; species S (Cp is Base, Cpprim is Sprim (Cp)) = rep = unit ; theorem prm_refl2 : Cp!eq (Cpprim!param_one, Cpprim!param_one) proof = by property Cpprim!prm_refl ; end ;; in which prm_refl2 depends on Cpprim!param_one. There is no need to know that Cpprim!param_one is Base!one: it is lifted as _p_Cpprim_param_one: Later, when a collection will be built from S, the parameters Cp and Cpprim will be instantiated to determine the effective methods to apply to the collection generator. At this moment, _p_Cpprim_param_one will be instantiated by the effective value one of the collection used to instantiate Cp.

Definition 7.3. Representations of Species Parameters

Let S be a species such that Γ S pSq " p ÝÝÑ C ' tqt Ý Ñ Φ u, the set of parameters representations of S is defined by:

PReprsp ÝÝÑ C ' tq " $ ' & ' % H if ÝÝÑ C ' t " H C 0 ' PReprsp ÝÝÝÑ C 1 ' t 1 q if ÝÝÑ C ' t " C 0 is se ; ÝÝÝÑ C 1 ' t 1 PReprsp ÝÝÝÑ C 1 ' t 1 q if ÝÝÑ C ' t " c in C 0 ; ÝÝÝÑ C 1 ' t 1 This
set represents the first λ-lifted material of the record type definition. In case of an entity parameter, no representation is recorded. Indeed if this parameter has a type containing a collection parameter of the species, then this latter inevitably appeared before the entity parameter and was already recorded. Otherwise, the entity parameter inevitably has a type containing a toplevel collection. The same remark applies on species expressions se.

Definition 7.4. Record Type Creation: GenRecord

The generation of the record type, done as follows and presented with some abuses of notation, is only done for a complete species. This operation relies on rrτ ss t the translation of types in the target language (c.f. definition 7.17).

• Let S be a species in normal form.

• Let Γ S pSq " p ÝÝÝÝÑ C n ' t n qt ÝÑ Φ m u • Let C " ( C j T : Set) for all C j P PReprsp ÝÝÝÝÑ C n ' t n q
, the code operating the λ-liftings of parameters representations.

• Let pm " Ť n j"1 pC j ˆŤm i"1 p rRtypes t m i u S,Cj qq an association list between a parameter name C j and the list of its methods upon which at least one method of S depends, according to the rule [RTYPE], thus the list of methods of C j which must be λ-lifted in the record type. The generated code for theses λ-liftings is given by M " @pC j ˆmsq P pm, @m P ms, ( p C j x : rrT Cj pmqss t ) .

• Let F be the list of the names of methods of S, with their logical types.

The type of the record is built as follows:

Γ S pSq " p ÝÝÝÝÑ C n ' t n qt ÝÑ Φ m u C " @C j P PReprsp ÝÝÝÝÑ C n ' t n q, ( C j T : Set) pm " n ď j"1 pC j ˆm ď i"1 p rRtypes t x i u S,Cj qq
M " @pC j ˆmsq P pm, @m P ms, ( p C j m :rrT Cj pxqss t ) F " @m : τ P t ÝÑ Φ m u, rf m :rrτ ss t . S ÝÑ Record me as species CM (abst T: Set): Type := mk record { F }.

Note

that by C, the record type is λ-lifted by all the parameters representations, even if some do not effectively appear inside the record's fields. It is mostly uncommon to have species not using their parameters, hence we choose to have a simplified abstraction computation.

Definition 7.5. Dependencies of a Method on Methods of a Parameter: Last Stage

Let m be a method of a species S. Let C be a parameter of S. rGens t m u S,C is the complete set of dependencies of m on the methods of C. It is defined by: . This function is used to compute the λ-liftings for method generators (c.f. 7.8), the arguments of the methods they def-depend on (c.f. 7.9), and for local applications of method generators in collection generators (c.f 7.11). It is someway the largest set of dependencies.

rGens t m u S,C " rBodys t m u S,C Y rTypes t m u S,C Y D `prDef s t m u S,C Y rUniv s t m u S,C Y rPrms t m u S,

Parameters Instantiation

Let S be a species, parametrized by C p , containing a method generator for a method m having dependencies on some methods of C p . The following rules recursively determine the instantiation of C p along the inheritance tree of S, i.e. what the formal parameter C p refers to.

The following example illustrates the need to follow the instantiations of parameters to know the right effective methods to provide a method generator with.

species P0 = rep = int ; let m = 5 ; end ;; species S1 (P is P0) = rep = int ; let v = P!m ; end ;; species S2 (Q is P0) = inherit S1 (Q) ; end ;;
The species P0 defines a method m. S1 has a parameter P of interface P0 and defines a method v depending on its parameter P's method m. Then S2 also has a parameter Q of interface P0 and inherits from S1. During this instantiation, the parameter P of S1 is instantiated by the parameter Q of S2. Since S2 inherits from S1, S2 has a method v.

In S1 from where v comes, v depends on the parameter P. However, once in S2, it now depends on "by what" P has been instantiated during the inheritance: the parameter Q of S2. Hence, in the collection generator of S2, the method generator of v must be applied to the λ-lifting of Q!m (i.e. p Q m in the produced code) and not to something related to (the unbound in S2) parameter P. Following the parameters instantiations is also required when creating collections. The species P1 inherits from P0 and redefines its method m. The collections C0 and C1 are respectively created upon P0 and P1. When creating the collections D0 and D1 upon S1, the parameter P of S1 is instantiated by two different collections, the first one where m = 5, the second one where m = 25.

There are three possible kinds of instantiations of parameters: by a collection parameter (CP), by a toplevel collection (TC) and, for entity parameters, by an expression (EP).

Intuitively, the search for instantiations starts in the species S 0 containing the definition of the method m that depends on a parameter C p . Then, it recursively walks along the inheritance tree toward more recent species S i inheriting from S i´1 . At each step the formal parameter (initially C p ) of S i´1 is replaced by the effective argument provided in S i .

Definition 7.6. Provenance of a Method

Let S be a species of the form species S = inherit Ý Ñ se Ý Ñ φ and a method m P DpSq. The provenance of m in S (i.e. along the inheritance tree) is defined as follows. Depending on the kind of expression instantiating a parameter, the methods of this latter are accessed differently. Note that when instantiating by a toplevel collection, substitutions have no effect. When instantiating by a collection parameter, the substitution trivially consists in returning this collection parameter. When instantiating an entity parameter, the substitution takes all its sense since the effective expression used to instantiate has to replace each occurrence of the formal parameter.

Γ S pSq " p ÝÝÑ C ' tqt Ý Ñ Φ u @C i P ÝÝÑ C ' t,
ppr i , ms i q " pC i , rGens t m u S,Ci q insts " @C i P pr i , pPInstpS, C i , mq ˆms i q C " @pik, msq P insts, GenRepTypepikq P " @pik, msq P insts, GenPrmMethpik, msq S " GenSelfDeps S pt Ý Ñ Φ u \ mq GenM ethGenpS, mq " Definition m C P S : rrT S pmqss t := rrB S pmqss e .

[MG-METH]

Finally, the last rule, [MG-SPE] iterates on all the methods of the species.

Γ S pSq " p ÝÝÑ C ' tqt Ý Ñ Φ u GenM ethGenspSq " @m P t Ý Ñ Φ u, GenM ethGenpS, mq [MG-SPE]
Ęmitting λ-Liftings and Bindings. The following function GenSelfDeps emits the λliftings due to decl-dependencies and the definitions (:=-bindings) due to def-dependencies. If m has a def-dependency on n, then the method generator of n is applied to its own dependencies. These dependencies of n are methods either already λ-lifted or defined (:=-bound) as n is known when m is introduced. Definition 7.9. λ-lifting Dependencies on Methods of Self GenSelfDeps S pHq " GenSelfDeps S pn : τ ; lq " (abst n : rrτ ss t ) GenSelfDeps S plq GenSelfDeps S prep; lq " (abst T : Set) GenSelfDeps S plq GenSelfDeps S prep " τ ; lq " (abst T := rrτ ss t ) GenSelfDeps S plq

• Let S be a species in normal form.

• Let Γ S pSq " p ÝÝÑ C ' tqt Ý Ñ Φ u • Let S 1 " n é S the
species in which n is defined.

• Let N be the code emitted to access the method generator of n, depending on its provenance. • Let ppr i , ms i q " pC i , rGens t n u S,Ci q for all C i P ÝÝÑ C ' t, the list of couples recording each parameter C i and the list of dependencies of n on C i .

• Let insts " pPInstpS, C i , nq ˆms i q, the list of couples recording the instantiation of each parameter C i and the list of dependencies of n on C i . • Let C " GenRepTypepikq for all pik, msq P insts, the code operating the λliftings of parameters representations. • Let P " GenPrmMethpik, msq for all pik, msq P insts, the code operating the λ-liftings of parameters methods. • Let S " (abst m i : rrτ ss t ) for all pm i : τ i q P t Ý Ñ Φ u \ n, the code operating the application of the method generator of n to the dependencies it has on other methods of S. S 1 " n é S N " if S 1 " S, then n else S'. n Γ S pSq " p ÝÝÑ C ' tqt Ý Ñ Φ u @C i P ÝÝÑ C ' t, ppr i , ms i q " pC i , rGens t n u S,Ci q insts " @C i P pr i , pPInstpS, C i , nq ˆms i q C " @pik, msq P insts, GenRepTypepikq P " @pik, msq P insts, GenPrmMethpik, msq S " @pm i : τ i q P t Ý Ñ Φ u \ n, (abst m i : rrτ ss t ) GenSelfDeps S pn : τ " e; lq " (abst n := N C P S ) GenSelfDeps S plq 7.1.4.

Collection Generator Code If a species is complete, its collection generator is emitted by the following function GenCollGen. C is the code for λ-lifting the representations of parameters. pm is an association list between a parameter name C j and the list of its methods upon which at least one method of S depends. Note that C and pm are the same as those in GenRecord (technically, they are returned by this latter). P is the set of names used to λ-lift the methods in pm.

The applications of each method generator to its arguments are grouped inside a record. The code generation for these applications is the same as when these generators are used for :=-bindings in GenM ethGen (c.f. definition 7.1.3). In these applications, the methods coming from the collection parameters are still not defined hence must be λ-lifted. Hence the collection generator is the function parametrized by these λ-lifted methods, which returns a value of the record.

Definition 7.10. Collection Generator Code Generation

• Let S be a species in normal form.

• Let Γ S pSq " p ÝÝÝÝÑ C n ' t n qt ÝÑ Φ m u • Let C " ( C j T : Set) for all C j P PReprsp ÝÝÝÝÑ C n ' t n q, the code operating the λ-liftings of parameters representations.

• Let pm " Ť n j"1 pC j ˆŤm i"1 p rRtypes t m i u S,Cj qq an association list between a parameter name C j and the list of its methods upon which at least one method of S depends, according to the rule [RTYPE], thus the list of methods of C j which must be λ-lifted in the collection generator.

• Let P " p C j m for all pC j ˆmsq P pm and m P ms, the code operating the λ-liftings of parameters methods. • Let G be the code creating the local applications of the methods generators to their dependencies (from other methods of the species S or from parameters methods). • Let M be the code emitted to apply the record constructor to the local applications built by G.

Γ S pSq " p ÝÝÝÝÑ C n ' t n qt ÝÑ Φ m u C " @C P PReprsp ÝÝÝÝÑ C n ' t n q, ( C T : Set) pm " n ď j"1 pC j ˆm ď i"1
p rRtypes t m i u S,Cj qq P " @pC j ˆmsq P pm, @m P ms, p C j m G " @Φ i P ÝÑ Φ m , @m P DpΦ i q, GenLocal S pmq M " @Φ i P ÝÑ Φ m , @m P DpΦ i q z rep, local m GenCollGenpSq " Definition collection create C P := G mk record C P local rep M. Since the representation is the first method of the species λ-lifted in the record type, local rep is explicitly processed first in GenCollGen. Note that C and pm are the same as in GenRecord (technically, they are returned by this latter). Definition 7.11. Local Applications in a Collection Generator

S 1 " m é S N " if S 1 " S, then m else S'. m Γ S pSq " p ÝÝÑ C ' tqt Ý Ñ Φ u @C i P ÝÝÑ C ' t,
ppr i , ms i q " pC i , rGens t m u S,Ci q insts " @C i P pr i , pPInstpS, C i , mq ˆms i q C " @pik, msq P insts, GenRepTypepikq P " @pik, msq P insts, GenPrmMethpik, msq S " @pm i :

τ i q P t Ý Ñ Φ u \ m, local m i GenLocal S pm : τ " eq " let local m = N C P S in
The rule GenLocal S is very similar to GenSelfDeps S . It mostly forgets type annotations and prefixes each method name by local instead of abst . This is not surprising since the rule GenLocal S pmq provides m with the effective methods on which it depends: these methods have previously be λ-lifted by GenSelfDeps S .

Collections

The following InstCollGenP rms, in addition to generate code, returns the number of arguments generated to instantiate the λ-liftings of the record type. This returned number is used to know how many placeholders must be generated (for Coq) when generating records access in GenM eths (c.f. definition 7.14). Let pm be the list of methods per parameter computed in GenRecord (c.f. pm in the definition 7.4) (technically it is recorded in an environment, not computed again). This information represents the arguments expected by the collection generator. The instantiation of a collection generator's parameters structurally applies the substitution σ. In the following rule, C 1 and P 1 represent a collection (toplevel or parameter) name. Definition 7.13. Collection Generator Parameters Instantiation

• Let S be a species (in normal form).

• Let Γ S pSq " p ÝÝÝÝÑ C n ' t n qt ÝÑ Φ m u • Let σ " r
Ý ÝÝÝÝ Ñ C i Ð e i s, the substitution mapping, for each C i in ÝÝÝÝÑ C n ' t n , its effective value e i .

• Let pr " PReprsp ÝÝÝÝÑ C n ' t n q be the list of the parameters representations. • Let C be the code emitted to instantiate the λ-liftings corresponding to the types of parameters representations by collections representations if the parameters are collection parameters. In case of entity parameter no code is emitted. • Let M be the code emitted to instantiate the λ-liftings corresponding to the methods of the parameters.

Γ S pSq " p ÝÝÝÝÑ C n ' t n qt Ý Ñ Φ u pr " PReprsp ÝÝÝÝÑ C n ' t n q σ " r Ý ÝÝÝÝ Ñ C i Ð e i s
C " @C j P pr, if σpCq " C 1 then C 1 .me as carrier M " @pP, msq P pm, if σpP q " P 1 then @m P ms, P 1 . m else rrσpCqss e InstCollGenP rmspS, Ý Ñ e i q " C M Note that the application of σ can only return either a collection identifier (denoted in the above rule by P 1 and C 1 ) or an expression. The first case corresponds to the instantiation of a collection parameter. The second case is an instantiation of an entity parameter. In case of entity ("else" case), the instantiation simply translates the obtained expression. Definition 7.14. Collection's Methods Generation

Γ S pSq " p ÝÝÑ C ' tqtrep " τ ; Ý Ñ Φ u M " @pm i : τ i q P Ý Ñ Φ , Definition m i := effective collection.( m i . .

. loomoon n rtype args

).

GenM ethspC, S, n rtype argsq " Definition me as carrier := rrτ ss t . M

The record type has as many arguments as the collection generator has. The collection generator λ-lifts the dependencies of the record type. This number of arguments is recorded when the parameters of the collection generator are instantiated (c.f. definition 7.13).

Due to explicit polymorphism in Coq, field accesses in records require to explicitly mention the arguments of the record that encode polymorphism. We could have explicitly emitted the type expressions, however hopefully, the Coq type inference is able to recover them as long as their number is explicit, which is done by providing anonymous arguments (the placeholders denoted by above the horizontal brace in m i . . . ).

Translation of Types and Core Expressions

Several rules generate target code for both types and expressions. For expressions, the main difficulty toward Coq is the generation of explicit polymorphism. Any polymorphic definition has an extra fresh parameter of type Set to denote each type variable. Hence, each instantiation of the definition must be provided with as many arguments of type Set as the definition has polymorphic type variables. Again, Coq is able to infer these types as long is it provided with the right number of placeholders ( ). However, we need to maintain a mapping V between fresh generated parameters and their related type variables.

Emitting code for methods names needs to discriminate on their provenance which can be the species itself, a toplevel collection, a collection parameter or an entity parameter. Entity parameters fall into the regular case of identifiers. We omit the case where the toplevel collection belongs to another compilation unit, in which case the name of this unit should be added as prefix with a "dot notation".

In rr ss e , the translation of expressions, we voluntarily omit the code generation of recursive functions. It requires a very special processing due to the need of termination proofs, which is addressed in a dedicated paper [START_REF] Dubois | Termination Proofs in FOCALIZE[END_REF]. Presenting it here should increase a lot the length of this paper. Definition 7.15. Translation of Expressions Γ S , Γ e , V $ rr" pss p " " rrpss p Γ S , Γ e , V $ rrp 1 _ p 2 ss p " rrp 1 ss p z{ rrp 2 ss p Γ S , Γ e , V $ rrp 1 ^p2 ss p " rrp 1 ss p {z rrp 2 ss p Γ S , Γ e , V $ rrp 1 ñ p 2 ss p " rrp 1 ss p -> rrp 2 ss p Γ S , Γ e , V $ rrall x : τ, pss p " forall x : rrτ ss t , rrpss p Γ S , Γ e , V $ rrex x : τ, pss p " exists x : rrτ ss t , rrpss p Definition 7.17. Translation of Types For types, the same particularity as for expressions arises. The translation of the representations depends on the context: are they collection parameters or toplevel collections? This changes the way to access the type constructor denoting the representation. We also omit the case where the toplevel collection belongs to another compilation unit, in which case the name of this unit should be added as prefix. Note that the type prop is ultimately translated into the type Prop of Coq. However, this may only be required in case of logical let signatures, the only place where the user may mention this type, since it is impossible for him/her to create values of type prop.

V $ rrass t " a V $ @i, rrτ i ss t " t i V $ rrpp Ý Ñ τ i qss t " p( Ý Ñ t i ) V $ rrαss t " Vpαq V $ rrτ ss t 1 " t 1 V $ rrτ ss t 2 " t 2 V $ rrτ 1 Ñ τ 2 ss t " t 1 -> t 2
C is a toplevel collection V $ rrCss t " C .me as carrier C is a collection parameter V $ rrCss t " C T V $ rrSelfss t " abst T Despite this precise description of the compilation, several precise technical details have still be untold, like the following examples.

As it would need a deep presentation of Zenon we do not detail the compilation of proofs and the interaction with Zenon. Technically, it rests upon the dependency calculus and all the needed material is already computed for the core of the code generation presented here. The idea is to embed proofs steps invoking Zenon into Coq Sections to transform the λ-liftings into Parameters to stay with first-order formulae manipulated by Zenon. The compiler must generate the prelude of the section and its postlude to restore the λ-liftings. It must also give to Zenon the definitions which are used as Zenon hints.

The λ-lifting of dependencies requires a special care when two collection parameters get instantiated by a same collection. Weak polymorphic type variables must be handled slightly differently from polymorphic ones.

The compilation relies on different environments between passes to avoid computing several times some same or similar information: this requires slight modifications in a few rules (mostly substitutions in methods for the code generation environment in order to explicitly provide arguments for record accesses instead of placeholders).

The dependencies are computed once for all the target languages. To ensure that dependencies coming from logical methods do not flow into the computational code generated, dependencies must be tagged to remind their provenance.

On a purely practical point of view, the user's identifiers must not conflict with the keywords of the target languages, which is ensured by a convenient name mangling.

Discussion

The requirements and choices discussed in sections 2 and 5 were considered at the early beginning of the FoCaLiZe project. First, the intended semantics was specified in Coq by S. Boulmé [START_REF] Boulmé | Spécification d'un environnement dédié à la programmation certifiée de bibliothèques de calcul formel[END_REF]. It revealed the need of a careful treatment of dependencies. Then, a first prototype of the language, developed by V. Prevosto [START_REF] Prevosto | Conception et implantation du langage FoC pour le développement de logiciels certifiés[END_REF], designed the first concrete syntax and the first FoCaL compiler, whose correctness against FoCaL's semantics was proved (by hand) [START_REF] Prevosto | Proof contexts with late binding[END_REF]. After these pioneer studies, the compiler has been fully redesigned and extended to lead to the current FoCaLiZe system with a common code generation model, by the author. The interface with the Zenon automated theorem prover, already present in the first compiler, has also been extended a lot.

λ-lifting Parameters Instead of Methods. We considered also another possibility to obtain a collection generator. Instead of λ-lifting one by one the parameter method names from the record of collection generators, we could have lifted only the collection parameters names. Then, a collection generator should be directly applied to an effective collection. But typing this application needs to attribute a record type to collection parameters, so to collections and then to species. Since species define a form of subtyping (allowing a collection with more methods than expected to instantiate a collection parameter) we would need a kind of subtyping relation on record types. Although this feature exists in some languages, we prefer to require the minimum of constructs for target languages, hence leaving our code generation model open to a wider range of potential targets.

Theorems Versus Axioms. In the Coq model of a collection, since theorems have been proved should they remain theorems (choice 1) or should they be added as axioms (choice 2)?

The major drawback of choice 2 is that instead of containing a complete Coq source file, any FoCaLiZe compilation unit should be split into several intermediate Coq files, incrementally proving one theorem in the context where previously proved ones are replaced by axioms. For instance, instead of having Coq verifying one complete model: Theorem t1 : ... proof = ... Theorem t2 : ... proof = ... t1 ... Theorem t3 : ... proof = ... t1, t2 ... one should split this model in three parts: Theorem t1 : ... proof = ... Axiom t1 : ... Theorem t2 : ... proof = ... t1 ... Axiom t1 : ... Axiom t2 : ... Theorem t3 : ... proof = ... t1, t2 ... This would clearly seriously degrade readability, traceability and would require for each compilation unit to analyze several Coq files instead of one.

Using functors. An orthogonal model is also possible, keeping method generators but avoiding collection generators. Since a species is represented by a module, it may look convenient to represent parametrized species by functors and inheritance by module inclusion. This presents two major drawbacks. First, notions of functor and module inclusion are required in the target languages, hence may restrict target candidates. Second, even if the inheritance mechanism could be (possibly) simplified, we anyway still need to have it explicitly resolved by the compiler, at least for typechecking, normal form computation and automatic documentation generation. Hence, this intuitive idea of simplifying by using functors would indeed lead to more work than the one already done by the compiler.

Code Extraction. Since FoCaLiZe generates Coq and OCaml code, one may wonder why not directly develop in Coq and use the code extraction mechanism to get executable code.

First, the high-level modeling structures provided by FoCaLiZe are complex to manually express in Coq. It is just the work of the compiler to do this job: checking well-formedness of the components, resolving inheritance, early-binding and parameterization, generating the effective code, interfacing with the prover(s). Nobody would appreciate doing this job by hand.

Second, we decided not to impose an extraction mechanism on the target logical language in order to minimize requirements on it. Moreover, one can imagine to also emit computational code toward other languages than ML, which would require the logical target language to also have an extraction mechanism toward several languages. For instance, a back-end toward Dedukti [START_REF] Boespflug | Design and implementation of a proof verifying kernel for the λΠcalculus modulo[END_REF][START_REF] Boespflug | The lambda-pi-calculus modulo as a universal proof language[END_REF] is currently in progress, taking benefit from some evolutions of Zenon to handle deduction modulo [START_REF] Cauderlier | Checking Zenon Modulo Proofs in Dedukti[END_REF].

External Code. Aside species and collections which serve to make an incremental development, some primitive notions like booleans, integers, etc. are needed and given by the standard library of the language. The library can also provide proved properties on these primitives. It is possible to call FoCaLiZe collections methods from OCaml code, being aware of their proved properties. Conversely, external OCaml or Coq libraries can also be accessed via a binding mechanism. Their properties can be granted by other means (contracts, verification tools, etc). If no formal proof evidence can be issued for the properties of these external libraries, it is still possible to assume them as holding, giving them a proof reduced to the keyword assumed. This is a needed but dangerous feature as admitted properties can lead to logical inconsistencies. Depending on the context of the system, some "only nearly true" but "well-known theorems" may be safely considered as holding to simplify the problem and directly deal with "more functional" properties. For instance, @x P N, x `1 ą x doesn't hold since arithmetic is modulo the number of bits of machine integers, however some practical considerations can guarantee that no overflow will occur [START_REF] Clochard | How to avoid proving the absence of integer overflows[END_REF].

The use of this keyword is recorded in the automatically done documentation file provided by the compilation process. The assessment process must ultimately check that any occurrence of this keyword is harmless.

Contracts. Using contracts to take benefits from external code can be done in two ways. First, the contract may simply be blindly assumed as holding. In this case its property must be artificially proved using the keyword assumed as presented in the previous paragraph.

The second solution is to obtain a real proof, i.e. a λ-term of the target logical language, then embed it in the global logical model created during the compilation. Doing this way, the logical verifier is also able to check the proofs of the contracts. This implies that the contract has already been formally verified externally (for instance with a WP tool). The aim is then to rebuild a complete proof from the proved pre/postconditions. However, it is not yet clear if a deep embedding of the WP logic (and the foreign language) is unavoidable.

Proofs Writing. To write proofs, another solution could be to use the syntax and the tools of the chosen prover. We tried the first choice (it is still possible in FoCaLiZe to insert Coq proofs) and found several drawbacks.

• The user must have a deep knowledge of the prover to powerfully use it and to understand error messages. • The user must be aware of the mapping done by the compiler between the concrete language and the target logical one. • The proofs too deeply depend on this target logical language. Indeed, the proof format should allow translation of proofs to several theorem provers (based on type theory).

Recursive Functions. Termination proofs for recursive functions have recently been integrated in FoCaLiZe [START_REF] Dubois | Termination Proofs in FOCALIZE[END_REF]. The user can provide a measure (function returning an integer) or a well-founded relation. In both cases, the compiler automatically generates proof obligations that must be proved by the user with the usual proof style (i.e. helped by Zenon). For a measure, the core of the obligations requires a strict decreasing of the measure at each recursive call. For a well-founded relation, the argument of the recursive calls must be smaller than the initial argument according to this relation. In both cases, the user has to write proofs only taking care of the recursive parameter, the compiler ensures the transformation of the obligations and their proofs to cope with all the parameters of the function.

Pattern-Matching. The pattern-matching must still be handled in a finer way to hide the facts that Zenon only handles head-most patterns and that Coq requires expansion of nested patterns.

Related Work

Our choice was to consider a pure functional language, leaving side effects outside the model. Other tools made the choice of directly addressing an imperative language.

Spec7 [START_REF] Barnett | Boogie: A modular reusable verifier for object-oriented programs[END_REF] is such a language, a subset of C7 with an stronger static typing and a pre/post mechanism to specify properties of the manipulated entities. The compiler adds runtime verifications for contracts. The language is compiled toward Boogie [START_REF] Leino | This is boogie 2[END_REF] which serves as an intermediate verification language. This latter is able to perform loop-invariants inference and uses the Spec7 program annotations and type properties to try to statically prove that the inserted runtime checks are always satisfied (hence useless). Dafny [START_REF] Leino | An automatic program verifier for functional correctness[END_REF] follows the same scheme, also compiling toward Boogie, but extends the language with built-in sets and sequences, algebraic datatypes and termination metrics. Differently from us where termination proofs are written like the others, termination is checked thanks to an annotation (lexicographic tuple). In both cases, proofs are also done using an external theorem prover [START_REF] De Moura | Z3: An efficient smt solver[END_REF]. However, no logical term is produced as witness.

Why3 [START_REF] Filliâtre | Why3 -Where Programs Meet Provers[END_REF] relies on WhyML, a language with functional features similar to FoCaL-iZe but also providing references, loops and exceptions. It does not have inheritance and parametrization but a system of theories allowing modularity. Like for Spec7 and Dafny, the approach is different from ours, not only by the use of Hoare logic required to handle imperative programs. Proofs are done from pre/post-conditions and invariants given by the programmer and not from "lemmas" written outside the implementation of the functions. Wh3 is able to generate proof obligations and submit them to a large number of external provers, much more than FoCaLiZe currently does. No witness term is either produced.

Unfortunately, as far as we know, there is no available details on the implementation of B. Even if the logical framework differs from ours, it is clear that refinement and abstract machines have common points with our inheritance and parametrization, hence may induce questions similar to those presented in this paper.

In [START_REF] Leijen | Programming with row-polymorphic effect types[END_REF] D. Leijen presents a type system with effects to separate functional and imperative components of a program. Such a technique may be of interest since we also rely on an ML-like type system. This would not solve proof writing for imperative parts of a program but this could detect and forbid unfolding functions with side effects in our proofs.

It is clear that our work does not target the compilation of general object languages. We compile toward high-level target languages and not native code. Hence we do not care of register allocation, memory allocation, etc. Also, our object-oriented features are static (no dynamic dispatch). For these reasons, it is difficult to compare our compilation scheme with those of these languages.

Finally, our approach does not aim at proving the compiler unlike, for example, [START_REF] Chlipala | A certified type-preserving compiler from lambda calculus to assembly language[END_REF][START_REF] Leroy | A formally verified compiler back-end[END_REF]. The generated code is submitted to an external verifier (Coq). The guarantee of correctness for the computational target code relies on the common trunk of the compilation, as long as the logical generated code is accepted by Coq.

Conclusion and Future Work

The main objective of this paper is the presentation of the compiler which aims rather differ from those of most compilers of programming languages. This compiler produces both logical and computational codes tightly linked together. We try to give a very detailed, and as formal as possible, presentation for several reasons.

First, we consider important to explain the way the compiler produces error-free Coq and OCaml codes, without requiring the user to manipulate these languages. Errors are handled at the source language level. The proofs are done by the user, helped by Zenon, and Coq is used as both an "assembly" formal language and a guarantor which double-checks the complete development, including proofs. Both target codes are very close to each other, as they are emitted from the same intermediate form, by only adapting the syntax. The OCaml code is mostly an erasing of the logical parts of the Coq code. This closeness eases the assessment process when specifications and code must be compared.

Second, there are few papers on compilers with similar target languages. The system B [START_REF][END_REF] generates proof obligations and C/ADA code. DAFNY [START_REF] Leino | An automatic program verifier for functional correctness[END_REF][START_REF] Leino | Specification and verification of object-oriented software[END_REF] allows building executable or DLL libraries. It features a language with dynamic allocation and generic classes. WHY3 [5,[START_REF] Bobot | Why3: Shepherd your herd of provers[END_REF][START_REF] Filliâtre | Why3 -Where Programs Meet Provers[END_REF] is able to generate OCaml code, generating proof obligations and submitting them to various external provers. These languages allow imperative programming and Hoare logic styles. The user states his/her specifications using pre/post conditions, and more generally, invariants. Their goal is not to issue a complete formal model of the generated code to submit it to a prover.

Third, reading the source code of a compiler is generally not the good way to reuse some of its features. We hope that this presentation can help other projects with similar needs, and we write it with this aim in mind. For instance, developments with strong safety/security concerns can ask for Domain Specific Languages issuing proofs of conformance. All these details may also be enjoyed by anybody wishing to extend FoCaLiZe.

To justify such a compilation process and the induced difficulties, a preliminary presentation of the design choices was needed. These choices come from the will to avoid dissociating the computational and logical aspects in a formal development, while keeping the language palatable. The mix of inheritance, early-binding, encapsulation, inductive data types and unfolding of definitions in proofs creates complex dependencies, which have to be analyzed to ensure programs correctness. This analysis gives the basis of the compilation process through the notions of method and collection generators, that we introduced to maximize code sharing. These choices brought the main difficulties of the compilation process. Some work remains to be done in order to enhance FoCaLiZe and its compiler. The Zenon prover greatly contributes to the proof automation. Some works are currently extending it to handle arithmetic, and other provers than Coq. This may allow to experiment FoCaLiZe with other target type theories and other kinds of properties.

Temporal properties (à la "always", "never", "finally" . . . ) cannot currently be expressed in FoCaLiZe. This must be a point to address since many programs requiring a high level of confidence are embedded, real-time ones and require such properties to be proved. Zenon is able to handle TLA formulae, hence this direction has to be investigated.

  species TheInt = inherit OrdData; rep = int ; let id = "native int" ; let fromInt (x) : Self = x ; let lt (x, y) = x < y ; let eq (x, y) = x = y ; proof of ltNotGt = by definition of gt property int_ltNotGt ; end ;;

  species Poly = let id (x) = x ; end ;; species AsInt = inherit Poly ; rep = unit ; let id (x) = x + 1 ; end ;; species AsBool (P is Poly) = rep = unit ; let elt = P!id (true) ; end ;; collection CInt = implement AsInt end ;; collection Err = implement AsBool (CInt) end ;;

  theorem t : all a b c : bool, a -> (a -> b) -> (b -> c) -> c proof = <1>1 assume a b c : bool, hypothesis h1: a, hypothesis h2: a -> b, hypothesis h3: b -> c, prove c <2>1 prove b by hypothesis h1, h2 <2>2 qed by step <2>1 hypothesis h3 <1>2 qed by step <1>1 The proof has two outer steps <1>1 and <1>2. Step <1>1 introduces hypotheses h1, h2, h3 and the sub-goal c. It is proved by a 2-steps sub-proof. Step <2>1 uses h1 and h2 to prove b. Step <2>2 uses <2>1 and h3 in order to prove c. Step <1>2 ends the whole proof.

species

  Wrong = rep = int ; let inc (x) : Self = x + 1 ; theorem theo : all x : Self, inc (x) = x + 1 ; collection Bad = implement Wrong ; end ;; Bad interface rep : self inc (x) : Self -> int theorem theo : all x : Self, inc (x) = x + 1 ;

  species S = signature odd : int -> bool ; let even (n) = if n = 0 then true else odd (n -1) ; end ;; species T = inherit S ; let odd (n) = if n = 0 then false else even (n -1) ; end ;;

Definition 4 . 2 .

 42 Core Expressions long-ident :" ident | upper-ident!ident e :" literal | long-ident | fun identp, identq ˚Ñ e | let rrecs ident = e pand ident = eq ˚in e | e (ep, eq ˚)

Definition 4 . 3 .

 43 Logical Expressions (Propositions) p :" e | p _ p | p ^p | p ñ p | " p | all ident: τ , p | ex ident: τ , p ąll stands for the universal quantification and ex for the existential one. Note that logical expressions fully embed core expressions. Definition 4.4. Proof Script proof ::" proof-step ˚qed-step | leaf-proof leaf-proof ::" by fact `| conclude | assumed qed-step ::" bullet qed proof proof-step ::" bullet assumption ˚prove p proof assumption ::" assume ident: τ | hypothesis ident: p fact ::" definition of ident `| hypothesis ident | property ident `| type type-ident | step bullet `Ą

Definition 4 . 5 .

 45 Species and Collection Expressions sarg :" e | upper-ident se

Definition 4 . 11 .

 411 Type of Collection tc :" x Ý ÝÝ Ñ m : τ y

  bool theorem t: let le (x, y) =

Definition 4 .

 4 21. Syntactic Def-Dependencies of a ProofLet p be a proof. The set of syntactic def-dependencies of p is defined by: p " t m | by definition of m is a step of p u. Definition4.22.Names in a Same Field Let S be a species in flat form, L the list of its fields and m and n two methods of S. m 8 n if it exists φ P L such that m P N pφq and n P N pφq. This -reflexive -relation is used to compute the effective dependencies on other methods of the species and the well-formedness of the species. Definition 4.23. Dependencies of a Method in a Species

Definition 4 .

 4 24. Transitive Dependencies Let S be a species in flat form. The method m 1 of S has a transitive decl-dependency on the method m 2 of S, denoted by m 1 ă decl S m 2 (resp. a transitive def-dependency denoted by m 1 ă def S m 2 ) if:

  species A = let rec m1 = ... m2 and m2 = ... m1 ; end ;; species B = inherit A ; let m3 = ... m1 ; let m2 = ... m3 ; end ;; Once in flat form, the species B would have the form: species B = let m3 = ... m1 ; let rec m1 = ... m2 and m2 = ... m3 ; end ;;

Since 8

 8 is reflexive, we also ensure that two names do not have mutual dependencies (set m 1 " p 1 and p 2 " m 2 in the definition of ă decl S ) as shown the following example: species A = signature m1 : ... let m2 = ... m1 ; end ;; species B = inherit A ; signature m2 : ... ; let m1 = ... m2 ; end ;; Once in flat form, the species B would have this form species B = let m1 = ... m2 ; let m2 = ... m1 ; end ;;

Definition 4 . 28 .

 428 Erasure of TheoremsEptheorem m : p proof = proof q " property m : p Epmq " m otherwise Definition 4.29. Erasure in a Context Let N be a list of methods names, m be a typed field and l a list of typed fields. The erasure in the context of N is defined by:

Definition 4 . 32 .

 432 Abstraction of a Species Type w.r.t. a Collection Parameter Name

Definition 4 . 34 .

 434 Rule of Typechecking Collections Γ S , Γ e $ se : t Ý Ñ Φ u se represents a complete species Γ S , Γ e $ collection C = implements se end : Apt Ý Ñ Φ u, Cq

Let

  collection_create (V_T : Set) (minv : V_T) (maxv : V_T) V_lt V_gt V_ltNotGt := let t_filter := gen_filter V_T V_lt V_gt minv maxv in let t_getStatus := gen_getStatus V_T in let t_getValue := gen_getValue V_T in let t_lowMin := gen_lowMin V_T V_lt V_gt V_ltNotGt minv maxv t_filter t_getStatus in { filter = t_filter ; getStatus = t_getStatus ; getValue = t_getValue ; lowMin = t_lowMin }

  theorem ltNotGt : all x y : Self, lt (x, y) -> ˜gt (x, y) proof = by definition of gt property int_lt_not_gt ;

  rBodys t m u S,C " t B S pmq u S,C rTypes t m u S,C " t T S pmq u S,C rDef s t m u S,C " ď t B S pnq u S,C for all n such as n ă def S m rUniv s t m u S,C " ď t T S pnq u S,C for all n such as n P| m | The rule [BODY] (resp. [TYPE]) collects the syntactical dependencies on methods in the body (resp. type) of a definition. Note that the rule [TYPE] collects dependencies of properties and theorems upon only computational methods of C since properties cannot depend on properties.

species

  Sprim (K is Base) = theorem prm_reflex: all z : K, K!equal (z, z) proof = ... end ;; species S (Cp is Base, Cpprim is Sprim (Cp)) = theorem prm_reflex2 : ... proof = by property Cpprim!prm_reflex ; end ;;

  species A = signature f : Self -> int ; signature g : Self -> int ; property th0: all x : Self, f (x) = 0 /\ g (x) = 1 ; end ;; species B (P is A) = theorem th1 : all x : P, P!f (x) = 0 proof = by property P!th0 ; end ;;Omitting the application of this rule would lead to the following incorrect generated code where _p_P_g is unbound:Theorem th1 (_p_P_T : Set) (_p_P_f : _p_P_T -> int) (_p_P_th0 :forall x : _p_P_T, Is_true (_p_P_f x = 0) /\ Is_true ( p P g x = 1)) :forall x : _p_P_T, Is_true (_p_P_f x = 0).

Theorem

  th1 (_p_P_T : Set) (_p_P_f : _p_P_T -> int) ( p P g : p P T -> int) (_p_P_th0 : forall x : _p_P_T, Is_true (_p_P_f x = 0) /\ Is_true ( p P g x = 1)) : forall x : _p_P_T, Is_true (_p_P_f x = 0).

  Record me_as_species (Cp_T : Set) (Cpprim_T : Set) (_p_Cp_eq : Cp_T ->Cp_T -> bool) (_p_Cpprim_param_one : Cp_T) : Type := mk_record { rf_T : Set ; rf_prm_refl2 : Is_true (_p_Cp_eq _p_Cpprim_param_one _p_Cpprim_param_one) }.

  C , S, Cqrms rGens t m u S,C gathers the dependencies of m on C's methods found by applying the rules [TYPE], [BODY] and the rule [CLOSE] on the union of dependencies obtained by [DEF], [UNIV] and [PRM]

  C0 = implement P0 ;; collection C1 = implement P1 ;; collection D0 = implement S1 (C0) ;; collection D1 = implement S1 (C1) ;;

  m P DpSq m é S " S m R DpSq m é se i " S 1 with i the highest index in Ý Ñ se m é S " S 1 These rules search the definition of m in S first, otherwise in the latest inheritance node defining m (in case of multiple inheritance, the rightmost species in the inherit clause is considered first as stated in 2.2). Definition 7.7. Parameter Instantiation

Definition 7 .Ñ m 1 "

 71 12. Collection Generation pP, n rtype argsq " InstCollGenP rmspS, Ý Ñ e q M " GenM ethspC, S, n rtype argsq Ý SubstInM ethspS, Ý Ñ e q collection C implement Sp Ý Ñ e q ÝÑ Module C . Let effective collection := C .collection create P . M End C .

  e u S,C Ť i"1...n t e i u S,C t let x " e 1 in e 2 u S,C " t e 1 u S,C Y t e 2 u S,C t let rec x 1 " e 1 . . . and x n " e n in e n`1 u S,C " Ť i"1...n`1 t e i u S,C t p 1 _ p 2 u S,C " t p 1 ^p2 u S,C " t p 1 ñ p 2 u S,C " t p 1 u S,C Y t p 2 u S,C This definition is similar to 4.20 except it tracks calls on methods of a parameter. Note that if C is an entity parameter, the identifier of the parameter itself is considered as its only method.

t " p u S,C " t all x : τ, p u S,C " t ex x : τ, p u S,C " t p u S,C

Γepxq " @ Ý Ñ α .τ1 @ Ý Ñ α .τ 1 ďτ Γ S , Γe $ x : τ [VAR] Γ S ,Γe ' px1 : τ1q ' . . . ' pxn : τnq $ e : τ Γ S , Γe $ fun x1, . . . , xn ->e : τ1 Ñ . . . Ñ τn Ñ τ [FUN] Γ S , Γe $ e : τ1 Ñ . . . Ñ τn Ñ τ Γ S , Γe $ e1 : τ1 . . . Γ S , Γe $ en : τn Γ S , Γe $ epe1, . . . , enq : τ [APP] Γ S , Γe $ e1 : τ1 Γ S , Γe ' px : Genpτ1, Γeqq $ e2 : τ2 Γ S , Γe $ let x " e1 in e2 : τ2 [LET] Γ S , Γe ' pxi : @H.τiq $ ei : τi Γ S , Γe ' pxi : Genpτi, Γeqq $ e : τ Γ S , Γe $ let rec x1 = e1 and ... xn = en in e : τ [LETREC]

int -> int -> bool int -> int -> bool le (x, y) -> ~ le (y, x)x < y prop -> prop -> prop bool Γ S , Γ e $ e : bool Γ S , Γ e $ e : prop [REGEXPR] Γ S , Γ e $ p : prop Γ S , Γ e $" p : prop [NOT] Γ S , Γ e $ p 1 : prop Γ S , Γ e $ p 2 : prop Γ S , Γ e $ p 1 b p 2 : prop [OR/AND/IMPLY] pfor b " _, ^, ñq Γ S , Γ e ' px : Genpτ, Γ e qq $ p : prop Γ S , Γ e $ all x : τ, p : prop [ALL] Γ S , Γ e ' px : Genpτ, Γ e qq $ p : prop Γ S , Γ e $ ex x : τ, p : prop [EX] Definition 4.16. Typed Fields Let S be a species and φ a field of S. The typed field Φ is obtained by annotating φ with its inferred type. Judgments are of the form Γ S , Γ e $ φ : Φ. The rules for typechecking fields are presented below. As explained in Section 2.4, polymorphic methods are forbidden. However, typechecking rules do not enforce this restriction which is verified afterwards.$ rep : rep : Self $ rep " τ : rep : τ $ signature m : τ : signature m : τ Γ S , Γ e $ e : τ Γ S , Γ e $ let m = e : let m : τ = e Γ S , Γ e ' @i P r1 . . . ns, pm i : Genpτ i , Γ e qq $ @i P r1 . . . ns, e i : τ i Γ S , Γ e $ let rec m 1 = e 1 . . . and m n = e n : let rec m 1 : τ 1 = e 1 . . . and m n : τ n = e nThe types of computational definitions, thanks to the Curry-Howard isomorphism, are directly embedded into the logical type theory. The type of a property (or a theorem) is definitively not a "ML-like" type but a logical formula: the statement itself of the property (or of the theorem). Γ S , Γ e ' prep : Selfq $ p : prop Γ S , Γ e $ property m : p : property m : p

Γ e pxq " @ Ý Ñ α n .τ Γ e , V $ rrxss e " (x lo omo on n times ) Γ S , Γ e , V $ rrSelf!mss e " abst mΓ S $ C is a toplevel collection Γ S , Γ e , V $ rrC!mss e " C . m Γ S $ C is a collection parameter Γ S , Γ e , V $ rrC!mss e " p C m Γ e $ x 1 : τ 1 . . . Γ e $x n : τ n Γ e $ e : τ Γ S , Γ e , V $ rress e : e 1 Γ S , Γ e , V $ rrfun x 1 , . . . , x n ->ess e " ( x 1 rrτ ss t 1 ) . . . ( x n rrτ ss t n ) : rrτ ss t := e 1 Γ S , Γ e , V $ rre pe 1 , . . . , e n qss e " ( rress e rre 1 ss e . . . rre n ss e ) Γ S , Γ e , V $ rrlet x " e 1 in e 2 ss e " let x := rre 1 ss e in rre 2 ss e Γ e $ e : τ Genpτ, Γ e q " @α 1 . . . α n .τ v 1 . . . v n fresh variables Γ S , Γ e , V ' pα i Þ Ñ v i q $ rress e " e 1 Γ S , Γ e , V $ rress e " ( v 1 : Set) . . . ( v n : Set) e 1 Definition 7.16. Translation of Logical Expressions Logical expressions of type bool need to be explicitly injected in the type of logical properties (Prop) using Coq's construct Is true. In effect, expressions of type bool are computable terms: their value can be computed although logical properties are not always decidable.Γ S , Γ e , V $ e : bool Γ S , Γ e , V $ rress p " (Is true rress e ) Γ S , Γ e , V $ e : prop Γ S , Γ e , V $ rress p " rress e

Acknowledgments

I first want to strongly thank Thérèse Hardin, who greatly contributed to enhance this paper. I also want to thank people who gave me their comments (and also strongly participated to the FoCaLiZe adventure), David Delahaye, Damien Doligez, Catherine Dubois, Mathieu Jaume, Virgile Prevosto, Renaud Rioboo, Pierre Weis.

m é S " S PInstpS, C p , mq " CPpC p q m é S " S 1 with S 1 " S Sp. . . , C p ' t p , . . .q " inherit S 1 p. . . , e p , . . .q Γ S pS 1 q " p. . . , C 1 p ' t 1 p , . . .qt

PInstpS, C p , mq " IKind S pe p q m é S " S 2 with S 2 " S 1 " S SpC 1 ' t 1 , . . . , C p ' t p , . . .q " inherit S 1 pe 1 , . . . , e p , . . .q Γ S pS 1 q " pC 1 1 ' t The following functions GenRepType and GenPrmMeth serve to instantiate the λ-liftings induced by the representations of parameters and the methods, according to the parameters' instantiations (by other parameters, toplevel collection, or expression for entity parameters). The effective definition of the record field me as carrier is provided by the forthcoming definition 7.14.

GenRepTypepikq

Method Code Generation

In order to help the intuitive understanding of the relations between the rules, we illustrate the shape of a generated code for a method in the following figure.

We consider the method lowMin of the example introduced in Section 2.3. In order to also illustrate decl-dependencies, we voluntarily use an unnecessary method dummy (a property simply stating @x, x " x) as a hint of a proof step as shown is the following listing.

Collection parameters Parameters

The function GenM ethGen is the entry point for generating the code of the method generator of a method m belonging to a species S. It relies on three intermediate functions (GenRepType, GenPrmMeth and GenSelfDeps).

The first two rules of GenM ethGen state that methods only declared or defined in an inherited species do not lead to code. Note that in the following rule [MG-METH], depending on the kind of method, the binder may change: Definition for a computational method, Theorem for a theorem (not written in the rule).

• Let S be a species in normal form.

ms i q " pC i , rGens t m u S,Ci q for all C i P ÝÝÑ C ' t, the list of couples recording each parameter C i and the list of dependencies of m on C i .

• Let insts " pPInstpS, C i , mq ˆms i q, the list of couples recording the instantiation of each parameter C i and the list of dependencies of m on C i . • Let C " GenRepTypepikq for all pik, msq P insts, the code operating the λliftings of parameters representations. • Let P " GenPrmMethpik, msq for all pik, msq P insts, the code operating the λ-liftings of parameters methods. • Let S " GenSelfDeps S pt Ý Ñ Φ u\mq, the code operating the λ-liftings or bindings for decl-or def-dependencies on other methods of the species S.