
Software Engineering 1 : Abstraction and Modelling
Abstraction and Modelling
By: Dines Bjørner
Hardcover | 1 March 2005
At a Glance
756 Pages
23.5 x 15.88 x 3.18
Hardcover
$169.75
or 4 interest-free payments of $42.44 with
orShips in 5 to 7 business days
The art, craft, discipline, logic, practice, and science of developing large-scale software products needs a believable, professional base. The textbooks in this three-volume set combine informal, engineeringly sound practice with the rigour of formal, mathematics-based approaches.
Volume 1 covers the basic principles and techniques of formal methods abstraction and modelling. First this book provides a sound, but simple basis of insight into discrete mathematics: numbers, sets, Cartesians, types, functions, the Lambda Calculus, algebras, and mathematical logic. Then it trains its readers in basic property- and model-oriented specification principles and techniques. The model-oriented concepts that are common to such specification languages as B, VDM-SL, and Z are explained here using the RAISE specification language (RSL). This book then covers the basic principles of applicative (functional), imperative, and concurrent (parallel) specification programming. Finally, the volume contains a comprehensive glossary of software engineering, and extensive indexes and references.
These volumes are suitable for self-study by practicing software engineers and for use in university undergraduate and graduate courses on software engineering. Lecturers will be supported with a comprehensive guide to designing modules based on the textbooks, with solutions to many of the exercises presented, and with a complete set of lecture slides.
Industry Reviews
From the reviews:
"The book under review is the first one from a series of three volumes that provides a compelling framework for a more comprehensive understanding of both formal and practical concerns of software engineering. The major feature distinguishing these textbooks from other current ones ... is the natural manner in which the formal techniques smoothly glide from software design towards the requirements prescription phase and beyond to domain description. ... By its consistency and rigor, the book is, undoubtedly, remarkably useful to professional software developers." (Tudor Balanescu, Zentralblatt MATH, Vol. 1095 (21), 2006)
| Preface | p. VII |
| Reasons for Writing These Volumes | p. IX |
| Shortcomings of These Volumes | p. X |
| Methods of Approach | p. XII |
| A New Look at Software | p. XII |
| Formal Techniques "Light" | p. XIII |
| The "Super Programmer" | p. XIV |
| What Is Software Engineering? | p. XV |
| The Author's Aspirations | p. XVI |
| Role of These Volumes in an SE Education Programme | p. XVI |
| Why So Much Material? | p. XX |
| How to Use These Volumes in a Course | p. XX |
| Brief Guide to the Book | p. XXI |
| Guide to This Volume | p. XXI |
| Acknowledgments | p. XXIII |
| Opening | |
| Introduction | p. 3 |
| Setting the Stage | p. 3 |
| A Software Engineering Triptych | p. 7 |
| Documentation | p. 13 |
| Formal Techniques and Formal Tools | p. 25 |
| Method and Methodology | p. 31 |
| The Very Bases of Software | p. 33 |
| Aims and Objectives | p. 40 |
| Bibliographical Notes | p. 41 |
| Exercises | p. 41 |
| Discrete Mathematics | |
| Numbers | p. 45 |
| Introduction | p. 45 |
| Numerals and Numbers | p. 46 |
| Subsets of Numbers | p. 46 |
| Type Definitions: Numbers | p. 51 |
| Summary | p. 52 |
| Bibliographical Notes | p. 53 |
| Exercises | p. 53 |
| Sets | p. 55 |
| Background | p. 56 |
| Mathematical Sets | p. 56 |
| Special Sets | p. 58 |
| Sorts and Type Definitions: Sets | p. 58 |
| Sets in RSL | p. 59 |
| Bibliographical Notes | p. 60 |
| Exercises | p. 60 |
| Cartesians | p. 63 |
| The Issues | p. 63 |
| Cartesian-Valued Expressions | p. 64 |
| Cartesian Types | p. 64 |
| Cartesian Arity | p. 65 |
| Cartesian Equality | p. 66 |
| Some Construed Examples | p. 66 |
| Sorts and Type Definitions: Cartesians | p. 68 |
| Cartesians in RSL | p. 69 |
| Bibliographical Notes | p. 69 |
| Exercises | p. 69 |
| Types | p. 71 |
| Values and Types | p. 72 |
| Phenomena and Concept Types | p. 73 |
| Programming Language Type Concepts | p. 77 |
| Sorts or Abstract Types | p. 80 |
| Built-in and Concrete Types | p. 81 |
| Type Checking | p. 82 |
| Types as Sets, Types as Lattices | p. 84 |
| Summary | p. 84 |
| Exercises | p. 84 |
| Functions | p. 87 |
| General Overview | p. 89 |
| The Issues | p. 90 |
| How Do Functions Come About? | p. 94 |
| An Aside: On the Concept of Evaluation | p. 96 |
| Function Algebras | p. 98 |
| Currying and [lambda]-Notation | p. 103 |
| Relations and Functions | p. 104 |
| Type Definitions | p. 106 |
| Conclusion | p. 106 |
| Bibliographical Notes | p. 107 |
| Exercises | p. 107 |
| A [lambda]-Calculus | p. 109 |
| Informal Introduction | p. 110 |
| A "Pure" [lambda]-Calculus Syntax | p. 110 |
| A [lambda]-Calculus Pragmatics | p. 112 |
| A "Pure" [lambda]-Calculus Semantics | p. 112 |
| Call-by-Name Versus Call-by-Value | p. 116 |
| The Church-Rosser Theorems - Informal Version | p. 117 |
| The RSL [lambda]-Notation | p. 117 |
| Fix Points | p. 119 |
| Discussion | p. 122 |
| Bibliographical Notes | p. 123 |
| Exercises | p. 123 |
| Algebras | p. 127 |
| Introduction | p. 127 |
| Formal Definition of the Algebra Concept | p. 128 |
| How Do Algebras Come About? | p. 129 |
| Kinds of Algebras | p. 130 |
| Specification Algebras | p. 133 |
| RSL Syntax for Algebra Specifications | p. 137 |
| Discussion | p. 138 |
| Bibliographical Notes | p. 139 |
| Exercises | p. 139 |
| Mathematical Logic | p. 141 |
| The Issues | p. 142 |
| Proof Theory Versus Model Theory | p. 148 |
| A Language of Boolean Ground Terms | p. 156 |
| Languages of Propositional Logic | p. 165 |
| Languages of Predicate Logic | p. 171 |
| Axiom Systems | p. 186 |
| Summary | p. 196 |
| Bibliographical Notes | p. 197 |
| Exercises | p. 197 |
| Simple RSL | |
| General | p. 201 |
| RSL Versus VDM-SL, Z and B | p. 201 |
| What, Syntactically, Constitutes a Specification? | p. 202 |
| Towards an RSL "Standard" | p. 203 |
| RSL Tools | p. 203 |
| Atomic Types and Values in RSL | p. 205 |
| Introduction | p. 205 |
| The RSL Numbers | p. 206 |
| Enumerated Tokens | p. 208 |
| Characters and Texts | p. 212 |
| Identifiers and General Tokens | p. 213 |
| Discussion | p. 216 |
| Exercises | p. 217 |
| Function Definitions in RSL | p. 221 |
| The Function Type | p. 221 |
| Model-Oriented Explicit Definitions | p. 222 |
| Model-Oriented Axiomatic Definitions | p. 223 |
| Model-Oriented pre/post-Condition Definitions | p. 224 |
| Property-Oriented Axiomatic Definitions | p. 226 |
| Property-Oriented Algebraic Definitions | p. 227 |
| Summary of RSL Function Definition Styles | p. 228 |
| Discussion | p. 229 |
| Exercises | p. 229 |
| Property-Oriented and Model-Oriented Abstraction | p. 231 |
| Abstraction | p. 232 |
| Property-Oriented Abstractions | p. 235 |
| Model Versus Property Abstractions | p. 241 |
| Model-Oriented Abstractions | p. 250 |
| Principles, Techniques and Tools | p. 254 |
| Exercises | p. 260 |
| Sets in RSL | p. 263 |
| Sets: The Issues | p. 264 |
| The Set Data Type | p. 265 |
| Examples of Set-Based Abstractions | p. 273 |
| Abstracting and Modelling With Sets | p. 276 |
| Inductive Set Definitions | p. 284 |
| A Comment on Varying Sets | p. 287 |
| Principles, Techniques and Tools | p. 288 |
| Discussion | p. 289 |
| Bibliographical Notes | p. 289 |
| Exercises | p. 289 |
| Cartesians in RSL | p. 295 |
| Cartesians: The Issues | p. 295 |
| The Cartesian Data Type | p. 296 |
| Examples of Cartesian Abstractions | p. 300 |
| Abstracting and Modelling with Cartesians | p. 303 |
| Inductive Cartesian Definitions | p. 312 |
| Discussion | p. 315 |
| Exercises | p. 316 |
| Lists in RSL | p. 321 |
| Issues Related to Lists | p. 322 |
| The List Data Type | p. 322 |
| Small Examples of List-Based Abstractions | p. 328 |
| Abstracting and Modelling with Lists | p. 333 |
| Inductive List Definitions | p. 340 |
| A Review of List Abstractions and Models | p. 342 |
| Lists: A Discussion | p. 343 |
| Exercises | p. 343 |
| Maps in RSL | p. 349 |
| The Issues | p. 350 |
| The Map Data Type | p. 350 |
| Examples of Map-Based Abstractions | p. 356 |
| Abstracting and Modelling with Maps | p. 358 |
| Inductive Map Definitions | p. 383 |
| A Review of Map Abstractions and Models | p. 386 |
| Maps: A Discussion | p. 388 |
| Exercises | p. 388 |
| Higher-Order Functions in RSL | p. 393 |
| Functions: The Issues | p. 393 |
| Examples Using Function-Based Abstractions | p. 394 |
| Abstracting and Modelling With Functions | p. 395 |
| Inductive Function Definitions | p. 406 |
| Review of Function Abstractions and Models | p. 407 |
| Discussion | p. 408 |
| Exercises | p. 408 |
| Specification Types | |
| Types in RSL | p. 413 |
| The Issues | p. 413 |
| Type Categories | p. 415 |
| Enumerated Token Types Revisited | p. 416 |
| Records: Constructors and Destructors | p. 417 |
| Union Type Definitions | p. 420 |
| Short Record Type Definitions | p. 421 |
| Type Expressions, Revisited | p. 421 |
| Subtypes | p. 422 |
| Type Definitions, Revisited | p. 422 |
| On Recursive Type Definitions | p. 423 |
| Discussion | p. 423 |
| Bibliographical Notes | p. 424 |
| Exercises | p. 424 |
| Specification Programming | |
| On Specification Programming | p. 427 |
| On Problems and Exercises | p. 428 |
| Applicative Specification Programming | p. 429 |
| Scope and Binding | p. 430 |
| Intuition | p. 435 |
| Operator/Operand Expressions | p. 438 |
| Enumerated and Comprehended Expressions | p. 438 |
| Conditional Expressions | p. 439 |
| Bindings, Typings, Patterns and Matching | p. 440 |
| Review and Discussion | p. 455 |
| Bibliographical Notes | p. 455 |
| Exercises | p. 456 |
| Imperative Specification Programming | p. 467 |
| Intuition | p. 468 |
| Imperative Combinators: A [lambda]-Calculus | p. 468 |
| Variable References: Pointers | p. 473 |
| Function Definitions and Expressions | p. 480 |
| Translations: Applicative to Imperative | p. 486 |
| Styles of Configuration Modelling | p. 495 |
| Review and Discussion | p. 505 |
| Bibliographical Notes | p. 506 |
| Exercises | p. 508 |
| Concurrent Specification Programming | p. 511 |
| Behaviour and Process Abstractions | p. 512 |
| Intuition | p. 514 |
| Communicating Sequential Processes, CSP | p. 532 |
| The RSL/CSP Process Combinators | p. 537 |
| Translation Schemas | p. 543 |
| Parallelism and Concurrency: A Discussion | p. 547 |
| Bibliographical Notes | p. 548 |
| Exercises | p. 548 |
| And So On! | |
| Etcetera! | p. 557 |
| What Have We Covered? | p. 557 |
| What Is Next? | p. 557 |
| What Is Next-Next? | p. 558 |
| A Caveat | p. 559 |
| Formal Methods "Lite" | p. 559 |
| Bibliographical Notes | p. 560 |
| Appendixes | |
| Common Exercise Topics | p. 563 |
| Transportation Nets | p. 563 |
| Container Logistics | p. 564 |
| Financial Service Industry | p. 564 |
| Summary References to Exercises | p. 566 |
| Glossary | p. 567 |
| Categories of Reference Lists | p. 568 |
| Typography and Spelling | p. 569 |
| The Glosses | p. 570 |
| Indexes | p. 649 |
| Symbols Index | p. 650 |
| Concepts Index | p. 656 |
| Characterisations and Definitions Index | p. 680 |
| Authors Index | p. 682 |
| References | p. 687 |
| Table of Contents provided by Ingram. All Rights Reserved. |
ISBN: 9783540211495
ISBN-10: 3540211497
Series: Texts in Theoretical Computer Science. An EATCS Series
Published: 1st March 2005
Format: Hardcover
Language: English
Number of Pages: 756
Audience: College, Tertiary and University
Publisher: Springer Nature B.V.
Country of Publication: DE
Dimensions (cm): 23.5 x 15.88 x 3.18
Weight (kg): 1.17
Shipping
| Standard Shipping | Express Shipping | |
|---|---|---|
| Metro postcodes: | $9.99 | $14.95 |
| Regional postcodes: | $9.99 | $14.95 |
| Rural postcodes: | $9.99 | $14.95 |
Orders over $79.00 qualify for free shipping.
How to return your order
At Booktopia, we offer hassle-free returns in accordance with our returns policy. If you wish to return an item, please get in touch with Booktopia Customer Care.
Additional postage charges may be applicable.
Defective items
If there is a problem with any of the items received for your order then the Booktopia Customer Care team is ready to assist you.
For more info please visit our Help Centre.
You Can Find This Book In

Architecture Patterns with Python
Enabling Test-Driven Development, Domain-Driven Design, and Event-Driven Microservices
Paperback
RRP $125.75
$60.99
OFF
This product is categorised by
- Non-FictionComputing & I.T.Computer ScienceSystems Analysis & Design
- Non-FictionComputing & I.T.Computer Programming & Software DevelopmentSoftware Engineering
- Non-FictionComputing & I.T.Computer Programming & Software DevelopmentProgramming & Scripting Languages
- Non-FictionComputing & I.T.Computer ScienceComputer Architecture & Logic Design























