Software Abstractions: Logic, Language, and Analysis

Front Cover
MIT Press, 2012 - Computers - 354 pages

An approach to software design that introduces a fully automated analysis giving designers immediate feedback, now featuring the latest version of the Alloy language.

In Software Abstractions Daniel Jackson introduces an approach to software design that draws on traditional formal methods but exploits automated tools to find flaws as early as possible. This approach—which Jackson calls “lightweight formal methods” or “agile modeling”—takes from formal specification the idea of a precise and expressive notation based on a tiny core of simple and robust concepts but replaces conventional analysis based on theorem proving with a fully automated analysis that gives designers immediate feedback. Jackson has developed Alloy, a language that captures the essence of software abstractions simply and succinctly, using a minimal toolkit of mathematical notions. This revised edition updates the text, examples, and appendixes to be fully compatible with Alloy 4.

 

Contents

Introduction
1
A Whirlwind Tour
5
Logic
33
Language
85
Analysis
141
Examples
171
Exercises
233
Alloy Language Reference
259
Kernel Semantics
295
Diagrammatic Notation
299
Alternative Approaches
301
References
337
Index
345
Copyright

Other editions - View all

Software Abstractions, revised edition: Logic, Language, and Analysis
Daniel Jackson
Limited preview - 2016
Software Abstractions: Logic, Language, and Analysis
Daniel Jackson
Limited preview - 2006
Software Abstractions: Logic, Language and Analysis
Daniel Jackson
Snippet view - 2006
View all »

Common terms and phrases

abstract Addr address book Alias allows Alloy analysis analyzer appear applied argument assertion assigned associated atoms binary boolean bound cards column command components condition constraint contains contents corresponding counterexample declaration defined denotes described Directory Discussion domain elements empty entry equivalent exactly example execution expr expression extends fact field formula function given gives Group guest holds implies imported initial instance integers introduce join keyword language lock logic lone lookup machine mapping means memory module multiplicity Note Object operation particular possible predicate problem Process properties quantified refer relation represent require result Room says scalar scope selection shown signature simple single step structure style subset takes tion tool trace transitive true tuple union univ variables write written

About the author (2012)

Daniel Jackson is a photographer and Professor of Computer Science at MIT. His images of contemporary laboratories were shown at the MIT Museum in conjunction with a major exhibit of Berenice Abbott's MIT work in 2012, and other images have appeared in group shows nationwide.

Bibliographic information

TitleSoftware Abstractions: Logic, Language, and Analysis
The MIT Press
AuthorDaniel Jackson
Editionillustrated, revised
PublisherMIT Press, 2012
ISBN0262017156, 9780262017152
Length354 pages
Subjects ›  › 

Computers / Computer Science
Computers / Programming / General
Computers / Software Development & Engineering / General
Computers / Software Development & Engineering / Systems Analysis & Design
  
Export CitationBiBTeX EndNote RefMan