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