XYZ/SE程序的验证
DOI:
作者:
作者单位:

作者简介:

通讯作者:

基金项目:

本项目受王宽城基金的资助.


VERIFICATION OF XYZ/SE PROGRAMS
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
    摘要:

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

    Abstract:

    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.

    参考文献
    相似文献
    引证文献
引用本文

张文辉. XYZ/SE程序的验证.软件学报,1995,6(12):719-727

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
历史
  • 收稿日期:1994-05-12
  • 最后修改日期:1994-10-24
  • 录用日期:
  • 在线发布日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号