Introduction

Z语言

定义

Z语言是一种用“数学文字”或“数学符号”来描述计算机系统的规范化语言,它不但能应用于计算机硬件系统,而且也特别适用于计算机软件系统,Z语言描述“做什么”而不涉及“怎么做”,只对目标软件系统进行功能描述。实际上,Z语言仅仅是一套规定的数学符号,使用Z语言所写的“程序”是对计算机软件或硬件系统的一种抽象化设计。所以,利用Z语言写出来的内容不是计算机程序,更不是可以编译而生成能够在计算机上运行的代码。利用Z语言写出来的内容不是让计算机运行的,而是供人理解和分析的。用户可以通过这些内容去理解计算机系统的模块、数据类型、过程、函数、对象、类等,进而对计算机系统的行为、结构、逻辑进行分析、验证、改进、测试等。

特征

形式化描述语言Z指的是著名数学家Zermelo,它是使用最广泛的一种形式化描述语言,在软件产业的一些大型项目中已经获得成功的应用,Z以带等词的一阶谓词逻辑ZF(Zermelo-Fraenkel,蔡梅罗-弗兰科尔)公理集合论为主要数学基础。在Z中有两种语言:数学语言和模式(Schema)语言。数学语言用来描述系统的各种特征:对象及其之间的关系。模式语言是一种半图形化的语言,它用来构造、组织形式化说明的描述、整理、封装信息块并对其命名以便可以重用这些信息块。通常,形式化说明的可读性都不太好,但由于Z采用半图形化的模式语言,能用一种比较直观、有条理的方式来表达形式化说明,这就改善了可读性。

应用

Z语言是由牛津大学程序设计研究小组开发的一种形式语言,之后该小组与IBM的Hursley实验室合作,将Z语言用于IBM客户信息控制系统(Customer Information and Control System,CICS)的开发,使得最终的产品质量得到了全面的提高,所监测出的错误数量大大减少,并且整体开发费用降低了9%。在ISO指导下的国际标准化Z工作于2002年完成。

Sets

Types

  • 一个集合是指若干组成部分的集合,它们也被叫做元素或成员;
  • 集合中所有元素的值都有一些共通点,称这些元素是相同类型的;
  • 类型的作用体现在两方面:
    • 避免了数学悖论;
    • 它允许检查关于集合的声明是否有意义。(it allows checks to be made that statements about sets make sense.)
  • 通过计算机软件自动检查Z语言语句的连贯性,与对自然语言的拼写和语法的检查方法相同。

The built-in type Integer

Integer可以在Z语言中直接使用,不需要显式声明,用符号Z表示

它包括所有的整数 …,-3,-2,-1,0,1,2,3,…

The standard set Natural

用N表示,集合中的元素为非负整数

N1代表自然数

Operations on integers

+ addition
- subtraction
* multiplication
div division
mod modules

Numerical relations

= equal to
not equal to
less than
less than or equal to
greater than
greater than or equal to

Basic types

基本类型也被称为给定类型

声明基本类型时不需要关心如何表示其中的元素

For Example:

[REGISTRATION] the set of all possible car registrations

[PERSON] the set of all persons

可以在一行声明多个类型

[REGISTRATION, PERSON]

总的来说,基本类型的范围应该尽可能地广泛。此外,应保证该类型的元素具有唯一性。(Basic types should be chosen to be as widely encompassing as possible. Furthermore, it should be assumed that the elements of the type are uniquely identifiable.)

Free types

有时可以把一个类型的所有元素列出来

可以通过自由类型来实现

自由类型的一般形式为

freeType ::= element1 | e2 | e3 | … | en

For Example:

REPONSE ::= yes | no

STATUS ::= inUse | free | onHold | outOfOrder

Declaring variables

每个变量必须要先声明,意思是必须明确说明这个变量的类型

For Example:

chauffeur:PERSON

表示chauffeur的类型是PERSON

Single value from a type

