Tutorial FoC

Tutorial FoC

Documents
38 pages
Lire
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres

Description

A brief FoC tutorialVersion 0.0July, 01, 2003The FoC development teamConservatoire National des Arts et Metiers (CNAM)Institut National de Recherche en Informatique etAutomatique (INRIA)Laboratoire d’Informatique de Paris 6 (LIP6)AbstractIn this tutorial, we show through sample examples the main constructions of FoC.The rst part of this tutorial is a general description of FoC together with a FoCdevelopment of cartesian products of monoids (a set with an associative operationfor which there is a neutral element). In this part, we omit some properties. Thesecond part focuses on proof and explained how to make proof in Coq from a FoCdevelopment. Last, the third part shows how programming within FoC.1Contents1 First steps within FoC 61.1 Starting with FoC: Setoids . . . . . . . . . . . . . . . . . . . . . . . . . . . 61.2 Inheritance: Monoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81.3 Parameterized species: Cartesian product of setoids . . . . . . . . . . . . . 91.4 Multiple inheritance: product of monoids . . . . . . . . . . . . . . 101.5 Collection: Implementation ofZ andZZ . . . . . . . . . . . . . . . . . . 101.6 Compilation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111.6.1 Steps of compilation . . . . . . . . . . . . . . . . . . . . . . . . . . . 111.6.2 Interface of species . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121.6.3 Inheritance graph . . . . . . . . . . . . . . . . . ...

Sujets

Informations

Publié par
Nombre de visites sur la page 30
Langue English

Informations légales : prix de location à la page  €. Cette information est donnée uniquement à titre indicatif conformément à la législation en vigueur.

