Prentice Hall

Prentice Hall International Series in Computer Science

Note: Links to (New) ISBNs are to information on the main Prentice Hall Web site which may be missing for some books.


Links to home pages of many of the authors may be found in: Who's Who on the Web in Formal Methods.


Computer Science: A Modern Introduction, 2/e

Les Goldschlager

Monash University

Andrew Lister

University of Queensland

The bestselling introductory overview of the discipline of computer science.

Contents: Introduction. The Design of Algorithms. The Theory of Algorithms. The Execution of Algorithms: Computer Architecture. The Execution of Algorithms: System Software. Algorithms in Action. Some Computer Applications. Social Issues. Index.

1989 320pp Pbk 0-13-165945-6

David A. Watt, Brian A.Wichman, and William Findlay

University of Glasgow

1987 560pp Pbk 0-13-004078-9


Introduction to Modula-2

Jim Welsh

University of Queensland

John Elder

Queens University, Belfast

This introductory text teaches not only the Modula-2 language but also structured programming and programming techniques. Welsh and Elder isolate implementation-dependent features of the language.

1987 320pp Pbk 0-13-488610-0


Introduction to Pascal, 3/e

Jim Welsh

University of Queensland

John Elder

Queens University, Belfast

Provides a comprehensive introduction to the Pascal programming language, suitable for use by novice programmers, and by those with a knowledge of other programming languages.

1988 336pp Pbk 0-13-491549-6


Programming in occam 2

Geraint Jones and Michael Goldsmith

University of Oxford

1988 318pp Pbk 0-13-730334-3


occam 2 Reference Manual

INMOS Ltd

1988 144pp Pbk 0-13-629312-3


Programming Language Paradigms

Tim Clement

Adelard

For those familiar with programming in an imperative language, this book aims to develop an understanding of programming in higher level declarative languages. Haskell, Prolog and Smalltalk have been chosen as typical examples of the functional, logic and object oriented programming paradigms.

Each language is given its own section of the book, where a usable subset is developed, guidance is given on programming with it, and an extended example shows how the language features may be used in combination. A final chapter in each section sets the language in the context of similar languages and discusses the strengths and weaknesses of each. The last chapter of the book examines the practical aspects of using the languages to build systems. All the languages chosen have implementations that are freely available for academic use.

Contents: Introduction. I. The Functional Paradigm: Gofer. Beginning Gofer Programming. Types. Higher-order Functions. Monads. An Example. Assessing the Language. II. The Logic Paradigm: Prolog. The Elements of Prolog. The Basis of Prolog. Prolog Built-ins. An Example. Assessing the Language. III. The Object Oriented Paradigm: Smalltalk. The Elements of Smalltalk. The Class Hierarchy. Advanced Smalltalk. An Example. Assessing the Language. IV. Summing Up. Other Ways to Assess Languages. Bibliography. Running the Languages. A Guided Tour of Smalltalk.

Oct 1996 304pp Pbk 0-13-262270-X


Programming from Specifications, 2/e

Carroll Morgan

University of Oxford

About the first edition:

Overall, it is difficult to exaggerate the importance of this book, which breaks new ground in the way the formal manipulation of specifications is presented, even at the beginning of what is intended to be a first exposure to conventional programming.
T.H.E.S.

Programming from Specifications, 2/e presents a rigorous treatment of most elementary program development techniques, including iteration, recursion, procedures, parameters, modules and data refinement.

This new edition retains the simple approach of the original: the integration of specification, development and coding, and the use of ordinary (classical) logic. Additions include more material on data refinement, a complete chapter on recursively defined types, and two further extended case studies.

Contents: Programs and Refinement. The Predicate Calculus. Assignment and Sequential Composition. Alternation. Iteration. Types and Declarations. Case Study: Square Root. Initial Variables. Constructed Types. Case Study: Insertion Sort. Procedures and Parameters. Case Study: Heap Sort. Recursive Procedures. Case Study: The Gray Code. Recursive Types. Modules and Encapsulation. State Transformation and Data Refinement. Case Study: Majority Voting. Origins and Conclusions. Case Study: A Paragraph Problem. Case Study: The Largest Rectangle Under a Histogram. Case Study: A Mail System. Semantics. Some Laws for Predicate Calculation. Answers to Some Exercises. Summary of Laws.

1994 320pp Pbk 0-13-123274-6


Programming: The Derivation of Algorithms

Anne Kaldewaij

Vrije University

This text discusses the calculational style of programming where programs are derived from their specification by means of formula manipulation.