一个类型中只有一个取值

For Example:

1

homeland:EU

Set values

可以通过把值列在大括号内来给集合赋值

benelux={B, NL, L}

大括号内元素的顺序不影响集合的值

2

集合中每个元素只会出现一次

3

The empty set

当集合中没有元素时,称该集合为空集

可用 “∅” 或 “{}” 来表示

Singleton set

当集合中只包含一个元素,称该集合为单元素集

For Example:{GB}

4

Range of integers

m…n(m和n为整数)表示包括m到n所有整数的集合

如果m>n,则为空集

For Example:

5

Operators

Equivalence =

Non-equivalenc ≠

Membership ∈

Non-membership ∉

Validity of membership test

6

Size, cardinality

集合中元素个数称为集合的大小或集合的基数

For Example:

7

Powersets P

一个集合的幂集为包含这个集合所有子集的集合

S的幂集写作 “PS”

For Example:

8

幂集中元素的个数

#(PS)=2#S

9

Set inclusion ⊆

Union ∪

Intersection ∩

Difference \

10

Distributed union

11

Distributed intersection

12

Disjoint sets

表示不相交的集合

对于两个集合来说很容易表示,S∩T=∅

13

Summary of notation

14

15

Using sets to describe a system - a simple example

Logic

Negation ┐

Conjunction ∧

Disjunction ∨

Implication ⇒

P⇒Q等价于┐P∨Q

Equivalence ⇔

De Morgan’s laws

16

Summary of notation

17

The example extended

Schemas

Schemas

schema的一般形式如下

19

线性schema表示为

20

"=="表示代表

S==[a,b:N|a<b]

用schema表示如下

18

全局schema

21

Schema calculus

模式可以被视为单位,并通过各种操作符进行操作,这些操作符类似于逻辑操作符。(schemas can be regarded as units and manipulated by various operators that are analogous to the logical operators)

Decoration

当一个schema的名字S被标记为S’,表示一些操作被执行后的schema

For Example:

22

Inclusion

23

==

24

Schema conjunction

25

Schema disjunction

26

Delta convention

当一个schema的名字S被标记为ΔS,表示一些操作执行前后的约束

27

Xi convention

当一个schema的名字S被标记为ΣS,表示一些操作执行前后的状态相同

28

Decoration of input and output variables

输入用"?"标记

输出用"!"标记

For Example:

29

Further operations on schemas

Renaming

一般形式如下

30

For Example:

given

31

then

32

gives

33

Hiding

34

Projection

35

Schema composition

S与T的composition表示为 “S;T”

表示先做S,再做T

36

Overall structure of a Z specification document

Z规范文件由Z符号的数学文本组成,与自然语言的解释文本交错排列。解释文本应该用问题来表达,不应该直接引用数学公式。只有在作为Z语言教程的文件中才会打破这一规则。(A Z specification document consists of mathematical text in the Z notation, interleaved with explanatory text in a natural language. The explanatory text should be expressed in terms of the problem and should not refer directly to the mathematical formulation. This rule is broken only in the case of documents intended as tutorials on Z. )

Sections of a Z document

37

Predicates and quantifiers

Introduction

约束是取决于数值的逻辑表达式

当取值给定时约束就变成了一个命题

38

Quantifiers

约束可以使用量词来给出命题

Universal quantifier ∀

一般形式如下

39

有时predicate可以省略

For Example:

40

Existential quantifier ∃

一般形式如下:

41

For Example:

42

43

其中Even(x)的功能是判断x是否为偶数

Unique quantifier ∃1

唯一量词与存在量词类似,唯一的区别是唯一量词表达的是只有一个值可以使得约束条件为真

For Example:

44

Counting quantifier

Set comprehension

之前给集合赋值时是通过列出所有元素

也可以通过给定条件来给集合赋值,集合中的元素是符合条件的所有元素

一般形式如下

45

For Example:

给出一个无限集,包含所有偶数

