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:...
Saved in:
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thèse et Mémoire papier |
| Language: | Français |
| Published: |
[S.l.] :
[s.n.]
1995.
|
| Subjects: | |
| Note: |
1995ORLE2020 |
| Autres localisations: | Voir dans le Sudoc |
| Variante du titre: | UNIFORM APPROACH TO FITTING AND WELL-FOUNDED SEMANTICS. APPLICATION TO LOGIC PROGRAM VALIDATION |
| LEADER | 02595nam a22002657a 4500 | ||
|---|---|---|---|
| 001 | 197140 | ||
| 008 | 990313s1995 xxe ||| |||| 00| 0 fre d | ||
| 009 | PPN043999948 | ||
| 041 | 0 | |a fre |b fre | |
| 084 | |a 001.D.02.A.07_001.D.02.B.09_001.D.02.C.02 | ||
| 084 | |a 620 | ||
| 100 | 1 | |a Malfon, Bernard, |d 19..- . | |
| 240 | 1 | 0 | |a UNIFORM APPROACH TO FITTING AND WELL-FOUNDED SEMANTICS. APPLICATION TO LOGIC PROGRAM VALIDATION |
| 245 | 1 | 0 | |a APPROCHE UNIFORME DE LA SEMANTIQUE DE FITTING ET DE LA SEMANTIQUE BIEN FONDEE : |b APPLICATION A LA VALIDATION DE PROGRAMMES LOGIQUES |c BERNARD MALFON ; SOUS LA DIRECTION DE G. FERRAND. |
| 260 | |a [S.l.] : |b [s.n.], |c 1995. | ||
| 300 | |a 120 P. | ||
| 500 | |a 1995ORLE2020 | ||
| 502 | |a Thèse de doctorat. Sciences appliquées. Orléans. 1995 | ||
| 504 | |a 66 REF. | ||
| 520 | |a 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 | ||
| 650 | |a Thèses et écrits académiques | ||
| 700 | 1 | |a Ferrand, G. |4 ths | |
| 710 | 2 | |a Université d'Orléans. |4 dgg | |
| 997 | |0 197140 |1 Thèse et Mémoire papier |a Ressource papier |c 0/Orléans/ |c 1/Orléans/BU Sciences, Technologies, STAPS/ |z Orléans, BU Sciences, Technologies, STAPS, TS 19-1995-20 |z Orléans, BU Sciences, Technologies, STAPS, TS 19-1995-20b | ||
| 999 | |5 452342104:052173909 |a ORLEANS | ||