【英文】软件工程大会论文集 (17).pdf

An Approach to Reasoning about Z Specifications Based on
the Tactic Language*
MIAO Huaikou GAO Xiaolei CHEN Yihai
School puter Engineering and Science,
Shanghai University, Shanghai, 200072, P.
Email: ******@online.


The use of formal specification in software language. A tactic program defines what is to be done
development is ing increasingly prevalent. The and does not say how to do it. The details of how to
ideal of producing software which is provably correct do it is hidden in the implementations.
with respect to a formal specification, is very For a given conjecture about a Z specification,
attractive, One of the major advantages of using a before proving it we should do simplifications which
formal language like Z is that it is possible to reason involves expansion, eliminating of ‘N ’ and application
about the specifications written in it. of the One Point Rule. All these tactics, as basic
We are considering constructing a tactic-mands, have been implemented in ZDS. After
inference system containing tactic programs in ZDS being simplified the goal is separated into a series of
(Z Development Studio) which we are developing. subgoals.
Tactic program is a kind of automatic proof tool that Finding a proof is often one of trial and error, and
does not demand user to know the details of the the various attempts e very large. The structure