APPROCHE UNIFORME DE LA SEMANTIQUE DE FITTING ET DE LA SEMANTIQUE BIEN FONDEE : APPLICATION A LA VALIDATION DE PROGRAMMES LOGIQUES

LES METHODES DE VALIDATION ONT POUR BUT DE COMPARER DES PROPRIETES DE FAIT DU PROGRAMME AVEC DES PROPRIETES ATTENDUES QUI REFLETENT LES INTENTIONS DU PROGRAMMEUR. CES PROPRIETES ETANT EXPRIMEES SOUS FORME D'ENSEMBLES DE LITTERAUX CLOS, NOUS CONSIDERONS DEUX IMPORTANTES SEMANTIQUES DECLARATIVES:...

Descrizione completa

Salvato in:
Dettagli Bibliografici
Autore principale: Malfon, Bernard, 19..-
Altri autori: Ferrand, G. (Relatore della tesi)
Natura: Thèse et Mémoire papier
Lingua:Français
Pubblicazione: [S.l.] : [s.n.] 1995.
Soggetti:
Nota: 1995ORLE2020
Autres localisations: Voir dans le Sudoc
Variante du titre:UNIFORM APPROACH TO FITTING AND WELL-FOUNDED SEMANTICS. APPLICATION TO LOGIC PROGRAM VALIDATION
Descrizione
Riassunto:LES METHODES DE VALIDATION ONT POUR BUT DE COMPARER DES PROPRIETES DE FAIT DU PROGRAMME AVEC DES PROPRIETES ATTENDUES QUI REFLETENT LES INTENTIONS DU PROGRAMMEUR. CES PROPRIETES ETANT EXPRIMEES SOUS FORME D'ENSEMBLES DE LITTERAUX CLOS, NOUS CONSIDERONS DEUX IMPORTANTES SEMANTIQUES DECLARATIVES: LE MODELE DE FITTING ET LE MODELE BIEN FONDE. APRES AVOIR PRESENTE DE MANIERE UNIFORME CES SEMANTIQUES, NOUS EXPOSONS LES METHODES DE PREUVE DE CORRECTION PARTIELLE DE FERRAND ET DERANSART, QUI UTILISENT LES CARACTERISATIONS DE CES SEMANTIQUES COMME POINTS FIXES D'OPERATEURS CROISSANTS. NOUS DONNONS UNE AUTRE CARACTERISATION DE CES SEMANTIQUES A L'AIDE DE FONCTIONS DE NIVEAU, C'EST-A-DIRE A VALEURS DANS UN ENSEMBLE MUNI D'UN ORDRE BIEN FONDE, CE QUI OUVRE LA VOIE A DES METHODES POUR PROUVER LA COMPLETUDE. CES METHODES PERMETTENT DE CONSTRUIRE DES PREUVES DE FACON MODULAIRE. DANS LE BUT D'OBTENIR DES METHODES DE PREUVE PLUS SIMPLES, NOUS CARACTERISONS LES CLASSES DE PROGRAMMES POUR LESQUELS LES DEUX SEMANTIQUES COINCIDENT, OU L'UNE D'ELLES EST TOTALE. NOUS ETUDIONS DEUX APPLICATIONS DE CES METHODES DE VALIDATION: D'UNE PART, LA GENERALISATION ET L'EXTENSION AUX PROGRAMMES AVEC NEGATION DES RESULTATS DE NAISH CONCERNANT LES PROGRAMMES CORRECTEMENT TYPES ; D'AUTRE PART, POUR LE DIAGNOSTIC DECLARATIF D'ERREUR, LA DEFINITION D'UNE NOUVELLE NOTION D'ERREUR ADAPTEE AU MODELE BIEN FONDE
Descrizione del documento:1995ORLE2020
Descrizione fisica:120 P.
Bibliografia:66 REF.