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 best-selling 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 ISBN 0-13-165945-6 (order from Amazon USA or Amazon UK)
ADA: Language and Methodology []
David A. Watt, Brian A. Wichman, and William Findlay
University of Glasgow
1987 560pp Pbk ISBN 0-13-004078-9 (order from Amazon USA or Amazon UK)
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 ISBN 0-13-488610-0 (order from Amazon USA or Amazon UK)
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 ISBN 0-13-491549-6 (order from Amazon USA or Amazon UK)
Programming in occam 2 []
Geraint Jones and Michael Goldsmith
University of Oxford
1988 318pp Pbk ISBN 0-13-730334-3 (order from Amazon USA or Amazon UK)
occam 2 Reference Manual []
INMOS Ltd
1988 144pp Pbk ISBN 0-13-629312-3 (order from Amazon USA or Amazon UK)
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.
October 1996 304pp Pbk ISBN 0-13-262270-X (order from Amazon USA or Amazon UK)
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.
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 ISBN 0-13-123274-6 (order from Amazon USA or Amazon UK)
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 ISBN 0-13-204108-1 (order from Amazon USA or Amazon UK)
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 ISBN 0-13-020249-5 (order from Amazon USA or Amazon UK)
Verifiable Programming []
Ole-Johan Dahl↑
University of Oslo↑
1992 350pp Pbk ISBN 0-13-951062-1 (order from Amazon USA or Amazon UK)
Abstract Data Types and Modula-2 []
Richard Mitchell
University of Brighton
1991 350pp Pbk ISBN 0-13-006081-X (order from Amazon USA or Amazon UK)
Systematic Software Development Using VDM, 2/e []
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 ISBN 0-13-880733-7 (order from Amazon USA or Amazon UK)
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 ISBN 0-13-098831-6 (order from Amazon USA or Amazon UK)
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 ISBN 0-13-730409-9 (order from Amazon USA or Amazon UK)
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 ISBN 0-13-498502-8 (order from Amazon USA or Amazon UK)
Semantics of Programming Languages []
R.D. Tennent
Queen's University, Kingston
1991 255pp Pbk ISBN 0-13-805599-8 (order from Amazon USA or Amazon UK)
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 ISBN 0-13-728866-2 (order from Amazon USA or Amazon UK)
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.
April 1996 356pp Pbk ISBN 0-13-460643-4 (order from Amazon USA or Amazon UK)
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 PbkISBN 0-13-726274-4 (order from Amazon USA or Amazon UK)
Introduction to Functional Programming []
Richard Bird
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 ISBN 0-13-484197-2 (order from Amazon USA or Amazon UK)
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 ISBN 0-13-331661-0 (order from Amazon USA or Amazon UK)
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
- provides rigorous treatments of foundations
- includes source code for a small but complete Prolog implementation written in Pascal
- the implementation is capable of running all the programs presented in the book, and is available via the Internet↑
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 ISBN 0-13-536047-1 (order from Amazon USA or Amazon UK)
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 ISBN 0-13-770009-1 (order from Amazon USA or Amazon UK)
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.
- class tested and containing numerous practical examples and exercises
- more details of the book available via http://tawny.cs.nott.ac.uk/logic/
Contents: Introduction. Propositional Logic. Formal Approach to Propositional Logic. Application to Logic Design. Predicate Logic. Logic Programming. Formal Systems Specification. Solutions. Bibliography. Index.
March 1996 296pp Pbk ISBN 0-13-030263-5 (order from Amazon USA or Amazon UK)
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 ISBN 0-13-564139-X (order from Amazon USA or Amazon UK)
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.
- covers both the natural interpretations of logic program, as declarative specification and as procedure for computer execution
- class tested with exercises, examples and solutions
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.
October 1996 306pp Pbk ISBN 0-13-230368-X (order from Amazon USA or Amazon UK)
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 ISBN 0-13-291139-6 (order from Amazon USA or Amazon UK)
Implementation of Functional Programming Languages []
Simon L. Peyton-Jones
University of Glasgow
1987 500pp Pbk ISBN 0-13-453325-9 (order from Amazon USA or Amazon UK)
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 ISBN 0-13-720129-X (order from Amazon USA or Amazon UK)
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 ISBN 0-13-101825-6 (order from Amazon USA or Amazon UK)
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 ISBN 0-13-327099-8 (order from Amazon USA or Amazon UK)
Using Z: Specification, Refinement and Proof []
Jim Woodcock↑ and Jim Davies
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
- covers the essentials of specification, refinement and proof, revealing techniques never previously published
- thoroughly class-tested at both undergraduate and postgraduate levels
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 ISBN 0-13-948472-8 (order from Amazon USA or Amazon UK)
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
…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.
Contents: Tutorial Introduction. Background. The Z Language. The Mathematical Tool-kit. Sequential Systems. Syntax Summary. Glossary.
1991 150pp Pbk ISBN 0-13-978529-9 (order from Amazon USA or Amazon UK)
Applications of Formal Methods []
New Jersey Institute of Technology
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
- Chapter 1 provides a comprehensive introduction to formal methods for non-specialists
- World-class contributors provide expert advice based on practical experience
- Real-life case studies show how to choose the most appropriate formal method for each task 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 ISBN 0-13-366949-1 (order from Amazon USA or Amazon UK)
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 ISBN 0-13-832544-8 (order from Amazon USA or Amazon UK)
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 best-selling 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
- includes various Z features which were omitted from the first edition such as theta, free types, schema normalisation and schema promotion
- additional case studies and exercises
- substantial re-working of the refinement chapters
- full discussion of the relationship between Z and object orientation and other current analysis and design methods.
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 ISBN 0-13-242207-7 (order from Amazon USA or Amazon UK)
Case Studies in Systematic Software Development] 
[]
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 ISBN 0-13-116088-5 (order from Amazon USA or Amazon UK)
Communication and Concurrency []
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.
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 ISBN 0-13-115007-3 (order from Amazon USA or Amazon UK)
Communicating Sequential Processes []
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 ISBN 0-13-153289-8 (order from Amazon USA or Amazon UK)
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 ISBN 0-13-092990-5 (order from Amazon USA or Amazon UK)
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 ISBN 0-13-651597-5 (order from Amazon USA or Amazon UK)
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 ISBN 0-13-711821-X (order from Amazon USA or Amazon UK)
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 ISBN 0-13-215849-3 (order from Amazon USA or Amazon UK)
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.
October 1996 200pp Pbk ISBN 0-13-398389-7 (order from Amazon USA or Amazon UK)
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 ISBN 0-13-182155-5 (order from Amazon USA or Amazon UK)
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
- covers advanced scheduling theory, as well as new specification and verification methods, linked together by consideration of a common, non-trivial example
- all chapters have exercises in the text as well as graded exercises at the end of every chapter
- focuses on a large scale case study which is specified and analysed using different methods.
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 ISBN 0-13-455297-0 (order from Amazon USA or Amazon UK)
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 ISBN 0-13-629031-0 (order from Amazon USA or Amazon UK)
Object-Oriented Databases []
John G. Hughes
University of Ulster
1991 350pp Pbk ISBN 0-13-629874-5 (order from Amazon USA or Amazon UK)
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
- emphasis on undertaking concepts, rather than giving formal proofs of the theorems
- new chapters on categories, distributive categories, monoidal categories and autonomous categories
- over 300 exercises allow readers to monitor their own progress
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 ISBN 0-13-323809-1 (order from Amazon USA or Amazon UK)
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 ISBN 0-13-915380-2 (order from Amazon USA or Amazon UK)
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
- compact and concise, the text fully explains the fundamentals of mathematics in an easy to read style
- difficult but crucial areas of the subject are developed by example and counter example
- chapters are designed to be read in isolation with minimal interdependence between them
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.
April 1996 356pp Pbk ISBN 0-13-234717-2 (order from Amazon USA or Amazon UK)
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 ISBN 0-13-297425-8 (order from Amazon USA or Amazon UK)
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 ISBN 0-13-334301-4 (order from Amazon USA or Amazon UK)
Mechanised Reasoning and Hardware Design []
Ed. C.A.R. Hoare↑
Ed. M.J.C. Gordon↑
1992 250pp Hbk ISBN 0-13-572405-8 (order from Amazon USA or Amazon UK)
Microprocessor Programming and Software Development []
F.G. Duncan
University of Bristol
1979 320pp Hbk ISBN 0-13-581405-7 (order from Amazon USA or Amazon UK)
High Level Programmer's Guide to the 68000 []
Francis Gregory McCabe
Imperial College of Science & Technology
1991 250pp Pbk ISBN 0-13-388034-6 (order from Amazon USA or Amazon UK)
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 ISBN 0-13-163065-2 (order from Amazon USA or Amazon UK)
A Classical Mind: Essays in Honour of C.A.R. Hoare []
Edited by A.W. Roscoe
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 ISBN 0-13-294844-3 (order from Amazon USA or Amazon UK)
Essays in Computer Science []
C.A.R. Hoare
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 ISBN 0-13-284027-8 (order from Amazon USA or Amazon UK)