Note :
Il n'y a actuellement aucun avis de lecteur. La note est basée sur 2 votes.
Theories of Programming: The Life and Works of Tony Hoare
Sir Tony Hoare a eu une influence considérable sur l'informatique, de l'algorithme Quicksort à la science du développement de logiciels, en passant par la concurrence et la vérification de programmes. Ses contributions ont été largement reconnues : il a reçu le prix Turing de l'ACM en 1980, le prix Kyoto de la Fondation Inamori en 2000, et a été fait chevalier pour "services rendus à l'éducation et à l'informatique" par la reine Élisabeth II d'Angleterre en 2000.
Ce livre présente l'essence de ses différents travaux - la recherche d'abstractions efficaces - à la fois dans ses propres mots et dans des chapitres écrits par des experts de premier plan dans le domaine, y compris un grand nombre de ses collaborateurs de recherche. En outre, ce volume contient des éléments biographiques, sa conférence pour le prix Turing, la transcription d'une interview et certains de ses articles fondamentaux.
L'article fondateur de Hoare intitulé "An Axiomatic Basis for Computer Programming" (Une base axiomatique pour la programmation informatique) présentait son approche, communément appelée "logique de Hoare", pour prouver l'exactitude des programmes à l'aide d'assertions logiques. La logique de Hoare et les développements ultérieurs ont constitué la base d'une grande variété d'efforts de vérification de logiciels. Tony Hoare a joué un rôle déterminant dans la proposition de la Verified Software Initiative, un projet international coopératif visant à relever les défis scientifiques de la vérification des logiciels à grande échelle, qui englobe les théories, les outils et les expériences.
Les contributions de Tony Hoare à la théorie et à la pratique des systèmes logiciels concurrents sont tout aussi impressionnantes. L'algèbre de processus appelée Processus Séquentiels Communicants (CSP) a été l'un des paradigmes fondamentaux, à la fois comme théorie mathématique pour raisonner sur l'informatique concurrente et comme base pour le langage de programmation occam. Le CSP a servi de cadre à l'exploration de plusieurs idées de sémantique dénotationnelle, telles que les domaines de puissance, ainsi que les notions d'abstraction et de raffinement. Il est à la base d'une série d'outils industriels qui ont été utilisés dans un large éventail d'applications.
Ce livre présente également les travaux de Hoare au cours des dernières décennies. Ces travaux comprennent une approche rigoureuse des spécifications dans la pratique du génie logiciel, y compris les abstractions de procédures et de données, le raffinement des données et une théorie modulaire des conceptions. Plus récemment, il a travaillé avec des collaborateurs pour développer des théories unificatrices de la programmation (UTP). Leur objectif est d'identifier les théories algébriques communes qui sont au cœur des calculs séquentiels, concurrents, réactifs et cyber-physiques.
© Book1 Group - tous droits réservés.
Le contenu de ce site ne peut être copié ou utilisé, en tout ou en partie, sans l'autorisation écrite du propriétaire.
Dernière modification: 2024.11.14 07:32 (GMT)