软件形式规格说明语言Z/普通高等教育“十一五”国家级规划教材·软件工程专业核心课程系列教材

图书标准信息

• 作者 缪淮扣、陈怡海 著
• 出版社 清华大学出版社
• 出版时间 2012-11
• 版次 1
• ISBN 9787302292777
• 定价 34.50元
• 装帧 平装
• 开本 16开
• 纸张 胶版纸
• 页数 299页
• 字数 487千字
• 正文语种 简体中文
• 丛书 普通高等教育“十一五”国家级规划教材·软件工程专业核心课程系列教材

【内容简介】

形式方法是一种基于数学的软件开发方法。形式规格说明是形式方法最基本的部分，它精确描述用户需求和计算机软件系统的功能，并用于软件验证和精化。Z是目前颇受欢迎且使用较广泛的一种形式规格说明语言。《普通高等教育“十一五”国家级规划教材·软件工程专业核心课程系列教材：软件形式规格说明语言Z》旨在讨论软件工程中形式方法的概念、方法和表示法，并详细介绍Z的类型系统、数学语言和公理定义、通用式定义、模式等结构，还讨论了Z规格说明的推理和求精方法。本书还介绍了面向对象的规格说明语言Object-Z和其他形式方法表示和工具。全书结构合理、内容丰富、实例详尽多样。各章配有习题。
《普通高等教育“十一五”国家级规划教材·软件工程专业核心课程系列教材：软件形式规格说明语言Z》可作为计算机、软件工程、信息安全和信息管理等专业本科生和研究生的教材，也可作为大专院校有关专业的教师参考书，还可作为从事软件工程、软件开发和软件应用的研究人员和技术人员的参考资料。

【目录】

第1章绪论
1.1软件生命周期
1.2存在的问题
1.3形式方法
1.3.1形式化和抽象的需要
1.3.2什么是形式方法
1.3.3形式验证技术
1.3.4形式方法发展的历史简介
1.3.5形式规格说明语言的分类
1.3.6形式方法的应用
1.3.7推荐使用形式方法的相关标准
1.3.8形式方法的优缺点
1.4形式规格说明语言Z
1.4.1Z语言概述
1.4.2Z规格说明简例
小结
习题

第2章一阶逻辑与集合论
2.1命题逻辑
2.1.1命题与连接词
2.1.2命题公式与真值表
2.2谓词逻辑
2.2.1量词
2.2.2谓词公式
2.2.3约束变量与自由变量
2.2.4谓词公式的解释
2.3一阶逻辑中的证明
2.3.1什么是证明
2.3.2命题逻辑中的证明
2.3.3命题逻辑中的定律
2.3.4谓词逻辑中的证明
2.3.5谓词逻辑中的定律
2.4集合论
2.4.1集合的表示法
2.4.2集合谓词
2.4.3空集、全集与幂集
2.4.4集合运算
2.4.5序偶与笛卡儿积
小结
习题

第3章Z的类型与构造单元
3.1Z的类型系统
3.1.1基本类型
3.1.2幂集类型
3.1.3笛卡儿积类型
3.1.4对象声明
3.1.5枚举类型
3.2扩充表示法
3.2.1量词化扩充表示法
3.2.2集合表达式扩充表示法
3.2.3Z的基本库
3.3Z规格说明的构造单元
3.3.1Z的符号
3.3.2公理定义
3.3.3模式
3.3.4通用式定义
小结
习题

第4章关系和函数
4.1关系
4.1.1关系表示法
4.1.2定义域和值域
4.2关系的运算
4.2.1关系复合
4.2.2恒等和闭包
4.2.3关系的逆
4.2.4关系限定和限定减
4.2.5关系映像
4.3函数
4.3.1部分函数与全函数
4.3.2入射函数与满射函数
4.3.3函数叠加操作和通用式定义
4.3.4文具用品管理的模型示例
4.3.5λ-表示法
小结
习题

第5章模式和规格说明
第6章序列和包
第7章规格说明的实例
第8章Z规格说明的形式推理
第9章Z规格说明的若干推理实例
第10章从规格说明到程序
第11章Object-Z规格说明语言
第12章形式方法及其工具
附录AZ语法
附录BZ语言术语
附录CObject-Z语法
附录D部分习题解答
参考文献