Contents: Preface. Introduction. Predicate Calculus. The Guarded Command Language. Quantifications. General Programming Techniques. Deriving Efficient Programs. Searching. Segment Problems. Slope Search. Mixed Problems. Array Manipulations. Sorting. Auxiliary Arrays.

1990 240pp Pbk 0-13-204108-1

Teachers Manual Available


Partial Evaluation and Automatic Program Generation

Neil D. Jones, Carsten K. Gomard and Peter Sestoft

University of Copenhagen

Partial evaluation reconciles generality with efficiency by providing automatic specialisation and optimisation of programs.

Contents: Introduction. Functions, Types and Expressions. Programming Languages and their Operational Semantics. Compilation. Partial Evaluation of a Flow Chart Language. Partial Evaluation of a First-order Functional Language. The View from Olympus. Partial Evaluation of Prolog. Aspects of Similix: A Partial Evaluator for a Subset of Scheme. Partial Evaluation of C. Applications of Partial Evaluation. Termination of Partial Evaluation. Program Analysis. More General Program Transformation. Guide to the Literature. The Self-applicable Scheme Specialiser. Bibliography.

1993 400pp Pbk 0-13-020249-5


Verifiable Programming

Ole-Johan Dahl

University of Oslo

1992 350pp Pbk 0-13-951062-1


Abstract Data Types and Modula-2

Richard Mitchell

University of Brighton

1991 350pp Pbk 0-13-006081-X


Systematic Software Development Using VDM, 2/e (New) (ON-LINE BOOK!)

Cliff B. Jones

University of Manchester

A practical guide to software development using the Vienna Development Method, a mathematically based technique for formal specification and correctness arguments. Featuring seven chapters on specification and three on design, the second edition uses BSI (draft) standard VDM notation and includes a chapter that provides a small case study of the design method.

Contents: Foreword to the First Edition. Preface. Logic of Propositions. Reasoning About Predicates. Functions and Operations. Set Notation. Composite Objects and Invariants. Map Notation. Sequence Notation. Data Reification. More on Data Types. Operation Decomposition. A Small Case Study. Postscript

1991 350pp Pbk 0-13-880733-7


Reasoned Programming

Krysia Broda, Susan Eisenbach, Hessam Khoshnevisan and Steve Vickers

all at Imperial College of Science and Technology

This book shows how to apply mathematical reasoning to the development of computer programs. The book stresses the importance of first understanding the program users' needs, using logical specifications to express these, then writing program code to achieve the objectives set out in the specifications. It starts with functional programming chosen for its simplicity and also for its merits as a reasoning tool for imperative programming. Specifications are presented as contracts and students are taught how to develop codes from their specifications.

Contents: Introduction. Functions and Expressions. Specifications. Functional Programming in Miranda. Recursion and Induction. Lists. Types. Higher-Order Functions. Specification for Modula-2 Programs. Loops. Binary Chop. Quick Sort. Warshall's Algorithm. Tail Recursion. An Introduction to Logic. Natural Deduction. Natural Deduction for Predicate Logic. Models.

1995 296pp Pbk 0-13-098831-6


Programming Language Theory and its Implementation: Applicative and Imperative Paradigms

Michael J.C. Gordon

University of Cambridge and SRI International

Providing an introduction to some of the formal theories that have been developed to support computer programs, this book introduces those parts of programming language theory that may have important applications in improving the quality of software.

1988 256pp Pbk 0-13-730409-9


Introduction to the Theory of Programming Languages

Bertrand Meyer

Interactive Sofware Engineering Inc.

Contents: Basic Concepts. Mathematical Background. Syntax. Semantics: The Main Approaches. Lambda Calculus. Denotational Semantics: Fundamentals. Denotational Semantics: Language Features. The Mathematics of Recursion. Axiomatic Semantics. The Consistency of Semantic Definitions. Bibliography. Index.

1989 350pp Pbk 0-13-498502-8


Semantics of Programming Languages

R.D. Tennent

Queen's University, Kingston

1991 255pp Pbk 0-13-805599-8


Programming Language Concepts and Paradigms

David A. Watt

University of Glasgow

Contents: Preface. Introduction. Values. Storage. Bindings. Abstraction. Encapsulation. Type Systems. Sequencers. Concurrency. The Imperative Programming Paradigm. The Concurrent Programming Paradigm. The Object-Oriented Paradigm. The Functional Programming Paradigm. The Logic Programming Paradigm. Conclusion. Answers to Selected Exercises. Bibliography. Index.

1990 300pp Pbk 0-13-728866-2


Semantics of Sequential and Parallel Programs

Eike Best

University of Hildesheim

