Für diesen Artikel ist leider kein Bild verfügbar.

Algebraic Approaches to Program Semantics

Ernest G Manes, Michael A Arbib (Autoren)

Buch | Hardcover

353 Seiten

1986 | 1986 ed.
Springer-Verlag New York Inc.
978-0-387-96324-2 (ISBN)

Titel ist leider vergriffen;
keine Neuauflage

Artikel merken

In the 1930s, mathematical logicians studied the notion of "effective comput ability" using such notions as recursive functions, A-calculus, and Turing machines. The 1940s saw the construction of the first electronic computers, and the next 20 years saw the evolution of higher-level programming languages in which programs could be written in a convenient fashion independent (thanks to compilers and interpreters) of the architecture of any specific machine. The development of such languages led in turn to the general analysis of questions of syntax, structuring strings of symbols which could count as legal programs, and semantics, determining the "meaning" of a program, for example, as the function it computes in transforming input data to output results. An important approach to semantics, pioneered by Floyd, Hoare, and Wirth, is called assertion semantics: given a specification of which assertions (preconditions) on input data should guarantee that the results satisfy desired assertions (postconditions) on output data, one seeks a logical proof that the program satisfies its specification. An alternative approach, pioneered by Scott and Strachey, is called denotational semantics: it offers algebraic techniques for characterizing the denotation of (i. e., the function computed by) a program-the properties of the program can then be checked by direct comparison of the denotation with the specification. This book is an introduction to denotational semantics. More specifically, we introduce the reader to two approaches to denotational semantics: the order semantics of Scott and Strachey and our own partially additive semantics."

1 Denotational Semantics of Control.- 1 An Introduction to Denotational Semantics.- 1.1 Syntax and Semantics.- 1.2 A Simple Fragment of Pascal.- 1.3 A Functional Programming Fragment.- 1.4 Multifunctions.- 1.5 A Preview of Partially Additive Semantics.- 2 An Introduction to Category Theory.- 2.1 The Definition of a Category.- 2.2 Isomorphism, Duality, and Zero Objects.- 2.3 Products and Coproducts.- 3 Partially Additive Semantics.- 3.1 Partial Addition.- 3.2 Partially Additive Categories and Iteration.- 3.3 The Boolean Algebra of Guards.- 4 Assertion Semantics.- 4.1 Assertions and Preconditions.- 4.2 Partial Correctness.- 4.3 Total Correctness.- 2 Semantics of Recursion.- 5 Recursive Specifications.- 5.1 The Kleene Sequence.- 5.2 The Pattern-of-Calls Expansion.- 5.3 Iteration Recursively.- 6 Order Semantics of Recursion.- 6.1 Domains.- 6.2 Fixed Point Theorems.- 6.3 Recursive Specification in FPF.- 6.4 Fixed Points and Formal Languages.- 7 Canonical Fixed Points.- 8 Partially Additive Semantics of Recursion.- 8.1 PAR Schemes.- 8.2 The Canonical Fixed Point for PAR Schemes.- 8.3 Additive Domains.- 8.4 Proving Correctness.- 8.5 Power Series and Products.- 9 Fixed Points in Metric Spaces.- 9.1 Contractions on Complete Metric Spaces.- 9.2 Differential Equations.- 9.3 Metrics on Trees.- 9.4 Context-Free Languages as Metric Fixed Points.- 3 Data Types.- 10 Functors.- 10.1 Data Types Lead to Functors.- 10.2 Fixed Points of Functors.- 11 Recursive Specification of Data Types.- 11.1 From Least Upper Bounds to Least Fixed Points.- 11.2 Co-continuous Functors.- 11.3 Continuous Functors and Greatest Fixed Points.- 12 Parametric Specification.- 12.1 Arrays.- 12.2 Stacks and Queues.- 12.3 A Functional Programming Fragment Revisited.- 13 Order Semantics of Data Types.- 13.1 Introduction.- 13.2 Constructions with Domains.- 13.3 Cartesian-Closed Categories.- 13.4 Solving Function Space Equations.- 14 Equational Specification.- 14.1 Initial Algebras.- 14.2 Sur-reflections.- Epilogue.- Author Index.

Reihe/Serie	Springer Texts in Electrical Engineering
Zusatzinfo	Bibliography
Verlagsort	New York, NY
Sprache	englisch
Gewicht	690 g
Themenwelt	Informatik ► Theorie / Studium ► Künstliche Intelligenz / Robotik
Themenwelt	Mathematik / Informatik ► Mathematik ► Logik / Mengenlehre
ISBN-10	0-387-96324-3 / 0387963243
ISBN-13	978-0-387-96324-2 / 9780387963242
Zustand	Neuware