Signaler un problème
A brief FoC tutorial Version 0.0 July, 01, 2003
The FoC development team
ConservatoireNationaldesArtsetMe´tiers(CNAM) Institut National de Recherche en Informatique et Automatique (INRIA) Laboratoire d’Informatique de Paris 6 (LIP6)
Abstract In this tutorial, we show through sample examples the main constructions ofFoC. The first part of this tutorial is a general description ofFoCtogether with aFoC development of cartesian products of monoids (a set with an associative operation for which there is a neutral element). In this part, we omit some properties. The second part focuses on proof and explained how to make proof inCoqfrom aFoC development. Last, the third part shows how programming withinFoC.
1
Contents 1 First steps within FoC 6 1.1 Starting withFoC . . . . . . . . . . . . . . . . . . . . . . . . . . . 6: Setoids 1.2 Inheritance: Monoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 1.3 Parameterized species: Cartesian product of setoids . . . . . . . . . . . . . 9 1.4 Multiple inheritance: Cartesian product of monoids . . . . . . . . . . . . . . 10 1.5 Collection: Implementation ofZandZ×Z 10. . . . . . . . . . . . . . .. . . 1.6 Compilation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 1.6.1 Steps of compilation . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 1.6.2 Interface of species . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 1.6.3 Inheritance graph . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 1.6.4 Dependencies graph . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 1.7 More on dependencies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2 Proving properties: from FoC specifications to Coq specifications 17 2.1 Setoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.1.1 Defining a type for setoids . . . . . . . . . . . . . . . . . . . . . . . . 17 2.1.2 Methods of the species of setoids . . . . . . . . . . . . . . . . . . . . 19 2.1.3 Making a setoid . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 2.1.4 Coercion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 2.2 Monoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 2.3 Cartesian product of setoids . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2.4 Redefinitions: a little help from theFoC 29. . . . . . . . . . . . . compiler . 3 Programming 30 3.1 Defining data types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 3.2 Defining species and collections . . . . . . . . . . . . . . . . . . . . . . . . . 30 3.3 Recursive types and Pattern-matchings . . . . . . . . . . . . . . . . . . . . . 35 3.4 UsingOcamlcode inFoC. . . . . . . . . . . . . . . . . . . . .. . . . . .  36 2
Introduction The aim of theFoCproject is to build an environment dedicated to the development of certified computer algebra libraries. TheFoCenvironment provides a completely formal-ized representation of the relations between mathematical structures, which will serve as a common framework for both proofs and implementations. TheFoCsyntax allows the user to write programs, statements and proofs. Computer algebra libraries are based on a hierarchy of implementations of mathemat-ical structures. In mathematics, algebraic structures are defined according to a rather strict hierarchy: rings come up after groups, which rely themselves on monoids, and so on. In theFoCsystem, we represent these structures byspecieswhich are made of some func-tions, either abstract or defined by appropriate algorithms, as well as properties (some of them are abstract statements to be proved later, while other already have a proof). Going from a species to another along the hierarchy as a lot to do with the notion of inheritance in Object-Oriented Programming and with refinement-based software development. A species can be built from existing species through inheritance and refinement mechanisms provided by theFoCsystem1an informal point of view, the. From FoC’ ground concepts are the following ones: EntitiesEntities are the “things” we manipulate. They represent mathematical objects, such as 0,1 orX2+ 3XYin the computer universe. At this level, the main problem is that there is no simple relationship between these two worlds. For instance, the constant1 of theintegertype can be used to represent 12ZZas well as 15ZZ. Of course, it would be a mistake to mix them up, since they do not have the same properties at all. On the other hand, we have a lot of possible representations for the polynomialX it can be+ 2: viewed as an ordered list of coefficients,[1;2], or as a list of pairs (sparse representation): [(1,1);(2,0)] this case, adding (or multiplying) two polynomials who don’t share the. In same concrete representation is likely to produce an error. To avoid such confusion, we use an Abstract Data Type (ADT) mechanism: entities are accessible to the end user only through appropriate functions. SpeciesSpecies play a very important role inFoCIndeed they are the nodes of the. hierarchy of structures upon which the library is based. They are the equivalent of the algebraic structures in mathematics. A species can be seen as a set ofmethods, which are identified by their names. A method can be eitherdeclaredordefined.Declared methods reflect the constants, primitive operations, and axioms that define a structure in mathematics, whiledefinedones represent implemented operations and theorems built up (and proved) from the declared methods in a given structure. There are several different categories of methods: The carrier, or representation type, introduced by the keywordrep, of a species is a type from theFoCit can be an atomic type, a other words, type language. In 1Note that combining these features may introduce some inconsistencies, invalidating some properties of the formal specifications or even leading to programming errors. Hence, theFoCsystem performs static analyses, which reject such problematic programs.
3
product, an arrow, or parameterized type (such aslist(int) represents the type). It of the entities that the species manipulates. Each speciesmusthave auniquecarrier. the “computational” methods which can be declared (as a signature) or defined (as a function). Such methods are introduced by the keywordsigwhen they are declared and by the keywordlet denote the operations that are Theywhen they are defined. allowed on carrier’s inhabitants. The “non-computational” methods can also be declared or defined. They allow the developer of a new species to specify the properties that further implementations of this species must meet. He may also prove some of these properties through theorems (for the current definitions of functions or properties). Declared methods introduced by the keywordpropertyexpress properties that must be satisfied. Hence, before the complete implementation of the species, one will have to prove them. Defined methods introduced by the keywordletpropcorrespond to definitions of (non necessary decidable) relations (or predicates). Defined methods introduced by the keywordtheoremexpress properties that are proved in the context of the species. In this case, the proof itself constitutes the definition. InheritanceThe general mechanism for defining a new species from previous one(s) is calledinheritance If two. Thenew species inherits all the methods of its parent(s). parents have methods that share the same name, their types must be unifiable. If both methods are defined, then we have to choose the definition that will be exported in the new species. Currently, we have chosen to follow the order of inheritance specified by the species’ developer2course, a species is free to define some methods that were . Of previously only declared or even didn’t exist. It can also declare a new method (but not redeclare an old one, since a method must have the same type all along the inheritance graph). At last, it may redefine some methods. For instance, a group inherits from monoid, and declares a new operation (for the opposite) with its axioms. InterfaceEach species defines aninterfacesimply the list of all the methods of the is : it species considered as declared. Interfaces correspond to the end-user point of view, who wants to know which functions he can use, and which properties these functions have, but doesn’t care about the details of the implementation. InFoC, eachspeciesmust have a correspondinginterfaceby abstracting all its defined fields. 2However, it is not always possible to choose some definitions from speciesAand others from species B, and some coherence checks must be done (that are not needed by the policy chosen yet). For instance, assume we have two speciesAandBthat both defines a recursive functionfand give a prooff endsthat f if we want to build a species that inherits both fromalways terminates. Then,AandB, it won’t be safe to take the definition offinA, and the prooff endsofB. Indeed, the resulting species will have a proof f endsthat does not correspond to the body off.
4
CollectionsAcollection means that every fieldis a completely defined species. This must be defined, and every parameter instantiated. In addition, a collection is “frozen”. Namely, it can not be used as a parent of a species in the inheritance graph. It represents a particular mathematical structure, such asZ, orZ[X]. Moreover, we can not access directly the entities belonging to a given collection. ParametersIn addition, we distinguish between “atomic” species and “parameterized” ones. There are two types of parameters: entities and collections. For instance, a species defining the matrices will take two integers (representing its dimensions) as parameters. This integers are entities of a certain type. For its coefficients, it will also take a collection as argument, which must have at least all the features specified by the interface ofring. Of course, it can be a richer structure, afieldfor instance. Programming within FoCThe current version of the language is tuned to a kind of functional programming style, in order to ease proofs of correctness. The main pro-gramming features are multiple inheritance, late binding and parameterisation, which are used to build species and an abstraction mechanism, used to build collections. However, programming withFoCleads to a new style of development. one starts by Typically, expressing the specification of the problem, by introducing some properties and some dec-larations. Then, the representation and definitions can be given, step by step. At last, proofs are done. Some pitfalls must be avoided. Sometimes, it is possible to express some facts either by abstract properties or more concretely, using defintions. As late bindings lead to redo proofs def-depending upon definitions, this a very good idea to express prop-erties as abstractly as possible. This leads to a better understanding on what are the properties coming from the specification and the ones which are dependent of the cho-sen representation. In the same spirit, it is sometimes possible to code an algorithm, by considering only some properties of the representation. A good example is Strassen algo-rithm, which computes the product of square matrices of dimension 2nby decomposing them into matrices of dimension 2n1. Thealgorithm may be written at the species level, the recursive call being done on matrices of dimension 2n1. Or it may be written at the representation level, the recursive call being done on arrays of dimension 2n1 last. This version does not fit withFoCas the mathematical structures are lost in recursivestyle calls. Such a coding cannot reap the benefits of compiler verification and almost forbids proofs.
5
1 First steps within FoC In this section, we present aFoCdevelopment of the productZ×Z development. This is obtained by defining: 1. setoids as non empty sets on which an equivalence relation is defined (equal) 2. monoids as setoids with a binary operation (mult) and a particular element (the neutral elementone) 3.Zas a monoid over the typeint. 4. cartesian product of two setoids (which is a setoid) 5. cartesian product of two monoids (which is a monoid) 6.Z×Z Such a development involves the main constructions ofFoC: nitionsofspeciesde)a..,.dsecllconddı¨otes(ı¨onom,s(sitnoZandZ×Z). declared and defined methods inheritance (monoids inherits from setoids) and multiple-inheritance (for the carte-sian product of monoids) parameterized species (for cartesian products) 1.1 Starting with FoC: Setoids The root of the considered hierarchy, developed in a filespecies general.foc, is the species basic objectwhose specification is contained in the filebasic.foc our specification. Hence, begins with the two following directives: usesbasics;; openbasics;; The first directive allows to use the definitions contained in the filebasics.foc files. This introduces basic functions over integers and booleans and the root of theFoChierarchy which is the speciesbasic object. By using this directive, in the filespecies general.foc, names of functions defined inbasics.fochas to be prefixed by the namebasics. Iffis a function defined in a filea file.focthen one can usefin a fileanother file.focafter the directiveuses a file;;by prefixingfas followsa file#f. The second directive (open) allows to avoid to prefix the names of functions defined in another files. However, in order to use this directive, each name has to be unique. For instance, if the filesfile1andfile2both contain the definition of a functionf, it won’t be possible to use the directiveopenwith these two files.
6
The first species which inherits of the root of theFoChierarchy corresponds to setoids. A setoid is a non-empty setEwith an equivalence relation overE(i.e., a reflexive, symetric and transitive relation) and is defined withinFoCas follows: speciessetoidinheritsbasic object= sigequalin self>self>bool;(** equal is decidable equality *) (** element returns some element of our non empty setoid *) sigelementin self; propertyequal reflexive:allxin self, !equal(x,x); propertyequal symetric:allx yin self, !equal(x,y)>!equal(y,x); propertyequal transitive:allx y zin self, !equal(x,y)>!equal(y,z)>!equal(x,z); letdifferent(x,y) =basics#not b(!equal(x,y)); theoremsame is not different:allx yin self, !equal(x,y)>not(!different(x,y)) proof: def:different; decl:equal; assumed; end The speciessetoidinherits of the root of the hierarchy, the speciesbasic object, containing three methods: the carrierrepand two toolsparseandprint carrier is. The only declared in the speciesbasic object(it will be instantiated later during inheritance between species). The functionparse, of type3string->self, is defined (i.e., implemented) as a function allowing to convert a string into an element of the collection, the function print Inperforms the inverse conversion.basic object, we provide a generic definition of both:parsealways fails, whileprintreturns the constant string"<abst>". It is up to the more refined species of the hierarchy to define more specialized versions. The speciessetoidintroduces its own methods: equalandelementare methods corresponding to some effective computations (from which executable code will be obtained). Here, they are only declared. Such methods are introduced by the keywordsig only know that they exist for each setoid: we but we don’t know how they will be implemented. The explicit definitions of these methods will be done later during inheritance.equalis the equivalence relation 3Recall that in theFoClanguage,selfdenotes the current collection andc!mdenotes the methodm of the collectionc(if the name of the collection is not specified then it isself).
7
over the setoid. Its type isobloself->self->clearly specifies that it is a binaryand relation between elements of the setoid. Furthermore, this relation is decidable since the type of the result ofequalisbool, and then, later, during the definition of this method, one will have to implement a total function of this type and to prove its termination. The methodelementin order to ensure that a setoid is ais declared non-empty set. The three methodsequal reflexive,equal symetricandequal transitiveare also abstract. However they don’t correspond to effective computations: they specify the properties making the relationequalan equivalence relation. Such methods are introduced by the keywordproperty. Here again, later, during the implementation of the species, one will have to define these methods by providing the proofs of these properties. In theFoClanguagealldenotes the universal quantifier. Furthermore, as we said,!equalis a shortcut toself!equaland then denotes the methodequal of each collection corresponding to an implementation of the speciessetoid. different methods are introduced by theis a “computational” defined method. Such keywordlet. Its body uses the_tion:not b global”is a function, basics#not bfunc “ defined in the filebasics.foc, corresponding to the negation operator over the type bool. Last, the methodsame is not differentis introduced by the keywordtheorem: it corresponds to a “non-computational” defined method4expressing a property, so its definition is a proof which is given after the keywordproof keyword. Thenot corresponds to the negation over propositions. First, before the proof, we have to express some dependencies between methods. There are two kinds of dependency. A decl-dependency, introduced inFoCby the keyworddecl, specifies a dependency upon methods viewed as declared methods. In this case, the proof will only depend on the types of these methods. In other words,Ais decl-dependent uponBif it suffices to know the type ofBto typeA def-dependency, introduced in. AFoCby the keyworkdef, specifies a dependency upon methods viewed as defined methods. In this case, the proof will depend both upon the types and the definitions of these methods. In other words,Ais def-dependent uponBif typingArequires to know both the type and the definition ofB our example, the proof depends upon the. In type and the definition ofdifferent– it is a def-dependency – while it only depends upon the type ofequal(it is not necessary to know howequalis implemented) – it is a decl-dependency. Now, the proof can be done: we write hereassumedto express that we don’t want to prove the property. Thus, this property will be viewed as an axiom. 1.2 Inheritance: Monoids We can now define monoids as setoids with a binary operation (mult) and a particular element (one) from which we can define the declared methodelementof the speciessetoid as the result ofmultapplied tooneandone. TheFoCspecification of monoids is defined 4even if we define it here from the “computational” methodsequalanddifferent
8
as follows: speciesmonoidinheritssetoid= sigmultin self>self>self; sigonein self; letelement= !mult(!one,!one); end Of course, the type of the defined methodelementin the speciesmonoidmust be compatible with (i.e., be the same as) the type ofelementin the speciessetoid. 1.3 Parameterized species: Cartesian product of setoids WithinFoCone can define a species parameterized by some collections. For,  example, we can define the species of cartesian products of two setoidsaandbas a setoid (thus this new species inherits of the speciessetoid) whose carrier is the product of the carrier ofaandband whose methods are defined as follows: speciessetoid product(aissetoid,bissetoid)inheritssetoid= rep=a*b; letequal(x,y) = #and b(a!equal(#first(x),#first(y)), b!equal(#scnd(x),#scnd(y))); proof ofequal reflexive=assumed; proof ofequal symetric=assumed; proof ofequal transitive=assumed; letmk sp(x,y)in self=#crp(x,y); letelement=self!mk sp(a!element,b!element); letprint=funx> #sc("(", #sc(a!print(#first(x)), #sc(" " , , #sc(b!print(#scnd(x)), ")")))); end In the definition of the methodrep,a*bdenotea!rep * b!rep functions. The#crp,#first and#scndare primitives which allow respectively to obtain a pair, to obtain the first component of a pair, and to obtain the second component of a pair. The methodequal 9
defines a relation between two pairs (x1, y1) and (x2, y2 that) in a standard way. Remark it is defined from the methodsequalofaandb. The methodmk spis introduced in order to be able to build an object “inself” from entities ofaandb5. Last, the methodelement is defined from the methodselementofaandb that we also define the method. Note print. 1.4 Multiple inheritance: Cartesian product of monoids Multiple inheritance is possible withinFoC. For example, we can define the cartesian product of two monoidsaandbas a species which inherits both from the speciesmonoid (since the cartesian product of two monoids is also a monoid) and from the species setoid product(a,b) we write the. HenceFoCspecification as follows: speciesmonoid products(aismonoid,bismonoid) inheritsmonoid,setoid product(a,b) = letone= !mk sp(a!one,b!one); letmult(x,y) =#crp(a!mult(#first(x),#first(y)), b!mult(#scnd(x),#scnd(y))); end Here, the speciesmonoid productsinherits of all the methods of its two parents. However, both of them have methods that have the same name: in this case, theFoCcompiler verifies that the types of these methods are unifiable. This is the case in our example. Furthermore, the two methods from whichmonoid productsinherits define the method element: theFoCcompiler solve such a “conflict” by choosing the definition of the last species (containing it) in the list of parent species. In our example, the definition of elementwill be obtained from the speciessetoid product. 1.5 Collection: Implementation ofZandZ×Z Now, we can introduce the collectionintegersimplementingZby defining the carrier as intand by defining the methods as basics operations overint order to give a definition. In 5Recall that outside of a species,selfis an abstract data type.
10
to all the methods, we also have to provide proofs of properties overequal. collectionintegersimplementsmonoid= rep=int; letone=1; letmult=basics#int mult; letequal=basics#base eq; letprint=basics#string of int; letparse=basics#int of string; proof ofequal reflexive=assumed; proof ofequal symetric=assumed; proof ofequal transitive=assumed; end Then, it suffices to implement the speciesmonoid productswithintegersas parameters to obtainZ×Z. collectionintegers2implementsmonoid products(integers,integers) = end Now, we can define entites of such collections as follows: letfive=integers!parse("5");; letfive 2=integers!mult(#five,#five);; letfoo=integers2!mk sp(#five,#five 2);; letfoo2=integers2!mult(#foo,#foo);; #print string(integers2!print(#foo2));; 1.6 Compilation 1.6.1 Steps of compilation Compilation of aFoCfile is obtained in several steps (in the directoryfocc): fromFoCtoOcamlandCoq [Example]$ focc ../lib/species_tutorial.foc compilation ofCoqsource [Example]$ coqc ../lib/species_tutorial.v compilation ofOcamlsource [Example]$ ocamlc ../lib/species_tutorial.mli [Example]$ ocamlc -c -w mv ../lib/species_tutorial.ml [Example]$ ocamlc -I ‘focc -where‘ openmath.cmo caml basics.cmo _ basics.cmo ../lib/species tutorial.ml _
Then, one can execute aFoC our example, we obtain:program. In [Example]$ a.out (25,625)
11