English

应用科学学报 ›› 1999, Vol. 17 ›› Issue (4): 450-456.

• 论文 • 上一篇    下一篇

语法制导的Z规格说明检查器

李刚1,2, 缪淮扣1, 童頫1   

  1. 1. 上海大学;
    2. 中国科学院软件研究所
  • 收稿日期:1998-06-12 修回日期:1998-09-21 出版日期:1999-12-31 发布日期:1999-12-31
  • 基金资助:
    国家自然科学基金(69773038);上海市高校科技发展基金资助项目(97A42)

Design and Implementation of a Syntax-driven Z Specification Checker

LIGANG1,2, MIAO HUAIKOU1, TONG FU1   

  1. 1. Shanghai University, Shanghai 201800;
    2. Institute of Software, Chinese Academy of Sciences, Beijing 100080
  • Received:1998-06-12 Revised:1998-09-21 Online:1999-12-31 Published:1999-12-31

PDF

70

被引次数

15

摘要： Z语言是牛津大学程序设计研究组设计的形式规格说明语言.作为Z语言处理前端的Z规格说明检查器用于Z规格说明的语法检查和类型检查,它通过自顶向下和自底向上相结合的方法,实现了Z语言的语法分析功能;此外,还结合Z语言的类型特征,实现了Z语言的类型检查,介绍了Z规格说明检查器的设计与实现.

关键词: 类型检查, 语法制导, 形式方法, Z语言

Abstract: Z specification language is an active domain in the field of formal methods. As the front-end of any Z supporting system,Z specification checker can support other subsystems,such as refining subsystem,and specification-based software testing subsystem.By the integration of top-down parsing and bottom-up parsing,a syntax-driven Z specification checker has been implemented.This paper gives a description of the principle and implementation of this tool.

Key words: Z language, syntax-driven, type check, formal methods