| 摘要: |
| 在软件方法学中，形式方法越来越受到人们的重视，并已被应用于软件开发．Z是一种基于数学表示的软件规格说明方法．前置条件的简化是Z规格说明方法中一种标准的检查，本文讨论了Z规格说明中关于操作的前置条件及其计算．提出了简化过程的终止条件，给出了一个用于简化前置条件的算法，该算法可自动产生简化过程的证据． |
| 关键词: 形式方法 Z规格说明 前置条件 简化 |
| DOI： |
| 分类号: |
| 基金项目:本文研究得到国家863高科技项目基金资助. |
|
| THE SIMPLIFICATION OF PRECONDITION IN Z SPECIFICATIONS |
|
MIAO Huaikou
|
| Abstract: |
| In software methodology，formal methods is being paid more and more atten-tion and has been applied to software development．Z is a kind of software specification notations based on mathematics．The simplification of precondition is a standard check for Z sDecifications．This paper discusses the precondition in Z specifications and its calcula-tion. Droposes a termination condition for simplifying the precondition and presents a sim-plifying aIgorithm which can automatically produce the justifications during the process of simplifying precondition． |
| Key words: Formal methods Z specifications precondition simplification |
