Software Abstractions: Logic, Language, and Analysis (Paperback)

Daniel Jackson

Software Abstractions: Logic, Language, and Analysis (Paperback)
  • 出版商: MIT
  • 出版日期: 2006-03-24
  • 售價: $1,640
  • 貴賓價: 9.8 折 $1,607
  • 語言: 英文
  • 頁數: 366
  • 裝訂: Hardcover
  • ISBN: 0262101149
  • ISBN-13: 9780262101141
  • 相關分類: Design Pattern 、軟體工程

    • 立即出貨(限量) (庫存=2)

買這商品的人也買了...

相關主題

商品描述

Description

In Software Abstractions Daniel Jackson introduces a new 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. The designer can use automated analysis not only to correct errors but also to make models that are more precise and elegant. This approach, Jackson says, can rescue designers from "the tarpit of implementation technologies" and return them to thinking deeply about underlying concepts.

Software Abstractions introduces the key elements of the approach: a logic, which provides the building blocks of the language; a language, which adds a small amount of syntax to the logic for structuring descriptions; and an analysis, a form of constraint solving that offers both simulation (generating sample states and executions) and checking (finding counterexamples to claimed properties). The book uses Alloy as a vehicle because of its simplicity and tool support, but the book's lessons are mostly language-independent, and could also be applied in the context of other modeling languages.

Daniel Jackson is Professor in the Department of Electrical Engineering and Computer Science and leads the Software Design Group at the Computer Science and Artificial Intelligence Lab at MIT.

 

Table of Contents

Preface
 
 Acknowledgments xv
 
1 Introduction
 
2 A Whirlwind Tour
 
      2.1 Statics: Exploring States 
 
      2.2 Dynamics: Adding Operations 
 
      2.3 Classification Hierarchy 
 
      2.4 Execution Traces 
 
      2.5 Summary 
 
3 Logic 33
 
      3.1 Three Logics in One 
 
      3.2 Atoms and Relations 
 
      3.3 Snapshots 
 
      3.4 Operators 
 
      3.5 Constraints 
 
      3.6 Declarations and Multiplicity Constraints 
 
      3.7 Cardinality Constraints 
 
4 Language 83
 
      4.1 An Example: Self-Grandpas 
 
      4.2 Signatures and Fields 
 
      4.3 Model Diagrams 
 
      4.4 Types and Type Checking 
 
      4.5 Facts, Predicates, Functions, and Assertions 
 
      4.6 Commands and Scope 
 
      4.7 Modules and Polymorphism 
 
      4.8 Integers and Arithmetic 
 
5 Analysis  139
 
      5.1 Scope-Complete Analysis 
 
      5.2 Instances, Examples, and Counterexamples 
 
      5.3 Unbounded Universal Quantifiers 
 
      5.4 Scope Selection and Monotonicity 
 
6 Examples  169
 
      6.1 Leader Election in a Ring 
 
      6.2 Hotel Room Locking 
 
      6.3 Media Asset Management 
 
      6.4 Memory Abstractions 
 
 Appendix A: Exercises 229
 
      A.1 Logic Exercises 
 
      A.2 Extending Simple Models 
 
      A.3 Classic Puzzles 
 
      A.4 Metamodels 
 
      A.5 Small Case Studies 
 
      A.6 Open-Ended Case Studies 
 
 Appendix B: Alloy Language Reference  253
 
      B.1 Lexical Issues 
 
      B.2 Namespaces 
 
      B.3 Grammar 
 
      B.4 Precedence and Associativity 
 
      B.5 Semantic Basis 
 
      B.6 Types and Overloading 
 
      B.7 Language Features 
 
 Appendix C: Kernel Semantics  291
 
      C.1 Semantics of the Alloy Kernel 
 
      C.2 Semantics of Integer Expressions and Formulas 
 
 Appendix D: Diagrammatic Notation  295
 
 Appendix E: Alternative Approaches  297
 
      E.1 An Example 
 
      E.2 B 
 
      E.3 OCL 
 
      E.4 VDM 
 
      E.5 Z 
 
 References
 
 Index

商品描述(中文翻譯)

描述

在《軟體抽象》一書中，丹尼爾·傑克遜介紹了一種新的軟體設計方法，該方法借鑒了傳統的形式化方法，但利用自動化工具盡早發現缺陷。這種方法，傑克遜稱之為“輕量級形式化方法”或“敏捷建模”，它從形式化規範中借鑒了基於簡單且堅固概念的精確和表達力強的符號，但用全自動化分析取代了基於定理證明的傳統分析，從而為設計師提供即時反饋。傑克遜開發了一種名為Alloy的語言，它以簡潔明瞭的方式捕捉軟體抽象的本質，並使用最小的數學概念工具。設計師不僅可以使用自動化分析來糾正錯誤，還可以製作更精確和優雅的模型。傑克遜表示，這種方法可以拯救設計師免於“實現技術的泥潭”，使他們重新深入思考底層概念。

《軟體抽象》介紹了這種方法的關鍵要素：一種邏輯，提供語言的基本構建塊；一種語言，將少量語法添加到邏輯中以結構化描述；以及一種分析方法，一種約束求解方法，既可以進行模擬（生成樣本狀態和執行）又可以進行檢查（找到對所聲明的屬性的反例）。本書選擇使用Alloy作為載體，因為它簡單且具有工具支持，但本書的教訓大多數與語言無關，也可以應用於其他建模語言的上下文中。

丹尼爾·傑克遜是麻省理工學院電機工程與計算機科學系的教授，並領導著該學院的軟體設計小組。

目錄

前言
致謝
1 引言
2 一場旋風之旅
2.1 靜態：探索狀態
2.2 動態：添加操作
2.3 分類層次
2.4 執行軌跡
2.5 總結
3 邏輯
3.1 三種邏輯合一
3.2 原子和關係
3.3 快照
3.4 運算符
3.5 約束
3.6 声明和多重性約束
3.7 基數約束

類似商品