Bewertung:

Derzeit gibt es keine Leserbewertungen. Die Bewertung basiert auf 2 Stimmen.
Theories of Programming: The Life and Works of Tony Hoare
Sir Tony Hoare hatte einen enormen Einfluss auf die Informatik, vom Quicksort-Algorithmus bis hin zur Wissenschaft der Softwareentwicklung, Nebenläufigkeit und Programmverifizierung. Seine Beiträge wurden weithin anerkannt: 1980 wurde er mit dem Turing Award der ACM ausgezeichnet, im Jahr 2000 erhielt er den Kyoto-Preis der Inamori-Stiftung, und im Jahr 2000 wurde er von der englischen Königin Elisabeth II. für seine "Verdienste um Bildung und Informatik" zum Ritter geschlagen.
Dieses Buch stellt die Essenz seiner verschiedenen Arbeiten - die Suche nach effektiven Abstraktionen - sowohl in seinen eigenen Worten als auch in Kapiteln vor, die von führenden Experten auf diesem Gebiet, darunter viele seiner Forschungsmitarbeiter, geschrieben wurden. Darüber hinaus enthält dieser Band biografisches Material, seine Turing-Preis-Vorlesung, die Mitschrift eines Interviews und einige seiner bahnbrechenden Arbeiten.
In seinem grundlegenden Werk "An Axiomatic Basis for Computer Programming" (Eine axiomatische Grundlage für die Computerprogrammierung) stellte Hoare seinen Ansatz vor, der allgemein als Hoare-Logik bekannt ist, um die Korrektheit von Programmen mit Hilfe logischer Behauptungen zu beweisen. Die Hoare-Logik und nachfolgende Entwicklungen haben die Grundlage für eine Vielzahl von Software-Verifizierungsbemühungen gebildet. Hoare war maßgeblich daran beteiligt, die Verified Software Initiative vorzuschlagen, ein kooperatives internationales Projekt, das sich mit den wissenschaftlichen Herausforderungen einer groß angelegten Softwareverifizierung befasst und Theorien, Werkzeuge und Experimente umfasst.
Tony Hoares Beiträge zur Theorie und Praxis von nebenläufigen Softwaresystemen sind ebenso beeindruckend. Die Prozessalgebra, die als Communicating Sequential Processes (CSP) bezeichnet wird, war eines der grundlegenden Paradigmen, sowohl als mathematische Theorie, um über gleichzeitige Berechnungen nachzudenken, als auch als Grundlage für die Programmiersprache Occam. CSP diente als Rahmen für die Erforschung verschiedener Ideen in der denotationalen Semantik, wie z.B. Powerdomains, sowie für Begriffe wie Abstraktion und Verfeinerung. Sie ist die Grundlage für eine Reihe von industrietauglichen Werkzeugen, die in einem breiten Spektrum von Anwendungen eingesetzt werden.
In diesem Buch werden auch Hoares Arbeiten der letzten Jahrzehnte vorgestellt. Diese Arbeiten umfassen einen rigorosen Ansatz für Spezifikationen in der Software-Engineering-Praxis, einschließlich prozeduraler und datenbezogener Abstraktionen, Datenverfeinerung und einer modularen Theorie von Designs. In jüngerer Zeit hat er zusammen mit Kollegen an der Entwicklung von Vereinheitlichenden Theorien der Programmierung (UTP) gearbeitet. Ihr Ziel ist es, die gemeinsamen algebraischen Theorien zu identifizieren, die den Kern von sequentiellen, nebenläufigen, reaktiven und cyber-physischen Berechnungen bilden.