Contribution à la réalisation d'une spécification formelle pour PROLOG / Gilles Richard

Auteur: Richard, Gilles (1956-) - AuteurAuteur secondaire : Lorho, Bernard (1944-) - Directeur de thèseCollectivité secondaire: Université d'Orléans - Etablissement de soutenanceType de document: ThèseLangue: françaisPays: FranceÉditeur: [S.l.] : [s.n.], 1989Description: 1 vol. (201 p.) ; 30 cm ISBN: 2726105971 ; br. Résumé: Au debut des annees 80, un grand nombre de versions du langage prolog cohabitaient, differenciees par leur syntaxe, les predicats predefinis et aussi leur semantique operationnelle. L'afnor (association francaise pour la normalisation) et la bsi (british standards institution) deciderent en 1984 de definir un prolog standard; l'iso (international standard organisation) officialisa ce projet en 1987 en creant un groupe de travail. Dans ce cadre precis, notre objectif etait de donner une definition formelle de la semantique operationnelle de prolog, en utilisant comme langage de specification les clauses de horn augmentees de la negation. L'interet d'une telle approche est: la specification, decrivant un arbre de recherche generalise, est bien comprise dans la communaute prolog et satisfait bon nombre des criteres imposes a ce type de realisation (minimalite, extensibilite, etc. . . ); nous pouvons partiellement des proprietes de correction et completude, assurant d'une certaine maniere la consistance de la definition. Un des obstacles a la realisation des preuves completes est la taille de la specification manipulee; nous derivons simplement une specification executable, outil de test de la validite de la version formelle; un inconvenient est, qu'il est difficile de faire des preuves de proprietes de programmes en l'absence d'outils formels de manipulation des arbres de recherche. Actuellement integree dans le document de travail iso (iso/iec jtc1 sc22 wg17 n28 february 1989), la specification formelle semble en bonne voie pour figurer dans le document final definissant prolog standard.Bibliographie: Bibliogr. p. 200-202.Thèse: Thèse de doctorat en informatique, soutenue en 1989, organisme : université d'Orléans Sujets MSC: 68N17 Computer science -- Software -- Logic programming
68N15 Computer science -- Software -- Programming languages
68Q60 Computer science -- Theory of computing -- Specification and verification (program logics, model checking, etc.)
68Q55 Computer science -- Theory of computing -- Semantics
97A70 Mathematics education - General, mathematics and education -- Theses and postdoctoral theses
Location Call Number Status Date Due
Salle S 09886-01 / Thèses RIC (Browse Shelf) Available

Bibliogr. p. 200-202

Thèse de doctorat informatique 1989 université d'Orléans

Au debut des annees 80, un grand nombre de versions du langage prolog cohabitaient, differenciees par leur syntaxe, les predicats predefinis et aussi leur semantique operationnelle. L'afnor (association francaise pour la normalisation) et la bsi (british standards institution) deciderent en 1984 de definir un prolog standard; l'iso (international standard organisation) officialisa ce projet en 1987 en creant un groupe de travail. Dans ce cadre precis, notre objectif etait de donner une definition formelle de la semantique operationnelle de prolog, en utilisant comme langage de specification les clauses de horn augmentees de la negation. L'interet d'une telle approche est: la specification, decrivant un arbre de recherche generalise, est bien comprise dans la communaute prolog et satisfait bon nombre des criteres imposes a ce type de realisation (minimalite, extensibilite, etc. . . ); nous pouvons partiellement des proprietes de correction et completude, assurant d'une certaine maniere la consistance de la definition. Un des obstacles a la realisation des preuves completes est la taille de la specification manipulee; nous derivons simplement une specification executable, outil de test de la validite de la version formelle; un inconvenient est, qu'il est difficile de faire des preuves de proprietes de programmes en l'absence d'outils formels de manipulation des arbres de recherche. Actuellement integree dans le document de travail iso (iso/iec jtc1 sc22 wg17 n28 february 1989), la specification formelle semble en bonne voie pour figurer dans le document final definissant prolog standard

There are no comments for this item.

Log in to your account to post a comment.
Languages: English | Français | |