ONT Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| Algebraic Approaches to Program Semantics
|
| Preface
|
| In the 1930's, mathematical logicians studied the notion
| of "effective computability" using such notions as recursive
| functions, lambda calculus, and Turing machines. The 1940's 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'. Moreover, we show how each
| approach may be applied both to the specification of the semantics of programs,
| including recursive programs, and to the specification of new data types from old.
| There has been a growing acceptance that 'category theory', a branch of abstract
| algebra, provides a perspicuous general setting for all these topics, and for
| many other algebraic approaches to program semantics as well. Thus, an
| important aim of this book is to interweave the study of semantics
| with a completely self-contained introduction to a useful core
| of category theory, fully motivated by basic concepts of
| computer science.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