Z语言：形式化描述与证明基础

5星 · 超过95%的资源需积分: 10 75 浏览量更新于2024-07-29 收藏 4.74MB PDF 举报

"Z语言是一种基于一阶谓词演算的形式化描述语言，常用于规格说明、精炼和证明。本书由Jim Woodcock和Jim Davies撰写，探讨了Z语言的使用，包括命题逻辑和谓词逻辑等内容，以及抽象概念在形式化方法中的重要性。" 在计算机科学领域，Z语言是一个强大的工具，它被设计用来精确地描述复杂系统的行为和结构，特别是在软件工程和形式验证中。Z语言的核心是其一阶谓词演算基础，这使得它可以表达复杂的逻辑关系和数学结构。 1. **形式化方法**：形式化方法是一种利用严格的数学语言来描述软件和系统的方法，旨在提高软件的可靠性和可验证性。通过使用Z语言，开发者可以更准确地定义系统的规格，减少因理解不清导致的错误。 2. **CICS体验**：CICS（Customer Information Control System）是IBM的一个交易处理系统，Z语言在CICS项目中的应用展示了形式化方法在大型系统开发中的价值，它能帮助识别和解决潜在问题，提高系统质量。 3. **Z符号**：Z语言的符号系统包括一套图形和文字符号，用于表示数据结构、函数、操作和逻辑关系。例如，区分数学表达式和逻辑连接符，如合取（ conjunction）、析取（disjunction）、蕴含（implication）和等价（equivalence）。 4. **证明的重要性**：在Z语言中，证明是验证规格正确性的关键步骤。通过构造和检查证明，可以确保规格满足预期的性质和行为，这在关键领域的软件开发中尤其重要。 5. **抽象**：抽象是Z语言中的一个核心概念，它允许我们将复杂系统分解成更小、更易于管理的部分，同时保持整体行为的准确性。这有助于理解和验证大型系统的复杂性。 6. **命题逻辑**：这部分介绍了基本的逻辑运算，如与（conjunction）、或（disjunction）、蕴含（implication）、等价（equivalence）和否定（negation）。这些概念是构建更复杂逻辑表达式的基础。 7. **谓词逻辑**：谓词逻辑进一步扩展了命题逻辑，引入了量词（quantifiers）和声明（declarations），允许我们描述涉及个体变量的普遍和特定事实。还包括子代换（substitution）、通用引出（universal introduction）和消除（elimination）以及存在引出和消除规则。 8. **等价性**和"..."：这部分可能涉及到Z语言中的等价关系概念，例如等价关系的性质（对称性、传递性和自反性），以及如何用Z语言描述和处理这些关系。通过深入学习和应用Z语言，开发者和分析师能够构建严格的形式化规格，这有助于提高软件的可靠性和维护性，并降低系统风险。此外，掌握Z语言的证明技术对于验证复杂系统的正确性至关重要。

2 1 / Introduction

There is an alternative. Formal methods, based upon elementary mathe-

matics, can be used to produce precise, unambiguous documentation, in which

information is structured and presented at an appropriate level of abstraction.

This documentation can be used to support the design process, and as a guide

to subsequent development, testing, and maintenance.

It seems likely that the use of formal methods will become standard prac-

tice in software engineering. The mathematical basis is diﬀerent from that of

civil or mechanical engineering, but it has the same purpose: to add precision,

to aid understanding, and to reason about properties of a design. Whatever the

discipline, the use of mathematics can be expensive, but it is our experience

that it can actually reduce costs.

Existing applications of formal methods include: the use of probability

theory in performance modelling; the use of context-free grammars in compiler

design; the use of the relational calculus in database theory. The formal method

described in this book has been used in the speciﬁcation and design of large

software systems. It is intended for the description of state and state-based

properties, and includes a theory of reﬁnement that allows mathematics to be

used at every stage of program development.

1.2 The CICS experience

CICS is one of the most successful pieces of software in the world: there are

over 30 000 licences, and most of the world’s top companies use it. CICS stands

