Comprendre les méthodes formelles : panorama et outils logiques / Jean-François, Monin ; Gérard, Huet (préface de) [ Livre]
Langue: Français ; de l'oeuvre originale, Français.Publication : Paris, Milan, Barcelone : Masson, 1996Description : XVII-306 pages ; 24 cmISBN: 2225853045.Collection: Collection technique et scientifique des télécommunications, 0221-2579Classification: 004.16 Logique mathématiqueRésumé: Sommaire I. MOTIVATIONS 1. Quelques applications industrielles 2. Qu'appelle-t-on méthode formelle? 3. Du génie logiciel aux approches formelles 4. Quelques bémols...et bécarres 5. But de cet ouvrage 6. Plan de l'ouvrage et guide de lecture 7. Notes bibliographiques II. EXERCICE INTRODUCTIF 1. Enoncé 2. Ebauche de spécification formelle 3. Ya-t-il une solution au problème posé? 4. Développement de programme 5. Bilan 6. Sémantique des langages 7. Notes bibliographiques III. PRESENTATION DES OUTILS LOGIQUES 1. Quelques applications de la logique 2. Les antécédents 3. Les branches de la logique 4. Rappels mathématiques 5. Relations bien fondées et ordinaux 6. Compléments sur la calculabilité 7. Notes bibliographiques IV. QUELQUES METHODES FORMELLES 1. Logique de Hoare 2. Langages ensemblistes 3. Spécification algébrique 4. Spécification en logique typée d'ordre supérieur 5. Spécification de systèmes communicants 6. Notes bibliographiques V. LOGIQUE CLASSIQUE 1. Logique des propositions 2. Logique des prédicats du premier ordre 3. Exemples importants 4. Fonctions totales, logiques multi-sortées 5. Logiques d'ordre 2 et d'ordre supérieur 6. Théorie des modèles 7. Notes bibliographiques VI. SYSTEMES DE DEDUCTION 1. Systèmes hilbertiens 2. La déduction naturelle 3. Le calcul des séquents 4. Applications à la démonstration automatique 5. Au-delà du premier ordre 6. Le système de Dijkstra-Scholten 7. Un mot sur la réécriture 8. Résultats de complétude et de décidabilité 9. Notes bibliographiques VII. THEORIE DES ENSEMBLES 1. Caractéristiques générales 2. Le système de Zermelo-Fraenkel 3. Récurrence, imprédicativité 4. Ensembles, types abstraits et polymorphisme 5. Propriétés de ZF et ZFC 6. Bilan 7. Notes bibliographiques VIII. SYSTEMES DE TYPES ET LOGIQUES CONSTRUCTIVES 1. Utilisations du typage 2. Différentes notions de type 3. Le lambda-calcul 4. Logique intuitionniste et typage simple 5. Puissance expressive du -calcul simplement typé 6. Typage au second ordre : le système F 7. Types dépendants 8. Le calcul des constructions inductives 9. Vers la logique linéaire 10. Notes bibliographiques.Sujet - Nom commun: Logique symbolique et mathématique | Logiciels -- Développement | Langages formels | Génie logiciel | Ensembles, Théorie des | Calcul formel -- Informatique| Current location | Call number | Status | Notes | Date due | Barcode |
|---|---|---|---|---|---|
| ENS Rennes - Bibliothèque Informatique | 004.16 MON (Browse shelf) | Available | 004.16 Logique mathématique | 00001804 |
Bibliogr. p. 281-292. Index
Sommaire
I. MOTIVATIONS
1. Quelques applications industrielles
2. Qu'appelle-t-on méthode formelle?
3. Du génie logiciel aux approches formelles
4. Quelques bémols...et bécarres
5. But de cet ouvrage
6. Plan de l'ouvrage et guide de lecture
7. Notes bibliographiques
II. EXERCICE INTRODUCTIF
1. Enoncé
2. Ebauche de spécification formelle
3. Ya-t-il une solution au problème posé?
4. Développement de programme
5. Bilan
6. Sémantique des langages
7. Notes bibliographiques
III. PRESENTATION DES OUTILS LOGIQUES
1. Quelques applications de la logique
2. Les antécédents
3. Les branches de la logique
4. Rappels mathématiques
5. Relations bien fondées et ordinaux
6. Compléments sur la calculabilité
7. Notes bibliographiques
IV. QUELQUES METHODES FORMELLES
1. Logique de Hoare
2. Langages ensemblistes
3. Spécification algébrique
4. Spécification en logique typée d'ordre supérieur
5. Spécification de systèmes communicants
6. Notes bibliographiques
V. LOGIQUE CLASSIQUE
1. Logique des propositions
2. Logique des prédicats du premier ordre
3. Exemples importants
4. Fonctions totales, logiques multi-sortées
5. Logiques d'ordre 2 et d'ordre supérieur
6. Théorie des modèles
7. Notes bibliographiques
VI. SYSTEMES DE DEDUCTION
1. Systèmes hilbertiens
2. La déduction naturelle
3. Le calcul des séquents
4. Applications à la démonstration automatique
5. Au-delà du premier ordre
6. Le système de Dijkstra-Scholten
7. Un mot sur la réécriture
8. Résultats de complétude et de décidabilité
9. Notes bibliographiques
VII. THEORIE DES ENSEMBLES
1. Caractéristiques générales
2. Le système de Zermelo-Fraenkel
3. Récurrence, imprédicativité
4. Ensembles, types abstraits et polymorphisme
5. Propriétés de ZF et ZFC
6. Bilan
7. Notes bibliographiques
VIII. SYSTEMES DE TYPES ET LOGIQUES CONSTRUCTIVES
1. Utilisations du typage
2. Différentes notions de type
3. Le lambda-calcul
4. Logique intuitionniste et typage simple
5. Puissance expressive du -calcul simplement typé
6. Typage au second ordre : le système F
7. Types dépendants
8. Le calcul des constructions inductives
9. Vers la logique linéaire
10. Notes bibliographiques