D0I:10.13374/j.issn1001-053x.1998.06.018 第20卷第6期 北京科技大学学报 Vol.20 No.6 1998年12月 Journal of University of Science and Technology Beijing Dec.1998 基于ECC的程序规范描述 蔡家楣)杜国维) 1)浙江工业大学信息工程学院，杭州3100142)北京科技大学应用科学学院，北京100083 摘要介绍一种扩展的类型理论构造演算ECC;讨论了用它表示松散语义抽象类型的程序规范 的方法.然后介绍如何用函数型语言ML使这种方法得以实现. 关键词扩展构造演算(ECC):程序规范；函形象型语言 分类号TP311.1 长期以来，在程序形式化表示的问题上存在着困难，一阶逻辑被证明是不适合用于计算 机的.人们把兴趣开始转向类型理论(typr theory).因为它在程序规范说明、程序构造和程 序验证方面提供了一种统一的框架.类型理论最初是作为数学原理和形式来开发的，由于 Matin-lof等人的工作而日益著名.现在除Main-lof的类型理论外，还有如Eindhoven大学的 Automath类型理论，康奈尔大学的Nuprl,.以及Coquand-Huet的构造演算等.在某些类型理 论中已经讨论了程序推导的问题，有的也可作为编写规范说明和程序的语言使用，但在涉及 模块设计和结构化方面，还没有很好解决.因而类型理论的应有潜力还没有得到很好的开发， 扩展构造演算ECC(Extended Calculus of Construction)是英国Edinbjurgh大学计算机 系在90年代初提出的一扩充了的类型理论.它具有很好的结构化机制，提供了进行结构化模 块化规范设计的手段，把它应用与程序规范说明，将克服上面提到的一阶逻辑和一般类型理 论的各种困难.下面我们讨论它的形式语法及如何将程序规范用EC℃表示的问题.以及如何 用函数型语言来实现ECC的形式定义， 1 ECC的形式描述 ECC是在Coquand-Huet的构造演算基础上扩充了谓词类型论域和∑类型（强和类型），也 可认为是在Matin-lof的类型理论上增加了一个命题的最低层的非谓词层，这样，ECC实际上 就有了与前两者都不同的特性，它包罗了谓词空间和非谓词空间，进一步强化了逻辑分工类 型和集合（数据类型）之间的区别，从而形成了一种关于相关类型(dependent type)的统一理 论，不但提供了很强的逻辑能力，也提供了很好的抽象机制，因而ECC就特别适用于程序规 范和抽象推理 EC℃是由演算和断言的推理规则集两部分组成，项演算的基本表示是项(tem),它由 下面的子句归纳出定义： ●常元Prop和Typei是项；(i<w) 1998-03-25收稿 蔡家帽男，52岁，副教授 *“863“计划和浙江省自然科学基金资助的课题第 卷 第 期 年 月 北 京 科 技 大 学 学 报 灰 】 基于 的程序规范描述 蔡家循 ’ 浙 江工 业大学信息工程学 院 ， 杭州 杜 国维 北京科技大学应用科学学 院 ， 北京 摘要 介绍一种扩展 的类型理论构造演算 讨论 了用 它表示 松散语义抽象类型 的程序规范 的方法 然后介绍如何用 函数型语言 使这种方法得 以 实现 关挂词 扩展构造演算 程序规范 函形象型语言 分类号 长期 以来 ， 在程序形 式化表示 的 问题 上存在 着 困难 ， 一 阶逻 辑被 证 明是 不 适 合用 于 计算 机 的川 人们把兴 趣 开始转 向类 型理 论 因 为它 在 程 序规 范说 明 、 程 序 构 造 和 程 序验 证 方 面 提 供 了 一 种 统一 的框 架 类 型 理 论 最 初 是 作 为数 学 原 理 和 形 式来 开 发 的 ， 由于 一 等人 的工 作而 日益著名 现在除 一 的类 型 理 论外 ， 还 有如 大 学 的 类 型理 论 ， 康奈尔大学 的 吻 ， 以及 一 的构造 演算等 在某 些 类 型 理 论 中 已 经讨论 了程 序推 导的 问题 ，有 的也可作为编 写规范说 明和程 序的语 言使用 但 在 涉及 模块 设计和结构化方 面 ， 还没有很好解决 因而类型理论 的应有潜力还 没有得 到很好 的开 发 扩展 构造 演算 是 英 国 大学计算 机 系在 年代 初提 出的一扩充 了的类型理论 它具有很好 的结构化机制 ， 提供 了进行结 构化模 块化规范设计 的 手段 ， 把它应用 与程序规 范说 明 ， 将克服 上 面提到 的一 阶逻 辑和 一般类 型理 论 的各种 困难 下 面我们讨论它的形式语法及 如何将程序规范用 表示 的问题 以及 如何 用 函数型语言来实现 的形式定义 的形式描述 是 在 一 的构造演算基础 上 扩充 了谓 词类 型论域和 类型 强 和类型 ， 也 可认 为是在 一 的类型理论上增加 了一个命题 的最低层 的非谓词层 这样 ， 实际上 就有 了 与前 两者都不 同的特性 ， 它包罗 了谓词 空 间和 非谓词 空 间 ， 进 一 步强化 了逻 辑分工类 型 和 集合 数据类型 之 间的 区别 ， 从而 形 成 了一 种 关于 相 关类 型 的 统一 理 论 ， 不 但提供 了很 强 的逻 辑能力 ， 也提供 了很 好 的抽象机 制 ， 因而 就特别适用 于 程 序规 范和 抽象推理 是 由演算和 断言 的推理 规则集 两部分 组 成 项 演算 的基 本表示 是 项 ， 它 由 下 面 的子句 归纳 出定义 常元 和 升 是 项 一 一 收稿 蔡家相 男 ， 岁 ， 副教授 “ ” 计划和浙 江省 自然科学基金 资助 的课题 DOI ：10．13374／j ．issn1001－053x．1998．06．018