没有合适的资源?快使用搜索试试~ 我知道了~
首页Z specification
Z specification
需积分: 10 10 下载量 149 浏览量
更新于2023-03-03
评论
收藏 4.74MB PDF 举报
Z specification Z specification Z specification
资源详情
资源评论
资源推荐
Using Z
Specification, Refinement, and Proof
Jim Woodcock
University of Oxford
Jim Davies
University of Oxford
Copyright: this hypertext version of Using Z is easily copied, distributed, and
printed; if you choose to do this, we would ask you to remember that it is under
copyright: if you reproduce any of the material, please include an appropriate
acknowledgement, and—if you find the material useful—please encourage us
(and our publishers) by buying a copy of the book.
Contents
Foreword xi
Using this Book xiii
Acknowledgments xv
1 Introduction 1
1.1 Formal methods 1
1.2 The CICS experience 2
1.3 The Z notation 3
1.4 The importance of proof 4
1.5 Abstraction 5
2 Propositional Logic 9
2.1 Propositional logic 9
2.2 Conjunction 10
2.3 Disjunction 13
2.4 Implication 14
2.5 Equivalence 17
2.6 Negation 20
2.7 Tautologies and contradictions 23
3 Predicate Logic 27
3.1 Predicate calculus 28
3.2 Quantifiers and declarations 30
3.3 Substitution 34
vi
3.4 Universal introduction and elimination 36
3.5 Existential introduction and elimination 40
3.6 Satisfaction and validity 43
4 Equality and Definite Description 45
4.1 Equality 45
4.2 The one-point rule 48
4.3 Uniqueness and quantity 50
4.4 Definite description 52
5 Sets 57
5.1 Membership and extension 57
5.2 Set comprehension 61
5.3 Power sets 65
5.4 Cartesian products 66
5.5 Union, intersection, and difference 68
5.6 Types 69
6 Definitions 73
6.1 Declarations 73
6.2 Abbreviations 74
6.3 Generic abbreviations 75
6.4 Axiomatic definitions 77
6.5 Generic definitions 79
6.6 Sets and predicates 81
7 Relations 83
7.1 Binary relations 83
7.2 Domain and range 85
7.3 Relational inverse 88
7.4 Relational composition 91
7.5 Closures 94
8 Functions 99
8.1 Partial functions 99
8.2 Lambda notation 101
8.3 Functions on relations 103
8.4 Overriding 105
8.5 Properties of functions 107
8.6 Finite sets 111
vii
9 Sequences 115
9.1 Sequence notation 115
9.2 A model for sequences 119
9.3 Functions on sequences 122
9.4 Structural induction 124
9.5 Bags 128
10 Free Types 133
10.1 The natural numbers 133
10.2 Free type definitions 135
10.3 Proof by induction 140
10.4 Primitive recursion 142
10.5 Consistency 145
11 Schemas 147
11.1 The schema 147
11.2 Schemas as types 152
11.3 Schemas as declarations 154
11.4 Schemas as predicates 158
11.5 Renaming 160
11.6 Generic schemas 162
12 Schema Operators 165
12.1 Conjunction 165
12.2 Decoration 168
12.3 Disjunction 174
12.4 Negation 177
12.5 Quantification and hiding 178
12.6 Composition 182
13 Promotion 185
13.1 Factoring operations 185
13.2 Promotion 193
13.3 Free and constrained promotion 196
14 Preconditions 201
14.1 The initialisation theorem 201
14.2 Precondition investigation 203
14.3 Calculation and simplification 206
14.4 Structure and preconditions 210
剩余406页未读,继续阅读
chanvwy
- 粉丝: 0
- 资源: 6
上传资源 快速赚钱
- 我的内容管理 收起
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
会员权益专享
最新资源
- ExcelVBA中的Range和Cells用法说明.pdf
- 基于单片机的电梯控制模型设计.doc
- 主成分分析和因子分析.pptx
- 共享笔记服务系统论文.doc
- 基于数据治理体系的数据中台实践分享.pptx
- 变压器的铭牌和额定值.pptx
- 计算机网络课程设计报告--用winsock设计Ping应用程序.doc
- 高电压技术课件:第03章 液体和固体介质的电气特性.pdf
- Oracle商务智能精华介绍.pptx
- 基于单片机的输液滴速控制系统设计文档.doc
- dw考试题 5套.pdf
- 学生档案管理系统详细设计说明书.doc
- 操作系统PPT课件.pptx
- 智慧路边停车管理系统方案.pptx
- 【企业内控系列】企业内部控制之人力资源管理控制(17页).doc
- 温度传感器分类与特点.pptx
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功
评论0