程序设计方法学PDF电子书下载

第一部分 模型与正确性 1

Section A 并行与交互 1

第1章 需要：并行性的组构方法 3

1.1 组构性 3

1.2 并发性的本质是干扰 4

1.3 推理干扰 5

1.4 关于假设／承诺推理的一些问题 7

1.5 寄生变量的作用 7

1.6 粒度所关心的事情 7

1.7 抽象的原子性及其精化 8

1.8 结论 8

1.9 致谢 8

参考文献 9

第2章 用契约强制行为 11

2.1 引言 11

2.2 契约 12

2.2.1 状态与状态变化 12

2.2.2 契约 13

2.2.3 操作语义 14

2.2.4 契约举例 15

2.2.5 行动系统 16

2.2.6 行动系统举例 17

2.3 利用契约达到目标 18

2.3.1 最弱的前置条件 18

2.3.2 正确性与成功策略 20

2.3.3 契约的精化 22

2.4 强制行为属性 23

2.4.1 分析行为 23

2.4.2 构造解释程序 24

2.4.3 其他暂态属性 25

2.5 分析行动系统的行为 27

2.5.1 行动系统的分类 27

2.5.2 分析行为 28

2.6 验证强制 30

2.6.1 谓词级正确性条件 30

2.6.2 基于不变量的方法 31

2.6.3 示范方法 32

2.6.4 例子系统中的强制性 33

2.7 结论及相关工作 36

参考文献 36

Section B 异步逻辑方法 38

第3章 异步进展 40

3.1 引言 40

3.2 程序 41

3.3 达成 43

3.4 退耦 44

3.5 举例——松耦合程序 45

3.6 异步安全 46

3.7 警告 47

3.8 结论 48

3.9 致谢 48

参考文献 48

第4章 并发面向对象程序简化定理 50

4.1 引言 50

4.2 Seuss程序设计符号 51

4.2.1 Seuss语法 52

4.2.2 Seuss语义（可选） 55

4.3 Seuss程序模型 56

4.4 对程序的限制 58

4.4.1 方框上的偏序 58

4.4.2 把过程看作关系 59

4.4.3 方框条件 60

4.5 兼容性 61

4.5.1 兼容性举例 61

4.5.2 兼容过程的半交换性 62

4.6 简化定理的证明 64

4.6.1 松执行 64

4.6.2 简化方案 65

4.7 结束语 66

4.8 致谢 67

参考文献 67

Section C 系统与实时性 68

第5章 抽象时间 70

5.1 引言 70

5.2 流 70

5.2.1 数学基础：流 71

5.2.2 建时间模型 71

5.3 把组件看作流函数 73

5.4 时间抽象 74

5.4.1 抽象的一般概念 74

5.4.2 抽象时间 75

5.5 结论 76

5.5.1 文献中的时间模型 76

5.5.2 结语 77

5.6 致谢 77

参考文献 78

第6章 实时精化的谓词语义 80

6.1 背景知识 80

6.2 语言和语义 81

6.2.1 实时规范命令 83

6.2.2 简单实时命令 86

6.2.3 顺序组合 86

6.2.4 不确定选择、条件和挑选 88

6.2.5 局部和辅助变量 90

6.3 一个例子 91

6.4 循环 93

6.5 定时约束分析 96

6.6 结论 97

6.7 致谢 98

参考文献 98

Section D 规定复杂的行为 100

第7章 系统描述的方面 102

7.1 引言 102

7.2 符号处理 102

7.3 机器和领域 104

7.3.1 规范接口 104

7.3.2 需求接口 104

7.3.3 系统描述 104

7.3.4 有目的的描述 105

7.3.5 为什么需要单独的描述 106

7.4 描述实际领域 107

7.4.1 标记 107

7.4.2 使用定义 108

7.4.3 区分定义和描述 109

7.5 描述与模型 109

7.5.1 电梯模型 110

7.5.2 模型的关系 111

7.5.3 实际模型 112

7.5.4 描述模型和所建模的域 112

7.6 问题分解与描述结构 113

