Z语言:谓词演算为主要理论基础的规约语言_Z语言形式化语言

4星 · 超过85%的资源需积分: 50 321 浏览量更新于2023-03-03 评论 1 收藏 1.11MB PDF 举报

身份认证购VIP最低享 7 折!

领优惠券(最高得80元）

资源详情

资源评论

资源推荐

Z Notation

Final Committee Draft, CD 13568.2

August 24, 1999

Developed by members of the Z Standards Panel

BSI Panel IST/5/-/19/2 (Z Notation)

ISO Panel JTC1/SC22/WG19 (Rapporteur Group for Z)

Pro ject number JTC1.22.45

Pro ject editor: Ian Toyn

ian@cs.york.ac.uk

http://www.cs.york.ac.uk/~ian/zstan/

This draft expresses the consensus position of the members of the Z Standards Panel. It is published for review

by the wider community: comments should be submitted via national standards b odies. The Foreword includes

a comparison with the rst committee draft, which will be excluded from the future International Standard.

ISO.

Z Notation:1999(E)

Contents

Page

Foreword . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . iv

Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . viii

1 Scope . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2

2 Normative references . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

3 Terms and denitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

4 Symbols and denitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

5 Conformance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18

6 Zcharacters . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

7 Lexis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28

8 Concrete syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34

9 Characterisation rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42

10 Annotated syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44

11 Prelude . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47

12 Syntactic transformation rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48

13 Type inference rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58

14 Instantiation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68

15 Semantic transformation rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70

16 Semantic relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75

Annex A (normative) Mark-ups . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82

Annex B (normative) Mathematical to olkit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92

Annex C (informative) Organisation by concrete syntax pro duction . . . . . . . . . . . . . . . . . . . . . . 109

Annex D (informative) Tutorial . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 152

Annex E (informative) Conventions for state-based descriptions . . . . . . . . . . . . . . . . . . . . . . . . 165

Bibliography . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 167

Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 168

FCD typeset August 24, 1999

Z Notation:1999(E)

Figures

1 Phases of the denition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18

B.1 Parent relation b etween sections of the mathematical toolkit . . . . . . . . . . . . . . . . . . . . . . . 92

D.1 Parse tree of birthday b ook example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 154

D.2 Annotated parse tree of part of axiomatic example . . . . . . . . . . . . . . . . . . . . . . . . . . . . 157

D.3 Annotated parse tree of part of generic example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 160

D.4 Type constraints for chained relation example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 163

Tables

1 Syntactic metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

2 Use of parentheses in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

3 Propositional connectives in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

4 Quantiers in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

5 Abbreviations in quantications in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

6 Conditional expression and

let

in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

7 Propositions ab out sets in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

8 Set extensions and unions in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

9 Powerset in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

10 Operations on numbers in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

11 Decorations of names in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

12 Tuples and Cartesian products in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

13 Further comprehensions in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

14 Relations in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

15 Proposition ab out relations in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

16 Functions in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

17 Function use in metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12

18 Metavariables for phrases . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12

19 Metavariables for op erator words . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13

20 Environments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

21 Variables over environments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

22 Type sequents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

23 Semantic universe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

24 Variables over semantic universe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

25 Semantic relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

26 Semantic idioms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

27 Operator precedences and asso ciativities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39

FCD typeset August 24, 1999

iii

Foreword Z Notation:1999(E)

Foreword

The International Organization for Standardization (ISO) is a worldwide federation of national standards b odies

(ISO member bodies). The work of preparing International Standards is normally carried out through ISO

technical committees. Each member body interested in a sub ject for which a technical committee has been

established has the right to be represented on that committee. International organizations, governmental and

non-governmental, in liaison with ISO, also takepartinthework. ISO collab orates closely with the International

Electrotechnical Commission (IEC) on all matters of electrotechnical standardization.

Draft International Standards adopted by technical committees are circulated to the member bo dies for voting.

Publication as an International Standard requires approval by at least 75% of the member b odies casting a vote.

This do cumentwas prepared byISOPanel JTC1/SC22/WG19 (Rapporteur Group for Z) for pro ject JTC1.22.45.

Its structure is in accordance with ISO Directives Part 3. The membership of JTC1/SC22/WG19 (Rapp orteur

Group for Z) includes the members of BSI Panel IST/5/-/19/2 (Z Notation). Annexes A and B are normative

parts of this International Standard; the other annexes are for information only.

The normative clauses of this International Standard organise the language denition as a sequence of phases.

This sequence is illustrated in Figure 1 in 5.1, and the corresp onding clauses are detailed in 5.3. Informative

annex C duplicates some of the denition reorganised bysyntactic production, but there is much that does not

t into this organisation, as explained in its introduction.

The following comparison is included only for the b enet of reviewers; it will b e excluded from the International

Standard.

Comparison with rst Committee Draft (Version 1.2) and comments thereon

Manychanges since Version 1.2 are identied here, rst those with widespread eects through the document, and

then those with more lo calised eects. Attention is drawn to comments that relate to those changes. After that,

those comments that are still outstanding are enumerated, and nally the other comments are identied.

Widespread changes

a) The document has b een revised to comply with ISO directives (comment UK9).

b) Types have been separated from the semantics (comments UK4{6): elements and situations have gone, and

generic lifting has simplied to something that happens within the semantic relation for generic axiomatic

description paragraphs. Free variable and alphabet functions have b een subsumed by calculations on type

signatures. A new meta-op eration called

decor

assists in dening schema op erations (comment CA10).

c) More consistent metalanguage is now used | for syntactic metalanguage, ISO/IEC 14977:1996 is used

