程序設(shè)計方法學(xué)

撰稿者名單
譯者序
前言
第一部分　模型與正確性
　Section A　并行與交互
　第1章　需要：并行性的組構(gòu)方法
　　1.1　組構(gòu)性
　　1.2　并發(fā)性的本質(zhì)是干擾
　　1.3　推理干擾
　　1.4　關(guān)于假設(shè)/承諾推理的一些問題
　　1.5　寄生變量的作用
　　1.6　粒度所關(guān)心的事情
　　1.7　抽象的原子性及其精化
　　1.8　結(jié)論
　　1.9　致謝
　　參考文獻(xiàn)
　第2章　用契約強制行為
　　2.1　引言
　　2.2　契約
　　　2.2.1　狀態(tài)與狀態(tài)變化
　　　2.2.2　契約
　　　2.2.3　操作語義
　　　2.2.4　契約舉例
　　　2.2.5　行動系統(tǒng)
　　　2.2.6　行動系統(tǒng)舉例
　　2.3　利用契約達(dá)到目標(biāo)
　　　2.3.1　最弱的前置條件
　　　2.3.2　正確性與成功策略
　　　2.3.3　契約的精化
　　2.4　強制行為屬性
　　　2.4.1　分析行為
　　　2.4.2　構(gòu)造解釋程序
　　　2.4.3　其他暫態(tài)屬性
　　2.5　分析行動系統(tǒng)的行為
　　　2.5.1　行動系統(tǒng)的分類
　　　2.5.2　分析行為
　　2.6　驗證強制
　　　2.6.1　謂詞級正確性條件
　　　2.6.2　基于不變量的方法
　　　2.6.3　示范方法
　　　2.6.4　例子系統(tǒng)中的強制性
　　2.7　結(jié)論及相關(guān)工作
　　參考文獻(xiàn)
　Section B　異步邏輯方法
　第3章　異步進(jìn)展
　　3.1　引言
　　3.2　程序
　　3.3　達(dá)成
　　3.4　退耦
　　3.5　舉例——松耦合程序
　　3.6　異步安全
　　3.7　警告
　　3.8　結(jié)論
　　3.9　致謝
　　參考文獻(xiàn)
　第4章　并發(fā)面向?qū)ο蟪绦蚝喕ɡ?br />　　4.1　引言
　　4.2　Seuss程序設(shè)計符號
　　　4.2.1　Seuss語法
　　　4.2.2　Seuss語義（可選）
　　4.3　Seuss程序模型
　　4.4　對程序的限制
　　　4.4.1　方框上的偏序
　　　4.4.2　把過程看作關(guān)系
　　　4.4.3　方框條件
　　4.5　兼容性
　　　4.5.1　兼容性舉例
　　　4.5.2　兼容過程的半交換性
　　4.6　簡化定理的證明
　　　4.6.1　松執(zhí)行
　　　4.6.2　簡化方案
　　4.7　結(jié)束語
　　4.8　致謝
　　參考文獻(xiàn)
　Section C　系統(tǒng)與實時性
　第5章　抽象時間
　第6章　實時精華的謂詞語義
　Section D　規(guī)定復(fù)雜的行為
　第7章　系統(tǒng)描述的方面
　第8章　建立動態(tài)系統(tǒng)的體系結(jié)構(gòu)的模型
　第9章　“方法是什么？”——關(guān)于域工程方面的一篇短文
第二部分　應(yīng)用和自動機理論
　Section E　面向?qū)ο?br />　第10章　面向?qū)ο蟪绦蛟O(shè)計和軟件開發(fā)——一種重要的評價方法
　第11章　指針和對象的痕跡模型
　第12章　作為堆不變量的對象模型
　Section F　類型理論
　第14章　類型系統(tǒng)
　第15章　類型的含義是什么？——從本質(zhì)到外在語義
第三部分　應(yīng)用與自動機理論
　Section G　通過自動機將理論應(yīng)用于實踐
　第16章　利用推理、探索和抽象進(jìn)行自動驗證
　第17章　特征工程實驗
　Section H　程序設(shè)計電路
　第18章　高級電路設(shè)計
　Section I　安全與保密
　第19章　能量分析：攻擊與防御策略
　第20章　信息隱藏的概率方法