XYZ／SE程序的验证

VERIFICATION OF XYZ/SE PROGRAMS

ＸＹＺ／Ｅ的好处之一在于高级和低级的说明能够在同一框架下表示，因而使得软件的说明和实现变得容易一些．在这同时，开发验证工具以验证不同层次的说明是否满足所期望的关系是很重要的．谢洪亮等同志曾研究过ＸＹＺ／ＳＥ程序的验证规则．本篇文章增加了有关使用数组、过程说明和过程调用的规则．同时着重说明ＸＹＺ／ＳＥ程序验证的自动化方面的问题，且实现了一些化简验证条件的规则．

One of the advantages of XYZ/E is that both high level and low level specifications can be represented in the same frame work, so that it makes specification and implementation of software systems easier. It is important to develop verification tools to verify whether the expected relation between different levels of specifications holds. Rules for verification of XYZ/SE programs had been studied by Xie Hongliang et al. in a previous paper. This paper extends the set of the rules to include rules for use of arrays, for procedure specification and for procedure call. It puts the emphasis on the practical and mechanical aspects of the verification of XYZ/SE programs. A set of rules for simplifying verification conditions is also implemented.