for Customer Information Control System, a family of transaction processing

products produced by IBM UK Laboratories at Hursley Park. CICS provides

data access, communications, integrity, and security services. Put simply, CICS

manages information.

When we use an automated teller machine in San Francisco, an account at

our local branch in Oxford is debited, even though the machine is thousands

of miles away. During the busiest times, there may be many thousands of

customers of the bank using the service all over the world, and we all expect to

be served within a reasonable time. CICS oﬀers a way of achieving this.

There have been regular releases of CICS since the mid-1970s. Each release

has introduced additional features and extended the structure of the existing

code. In the early 1980s, the complexity of the system started to become a

serious problem for the company. A decision was made to re-design some of

the CICS modules with the aim of making extensions easier. An important

part of the proposed solution involved ﬁnding a more precise way to specify

functionality.

1.3 / The Z notation 3

Such precision requires the use of mathematical techniques that were, at

that time, little known outside academia. A happy coincidence brought the

CICS manager, Tony Kenny, and the Oxford professor, Tony Hoare, together at a

conference. They hatched a plan to apply Oxford’s ideas to Hursley’s problems.

Oxford advised on how formal methods could be used for the speciﬁcation

and design of new CICS modules. Hursley showed how the methods could be

adapted to problems on an industrial scale.

A particular formal method, the Z notation, was used to specify the new

CICS functionality. Hursley’s programmers were used to writing speciﬁcations

in English, and the rigorous, mathematical notation was seen as a challenge.

In practice, the notation proved easy to learn and to apply, even for program-

mers with no previous experience of mathematics. The result was a perceived

improvement in the quality and reliability of delivered code.

The ﬁrst CICS product to be designed using Z was CICS/ESA version 3, an-

nounced in June 1989. In April 1992, the Queen’s Award for Technological

Achievement was conferred upon IBM United Kingdom Laboratories Limited

and Oxford University Computing Laboratory for ‘the development and use of

an advanced programming method that reduces development costs and signif-

icantly enhances quality and reliability’: namely, Z.

1.3 The Z notation

The Z notation is based upon set theory and mathematical logic. The set theory

used includes standard set operators, set comprehensions, Cartesian products,

and power sets. The mathematical logic is a ﬁrst-order predicate calculus. To-

gether, they make up a mathematical language that is easy to learn and to apply.

However, this language is only one aspect of Z.

Another aspect is the way in which the mathematics can be structured.

Mathematical objects and their properties can be collected together in schemas:

patterns of declaration and constraint. The schema language can be used to

describe the state of a system, and the ways in which that state may change. It

can also be used to describe system properties, and to reason about possible

reﬁnements of a design.

A characteristic feature of Z is the use of types. Every object in the mathe-

matical language has a unique type, represented as a maximal set in the current

speciﬁcation. As well as providing a useful link to programming practice, this

notion of types means that an algorithm can be written to check the type of

every object in a speciﬁcation; several type-checking tools exist to support the

practical use of Z.

4 1 / Introduction

A third aspect is the use of natural language. We use mathematics to state

the problem, to discover solutions, and to prove that the chosen design meets

the speciﬁcation. We use natural language to relate the mathematics to objects

in the real world; this job is often partly achieved by the judicious naming

of variables, but additional commentary is vital. A well-written speciﬁcation

should be perfectly obvious to the reader.

A fourth aspect is reﬁnement. We may develop a system by constructing a

model of a design, using simple mathematical data types to identify the desired

behaviour. We may then reﬁne this description by constructing another model

which respects the design decisions made, and yet is closer to implementation.

Where appropriate, this process of reﬁnement can be continued until executable

code is produced.

The Z notation, then, is a mathematical language with a powerful struc-

turing mechanism. In combination with natural language, it can be used to

produce formal speciﬁcations. We may reason about these speciﬁcations using

the proof techniques of mathematical logic. We may also reﬁne a speciﬁcation,

yielding another description that is closer to executable code.

Z is not intended for the description of non-functional properties, such as