7.6.1 检查子问题 113

7.6.2 诸多的矛盾 114

7.6.3 身份关注点 114

7.6.4 病人监测 115

7.7 软件开发的前景 115

7.7.1 无意义的规范 116

7.7.2 离散复杂性 116

7.8 致谢 117

参考文献 117

第8章 建立动态系统的体系结构的模型 118

8.1 引言 118

8.1.1 动态系统 118

8.1.2 连续变化的情境 118

8.2 动态系统的模型 119

8.2.1 ARC的符号 119

8.2.2 模型的确认 122

8.3 适于重用的体系结构 123

8.3.1 生存 123

8.3.2 递增的变化 124

8.3.3 松散耦合的组件 125

8.3.4 游戏很重要 126

8.4 结论 126

参考文献 127

第9章 “方法是什么？”——关于域工程方面的一篇短文 130

9.1 引言 130

9.1.1 域、需求和软件设计 130

9.1.2 要解决的问题 131

9.1.3 愿望 131

9.1.4 本文的结构 131

9.1.5 一些格式上的约定 132

9.2 方法和方法论 132

9.2.1 方法 132

9.2.2 方法论 132

9.2.3 方法构成 132

9.2.4 方法的原理 133

9.2.5 讨论 134

9.3 域观点和方面 134

9.3.1 涉众与涉众的观点 135

9.3.2 域方面 138

9.3.3 讨论 146

9.4 结论 147

9.4.1 讨论 147

9.4.2 未来的工作 147

9.5 致谢 148

参考文献 148

第二部分 程序设计技术 151

Section E 面向对象 151

第10章 面向对象程序设计和软件开发——一种重要的评价方法 153

10.1 引言 153

10.2 面向对象——其要求与限制 154

10.3 面向对象程序设计——评论 155

10.3.1 类规范 155

10.3.2 对象实例化 156

10.3.3 软件体系结构和组件概念 156

10.3.4 继承和多态 157

10.3.5 顺序性 157

10.4 短评面向对象分析与设计 158

10.4.1 系统模型和语义综合 158

10.4.2 软件和系统的体系结构 158

10.4.3 并发性 158

10.4.4 UML中的数据建模 158

10.5 结论 159

参考文献 159

第11章 指针和对象的痕迹模型 161

11.1 引言：图模型 161

11.2 痕迹模型 165

11.3 应用 169

11.4 结论 173

11.5 致谢 174

参考文献 174

附录 175

第12章 作为堆不变量的对象模型 177

引言 177

12.1 瞬象和对象模型 178

12.2 对象模型举例 179

12.2.1 链表 179

12.2.2 记录表 180

12.2.3 记录数组 180

12.2.4 记录的集合 180

12.2.5 映射 181

12.3 关系逻辑 181

12.4 图逻辑 183

12.4.1 转换字段和分类 183

12.4.2 限定的集合 183

12.4.3 解释具体的对象模型 183

12.4.4 组合对象模型 184

12.4.5 抽象字段 184

12.4.6 索引字段 184

12.5 文本注释 184

12.5.1 表示不变量 185

12.5.2 全局不变量 185

12.5.3 抽象字段的定义 186

12.6 讨论 187

12.6.1 相关方法 187

12.6.2 相关语言 187

12.6.3 代码与问题对象模型的比较 188

12.6.4 抽象字段与抽象对象的比较 188

12.6.5 字段作为关系 189

12.6.6 限定的集合 189

12.6.7 索引字段 190

12.6.8 外延相等 190

12.7 致谢 190

参考文献 191

第13章 抽象依赖 193

13.1 引言 193

13.2 数据抽象的必要性 194

13.3 抽象变量的有效性 195

13.4 符号的定义 196

13.5 举例：Readers 199

13.6 有关工作 204

13.7 结论 205

13.8 致谢 206

参考文献 206

Section F 类型理论 209

第14章 类型系统 210

14.1 计算机科学中的类型系统 210

14.2 类型系统的用途 211

14.2.1 错误检测 211

14.2.2 抽象 212

14.2.3 文档 212

