|
| Titre : |
The formal semantics of programming languages : An introduction |
| Type de document : |
texte imprimé |
| Auteurs : |
G. Winskel |
| Editeur : |
Cambridge, Mass : MIT Press |
| Année de publication : |
1993 |
| Importance : |
xviii, 361 p |
| Format : |
24 cm |
| ISBN/ISSN/EAN : |
978-0-262-23169-5 |
| Catégories : |
Informatique
|
| Mots-clés : |
Langages de programmation : Sémantique
Méthodes formelles (informatique) |
| Index. décimale : |
005.13 Langages de programmation (codage des programmes, éditeurs de texte conçus spécialement pour le codage des programmes, générateurs d'application ; langages déclaratifs, non procéduraux) |
| Résumé : |
La sémantique formelle des langages de programmation fournit les techniques mathématiques de base nécessaires pour ceux qui commencent une étude de la sémantique et des logiques des langages de programmation. Ces techniques permettront aux élèves d'inventer, de formaliser et de justifier des règles permettant de raisonner sur une variété de langages de programmation. Bien que le traitement soit élémentaire, plusieurs des sujets abordés proviennent de recherches récentes, y compris le domaine vital de la simultanéité. Le livre contient de nombreux exercices allant du simple au miniprojet.
À partir de la théorie des ensembles de base, la sémantique opérationnelle structurelle est présentée comme un moyen de définir la signification des langages de programmation ainsi que les techniques de preuve associées. la sémantique dénotationnelle et axiomatiques sont illustrés sur un langage simple while-programmes, et à l'automne preuves sont données de l'équivalence de la sémantique opérationnelle et denotational et la solidité et l'exhaustivité relative de la sémantique axiomatique. Une preuve du théorème d'incomplétude de Gödel, qui souligne l'impossibilité d'obtenir une sémantique axiomatique complète, est incluse. Il est soutenu par une annexe fournissant une introduction à la théorie de la calculabilité basée sur while-programs.
Après une présentation de la théorie des domaines, la sémantique et les méthodes de preuve de plusieurs langages fonctionnels sont évaluées. Le langage le plus simple est celui des équations de récursion avec évaluation à la fois appel par valeur et appel par nom. Ce travail est étendu aux langues avec des types plus élevés et récursifs, y compris un traitement des lambda-calculi désireux et paresseux. Tout au long de la relation entre la sémantique dénotationnelle et opérationnel est souligné et les preuves de thecorrespondence entre l'opération et la sémantique dénotationnelle sont fournis. Le traitement des types récursifs - l'une des parties les plus avancées du livre - repose sur l'utilisation de systèmes d'information pour représenter les domaines. Le livre se termine par un chapitre sur les langages de programmation parallèles, accompagné d'une discussion sur les méthodes de spécification et de vérification des programmes non déterministes et parallèles. |
| Note de contenu : |
Sommaire :
1. Basic set theory
2. Introduction to operational semantics
3. Some principles of induction
4. Inductive definitions
5. The denotational semantics of IMP
6. The axiomatic semantics of IMP
7. Completeness of the Hoare rules
8. Introduction to domain theory
9. Recursion equations
10. Techniques for recursion
11. Languages with higher types
12. Information systems
13. Recursive types
14. Nondeterminism and parallelism
Appendix A. Incompleteness and undecidability
|
| Côte titre : |
Fs/19752 |
The formal semantics of programming languages : An introduction [texte imprimé] / G. Winskel . - Cambridge, Mass : MIT Press, 1993 . - xviii, 361 p ; 24 cm. ISBN : 978-0-262-23169-5
| Catégories : |
Informatique
|
| Mots-clés : |
Langages de programmation : Sémantique
Méthodes formelles (informatique) |
| Index. décimale : |
005.13 Langages de programmation (codage des programmes, éditeurs de texte conçus spécialement pour le codage des programmes, générateurs d'application ; langages déclaratifs, non procéduraux) |
| Résumé : |
La sémantique formelle des langages de programmation fournit les techniques mathématiques de base nécessaires pour ceux qui commencent une étude de la sémantique et des logiques des langages de programmation. Ces techniques permettront aux élèves d'inventer, de formaliser et de justifier des règles permettant de raisonner sur une variété de langages de programmation. Bien que le traitement soit élémentaire, plusieurs des sujets abordés proviennent de recherches récentes, y compris le domaine vital de la simultanéité. Le livre contient de nombreux exercices allant du simple au miniprojet.
À partir de la théorie des ensembles de base, la sémantique opérationnelle structurelle est présentée comme un moyen de définir la signification des langages de programmation ainsi que les techniques de preuve associées. la sémantique dénotationnelle et axiomatiques sont illustrés sur un langage simple while-programmes, et à l'automne preuves sont données de l'équivalence de la sémantique opérationnelle et denotational et la solidité et l'exhaustivité relative de la sémantique axiomatique. Une preuve du théorème d'incomplétude de Gödel, qui souligne l'impossibilité d'obtenir une sémantique axiomatique complète, est incluse. Il est soutenu par une annexe fournissant une introduction à la théorie de la calculabilité basée sur while-programs.
Après une présentation de la théorie des domaines, la sémantique et les méthodes de preuve de plusieurs langages fonctionnels sont évaluées. Le langage le plus simple est celui des équations de récursion avec évaluation à la fois appel par valeur et appel par nom. Ce travail est étendu aux langues avec des types plus élevés et récursifs, y compris un traitement des lambda-calculi désireux et paresseux. Tout au long de la relation entre la sémantique dénotationnelle et opérationnel est souligné et les preuves de thecorrespondence entre l'opération et la sémantique dénotationnelle sont fournis. Le traitement des types récursifs - l'une des parties les plus avancées du livre - repose sur l'utilisation de systèmes d'information pour représenter les domaines. Le livre se termine par un chapitre sur les langages de programmation parallèles, accompagné d'une discussion sur les méthodes de spécification et de vérification des programmes non déterministes et parallèles. |
| Note de contenu : |
Sommaire :
1. Basic set theory
2. Introduction to operational semantics
3. Some principles of induction
4. Inductive definitions
5. The denotational semantics of IMP
6. The axiomatic semantics of IMP
7. Completeness of the Hoare rules
8. Introduction to domain theory
9. Recursion equations
10. Techniques for recursion
11. Languages with higher types
12. Information systems
13. Recursive types
14. Nondeterminism and parallelism
Appendix A. Incompleteness and undecidability
|
| Côte titre : |
Fs/19752 |
|  |
Ajouter le résultat dans votre panier Affiner la recherche
