图书介绍
软件开发的形式化方法PDF|Epub|txt|kindle电子书版本网盘下载
- 古天龙著 著
- 出版社： 北京：高等教育出版社
- ISBN：704016079X
- 出版时间：2005
- 标注页数：265页
- 文件大小：10MB
- 文件页数：273页
- 主题词：软件开发－方法
PDF下载
下载说明
软件开发的形式化方法PDF格式电子书版下载
下载的文件为RAR压缩包。需要使用解压软件进行解压得到PDF格式图书。建议使用BT下载工具Free Download Manager进行下载,简称FDM(免费,没有广告,支持多平台）。本站资源全部打包为BT种子。所以需要使用专业的BT下载软件进行下载。如BitComet qBittorrent uTorrent等BT下载工具。迅雷目前由于本站不是热门资源。不推荐使用！后期资源热门了。安装了迅雷也可以迅雷进行下载！
（文件页数 要大于 标注页数，上中下等多册电子书除外）
注意：本站所有压缩包均有解压码： 点击下载压缩包解压工具
图书目录
第1章 软件及其开发概述1
1.1 软件开发的历史1
1.2 软件危机2
1.3 软件工程5
1.4 形式化方法15
习题22
第2章 有限状态机及其扩展23
2.1 有限状态机23
2.1.1 基本概念23
2.1.2 有限状态机的复合30
2.1.3 生产者-消费者系统32
2.2 Statecharts34
2.2.1 Statecharts中的状态34
2.2.2 Statecharts中的迁移36
2.2.3 电梯控制系统40
习题45
第3章 Petri网47
3.1 位置／迁移Petri网47
3.1.1 基本定义47
3.1.2 特殊Petri网51
3.1.3 Petri网的性质53
3.1.4 Petri网的分析56
3.1.5 Petri网规格的例62
3.2 高级Petri网66
3.2.1 谓词／迁移Petri网66
3.2.2 有色Petri网69
3.2.3 计时Petri网71
习题72
第4章 进程代数74
4.1 通信顺序进程74
4.1.1 进程及其表示74
4.1.2 事件迹及其操作77
4.1.3 进程的复合操作81
4.1.4 进程的模型85
4.1.5 进程之间的通信89
4.1.6 CSP规格的例93
4.2 通信系统演算95
4.2.1 CCS的基本概念95
4.2.2 AB协议的规格96
习题98
第5章 一阶逻辑99
5.1 命题逻辑99
5.1.1 命题与联结词99
5.1.2 命题公式101
5.1.3 命题逻辑演算102
5.2 谓词逻辑105
5.2.1 谓词公式105
5.2.2 谓词逻辑演算107
5.2.3 谓词逻辑的应用108
5.3 程序正确性证明112
5.3.1 归纳断言方法112
5.3.2 公理化方法116
5.3.3 良序集方法121
5.3.4 计数器方法125
5.3.5 最弱前置谓词方法127
习题137
第6章 时态逻辑140
6.1 模态逻辑140
6.2 线性时态逻辑143
6.2.1 命题线性时态逻辑143
6.2.2 一阶线性时态逻辑146
6.3 计算树逻辑150
6.4 模型检验154
习题157
第7章 Z159
7.1 概述159
7.2 表示抽象162
7.2.1 集合、关系及函数162
7.2.2 序列和包168
7.2.3 自由类型169
7.2.4 模式171
7.3 操作抽象173
7.3.1 模式运算及合成173
7.3.2 通用式函数183
7.4 Z规格的例184
7.4.1 图书数据库管理184
7.4.2 自动售货机194
习题199
第8章 VDM202
8.1 概述202
8.2 表示抽象203
8.2.1 基本运算和基本类型203
8.2.2 集合与序列204
8.2.3 映射与函数207
8.2.4 复合类型210
8.2.5 状态和不变量212
8.3 操作抽象214
8.3.1 操作的表示214
8.3.2 声明216
8.4 VDM规格的例220
8.4.1 家庭供暖系统220
8.4.2 计算机网络问题225
习题233
第9章 Larch235
9.1 概述235
9.2 Larch共享语言236
9.3 Larch/C++接口语言248
9.4 Larch规格的例254
习题261
参考文献263