First-Order Programming Theories / Edition 1

First-Order Programming Theories / Edition 1

by Tamas Gergely, Laszlo Ury
     
 

ISBN-10: 3540542779

ISBN-13: 9783540542773

Pub. Date: 11/20/1991

Publisher: Springer Berlin Heidelberg

This book proposes a purely classical first-order logical approach to the theory of programming. The authors, leading members of the famous "Hungarian school", use this approach to give a unified and systematic presentation of the theory. This approach provides formal methods and tools for reasoning about computer programs and programming languages by allowing the

Overview

This book proposes a purely classical first-order logical approach to the theory of programming. The authors, leading members of the famous "Hungarian school", use this approach to give a unified and systematic presentation of the theory. This approach provides formal methods and tools for reasoning about computer programs and programming languages by allowing the syntactic and semantic characterization of programs, the description of program properties, and ways to check whether a given program satisfies certain properties. The basic methods are logical extension, inductive definition and their combination, all of which admit an appropriate first-order representation of data and time. The framework proposed by the authors allows the investigation and development of different programming theories and logics from a unified point of view. Dynamic and temporal logics, for example, are investigated and compared with respect to their expressive and proof-theoretic powers. The book should appeal to both theoretical researchers and students. For researchers in computer science the book provides a coherent presentation of a new approach which permits the solution of various problems in programming theory in a unified manner by the use of first-order logical tools. The book may serve as a basis for graduate courses in programming theory and logic as it covers all important questions arising between the theory of computation and formal descriptive languages and presents an appropriate derivation system.

Product Details

ISBN-13:
9783540542773
Publisher:
Springer Berlin Heidelberg
Publication date:
11/20/1991
Series:
Monographs in Theoretical Computer Science. An EATCS Series, #24
Edition description:
1991
Pages:
353
Product dimensions:
6.69(w) x 9.61(h) x 0.03(d)

Table of Contents

Mathematical Background.- 1. Logic and Model Theory.- 2. Inductive Definability.- I Computability.- 3. Introduction to Part I.- 4. Main Properties of Program Schemas.- 5. Extension of Program Schemas.- 6. Program Schemas with Stacks.- 7. Computability.- 8. On Inductive Definability of 1- and 2-Computable Relations.- II Extended Dynamic Logics.- 9. Introduction to Part II.- 10. Description of Program Properties.- 11. Den-based Descriptive Languages.- 12. The Problem of Completeness.- 13. Dynamic Logic Generated by Extension.- 14. Continuous Denotational Semantics.- 15. Definable Denotational Semantics.- III Temporal Characterization of Programs.- 16. Introduction to Part III.- 17. Temporal Logic.- 18. Temporal Logical Description of Program Properties.- 19. Is Temporal Logic Expressible in Dynamic Logic?.- 20. Is Dynamic Logic Expressible in Temporal Logic?.- 21. The Case of Enumerable Models.- 22. Temporal Axiomatization of Program Verification Methods.- IV Programming Logic with Explicit Time.- 23. Introduction to Part IV.- 24. Time Logic.- 25. Definability in Regular Time Theories.- 26. Expressive Power of Time.- Epilogue.- References.- Notations.

Customer Reviews

Average Review:

Write a Review

and post it to your social network

     

Most Helpful Customer Reviews

See all customer reviews >