{ … -8, -6, -4, -2, 0, 2, 4, 6, 8 … }

46

Ranges of numbers

47

Relationship between logic and set theory

48

Summary of notation

49

Relations

A relation is a set

目前考虑的都是单类型实例,这就意味着形式不可能过于复杂。现在需要的是将一个集合映射到另一个集合的方法。这可以通过关系来完成,基于笛卡尔乘积。

Cartesian product(笛卡尔乘积)

50

Relations

51

Declaring a relation ↔

52

53

Maplets |→

54

Membership

判断一对值是否有关,只需要判断这对值或maplet是否属于这个关系

55

Infix relations

56

Domain and range

57

Domain

大多数情况下,一个关系只会涉及到source的子集。这个子集被称作domain(定义域),写作 “dom”

58

Range

大多数情况下,一个关系也只会涉及到target集合的子集。这个子集被称作range(值域),写作 “ran”

59

60

Examples

61

Relational image

从source集合得到target集合

62

Constant value for a relation

有一些关系中含有常量。如果这个量已知,可以通过定理定义给出。

63

64

Restriction

还有更多的运算符可用于限制一个关系

Domain restriction ◁

65

Range restriction ▷

66

Domain subtraction

67

Range subtraction

68

Example of restriction

69

70

Composition

71

Forward composition

72

Backward composition

Forward composition的另一种写法

73

Repeated composition

74

Example

75

当不同国家有共同的边界时,通过关系borders连接

当两个国家都与第三个国家有borders的关系时,可以进行关系合成

Transitive closure

传递闭包

76

77

传递闭包的一般格式为 x R+ y,表示x与y间的关系是由关系R重复组合而成

Identity relation

78

Identity relation is the one in which every elements maps to itself only. The rule for identity relation is given below. “Every element is related to itself only”

79

所有的元素只与自己有关

Reflexive transitive closure

80

与传递闭包的区别是,组合关系=R+∪ id X

Inverse of a relation

81

if x R y then y R~ x

Examples

Definitions

84

given pyz father pyq ∩ pyz mother clx

Parent

85

x parent {f, m} means x has f and m as parent

so giving pyz parent {pyq, clx}

Sibling

86

表示除自己外的兄弟姐妹

Ancester

87

Summary of notation

82

83

Funtions

A function is a relation

Definition

88

在编程语言中函数是一个方法,它规定了一种产生结果的处理过程

在Z语言中,函数是一种数据结构

函数是关系的一种特殊情况,定义域中的每个值唯一对应值域中的某个值

定义域有限的函数也叫做映射

89

90

定义域对值域,可以多对一,不可以一对多

Examples of functions

91

92

每个人和身份证号是一一对应的关系

每个人只有一个母亲,但是可能有几个人的母亲是相同的

Function application

93

所有与关系有关的概念都可以应用到函数中

对于给定的一个x值,在值域中最多只能有一个值与之对应

应用到函数中的前提是x必须在定义域中

Partial and total functions

Definition

94

95

上面例子中的函数只是一部分,部分source集中的值并不在函数的定义域中

total函数表示,任何集合X中的值x,f x都有意义。即source集就是函数的定义域

Examples of total functions

96

函数age:PERSON型指向N型,这是一个total函数,因为每个人都有年龄

同理,函数hasMother:PERSON型指向PERSON型,也是一个total函数

Other classes of functions

97

除了total和partial,还有一些其他类型的函数

Injection

98

99

单射:一对一,对于值域内内一个y,都只有唯一的一个x使得f x=y成立

Surjection

100

满射:值域上任何一个值都有定义域的值与之对应,即target集就是值域

Bijection

101

双射:既是单射,又是满射。一一对应。

Constant functions

102

103

有一些函数的功能就是提供一个数值,根据所给的参数得到相应的输出。

Overriding ⊕

104

105

f g为两个函数,两个关系

f 被 g 重写为:f⊕g,then f⊕g x=g x

