规格说明语言Z的类型检查  

TYPE CHECK FOR SPECIFICATION LANGUAGE Z

作　　者：张晓莺[1] 朱关铭[1] 缪淮扣[1] 

机构地区：[1]上海大学计算机科学系,上海201800

出　　处：《计算机应用与软件》2000年第2期1-9,29,共10页Computer Applications and Software

基　　金：国家863高科技计划;上海市高校科技发展资金资助(编号:69773038)

摘　　要：软件规格说明的正确性是软件目标代码正确性的前提。正确性要求之一就是类型正确。本文介绍Z规格说明类型检查器的实现方法,并对类型检查的环境、一致化方法、替换策略和类型变量的应用等问题进行讨论。Hie correctness of the specification of a software is the precondition of the correctness of the destination code. One of the correctness requirements is the correctness of type. This paper introduces the implementation of a Z specification type checker, meanwhile the environment of type check, unification method, substitution strategy are also discussed.

关 键 词：类型检查 规格说明语言 Z语言 形式谱义 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构] TP312[自动化与计算机技术—计算机科学与技术]