14.2.4 语言设计 212

14.2.5 语言安全 213

14.2.6 效率 214

14.2.7 更多的应用 214

14.3 历史 215

参考文献 216

第15章 类型的含义是什么？——从本质到外在语义 222

15.1 语法和类型化规则 223

15.2 本质语义 224

15.3 未类型化的语义 225

15.4 逻辑关系 226

15.5 分类 230

15.6 外在的PER语义 233

15.7 进一步的工作与未来方向 235

15.8 致谢 235

参考文献 235

第三部分 应用与自动机理论 237

Section G 通过自动机将理论应用于实践 237

第16章 利用推理、探索和抽象进行自动验证 238

16.1 计算模型 239

16.2 程序行为逻辑 240

16.3 验证技术 242

16.3.1 推理法 242

16.3.2 探索性方法 243

16.4 程序和属性的抽象 244

16.4.1 数据抽象 244

16.4.2 谓词抽象 245

16.5 验证方法 248

16.6 结论 249

参考文献 249

第17章 特征工程实验 253

17.1 面向特征的规范 253

17.2 特征工程面临的难题 254

17.3 面向特征的规范技术 255

17.4 一种朴素的特征工程方法 257

17.4.1 适用范围 257

17.4.2 特征和特征合成语义 258

17.4.3 特征的语法 261

17.4.4 特征交互的语义 262

17.4.5 与呼叫有关的特征交互 262

17.4.6 与状态信号有关的特征交互 263

17.4.7 与语音有关的交互 264

17.5 方法的应用 265

17.5.1 特征上下文 265

17.5.2 无约束目标特征集 266

17.5.3 特征集分析 268

17.6 评价 270

17.7 致谢 270

参考文献 270

Section H 程序设计电路 272

第18章 高级电路设计 273

18.1 引言 273

18.2 电路图 274

18.3 定时 275

18.4 触发器 276

18.5 边沿触发 277

18.6 存储器 279

18.7 合并 280

18.8 命令电路 282

18.9 函数电路 290

18.10 混合电路 293

18.11 性能 293

18.12 正确性 294

18.13 同步和异步电路 296

18.14 结论 297

18.15 致谢 297

参考文献 298

Section I 安全与保密 299

第19章 能量分析：攻击与防御策略 301

19.1 引言 301

19.1.1 背景知识 301

19.1.2 能量分析攻击 301

19.1.3 贡献 302

19.1.4 相关工作 302

19.1.5 本文的计划 303

19.2 Twofish实现的能量分析 303

19.2.1 目标实现 303

19.2.2 能量攻击装置 304

19.2.3 Twofish变白过程攻击 304

19.2.4 实验结果 305

19.2.5 由变白密钥到128位主密钥 307

19.3 能量模型与攻击 308

19.3.1 能量模型 308

19.3.2 统计能量攻击 309

19.4 对能量分析的防御策略 310

19.4.1 ad-hoc方法 310

19.4.2 一种通用的防御策略 311

19.4.3 编码 311

19.4.4 分析 312

19.4.5 概率论基础 313

19.4.6 双向分解的下限 313

19.4.7 编码字节 317

19.5 结论 317

19.6 致谢 317

参考文献 317

第20章 信息隐藏的概率方法 320

20.1 引言 320

20.2 背景知识：多级安全和信息流 320

20.3 经典信息论与程序精化 321

20.3.1 概率分布与随机变量 321

20.3.2 条件分布 322

20.3.3 熵 322

20.3.4 条件熵 323

20.3.5 信息泄漏与信道容量 323

20.3.6 概率条件命令 323

20.4 命令程序中的信息流 325

20.4.1 信息流与程序精化 326

20.4.2 与其他工作的比较 329

20.5 举例：安全文件存储器 330

20.5.1 本质 330

20.5.2 添加文件名和数据 330

20.5.3 证明安全性与论证不安全性的对比 331

20.6 精化悖论 332

20.6.1 一些代数难题 332

20.6.2 量子模型 333

20.6.3 安全的本质 333

参考文献 334