Example from business - stock control

107

108

Example from data processing

Indexed-sequential files

109

COBOL语言,是一种面向过程的高级程序设计语言,主要用于数据处理,是目前国际上应用最广泛的一种高级语言。COBOL是英文Common Business-Oriented Language的缩写,原意是面向商业的通用语言。它采用 300多个英语单词作为保留字,以一种接近于英语书面语言的形式来描述数据特性和数据处理过程,因而便于理解和学习。COBOL语言是专门为企业管理而设计的高级语言,可用于统计报表、财务会计、计划编制、作业调度、情报检索和人事管理等方面。

在COBOL语言中,有一种数据文件为索引顺序文件

110

Read operation

111

Rewrite operation

112

113

Write operation

114

Delete operation

115

Error conditions

116

Further facilities

117

Summary of notation

106

A seat allocation system

Introduction

This example concerns recording the allocation of seats to passengers on an aircraft

The types

118

The state

119

一个座位只能被一个人预定,但是一个人可以预定多个座位

Initialization operation

120

对于一个系统必须有一个初始化状态

这个系统的初始化状态为,所有座位都没有被预定

Operations

Booking

121

Cancel

122

Enquiry operations

询问操作并不改变系统的状态

Whose seat

除了会改变系统状态的操作,查询座位主人的操作也是必要的

REPLY ::= yes | no

123

Dealing with errors

124

Booking

125

在predicate中应写 s?∈dom bookedTo

Cancel

A schema to handle errors on canceling a booking is defined:

126

Sequence

Definition and Representation

在集合中我们不关系元素的顺序,且集合中没有重复的元素

在序列中,元素的顺序是很重要的,且可以包含相同的元素

127

序列可以被看作一个函数

128

Example:

129

第 i 个元素

130

Example:

131

序列的长度 #

132

Example:

133

Sequence Operators

138

141

Concatenation 连接

134

Example:

135

Reverse 逆置

136

Example:

137

139

Head,Last,Tail and Front

given a sequence <a,b,c,d,e,f,g>

head<…>=a

last<…>=g

tail<…>=<b,c,d,e,f,g>

front<…>=<a,b,c,d,e,f>

140

142

Squash (压缩)

143

其中min(dom f)代表f的定义域的最小值

Example:

144

145

146

Extraction 提取

提取操作是对定义域的限制

147

148

Example:

149

Filter 过滤

过滤操作是对值域的限制

150

151

Example:

152

Extraction and Filter

153

154

155

Distributed catenation(分布连接) / flattening(平展)

156

157

Example:

158

Bag

Definition and Representation

a.k.a. multiset

[[·]]-representation of a bag

159

一个包中的元素必须是同类型的

包中的元素顺序不重要

Example:

160

Limitation

161

包中可以有无限个元素

但是上面的这种表示方法并不能表示无限个元素的包

Function-representation of a bag

162

Example:

163

Bag Operators

Bag count

164

Example:

165

Bag scaling

166

Example:

167

count and ⊗

168

169

要与函数重写区分开

170

171

Bag membership and sub-bag relation

175

176

membership

172

sub-bag

173

Example:

174

177

Bag union and bag difference

178

179

Example:

180

181

182

Function items

183

Example:

184

185

Formal Specification Examples

More about Logic

Language

Example

186

187

Terms (项)

188

Example:

189

Formulas (公式)

190

unary:一元的

Example:

191

Sentences (语句)

192

Every sentence is a formula without free variable

w.r.t.:with respect to

i.e.:也就是,换言之

Example:

193

Informal semantics

194

195

Conventions

196

Example:

197

198

Deductive System

Introduction

199

syntactic:adj.句法的

200

Inference rules

201

202

203

204

205

206

208

209

210

211

212

213

Formal proof

207

Points

  • Relation和Maplet之间的区别?
  • 传递闭包?例题?Reflexive transitive closure
  • 离散数学
  • 符号

Material

课程资料