(comment CA2), and for semantic metalanguage, a Z-like syntax for ZF set theory is used, with the same

precedences as used in Z (comment JP1). Far fewer bracket shap es are used (comments CA18, US33).

d) Many Z notations were not fully dened but now are, e.g. sections (comments JP44, UK1), free types

(comment JP49, UK54), numbers (comment UK77), and schema operations (comments JP54, JP80, UK63,

US71, US72).

e) The organisation of the normative technical material by syntactic productions has been relegated to an

annex, with clauses now organising the normative technical material by phase of denition. This is b ecause

some parts of the denition cannot b e accommodated by the organisation bysyntactic pro duction (proposal

IT.50.8).

f) Schema has b een merged into Expression (prop osal IT.48.2 part c, comments CA36, UK34). The term text

or expression is no longer used, as the traditional term schema text now suces (comment JP4 part 2).

g) Onlyafewchanges have b een done to the Z notation itself:

FCD typeset August 24, 1999

Z Notation:1999(E) Foreword

1) free type paragraphs can now dene mutually recursivefreetyp es;

2) schema piping is included;

3) let and

notations with == lo cal declarations are used in place of substitution



and



notations. If

the substitution notation were wanted, it could b e dened by the following syntactic transformations.



)



g



) 9 f

g

Lo calised changes

a) Acknowledgements of contributors and membership of the Z Standards Panel have b een omitted (proposal

IT.48.4). There does not seem to be anymention of acknowledgements in ISO directives. I expect myname

to disappear from the cover; it is there on this Working Draft so that you know who to send your comments

to.

b) The Foreword is where commentary on a particular draft appears, and so is necessarily dierent from Version

1.2. Two paragraphs of \b oilerplate text" provided by the L

X macros start the Foreword. They are similar

to (though not word-for-word the same as) text present in another standard, though there does not seem to

be an ISO directive requiring them (prop osal IT.48.1 part c).

c) An alternativeIntro duction is presented (prop osal IT.48.7).

d) A title page has b een added, as required by ISO directive 6.1.1 (prop osal IT.48.1 part a).

e) The Scop e clause has been rewritten in the style required by ISO directive 6.2.1 (proposal IT.48.1 part b).

f) The Conformance clause has b een extended. (Comments CA6, CA8 and UK12 noted the need for this.) It

has also been moved later in the document, according to ISO directive 5.1.3 (prop osal IT.48.3). Discussion

of the structure of this standard do cument has b een included here.

g) In Normative references, ISO directive 6.2.2 requires a paragraph of \boilerplate text" at the start, the

omission of which in 1.2 has been corrected (prop osal IT.48.1 part c). A reference to the ISO standard on

which Unicode is based has been added (US13).

h) The three clauses Semantic metalanguage, Semantic universe and Language description have b een replaced

bythetwo clauses Terms and denitions, and Symbols and denitions, those being the headings required

by ISO for the clauses that introduce the terminology and notation that is to be used in dening the Z

notation. The separation of types from the semantics (comments UK4{6) has led to substantial changes in

contenthere. Within Terms and denitions, a stylethatallows an o ccurrence of a term to be replaced by

its denition in suchaway that the sentence in which it appears remains grammatically correct has been

used, as required by ISO directive C.1.5.3 (proposal IT.48.1 part b). Within Symbols and denitions, more

explanation of the semantic metalanguage has b een included (comment US14).

i) Zcharacters are now dened in terms of Unico de (proposal IT.51.1). TheZcharacters clause and Mark-ups

annex have been separated from Lexis (proposal IT.48.2 part a), arising from progress that allows denition

of the widely-used L

X mark-up, whichwas not present in 1.2, and description of how formal and informal

parts are delimited (comment US11). The Z characters corresponding to schema outlines are explicitly

permitted to b e rendered in either of two dierent ways, corresponding to past practice. UP and DOWN

haveevolved (comment US146), and digit strokes are specied dierently. The syntax is specied in terms

of individual strokes, decoration b eing what is done toaschema by astroke (comment US40). There are

more characters in the SPECIAL class, to reduce the need for spaces between tokens (prop osal IT.48.13).

The turnstile

has b een replaced by

=?.

FCD typeset August 24, 1999

剩余181页未读，继续阅读

silikmel

2012-11-03

英文原件，版本比较老，还算推荐

zeamiaomiao

粉丝: 2
资源: 5

会员权益专享

Z语言:谓词演算为主要理论基础的规约语言

评论2

会员权益专享

最新资源

Z语言:谓词演算为主要理论基础的规约语言

评论2

离散数学前七章十个重要知识点

谓词逻辑python实验

一阶谓词逻辑表示法是结构化知识还是非结构化知识？适合于表示那种类型的知识？它有哪些特点？

谓词公式：P ∧ (Q ∨R) -> (P ∧ Q) ∧R，已知前件为真，求谓词公式的真值，并给出计算过程

将谓词公式转化为合取样式代码

集合论、关系论、图论、逻辑、代数系统、组合数学等基础理论有哪些内容

离散数学问题：找出谓词公式∀xョy(P(f(x,y),a)→P(x,y))真值为1的解释

将谓词公式字符串改为合取样式代码

将谓词公式转化为合取样式

解释一阶逻辑，举个例子

输入一个符号串，判断其是否为谓词公式 (可选) 。 2. 对于任意一阶谓词逻辑描述的定理，给出基于归结原理的证明过程

计算（和简化）每个子句决定谓词p= a v b v ( c ^ d)的条件

回答集程序ASP语言中，项、元素、原子、常量、变量、函数、谓词的关系是什么

人工智能谓词逻辑———猴子摘香蕉

会员权益专享

最新资源