程序設(shè)計(jì)方法學(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章　用契約強(qiáng)制行為
　　2.1　引言
　　2.2　契約
　　　2.2.1　狀態(tài)與狀態(tài)變化
　　　2.2.2　契約
　　　2.2.3　操作語義
　　　2.2.4　契約舉例
　　　2.2.5　行動(dòng)系統(tǒng)
　　　2.2.6　行動(dòng)系統(tǒng)舉例
　　2.3　利用契約達(dá)到目標(biāo)
　　　2.3.1　最弱的前置條件
　　　2.3.2　正確性與成功策略
　　　2.3.3　契約的精化
　　2.4　強(qiáng)制行為屬性
　　　2.4.1　分析行為
　　　2.4.2　構(gòu)造解釋程序
　　　2.4.3　其他暫態(tài)屬性
　　2.5　分析行動(dòng)系統(tǒng)的行為
　　　2.5.1　行動(dòng)系統(tǒng)的分類
　　　2.5.2　分析行為
　　2.6　驗(yàn)證強(qiáng)制
　　　2.6.1　謂詞級(jí)正確性條件
　　　2.6.2　基于不變量的方法
　　　2.6.3　示范方法
　　　2.6.4　例子系統(tǒng)中的強(qiá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ū)ο蟪绦蚝?jiǎn)化定理
　　4.1　引言
　　4.2　Seuss程序設(shè)計(jì)符號(hào)
　　　4.2.1　Seuss語法
　　　4.2.2　Seuss語義（可選）
　　4.3　Seuss程序模型
　　4.4　對(duì)程序的限制
　　　4.4.1　方框上的偏序
　　　4.4.2　把過程看作關(guān)系
　　　4.4.3　方框條件
　　4.5　兼容性
　　　4.5.1　兼容性舉例
　　　4.5.2　兼容過程的半交換性
　　4.6　簡(jiǎn)化定理的證明
　　　4.6.1　松執(zhí)行
　　　4.6.2　簡(jiǎn)化方案
　　4.7　結(jié)束語
　　4.8　致謝
　　參考文獻(xiàn)
　Section C　系統(tǒng)與實(shí)時(shí)性
　第5章　抽象時(shí)間
　第6章　實(shí)時(shí)精華的謂詞語義
　Section D　規(guī)定復(fù)雜的行為
　第7章　系統(tǒng)描述的方面
　第8章　建立動(dòng)態(tài)系統(tǒng)的體系結(jié)構(gòu)的模型
　第9章　“方法是什么？”——關(guān)于域工程方面的一篇短文
第二部分　應(yīng)用和自動(dòng)機(jī)理論
　Section E　面向?qū)ο?br />　第10章　面向?qū)ο蟪绦蛟O(shè)計(jì)和軟件開發(fā)——一種重要的評(píng)價(jià)方法
　第11章　指針和對(duì)象的痕跡模型
　第12章　作為堆不變量的對(duì)象模型
　Section F　類型理論
　第14章　類型系統(tǒng)
　第15章　類型的含義是什么？——從本質(zhì)到外在語義
第三部分　應(yīng)用與自動(dòng)機(jī)理論
　Section G　通過自動(dòng)機(jī)將理論應(yīng)用于實(shí)踐
　第16章　利用推理、探索和抽象進(jìn)行自動(dòng)驗(yàn)證
　第17章　特征工程實(shí)驗(yàn)
　Section H　程序設(shè)計(jì)電路
　第18章　高級(jí)電路設(shè)計(jì)
　Section I　安全與保密
　第19章　能量分析：攻擊與防御策略
　第20章　信息隱藏的概率方法