VERIFICATION OF XYZ/SE PROGRAMS
DOI:
Author:
Affiliation:

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:May 12,1994
  • Revised:October 24,1994
  • Adopted:
  • Online:
  • Published:
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063