- 1 Computer Science: A Modern Introduction, 2/e
- 2 ADA: Language and Methodology
- 3 Introduction to Modula-2
- 4 Introduction to Pascal, 3/e
- 5 Programming in occam 2
- 6 occam 2 Reference Manual
- 7 Programming Language Paradigms
- 8 Programming from Specifications, 2/e
- 9 Programming: The Derivation of Algorithms
- 10 Partial Evaluation and Automatic Program Generation
- 11 Verifiable Programming
- 12 Abstract Data Types and Modula-2
- 13 Systematic Software Development Using VDM, 2/e
- 14 Reasoned Programming
- 15 Programming Language Theory and its Implementation: Applicative and Imperative Paradigms
- 16 Introduction to the Theory of Programming Languages
- 17 Semantics of Programming Languages
- 18 Programming Language Concepts and Paradigms
- 19 Semantics of Sequential and Parallel Programs
- 20 Programming Language Syntax and Semantics
- 21 Introduction to Functional Programming
- 22 Functional Programming Using Standard ML
- 23 An Introduction to Logic Programming Through Prolog
- 24 Computation as Logic
- 25 Logic and its Applications
- 26 Mathematical Logic for Computer Science
- 27 From Logic Programming to Prolog
- 28 Compiler Construction: A Recursive Descent Model
- 29 Implementation of Functional Programming Languages
- 30 Programming Language Processors
- 31 Database Programming Languages
- 32 Foundations of Semantic Databases
- 33 Using Z: Specification, Refinement and Proof
- 34 The Z Notation: A Reference Manual, 2/e
- 35 Applications of Formal Methods
- 36 Specification Case Studies, 2/e
- 37 Introduction to Formal Specification and Z, 2/e
- 38 Case Studies in Systematic Software Development]
- 39 Communication and Concurrency
- 40 Communicating Sequential Processes
- 41 Finite Transition Systems
- 42 Parallel Numerical Algorithms
- 43 Principles of Concurrent and Distributed Programming
- 44 Distributed Systems and Computer Networks
- 45 Distributed Systems Analysis with CCS
- 46 Principles of Protocol Design
- 47 Real-time Systems: Specification, Verification and Analysis
- 48 Object-Oriented Software Construction
- 49 Object-Oriented Databases
- 50 Category Theory for Computing Science, 2/e
- 51 Introduction to the Theory of Complexity
- 52 Mathematics for Computer Science
- 53 Cornerstones of Undecidibility
- 54 Computer Arithmetic Systems: Algorithms, Architecture and Implementation
- 55 Mechanised Reasoning and Hardware Design
- 56 Microprocessor Programming and Software Development
- 57 High Level Programmer's Guide to the 68000
- 58 Computer and Communication Systems Performance Modelling
- 59 A Classical Mind: Essays in Honour of C.A.R. Hoare
- 60 Essays in Computer Science
Computer Science: A Modern Introduction, 2/e [edit | edit source]
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.
ADA: Language and Methodology [edit | edit source]
David A. Watt, Brian A. Wichman, and William Findlay
University of Glasgow
Introduction to Modula-2 [edit | edit source]
University of Queensland
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.
Introduction to Pascal, 3/e [edit | edit source]
University of Queensland
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.
Programming in occam 2 [edit | edit source]
Geraint Jones and Michael Goldsmith
University of Oxford
occam 2 Reference Manual [edit | edit source]
Programming Language Paradigms [edit | edit source]
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.
Programming from Specifications, 2/e [edit | edit source]
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.
Programming: The Derivation of Algorithms [edit | edit source]
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.
Teachers Manual Available
Partial Evaluation and Automatic Program Generation [edit | edit source]
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.
Verifiable Programming [edit | edit source]
Abstract Data Types and Modula-2 [edit | edit source]
University of Brighton
Systematic Software Development Using VDM, 2/e [edit | edit source]
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
Reasoned Programming [edit | edit source]
Krysia Broda, Susan Eisenbach, Hessam Khoshnevisan and Steve Vickers
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.
Programming Language Theory and its Implementation: Applicative and Imperative Paradigms [edit | edit source]
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.
Introduction to the Theory of Programming Languages [edit | edit source]
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.
Semantics of Programming Languages [edit | edit source]
Queen's University, Kingston
Programming Language Concepts and Paradigms [edit | edit source]
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.
Semantics of Sequential and Parallel Programs [edit | edit source]
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.
Programming Language Syntax and Semantics [edit | edit source]
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.
Introduction to Functional Programming [edit | edit source]
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.
Functional Programming Using Standard ML [edit | edit source]
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.
An Introduction to Logic Programming Through Prolog [edit | edit source]
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.
- 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.
Computation as Logic [edit | edit source]
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.
Logic and its Applications [edit | edit source]
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.
Mathematical Logic for Computer Science [edit | edit source]
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.
From Logic Programming to Prolog [edit | edit source]
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.
Compiler Construction: A Recursive Descent Model [edit | edit source]
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.
Implementation of Functional Programming Languages [edit | edit source]
Simon L. Peyton-Jones
University of Glasgow
Programming Language Processors [edit | edit source]
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.
Database Programming Languages [edit | edit source]
University of Manchester
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.
Foundations of Semantic Databases [edit | edit source]
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.
Using Z: Specification, Refinement and Proof [edit | edit source]
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.
- 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.
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 [edit | edit source]
…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.
Applications of Formal Methods [edit | edit source]
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.
- 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.
Specification Case Studies, 2/e [edit | edit source]
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.
Introduction to Formal Specification and Z, 2/e [edit | edit source]
University of Hertfordshire
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.
- 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.
Case Studies in Systematic Software Development] [edit | edit source]
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.
Communication and Concurrency [edit | edit source]
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.
Communicating Sequential Processes [edit | edit source]
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.
Contents: Processes. Concurrency. Non-determinism. Communication. Sequential Processes. Shared Resources. Discussion. Bibliography. Index.
Finite Transition Systems [edit | edit source]
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.
Parallel Numerical Algorithms [edit | edit source]
University of Manchester
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.
Principles of Concurrent and Distributed Programming [edit | edit source]
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.
Distributed Systems and Computer Networks [edit | edit source]
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.
Distributed Systems Analysis with CCS [edit | edit source]
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.
Principles of Protocol Design [edit | edit source]
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.
Real-time Systems: Specification, Verification and Analysis [edit | edit source]
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.
- 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.
Object-Oriented Software Construction [edit | edit source]
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.
Object-Oriented Databases [edit | edit source]
John G. Hughes
University of Ulster
Category Theory for Computing Science, 2/e [edit | edit source]
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.
- 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.
Supplement available from: ftp://triples.math.mcgill.ca/pub/barr/ctcs.elec.supp.dvi
Introduction to the Theory of Complexity [edit | edit source]
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.
Mathematics for Computer Science [edit | edit source]
Universite Bordeaux 1
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.
- 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.
Cornerstones of Undecidibility [edit | edit source]
University of Leiden
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.
Computer Arithmetic Systems: Algorithms, Architecture and Implementation [edit | edit source]
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.
Mechanised Reasoning and Hardware Design [edit | edit source]
Ed. C.A.R. Hoare↑
Ed. M.J.C. Gordon↑
Microprocessor Programming and Software Development [edit | edit source]
University of Bristol
High Level Programmer's Guide to the 68000 [edit | edit source]
Francis Gregory McCabe
Imperial College of Science & Technology
Computer and Communication Systems Performance Modelling [edit | edit source]
Peter J.B. King
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 [edit | edit source]
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 [edit | edit source]
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)