DETERMINATION STATIQUE DES TYPES POUR LE LANGAGE SET1 / CATHERINE DUBOIS BOCQUET ; SOUS LA DIRECTION DE VERONIQUE DONZEAU-GOUGE

Date : 1989

Editeur / Publisher : [S.l.] : [s.n.] , 1989

Type : Livre / Book

Langue / Language : français / French

Donzeau-Gouge Viguié, Véronique (Directeur de thèse / thesis advisor)

Conservatoire national des arts et métiers (France ; 1794-....) (Organisme de soutenance / degree-grantor)

Relation : DETERMINATION STATIQUE DES TYPES POUR LE LANGAGE SET1 / Catherine Dubois Bocquet ; sous la direction de Veronique Donzeau-Gouge / Grenoble : Atelier national de reproduction des thèses , 1989

Résumé / Abstract : LE LANGAGE SET1, FORMALISME FONDE SUR LA THEORIE DES ENSEMBLES, EST SOUVENT UTILISE COMME OUTIL DE PROTOTYPAGE. EN EFFET, IL OFFRE LA POSSIBILITE DE MANIPULER DES OBJETS COMPLEXES TELS QUE LES ENSEMBLES, LES SEQUENCES ET LES RELATIONS (LE TERME UTILISE EST MAP), DE LEUR APPLIQUER DES PRIMITIVES DE HAUT NIVEAU (LES QUANTIFICATEURS PAR EXEMPLE). D'AUTRE PART, OUTRE UNE FLEXIBILITE SYNTAXIQUE IMPORTANTE, IL PRESENTE UNE GRANDE FLEXIBILITE SEMANTIQUE: CERTAINS SYMBOLES D'OPERATEURS DENOTENT PLUS D'UNE OPERATION, UNE MEME VARIABLE PEUT RECEVOIR DES VALEURS DE DIFFERENTS TYPES TOUT AU LONG DU PROGRAMME, AUCUNE DECLARATION N'EST OBLIGATOIRE. COMPTE TENU DE CES CARACTERISTIQUES, DETERMINER STATIQUEMENT LES TYPES DES OBJETS QUE VONT RECEVOIR DYNAMIQUEMENT LES VARIABLES D'UN PROGRAMME SET1 EST UN PROBLEME CLASSIQUE DE FLOTS DE DONNEES, NECESSITANT ANALYSES AVANT ET ARRIERE. DANS LE CADRE DU PROJET ESPRIT SED, NOUS AVONS REALISE UN OUTIL D'INFERENCE DES TYPES POUR SET1, ECRIT AVEC LE LANGAGE TYPOL, FORMALISME DE SPECIFICATION SEMANTIQUE DU SYSTEME MENTOR. IL EST COMPOSE D'UN ENSEMBLE DE REGLES D'INFERENCE QUI AXIOMATISENT LA RELATION EST BIEN TYPE ENTRE ARBRES DE SYNTAXE ABSTRAITE ET TYPES. LA METHODE QUE NOUS UTILISONS NE NECESSITE QU'UN SEUL PARCOURS DE L'ARBRE ASSOCIE A UN PROGRAMME: LE MECANISME DE L'UNIFICATION SOUS-JACENT AU LANGAGE TYPOL ASSURE LA PROPAGATION ARRIERE DES INFORMATIONS. ENFIN, POUR FAIRE FACE AUX PROBLEMES POSES PAR LA SURCHARGE DES OPERATEURS, NOUS GENERONS DES EQUATIONS (APPELEES CONTRAINTES) QUI NE SONT RESOLUES QUE LORSQUE L'INFORMATION MINIMALE NECESSAIRE A SA RESOLUTION EST DETENUE DE MANIERE SURE. LE CALCUL DES TYPES DES VARIABLES D'UN PROGRAMME APPARAIT COMME UNE INTERPRETATION ABSTRAITE DE CE PROGRAMME: UN MODELE DE TYPE SIMPLE EST CONSIDERE MAIS D'AUTRES MODELES SONT ENVISAGES DANS CETTE ETUDE. NOUS MONTRONS EGALEMENT COMMENT NOTRE SYSTEME PEUT ETRE ETENDU POUR DETEC