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

商品描述(中文翻譯)

描述
在《Software Abstractions》中，Daniel Jackson 介紹了一種新的軟體設計方法，該方法借鑒了傳統的形式方法，但利用自動化工具儘早發現缺陷。這種方法——Jackson 稱之為「輕量級形式方法」或「敏捷建模」——從形式規範中提取了基於一小核心簡單且穩健概念的精確且表達力強的符號，但用完全自動化的分析取代了基於定理證明的傳統分析，這使設計者能夠立即獲得反饋。Jackson 開發了 Alloy，一種簡單而簡潔地捕捉軟體抽象本質的語言，使用最小的數學概念工具包。設計者可以利用自動化分析不僅修正錯誤，還能製作更精確和優雅的模型。Jackson 說，這種方法可以將設計者從「實現技術的泥潭」中拯救出來，讓他們重新深入思考基本概念。《Software Abstractions》介紹了這種方法的關鍵要素：一種邏輯，提供語言的基本構建塊；一種語言，為結構化描述的邏輯添加少量語法；以及一種分析，這是一種約束求解形式，提供模擬（生成樣本狀態和執行）和檢查（找到聲稱屬性的反例）。本書使用 Alloy 作為載體，因為它的簡單性和工具支持，但本書的教訓大多是語言無關的，也可以應用於其他建模語言的背景中。Daniel Jackson 是麻省理工學院電機工程與計算機科學系的教授，並領導計算機科學與人工智慧實驗室的軟體設計小組。

目錄
前言
致謝 xv
1 介紹
2 旋風之旅
2.1 靜態：探索狀態
2.2 動態：添加操作
2.3 分類層次
2.4 執行痕跡
2.5 總結
3 邏輯 33
3.1 三種邏輯合一
3.2 原子與關係
3.3 快照
3.4 運算子
3.5 約束
3.6 聲明與多重性約束
3.7 基數約束
4 語言 83
4.1 一個例子：自我祖父
4.2 簽名與欄位
4.3 模型圖
4.4 類型與類型檢查
4.5 事實、謂詞、函數與斷言
4.6 命令與範圍
4.7 模組與多型
4.8 整數與算術
5 分析 139
5.1 範圍完整分析
5.2 實例、範例與反例
5.3 無界的全稱量詞
5.4 範圍選擇與單調性
6 例子 169
6.1 環中的領導者選舉
6.2 酒店房間鎖定
6.3 媒體資產管理
6.4 記憶抽象
附錄 A：練習 229
A.1 邏輯練習
A.2 擴展簡單模型
A.3 經典謎題
A.4 元模型
A.5 小案例研究
A.6 開放式案例研究
附錄 B：Alloy 語言參考 253
B.1 詞彙問題
B.2 名稱空間
B.3 語法
B.4 優先級與結合性
B.5 語義基礎
B.6 類型與重載
B.7 語言特性
附錄 C：核心語義 291
C.1 Alloy 核心的語義
C.2 整數表達式與公式的語義
附錄 D：圖示符號 295
附錄 E：替代方法 297
E.1 一個例子
E.2 B
E.3 OCL
E.4 VDM
E.5 Z
參考文獻
索引

類似商品

最後瀏覽商品 (7)