This book presents formal semantics of sequential and parallel programs and emphasises formal relationships between different mathematical description techniques. Providing a self-contained introduction to all the necessary mathematics, proofs are presented in a readable form which will appeal to the novice.

  • offers an in-depth study of the most well-known and widely-used methods for achieving correctness in program design

  • presents all technical results at an adequate and easy to learn level

  • case studies and exercises (some of them with solutions) help illustrate results

    Contents: Introduction. Basic Mathematical Concepts. Semantics of Sequential Programs. Sequential vs. Parallel Systems. Control Programs and Petri Nets. Operational Semantics and Fairness. Programs with Shared Data. Communicating Programs. Proofs and Solutions. Bibliography. Index.

    Apr 1996 356pp Pbk 0-13-460643-4


    Programming Language Syntax and Semantics

    David A. Watt

    University of Glasgow

    Introduces students to the formal methods of specifying the syntax and semantics of programming languages.

    Contents: Introduction. Syntax. Algebraic Semantics. Denotational Semantics. Action Semantics. Other Semantic Methods. Conclusion. Appendices: Answers to Selected Exercises. Bibliography. Index.

    1991 350pp Pbk 0-13-726274-4


    Introduction to Functional Programming

    Richard Bird

    University of Oxford

    Philip Walder

    University of Glasgow

    Every student and teacher of computer science should buy - beg, borrow or steal - Richard Bird and Philip Wadler's Introduction to Functional Programming. Not only is it the best introduction to functional programming published, but it is also an excellent introduction to programming in general
    Richard Jones, T.H.E.S.

    Contents: Fundamental Concepts. Basic Data Types. Lists. Examples. Recurion and Induction. Efficiency. Infinite Lists. New Types. Trees. Programming in Miranda. Bibliography. Index.

    1988 350pp Pbk 0-13-484197-2


    Functional Programming Using Standard ML

    Åke Wikström

    Chalmers University of Technology

    An introduction to functional programming for students of computer science. Wikström provides a thorough explanation of important concepts in functional programming and ML.

    Contents: Preface. Computers, Data, and Programs. Numbers. Names and Declarations. Functions. Systematic Program Construction. Truth Values. Characters and Strings. Pairs and Tuples. Syntax. Semantics. Declarations. Pattern Matching and Case Analysis. Lists. Recursion and Repetitive Computations. Higher Order Functions. Operators. List Handling Functions. Classes of Recursive Functions. Concrete Data Types. Recursive Data Types. Abstract Data Types. Input and Output. Programming Methodology. References. Glossary. Answers to Exercises.

    1988 464pp Pbk 0-13-331661-0


    An Introduction to Logic Programming Through Prolog

    Mike Spivey

    University of Oxford

    This is one of the few texts that combines three essential theses in the study of logic programming: the logic that gives programs their unique character; the practice of programming effectively using this logic; and the efficient implementation of logic programming on computers. The book begins with a gentle introduction to logic programming using a number of simple examples, followed by a concise and self-contained account of the logic behind Prolog programming. This leads to a discussion of methods of writing programs to ensure that the process of deriving answers from them is as efficient as possible. The techniques are illustrated by practical examples and the final part of the book explains how logic programming can be implemented efficiently.

    Features

    Contents: Introduction. Programming with Relations. Recursive Structures. The Meaning of Logic Programs. Inference Rules. Unification and Resolution. SLD-Resolution and Answer Substitutions. Negation as Failure. Searching Problems. Parsing. Evaluating and Simplifying Expressions. Hardware Simulation. Program Transformation. About picoProlog. Implementing Depth-First Search. Representing Terms and Substitutions. Implementation Notes. Interpreter Optimizations. In Conclusion. Bibliography. Index.

    1996 306pp Pbk 0-13-536047-1


    Computation as Logic

    Rene Lalement

    L'ecole Nationale des Ponts et Chaussees, Paris

    Contents: Introduction. The Syntactic Landscape. Reduction. First-Order Logic. Models. Equational Logic. Resolution. The Computable Landscape. Hints for Selected Exercises. Bibliography. Index.

    1993 450pp Hbk 0-13-770009-1


    Logic and its Applications

    Edmund Burke and Eric Foxley

    University of Nottingham

    Providing a thorough introduction to logic programming, this new text covers both propositional and predicate logic with applications in circuit design, formal specification, and logic programming. Introducing the reader to mathematical logic, the book gives special emphasis to applications in computer science.

    Contents: Introduction. Propositional Logic. Formal Approach to Propositional Logic. Application to Logic Design. Predicate Logic. Logic Programming. Formal Systems Specification. Solutions. Bibliography. Index.

    Mar 1996 296pp Pbk 0-13-030263-5


    Mathematical Logic for Computer Science

    Moti Ben-Ari

    Technion - Israel Institute of Technology

    Designed to provide a firm foundation in mathematical logic, this book offers an elementary yet rigorous text for undergraduate courses in mathematical logic including applications to computer science, such as logic programming and formal specification and verification.

    Contents: Introduction. Propositional Calculus. Predicate Calculus. Resolution and Logic Programming. Temporal Logic. Formalisation of Programs. Further Reading. Appendices.

    1992 320pp Pbk 0-13-564139-X


    From Logic Programming to Prolog

    Krzysztof R. Apt

    CWI, Amsterdam and University of Amsterdam

    This text provides a systematic introduction to the theory of logic programming and shows how this theory can be applied to reason about pure Prolog programs. It includes an introduction to programming in prolog and deals with such programming issues as determination, occur-check freedom and absence of errors.

    Contents: Introduction. Unification. Logic Programs: Procedural Interpretation. Logic Programs: Declarative Interpretation. Programming in Pure Prolog. Termination. The Occur-Check Problem. Partial Correctness. Programming in Pure Prolog with Arithmetic. Verification of Pure Prolog. Programs with Arithmetic. Bibliography.

    Oct 1996 306pp Pbk 0-13-230368-X


    Compiler Construction: A Recursive Descent Model

    John Elder

    Queen's University, Belfast

    Blending theoretical knowledge with practical experience, each aspect of compiler design is related to the practical study of a working compiler for a substantial subset of Modula-2.

    Contents: Introduction. The Specification of a Compiler. Designing the User Interface. Source Handling. Compiler Structure: Analysis and Generation. Elementary Syntax Theory. Lexical Analysis. Top-down Syntax Analysis. A Recursive Descent Analyser. Syntax Error Recovery. Semantic Table Organisation. Semantic Table of Contents and Usage. Semantic Analysis: A Practical Example. Data Representation. Allocating and Accessing Data Storage. Forms of Object Code. Object Code Generation. A Code Generation Interface. Code Generation in the MiniPascal Compiler. Run-time Errors and Diagnostics. Appendices.

    1994 220pp Pbk 0-13-291139-6


    Implementation of Functional Programming Languages

    Simon L. Peyton-Jones

    University of Glasgow

    1987 500pp Pbk 0-13-453325-9


    Programming Language Processors

    David A. Watt

    University of Glasgow

    Studies the implementation of programming languages, examining language processors - such as compilers and interpreters, and showing how these clearly relate to the syntax and semantics of the implemented language. The book follows a top-down approach introducing compilers and interpreters as 'black-boxes', followed by an examination of their working in more detail.

    Contents: Introduction. Language Processors. Compilation. Syntactic Analysis. Run-time Organisation. Code Generation. Interpretation. Conclusion. Appendices. Bibliography. Index.

    1993 350pp Pbk 0-13-720129-X


    Database Programming Languages

    N. Paton

    University of Manchester

    M.H. Williams

    Heriott Watt University

    R. Cooper and P.H. Trinder

    University of Glasgow

    Database Programming Languages describes, compares and contrasts the following four approaches to database programming all of which are covered on an advanced database course: deductive, functional, imperative and object-oriented. Aimed at people studying in the area of advanced database systems, this book provides a comprehensive introduction to the four techniques.

    Contents: Introduction. Deductive, Functional, Imperative, Object-Oriented Approaches.

    1996 350pp Pbk 0-13-101825-6


    Foundations of Semantic Databases

    E.O. de Brock

    University of Gronigen

    Presents a formal introduction to relational database design and offers in-depth treatment of database integrity, supported by case studies. The book has a distinctive bias towards a formal description and provides thorough treatment of formal specifications of constraints and business rules, both static and dynamic.

    Contents: Preface. Basic Mathematical Concepts. From Tables to Database Universes. Some Database Concepts. Constructing Database Universes. A Non-trivial Example of a Database Universe. Dynamic Constraints. Retrieval. Maintenance. Data Dictionaries. Directions for Realisation in SQL. References.

    1995 234pp Pbk 0-13-327099-8


    Using Z: Specification, Refinement and Proof

    Jim Woodcock and Jim Davies

    University of Oxford

    This book contains enough material for three complete courses of study. It provides an introduction to the world of logic, sets and relations. It explains the use of the Z notation in the specification of realistic systems. It shows how Z specifications may be refined to produce executable code; this is demonstrated in a selection of case studies.

    Features

    Contents: Introduction. Propositional Logic. Predicate Logic. Equality and Definite Description. Sets. Definitions. Relations. Functions. Sequences. Free Types. Schemas. Schema Operators. Promotion. Preconditions. A File System. Data Refinement. Data Refinement and Schemas. Functional Refinement. Refinement Calculus. A Telecommunications Protocol. An Operating System Scheduler. A Bounded Buffer Module. A Save Area.

    1996 400pp Pbk 0-13-948472-8

    Supplementary material including exercises and solutions, available on the web at http://www.comlab.ox.ac.uk/usingz.html


    The Z Notation: A Reference Manual, 2/e

    Mike Spivey

    University of Oxford

    ...it remains a model of compact precision against which others will have to be judged. For newcomers and owners of dog-eared first editions alike, this second edition is inevitably a must-buy.
    Computer Weekly

    Contents: Tutorial Introduction. Background. The Z Language. The Mathematical Tool-kit. Sequential Systems. Syntax Summary. Glossary.

    1991 150pp Pbk 0-13-978529-9


    Applications of Formal Methods

    Michael G. Hinchey

    New Jersey Institute of Technology

    Jonathan P. Bowen

    University of Reading

    This collection of essays illustrates the application of formal methods to realistic problems, with an industrial relevance. All the examples are interesting in themselves, but also serve to highlight the appropriateness of formal methods for particular problems. Contributions are also included from an international base of well respected researchers and practitioners.

    Features

    Contributors: Stuart Anderson. Leonor Barroca. Jonathan Bowen. Glenn Bruns. Michiel de Boer. Tom Brookes. Andy Coombes. Dan Craigen. Babek Dehbonei. Norman Delisle. Eugene Durr. John Fitzgerald. David Garlan. Susan Gerhart. Peter Gorm Larsen. Michael Green. David Guaspari. Ute Hammer. Vivien Hamilton. Michael G Hinchey. CAR Hoare. Jonathan Hoare. Peter Mataga. John McDermid. Fernando. Mejia. Steve Miller. Paul Mukherjee. David Lodge Parnas. Jan Peleska. Nico Plat. Ted Ralston. Amer Saeed. Mike Seagar. Lynn Spencer. Mandayam Srivas. Matt Stillerman. Brian Wichmann. William D Young. Pamela Zave.

    1996 472pp Hbk 0-13-366949-1


    Specification Case Studies, 2/e

    Ian Hayes

    University of Queensland

    This book will be of interest to the professional software engineer involved in designing and specifying large software projects and includes contributions from leading researchers.

    1992 350pp Pbk 0-13-832544-8


    Introduction to Formal Specification and Z, 2/e

    Ben Potter

    University of Hertfordshire

    Jane Sinclair

    Open University

    David Till

    City University, London

    Following the success of the first edition, the authors have updated and revised this bestselling textbook to take into account the changes in the subject over the past five years. The opening chapters have been rewritten to reflect the needs of students who may require a gentle introduction to the world of software engineering.

    Features

    Contents: Introduction. Formal Specification within Software Engineering. An Informal Introduction to Logic and Set Theory. The Z Notation: Mathematical Language. The Z Notation: Relations and Functions. The Z Notation: Schemas and Specification Structure. A First Specification. Formal Reasoning. From Specification to Program. From Theory to Practice. Appendices. Bibliography. Index.

    May 1996 304pp Pbk 0-13-242207-7


    Case Studies in Systematic Software Development (New) (ON-LINE BOOK!)

    Cliff B. Jones

    University of Manchester

    Roger Shaw

    Praxis

    In this book, twelve case studies cover both the specification and development aspects of VDM. The cases included are: The Specification of NDB; Outline Specifications of the ISTAR Database; A Formal Description of Line Representations on Graphic Devices; Muffin; Unification: Specification and Development; Formalising Unification; Object-Oriented Languages; Heap Storage Specification and Development; Garbage Collection; Data Flow Architecture; Formally Describing Interactive Systems.

    1990 416pp Pbk 0-13-116088-5


    Communication and Concurrency

    Robin Milner

    University of Cambridge

    . . . this book is a valuable review of the description and verification of concurrent systems. As one of the leading theoretical computer scientists in Britain, Robin Milner has produced an excellent book containing a well-judged mixture of theory and practical applications which should form a solid base for academic courses and a valuable reference for practitioners.
    T.H.E.S.

    Contents: Modelling Communication. Basic Definitions. Equational Laws and Their Application. Strong Bisimulation and Strong Equivalence. Bisimulation and Observation Equivalence. Further Examples. The Theory of Observation Congruence. Defining a Programming Language. Operators and Calculi. Specifications and Logic. Determinacy and Confluence. Sources and Related Work.

    1983 300pp Pbk 0-13-115007-3


    Communicating Sequential Processes

    C.A.R. Hoare

    University of Oxford

    Professor Hoare has produced a book on a subject in which he is acknowledged as one of the foremost theoretical thinkers; the resulting text is quite likely to become a classic in the field.surprisingly easy reading.
    Data Processing

    Contents: Processes. Concurrency. Non-determinism. Communication. Sequential Processes. Shared Resources. Discussion. Bibliography. Index.

    1985 280pp Pbk 0-13-153289-8


    Finite Transition Systems

    André Arnold

    Universite Bordeaux I

    Contents: Introduction. Transition Systems. The Synchronous Product of Transition Systems. Transition System Logics. Verification of Properties of Transition Systems. Fixpoints in Transition Systems. Software Tools.

    1994 200pp Hbk 0-13-092990-5


    Parallel Numerical Algorithms

    Len Freeman

    University of Manchester

    Chris Phillips

    University of Newcastle upon Tyne

    Contents: Fundamentals. Systems Support. Numerical Libraries. Gaussian Eleminiation: A Case Study. Further Linear Algebra. Other Areas I. Other Areas II. Recent Developments.

    1992 316pp Pbk 0-13-651597-5


    Principles of Concurrent and Distributed Programming

    Moti Ben-Ari

    Technion - Israel Institute of Technology

    This complete introduction focuses on general principles, and offers a broad perspective for evaluating systems, algorithms, and languages.

    Contents: What is Concurrent Programming? The Concurrent Programming Abstraction. The Mutual Exclusion Problem. Semaphores. Monitors. The Problem of the Dining Philosophers. Distributed Programming Models. Ada. occam. Linda. Distributed Mutual Exclusion. Distributed Termination. The Byzantine Generals Problem. Single Processor Implementation. Multi-processor Implementation. Real-Time Programming. Ada Overview. Running Concurrent Programs. Implementation of the Ada Emulations.

    1990 300pp Pbk 0-13-711821-X


    Distributed Systems and Computer Networks

    Morris Sloman and Jeff Kramer

    Imperial College of Science and Technology

    This book provides an overview of the principles and concepts of distributed systems, providing details of the software architecture and communications support required.

    Contents: Distributed Systems. Distributed System Architecture. Software Structure. Communication Primitives and Related Software Issues. Communication System. Physical Layer. Local Area Networks. Data-Link. Network Layer. Transport and Session Layers. Presentation Layer. Application-Oriented Services. Appendices. Index.

    1987 400pp Pbk 0-13-215849-3


    Distributed Systems Analysis with CCS

    Glenn Bruns

    AT&T Bell Laboratories

    This book describes how distributed systems can be analysed using the process notation CCS, temporal logic, and automatic tools. The core of the book is a series of chapters showing how CCS has been applied to classic case studies in distributed systems and to systems recently developed in industry. In each case the system is described, a CCS model of the system is presented, properties of the system are expressed in temporal logic, and the analysis results are shown. The book is self-contained. It starts with a discussion of how CCS and its theory addresses the needs of software engineering. Then CCS and temporal logic are introduced in a tutorial style with many examples. Every chapter contains exercises to test the reader's understanding and to suggest alternative modelling approaches. Appendices describe the analysis tools and show the models in the format actually supplied to the tool.

    A unique feature of the book is its careful discussion of modelling issues and its pragmatic, engineering perspective. The book is suitable for advanced undergraduate and post-graduate students, as well as designers and programmers of distributed systems.

    Contents: CCS and Software Engineering. Modelling Systems. Reasoning About Systems. Triple-Modular Redundancy. On-the-fly Garbage Collection. A Shared-Memory Communication Protocol. Modelling Systems at the Design Stage. A More Expressive Notation for Specifications. The Concurrency Workbench. A Language for Value-Passing CCS. Workbench Input Files.

    Oct 1996 200pp Pbk 0-13-398389-7


    Principles of Protocol Design

    Robin Sharp

    Technical University of Denmark

    Principles of Protocol Design introduces the principles used in the construction of a large range of modern data communication protocols. Primarily based on descriptions of protocols in the notation of CSP, the book concentrates on standardised protocols.

    Contents: Introduction. CSP Descriptions and Proof Rules. Protocols and Services. Protocol Mechanisms. Naming, Addressing and Routing.

    1995 300pp Pbk 0-13-182155-5


    Real-time Systems: Specification, Verification and Analysis

    Ed. Mathai Joseph

    University of Warwick

    Provides a detailed account of real-time systems: program structures for real-time, timing analysis using scheduling theory and specification and verification in different frameworks. The presentation makes extensive use of recent research which has demonstrated the effectiveness and applicability of mathematically based methods for real-time system design. Each chapter focuses on a particular technique and examples help to reinforce the theory presented in the text.

    Features

    Contents: Introduction. Fixed Priority Scheduling - Simple Programs. Fixed Priority Scheduling with Communicating Tasks. Dynamic Priority Scheduling. Specification and Verification Using An Assertional Method. Specification and Verification in the Duration Calculus. Specification and Verification in Timed CSP. Real-time Systems and Fault-Tolerance. Bibliography. Index.

    1996 300pp Pbk 0-13-455297-0


    Object-Oriented Software Construction

    Bertrand Meyer

    Interactive Software Engineering Inc.

    The presentation of object-oriented concepts uses the Eiffel design and programming language. Detailed discussions are also devoted to the implementation of object-oriented concepts in classical languages such as Fortran, C and Ada, and in other object-oriented languages such as Simula and Smalltalk.

    Contents: ISSUES AND PRINCIPLES. Aspects of Software Quality. Modularity. Approaches to Reusability. The Road to Object-Orientedness. TECHNIQUES OF OBJECT-ORIENTED DESIGN AND PROGRAMMING. Basic Elements of Eiffel Programming. Genericity. Systematic Approaches to Program Construction. More Aspects of Eiffel. Designing Class Interfaces. Introduction to Inheritance. More About Inheritance. Object-oriented Design: Case Studies. Constants and Shared Objects. Techniques of Object-oriented Design. Implementation: The Eiffel Programming Environment. Memory Management. APPLYING OBJECT-ORIENTED TECHNIQUES IN OTHER ENVIRONMENTS. Object-oriented Programming in Classical Languages. Object-oriented Programming and Ada. Genericity Versus Inheritance. Other Object-oriented Languages. Further Issues. APPENDICES. Extracts From the Eiffel Library. Eiffel: A Quick Overview. Eiffel Grammer. Reserved Words and Special Symbols. Input, Output and Strings. Eiffel Syntax Diagrams. Bibliography. Index.

    1989 480pp Pbk 0-13-629031-0


    Object-Oriented Databases

    John G. Hughes

    University of Ulster

    1991 350pp Pbk 0-13-629874-5


    Category Theory for Computing Science, 2/e

    Michael Barr

    McGill University

    Charles Wells

    Case Western Reserve University

    Following the success of the first edition, the authors have revised this text in the light of their classroom experience. The fundamental concepts of category theory are explained throughout at a slow pace which allows readers to develop their understanding gradually. A wide coverage of topics in category theory and computer science is developed including introductory treatments of cartesian closed categories, sketches and elemental categorical model theory and triples.

    Features

    Contents: Preface. Preliminaries. Categories. Functors. Diagrams. Naturality and Sketches. Products and Sums. Cartesian Closed Categories. Finite Product Sketches. Limits and Colimits. Adjoints. Algebras for Endofunctors. Categories with Monoidal Structure. Bibliography. Index.

    1996 344pp Pbk 0-13-323809-1

    Supplement available from: ftp://triples.math.mcgill.ca/pub/barr/ctcs.elec.supp.dvi


    Introduction to the Theory of Complexity

    Daniel P. Bovet and Pierluigi Crescenzi

    University of Rome "La Sapienza"

    Reviewing in a systematic way the most significant results in the study of computational complexity, this book follows a balanced approach which is partly algorithmic and partly structuralist.

    Contents: Mathematical Preliminaries. Elements of Computability Theory. Complexity Classes. The class P. The class NP. The Complexity of Optimization Problems. Beyond NP. Space-complexity Classes. Probabilistic Algorithms and Complexity Classes. Interactive Proof Systems. Models of Parallel Computer. Parallel Algorithms.

    1994 282pp Hbk 0-13-915380-2


    Mathematics for Computer Science

    André Arnold

    Universite Bordeaux 1

    Irene Guessarian

    University of Paris

    This text provides the essential mathematics needed to study computing. The authors are aware that many students do not have the same mathematical background common five years ago and this book has been written to accommodate these changes. Many exercises are provided with detailed answers and difficult concepts are thoroughly illustrated to help learning.

    Features

    Contents: Introduction. Sets and Functions. Ordered Sets. Recursion and Induction. Boolean Algebras. Combinatorial Algebra and Applications. Recurrences. Generating Series. Asympotic Behaviour. Graphs and Trees. Rational Languages and Finite Automata. Discrete Probabilities. Finite Markov Chains. Applications and Examples. Answers to all Exercises. Index.

    Apr 1996 356pp Pbk 0-13-234717-2


    Cornerstones of Undecidibility

    Grzegorz Rozenberg

    University of Leiden

    Arto Salomaa

    University of Turku

    Contents: Preface. Halting Problem. Interlude 1. Post Correspondence Problem. Diophantine Problems. Interlude 2. Classes of Problems and Proofs. The Secret Number. Epilogue. Bibliography.

    1994 350pp Pbk 0-13-297425-8


    Computer Arithmetic Systems: Algorithms, Architecture and Implementation

    Amos Omondi

    University of Wellington

    Computer Arithmetic Systems provides a detailed discussion of arithmetic units for digital computers.

    Contents: Fixed-Point Number Systems. Fixed-Point Addition and Subtraction. Fixed-Point Multiplication. Fixed-Point Division. Summary and Miscellaneous Topics on Fixed-Point Systems. Floating-Point Number Systems and Basic Arithmetic. Basic Floating-Point Operations - Implementation. Elementary Functions. Summary and Miscellaneous Topics on Floating-Point Systems. Redundant Signed-Digit Number Systems. Residue Number Systems. Decimal Number Systems.

    1994 522pp Pbk 0-13-334301-4


    Mechanised Reasoning and Hardware Design

    Ed. C.A.R. Hoare

    University of Oxford

    Ed. M.J.C. Gordon

    University of Cambridge

    1992 250pp Hbk 0-13-572405-8


    Microprocessor Programming and Software Development

    F.G. Duncan

    University of Bristol

    1979 320pp Hbk 0-13-581405-7


    High Level Programmer's Guide to the 68000

    Francis Gregory McCabe

    Imperial College of Science & Technology

    1991 250pp Pbk 0-13-388034-6


    Computer and Communication Systems Performance Modelling

    Peter J.B. King

    Heriot-Watt University

    Contents: Preface. Introduction. Probability Theory. Stochastic Processes. Simple Queues. M/G/1 Queues. Queues With Breakdowns. Priority Queues. Waiting Time Distributions of Queues. Multiple Server Queues. Network of Queues. Computational Algorithms for Product Form Queueing Networks. Approximations and Bounds. Numerical Solution of Queueing Models. Local Area Networks. Index.

    1990 245pp Pbk 0-13-163065-2


    A Classical Mind: Essays in Honour of C.A.R. Hoare

    Edited by A.W. Roscoe

    University of Oxford

    A rich assembly of contributors have pulled together to provide a volume of essays which are dedicated to Tony Hoare and his approach to Computer Science. Recognising the huge difference that Tony has made to the way that computing is perceived, each contributor has a very personal way of expressing their respect for his commitment and enterprise. The book reads like a who's who of computing - each paper written by a key person in the field. Foreword by Robin Milner.

    Contents: Interaction Categories and Communicating Sequential Processes (Samson Abramsky). Relational Program Derivation and Context-Free Language Recognition (Richard Bird and Oege de Moor). Formal Model of Robots: Geometry and Kinematics (Dines Bjorner). Fair Communicating Processes (Stephen Brookes). Hiding and Behaviour: An Institutional Approach (Rod Burstall and Razvan Diaconescu). Monitors Revisited (Ole-Johan Dahl). On the Design of Calculational Proofs (Edsger W. Dijkstra). Proof of Correctness of Object Representations (Jospeh A. Goguen and Grant Malcolm). A Mechanized Hoare Logic of State Transitions (Mike Gordon). Constant-space Quicksort (David Gries). From CSP to Hybrid Systems (He Jifeng). Abstractions of Time (Eric C.R. Hehner). Software Development Method (M.A. Jackson). Process Arguments about an Object-Based Design Notation (C.B. Jones). Bracket Notation for the 'Coefficient of' Operator (Donald E. Knuth). Implementing Coherent Memory (Butler W. Lampson). How to Design a Parallel Computer (David May). Powerlist: A Structure For Parallel Recursion (Jayadev Misra). The Cuppest Capjunctive Capping, and Galois (Carroll Morgan). The Advantages of Free Choice: A Symmetric and Fully Distributed Solution for the Dinning Philosophers Problems (Michael O. Rabin and Daniel Lehmann). Model-Checking CSP (A.W. Roscoe). The Semantics of Id (J.E. Stoy). Correctness of Data Representations in Algol-like Languages (R.D. Tennent). Software is History! (Jim Welsh). A Mean Value Calculus of Durations (Zhou and Li Xiaoshan).

    1994 445pp Hbk 0-13-294844-3


    Essays in Computer Science

    C.A.R. Hoare

    University of Oxford

    C.B. Jones

    University of Manchester

    This book provides a unique insight into the intellectual development of one of the world's best known computer scientists. A collection of Tony Hoare's papers is presented together with helpful notes about their background and impact.

    1989 432pp Hbk 0-13-284027-8