usability, performance, size, and reliability. Neither is it intended for the de-

scription of timed or concurrent behaviour. However, there are other formal

methods that are well suited for these purposes. We may use these methods

in combination with Z to relate state and state-change information to comple-

mentary aspects of design.

1.4 The importance of proof

In this book, we place considerable emphasis upon proof. When we introduce

the language of mathematical logic, we explain the use of a proof system. When

we introduce the language of sets and relations, we explain how formal proofs

may be constructed about such objects. When we introduce the language of

schemas, we show how to prove that a speciﬁcation is consistent, and how to

prove that one speciﬁcation reﬁnes another. Our intentions are two-fold: ﬁrst,

to show that proof adds quality to software development; second, to show that

proof is a feasible part of the industrial use of formal methods.

If we reason about a speciﬁcation, if we attempt to construct proofs about

its properties, then we are more likely to detect problems at an early stage

of system development. The process of constructing proofs can help us to

understand the requirements upon a system, and can assist us in identifying

any hidden assumptions. Proof at the speciﬁcation stage can make a signiﬁcant

contribution to the quality of software.

1.5 / Abstraction 5

At the design stage, a proof can show us not only that a design is correct, but

also why it is correct. The additional insight that this aﬀords can be invaluable:

as requirements evolve and the design is modiﬁed, the consequences are easier

to investigate. At the implementation stage, a proof can help us to ensure that

a piece of code behaves according to the speciﬁcation. Again, a signiﬁcant

contribution to quality can be made.

The construction of proofs is an essential part of writing a speciﬁcation,

just as proof-reading is an essential part of writing a book. A speciﬁcation

without proofs is untested: it may be inconsistent; it may describe properties

that were not intended, or omit those that were; it may make inappropriate

assumptions. The practice of proof makes for better speciﬁcations.

It seems to be part of software engineering folklore that proof is impos-

sible on an industrial scale; however, our experience has been diﬀerent. We

have been involved in many large-scale applications of formal methods; some

involved proof, others did not. We have seen that techniques involving proof

are successful where formal methods are used with a light touch, and where

proofs are conducted at an appropriate level of formality.

In many situations, a rigorous argument, or a semi-formal justiﬁcation, will

be suﬃcient to bring about the desired improvement in quality. In other, more

critical situations, it may be necessary to increase the level of formality until

the correctness of the design is beyond doubt. In some situations, a completely

formal proof may be required. The trick of using formal methods eﬀectively is

to know when proofs are worth doing and when they are not.

1.5 Abstraction

An essential property of a good speciﬁcation is an appropriate choice of abstrac-

tion. A good example of this is provided by the various maps of the London

Underground. When the ﬁrst map was published in 1908, it was faithful to the

geography of the lines: all the twists and turns of the tracks and the relative

distances between stations were recorded faithfully and to scale. However, the

purpose of the map was to show travellers the order of stations on each line,

and the various interchanges between lines; the ﬁdelity of the map made it

diﬃcult to extract this information.

In 1933, the map was changed to a more abstract representation, called

the Diagram. Here, the connectivity of stations on the network was preserved,

and at last, passengers could see at a glance the route to their destination.

Abstraction from superﬂuous detail—in this case the physical layout of the

lines—was the key to the usefulness of the Diagram. Figures 1.1 and 1.2 show

published versions before and after the change.

剩余406页未读，继续阅读

jiangdmdr

粉丝: 58
资源: 764

Z语言：形式化描述与证明基础

Z语言--一种形式化描述语言

软件形式化方法Z语言.rar

形式化z语言辅助工具Z-EVES

移动Agent系统的Z语言形式化描述

基于Real-Time Object-Z语言的实时系统形式化描述* (2007年)

形式化规约——Z语言

形式化语言 Z语言 博士研究生课程收集

软件工程形式化z语言辅助工具

形式化语言 USING IN Z LANGUAGE

Z语言是由牛津大学程序设计研究小组开发的一种形式语言

最新资源

形式化语言 Z语言博士研究生课程收集