撰稿者名单
译者序
前言
第一部分 模型与正确性
Section A 并行与交互
第1章 需要：并行性的组构方法
1.1 组构性
1.2 并发性的本质是干扰
1.3 推理干扰
1.4 关于假设/承诺推理的一些问题
1.5 寄生变量的作用
1.6 粒度所关心的事情
1.7 抽象的原子性及其精化
1.8 结论
1.9 致谢
参考文献
第2章 用契约强制行为
2.1 引言
2.2 契约
2.2.1 状态与状态变化
2.2.2 契约
2.2.3 操作语义
2.2.4 契约举例
2.2.5 行动系统
2.2.6 行动系统举例
2.3 利用契约达到目标
2.3.1 最弱的前置条件
2.3.2 正确性与成功策略
2.3.3 契约的精化
2.4 强制行为属性
2.4.1 分析行为
2.4.2 构造解释程序
2.4.3 其他暂态属性
2.5 分析行动系统的行为
2.5.1 行动系统的分类
2.5.2 分析行为
2.6 验证强制
2.6.1 谓词级正确性条件
2.6.2 基于不变量的方法
2.6.3 示范方法
2.6.4 例子系统中的强制性
2.7 结论及相关工作
参考文献
Section B 异步逻辑方法
第3章 异步进展
3.1 引言
3.2 程序
3.3 达成
3.4 退耦
3.5 举例——松耦合程序
3.6 异步安全
3.7 警告
3.8 结论
3.9 致谢
参考文献
第4章 并发面向对象程序简化定理
4.1 引言
4.2 Seuss程序设计符号
4.2.1 Seuss语法
4.2.2 Seuss语义（可选）
4.3 Seuss程序模型
4.4 对程序的限制
4.4.1 方框上的偏序
4.4.2 把过程看作关系
4.4.3 方框条件
4.5 兼容性
4.5.1 兼容性举例
4.5.2 兼容过程的半交换性
4.6 简化定理的证明
4.6.1 松执行
4.6.2 简化方案
4.7 结束语
4.8 致谢
参考文献
Section C 系统与实时性
第5章 抽象时间
第6章 实时精华的谓词语义
Section D 规定复杂的行为
第7章 系统描述的方面
第8章 建立动态系统的体系结构的模型
第9章 “方法是什么？”——关于域工程方面的一篇短文
第二部分 应用和自动机理论
Section E 面向对象
第10章 面向对象程序设计和软件开发——一种重要的评价方法
第11章 指针和对象的痕迹模型
第12章 作为堆不变量的对象模型
Section F 类型理论
第14章 类型系统
第15章 类型的含义是什么？——从本质到外在语义
第三部分 应用与自动机理论
Section G 通过自动机将理论应用于实践
第16章 利用推理、探索和抽象进行自动验证
第17章 特征工程实验
Section H 程序设计电路
第18章 高级电路设计
Section I 安全与保密
第19章 能量分析：攻击与防御策略
第20章 信息隐藏的概率方法
缺书网
扫码进群