·588 北京科技大学学报 1998年第6期 Seroid=df2[Dom:Type,Eq:Dom→Dom→Prop].. Setoid是一个同该类型上的一个二元关系共存的类型，这个关系是一个在规范的公理部 分指明的一个同余关系，被用于表示该抽象类型上所要的相等性.这种相等性不同于具体数 据类型程序中的计算相等性.它对于今后要进行的分步方式提纯是很重要的. 于是，一个自然数堆栈的规范就可以如下给出：Str[Stack()]=df Stack:Setoid;: empty:Dim[Stack]; push:N-Dom[Dom]+Dom[Stack]; pop:Dom[Stack]Dom[Stack];top:Dom[Stack]+N. 而对于某个类型为Str[Stack(M]的结构S,有：Ax[Stack(Ml(S)=df ConqStack(M(Eq); Eq(pop(empty),empty); top(empty)=N n:N s:Dom[Stack].Eq(pop(push(n,s)),s);n:N s:Dom[Stack].top(push(n,s))=N.. 在这里，Stack是Stack[S]的简写，Eq是Eq[S]的简写，CongStack(M(Eq)表示堆栈间的一个同 余关系，有：CongStack()=df Equiv(Eq)& s,s'Dom[Stack].Eq(s,s);top(s)=Ntop(s&Eq(pop(s),pop(s'))& m,n:N.m =N Eq(push(m,s),push(n,s')). 这样，就建立了一个抽象数据类型的ECC表示，类似地还可以建立其他数据类型，在这些类 型的基础上按一定的语义关系加以复合就能组成较大的程序，这方面的探讨可参见文献[5]. 4 ECC的ML实现 上述内容是用函数型语言ML来实现的，其他编程语言，因它们的非描述型语言常会涉 及一些与机器有关的低级细节，并且缺乏直接定义代数类型的手段，程序也复杂冗长， ML是用一种叫结构的单元来实现程序的模块化.从静态角度看，程序形成一种相互关 联的分层组织.而对动态构造的支持则由一种所谓的functor函子来完成，ML的这些特性使 我们能用它很方便地描述前面的ECC类型层次.由于目前多数程序说明和证明环境直接是 用ML来实现的，因此将上述工作用ML加以描述会有助于将来和这些环境形成一个统一的 整体，是十分有意义的. 下面建立一个用ML表示的ECC特征ECC LANG: signatureECC LANG sig datatype term Var of string Bound of int Ipair of term of term Prop projL of term Ecc_Type of int projR of term Lam of string term prod of staring termterm App of term term Sum of string term term end 在这里，tem是ECC项，Bound是约束变量，Prop是命题类型，Ecc_ype是由int决定的 Typei,,Lam即为Ax:A.M,App有形式MN,pair定义了序偶类型，projL和projR分别对应前面 的πl(M)和π2(M)类型.prod和Sum则代表和类型与积类型. ECC的规则集在ML中可以作为一种抽象证明状态类型上的集合来对待，状态State提北 京 科 技 大 学 学 报 二 泛〔山 ， ，氏 ， 年 第 期 是 一个 同该类 型上 的一个二元 关系共存 的类 型 ， 这个 关系是 一个 在规范 的公理部 分指 明的一个 同余 关 系 ， 被 用 于 表示 该抽 象类型 上所要 的相 等性 这种 相 等性 不 同于 具 体数 据类型程序 中的计算相 等性 它 对于 今后要 进行的分步方式提纯是很重要 的 于 是 ， 一个 自然数堆 栈 的规范就可 以 如下 给出 匆」 以 那争 均 均 ， 均 姗 均 ，伪 的 ， 而 对于某 个类 型 为 姗 扔 的结构 ， 有 扔 泳 扔 鞠 鞠 卯试 ， 试 戈 万 伪 姗 训 ， ， 均 训 ， 从 在这 里 ， 是 泳 的简 写 ， 是 〔 的简写 ， 扔 鞠 表示 堆栈 间的一 个 同 余关系 ， 有 的 ， ， 心 ， 今 今 鞠 ， ’ ， 拟 戈 ， ， ， ’ 这 样 ， 就 建 立 了 一 个抽 象数据类型 的 表 示 ， 类 似地 还 可 以 建 立 其 他 数 据类 型 ， 在 这 些 类 型 的基础 上 按 一定 的语义 关 系加 以复合就 能组 成较大 的程 序 这方 面 的探讨可参见 文 献 【 的 实现 上述 内容是 用 函 数型语 言 来实现 的 ， 其他编 程 语 言 ， 因它 们 的非 描述 型语 言 常会涉 及 一些 与机器有 关 的低级 细节 ， 并且缺乏 直接定义代数类型 的手段 ， 程 序也复杂冗长 是 用 一 种 叫结构 的单元来 实现程 序 的模 块 化 从 静 态 角 度 看 ， 程 序 形 成 一 种 相 互 关 联 的分层 组织 而 对动态构 造 的支持则 由一种所 谓 的 伪 函子 来完成 ， 的这些 特性 使 我 们能用 它很 方便地描述 前 面 的 类型层 次’ 由于 目前多 数程序说 明和证 明环 境直接是 用 来 实现 的 ， 因此将 上 述 工作 用 加 以描述 会有 助 于将来 和这些 环境形 成 一个 统一 的 整 体 ， 是 十分有意义 的 下 面建 立 一个用 表示 的 特征 详 画 在 这 里 ， 是 项 ， 是 约束 变 量 ， 是命题 类 型 ， 一 是 由 决定 的 ， 城 即为又 ， 有形 式 囚 ， 呷 定义 了序偶类型 ， 和 分别对应前面 的兀 峋和 峋类 型 和 则代表和类型 与积类型 的规则集 在 中可 以作 为一种 抽象证 明状态类 型 上 的集合来对待 ， 状态 提