Advertisement

Algebraic Approaches to Program Semantics

  • Ernest G. Manes
  • Michael A. Arbib

Part of the Texts and Monographs in Computer Science book series (MCS)

Table of contents

  1. Front Matter
    Pages i-xi
  2. Denotational Semantics of Control

    1. Front Matter
      Pages 1-1
    2. Ernest G. Manes, Michael A. Arbib
      Pages 3-37
    3. Ernest G. Manes, Michael A. Arbib
      Pages 38-70
    4. Ernest G. Manes, Michael A. Arbib
      Pages 71-97
    5. Ernest G. Manes, Michael A. Arbib
      Pages 98-115
  3. Semantics of Recursion

    1. Front Matter
      Pages 117-117
    2. Ernest G. Manes, Michael A. Arbib
      Pages 119-145
    3. Ernest G. Manes, Michael A. Arbib
      Pages 146-175
    4. Ernest G. Manes, Michael A. Arbib
      Pages 176-179
    5. Ernest G. Manes, Michael A. Arbib
      Pages 180-209
    6. Ernest G. Manes, Michael A. Arbib
      Pages 210-231
  4. Data Types

    1. Front Matter
      Pages 233-233
    2. Ernest G. Manes, Michael A. Arbib
      Pages 235-257
    3. Ernest G. Manes, Michael A. Arbib
      Pages 258-278
    4. Ernest G. Manes, Michael A. Arbib
      Pages 279-292
    5. Ernest G. Manes, Michael A. Arbib
      Pages 293-317
    6. Ernest G. Manes, Michael A. Arbib
      Pages 318-340
  5. Back Matter
    Pages 341-353

About this book

Introduction

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.

Keywords

Boolean algebra computer control evolution formal language formal languages functional programming mathematical logic program semantics programming programming language proof proving semantics

Authors and affiliations

  • Ernest G. Manes
    • 1
  • Michael A. Arbib
    • 2
  1. 1.Department of Mathematics and StatisticsUniversity of MassachusettsAmherstUSA
  2. 2.Departments of Computer Science, Neurobiology and PhysiologyUniversity of Southern CaliforniaLos AngelesUSA

Bibliographic information

  • DOI https://doi.org/10.1007/978-1-4612-4962-7
  • Copyright Information Springer-Verlag New York 1986
  • Publisher Name Springer, New York, NY
  • eBook Packages Springer Book Archive
  • Print ISBN 978-1-4612-9377-4
  • Online ISBN 978-1-4612-4962-7
  • Series Print ISSN 0172-603X
  • Buy this book on publisher's site
Industry Sectors
Electronics
IT & Software
Aerospace