基于ECC的程序规范描述

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

·586· 北京科技大学学报 1998年第6期 ●变元(x,y,…)是项； ●如果A,B,M和N是项，那么Ix:A.B,1:A.MMN,∑x:A.B,pair∑x:A.BA,M, π1(0和π2(M都是项 用≡表示等同，△表示化简，≌表示变换，如：(ax:A.)N△[N/M. Typei叫类别，也叫类型空间，其中包含的类型形成一种所谓类型累积(ype comulativ-- ity).这种累积在语法上用下面的偏序关系来表示. 定义1类型累积. 定义≤为项上与变换≌有关的最小偏序，有：(1)Prop≤Typei≤Type1≤；(2)如果 A≌A,而且B≤B',那么ΠⅡx:A.B≤Ⅱx:A'.B';(3)如果A≤A,而且B≤B',那么∑x:A. B≤∑x:A'.B',Ais valid T,is valid(xEVO方 (C2 I.xA,I'is valid T,xAH M:B （vamT,xAP十xA；T-ixAMⅢEAB Tis valid Tis valid (KIProp:Type0' (K2 Typei:Typei+T° I,x水PPop；I2 Typei IHA;Typei I,x A-B:Typei (I1TPⅡA.P:Prop CeO T Tk∑xAB:Typei T-M:A I-N:[M/x]B I,x.A-B:Typei (pair) T-pair∑xAB(M,M:∑xA.B au'品是arn丽 T-M∑xA.B (conv) I-M:A I-4:Typei 4);(conv) TM:A IHA':Typei (AA). T-M:A' T M:A' 对断言J的推导形式一个有穷的断言序列J,…,Jn有J=J.比如，对于1≤i≤n,J是某 个推理规则某次施用的结果，其前提为J少<)，如果存在J的一个推导，则称断言J是可推 导的.用T上“A表示“如TM:A对某个A是可推导的，那么项M就有上下文中的类型A”. 下面从推理规则来看一下ECC的类型的分层累积特性.在ECC中，空间(universe)是一 个类型，它把许多类型作为其对象.也就是说，这些类型又是把空间作为它们的类型的.规则 (KI)、(K2)就引人了空间类型Prop和Typei(i∈w)可直接看出：Prop∈Type0 ETypel E·, 从而有，类型Prop的任一对象都是类型Type0的一个对象，而类型Typei的任一对象都是 Typei+I的一个对象.也就是说，PeopEType(0 Typel….这种空间之间的类型包含，与≤ 一起构成了前面定义的类型之间的子类型关系.其推理规则表示即是(cum).这一规则隐示

· · 北 京 科 技 大 学 学 报 年 第 期 变元 ， ， … 是 项 如果 ， ， 和 是 项 ， 那 么 ， 又 ， ， 艺 ， 艺 ， 扔 ， 们 哟和 二 娜都是 项 用 三 表示 等 同 ， △表示 化简 ， 望表示 变换 ， 如 认 娜 肥〔 肠 叫类 别 ， 也 叫类 型 空 间 ， 其 中包含 的类 型 形 成 一 种 所 谓 类 型 累 积 这种 累 积在语法 上 用 下 面 的偏 序关系来表示 定义 类 型累积 定 义 ‘ 为 项 上 与 变 换 望 有 关 的 最 小 偏 序 ， 有 ‘ 肠 ‘ ‘ … 如 果 望 才 ， 而 且 ， ， 那 么 才 尸 如 果 ’ ， 而 且 ‘ ， ， 那 么 区 ‘ 艺 才 了 ， ‘ 咬 当且仅 当 ‘ 且 哭 中的上下 文是 有 形 式 戈 的有穷系列 在此 是 一个变元 ， 而 是 一个项 空 上下 文 用 表示 ， 断言 的形 式 为 或厂 卜 胚 ， 在 此 是 上下 文 ， 而 和 是 项 下 面是 的推理规则 表示 在上下 文 中的 自由变量集 卜 厂 ，茉 苗 ， 汇 ， ‘ ，工 ，厂 ’ 卜 羌 ， 尤 卜 触 一又茉 掀 茉 了 训丫 产 ‘ 矛、 、 ，丫佘岩猛 击洗答恙 牛不焉备黑石 卜 次 ， 不 卜 卜 茉 一 触 汇 厂卜 卜 【 名 卜 ， 戈 卜 卜 艺二 厂卜 触月 卜 龙 万 ， 羌 卜 卜 叉 二 从 的 艺二 兀 厂卜 肚 艺二 厂卜 兀 娜 兀 卜 艺二 厂卜 兀 娜 二 娜 卜 触 卜 份 卜 几吏 ， 今 卜 掀 卜 几 卜 人更 ‘ 〕 对断言 的推 导形 式 一个 有穷 的断言序列 去 ， … ， 寿有 大兰 比如 ， 对于 ‘ ‘ 。 ， 是某 个推理规则某 次施 用 的结果 ， 其前提 为 弓以 · 如果存在 的一个推 导 ， 则称断言 是可 推 导的 用 卜 赫 表示 “ 如 卜 胚 对某个 是 可 推导的 ， 那么项 就有上下文 中的类型 ’尸 下 面从推理规则来 看 一下 的类 型 的分层累积特 性 在 中 ， 空 间 是 一 个类型 ， 它 把许多 类 型 作 为其 对象 也 就是 说 ， 这些 类型 又是 把空 间作为它 们 的类 型 的 规则 、 就 引人 了空 间类 型 和 可 直 接看 出 〔 ‘ 。 二 ， 从而有 ， 类 型 的任 一 对 象 都是 类 型 的 一 个 对象 ， 而 类 型 的 任 一 对象 都 是 的一 个 对象 也 就 是 说 ， 二 互 二 · … 这 种 空 间之 间 的类 型 包含 ， 与 一 起 构成 了前 面 定 义 的类 型 之 间 的子类 型 关系 其推理规则表示 即是 这 一规则 隐示

Vol.20 No.6 蔡家楣等；基于ECC的程序规范描述 ·587· 2个可转换类型具有相同对象，ECC中的空间给出了一种很强的多态概念，这就为结构化机 制提供了可能， 在ECC中，Ⅱ类型和∑类型是2个重要的相关类型.Π类型又叫相关积类型，它提供了相 关的函数空间和嵌人逻辑的逻辑公式.当B不相关于x(xFV(B)时，ⅡxA.B记作AB规则 I1)(I2)为其形成规则，(u)和(pp)为其引入规则和消去规则.它的计算规则是β变换，即(a xAb)(a)[a/刘b,在此[a/为普通的代人运算. 另一种相关类型是∑类型.∑xAB(),又叫强和类型.直觉上表示序偶(a/b)的集合.在 这里，a是类型A的对象，而b是类型B(a)的对象，当B是A上的谓词时，它直觉上就表示类 型A满足特性B的对象的子集.规则集中（∑）是其形成规则，(pai)是引人规则，（πl)(π2）是 消去规则，其变换规则为：πi(pairA(a,a,)》≌a,(i=1,2). 当B不相关于x(x∈FV(B)时，可以把∑xA.B表示为A×B,一般用(a,b)表示序偶，来 代替pairA(a,b). ECC的上述类型层和相关类型提供了对抽象数据类型进行描述和结构化的机制.同时， 由于类型层次的多态机制，也使建立参数化的高阶模块得以共享结构成为可能， 2程序规范的ECC表示 用Main-lof的类型理论，人们可以这样来写一个排序程序的规范： Sorting df f:List(N)-List(N).1:List(N).Sorted(1,f(1)). 它直接指明了内建在系统中的具体数据类型的程序，如自然数N,表Lst等.但是对于需要进 行分步方式提纯开发的大型程序来说，人们更希望用具有松散语义的抽象数据类型规范来表 示.而当我们用ECC来表示一个规范时，可以把它看成是由一个类型序偶组成的.这一类型 的对象即是可以实现这个规范的某个可能的结构.而在这类型上的一个谓词，则说明该规范 在实现时应满足的特性， 首先，我们应建立一个标准规范集类型SPEC: SPEC df >[Str:Type,Ax:Str-+Prop]. 在这个类型定义中可见，一个SPEC集中的规范SP是由一个SP的结构类型S[SP]和在 St[SP]上的谓词Ax[SP]组成的.Sr在类型层次中有Type类型（此处省去i下标），而Ax,则为 一介Ⅱ类型.把一个规范不仅看成是一个类型，而且看成是一个序偶，这样就把程序的公理性 要求和计算内容相分离，体现了抽象数据类型的特点， 对类型理论来说，重要的是对每个规范都要找到它的一个实现，规范SP的一个实现应是 某个结构s和Ax[SP]可满足的证据在一起就叫做SP的一个模型.SP模型集的类型为： Mod(SP)=df s:Str[SP].Ax[SP](s). 如果模型集非空，则存在一个SP的实现，称之为可实现的，或一致的(consisten),于是， 上面的自然数排序程序用ECC描述就应由结构类型ist(M)→List(W)和谓词1f:List() Lis().1Lis(M.sorted(1,f(1)两部分组成.这个规范的某个实现就是一个排序程序. 3自然数堆栈的ECC规范实例 要说明一个抽象数据类型，可用下面的定义：

蔡家嵋等 基于 的程序规范描述 个可 转 换类 型 具 有 相 同对象 ， 中的空 间给 出 了 一 种 很 强 的多 态 概 念 ， 这就 为结 构化机 制 提供 了 可 能 在 中 ， 类 型和 艺类型是 个重要 的相 关类 型 类 型 又 叫相 关积类 型 ， 它 提供 了相 关 的 函数空 间和嵌人逻辑的逻辑公式 当 不相 关于 苗 功时 ， 二 记作 争 规则 、 为其形 成规则 ， 以 和 为其引人规则 和 消去规则 它 的计算规则是月变 换 ， 即 以 二 〔 ， 在此 为普通 的代人 运算 另一 种相 关类型是 艺类型 艺二 ， 又 叫强 和类型 直觉上 表示 序偶 。 的集合 在 这 里 ， 是类型 的对象 ， 而 是类型 的对象 当 是 上 的谓词 时 ， 它直觉 上就表示 类 型 满足 特性 的对象的子集 规则集 中 艺 是 其形 成规则 ， 是 引人规则 ， 们 二 是 消去规则 ， 其变换规则为 二 ， 哭 ‘ ， · 当 不 相 关于 二 。 功 时 ， 可 以把 艺二 表 示 为 ， 一般用 ， 表示 序偶 ， 来 代替 滋 ， 的上述类型层和相 关类型提供 了对抽象数 据类 型 进行 描 述 和 结 构化 的机制 同时 ， 由于类型层次的多态机制 ， 也使建立参数化 的高阶模块得 以共享结构成 为可 能 程序规范的 表示 用 一 的类型理论 ， 人们可 以这样来写 一个排序程序 的规范 由 艺 叹扔 ， 《扔一 《 扔 ， 它直接指 明了 内建在系统中的具体数据类型 的程 序 ， 如 自然数 ， 表 等 但是 对于需 要 进 行分步方式提纯开发的大型程序来说 ， 人们更 希望 用 具有松散语义 的抽象数据类型规 范来表 示 而 当我们用 来表示 一个规范 时 ， 可 以 把 它 看 成是 由一 个类 型序 偶 组 成 的 这 一 类型 的对象 即是 可 以 实现这个规范的某个可 能的结构 而 在 这类 型 上 的一 个 谓 词 ， 则说 明该规范 在 实现 时应满足 的特性 首先 ， 我们应建立一个标准规范集类型 艺 ， 卜 在 这个类型定义 中可见 ， 一个 集 中的规范 是 由一个 的结构类型 和 在 试 上 的谓词 〔 组成的 在类型层次 中有 类型 此处省 去 下 标 ， 而 ， 则 为 一介 类型 把一个规范不仅看成是 一个类型 ， 而且 看 成是 一个序偶 ， 这样就 把程 序 的公 理性 要求和计算 内容相分离 ， 体现 了抽象数据类型 的特 点 对类型理论来说 ， 重要 的是对每个规范都要 找到 它 的一个实现 ， 规范 的一个实现应是 某个结构 和 【 可满足 的证据在 一起就 叫做 的一个模型 模 型集 的类 型 为 泛 虹 如果模 型集非空 ， 则存在一个 的实现 ， 称之 为可实现 的 ， 或一致 的 于是 ， 上 面 的 自然 数 排 序 程 序 用 描 述 就 应 由 结 构 类 型 《 扔 ， 《扔 和 谓 词 几 《 扔 ， 叹扔 《 扔 ， 两部分组成 这个规范的某个实现就是 一个排序程序 自然数堆栈的 规范实例 要说 明一个抽象数据类 型 ， 可 用 一 下面 的定义

·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提

北 京 科 技 大 学 学 报 二 泛〔山 ， ，氏 ， 年 第 期 是 一个 同该类 型上 的一个二元 关系共存 的类 型 ， 这个 关系是 一个 在规范 的公理部 分指 明的一个 同余 关 系 ， 被 用 于 表示 该抽 象类型 上所要 的相 等性 这种 相 等性 不 同于 具 体数 据类型程序 中的计算相 等性 它 对于 今后要 进行的分步方式提纯是很重要 的 于 是 ， 一个 自然数堆 栈 的规范就可 以 如下 给出 匆」 以 那争 均 均 ， 均 姗 均 ，伪 的 ， 而 对于某 个类 型 为 姗 扔 的结构 ， 有 扔 泳 扔 鞠 鞠 卯试 ， 试 戈 万 伪 姗 训 ， ， 均 训 ， 从 在这 里 ， 是 泳 的简 写 ， 是 〔 的简写 ， 扔 鞠 表示 堆栈 间的一 个 同 余关系 ， 有 的 ， ， 心 ， 今 今 鞠 ， ’ ， 拟 戈 ， ， ， ’ 这 样 ， 就 建 立 了 一 个抽 象数据类型 的 表 示 ， 类 似地 还 可 以 建 立 其 他 数 据类 型 ， 在 这 些 类 型 的基础 上 按 一定 的语义 关 系加 以复合就 能组 成较大 的程 序 这方 面 的探讨可参见 文 献 【 的 实现 上述 内容是 用 函 数型语 言 来实现 的 ， 其他编 程 语 言 ， 因它 们 的非 描述 型语 言 常会涉 及 一些 与机器有 关 的低级 细节 ， 并且缺乏 直接定义代数类型 的手段 ， 程 序也复杂冗长 是 用 一 种 叫结构 的单元来 实现程 序 的模 块 化 从 静 态 角 度 看 ， 程 序 形 成 一 种 相 互 关 联 的分层 组织 而 对动态构 造 的支持则 由一种所 谓 的 伪 函子 来完成 ， 的这些 特性 使 我 们能用 它很 方便地描述 前 面 的 类型层 次’ 由于 目前多 数程序说 明和证 明环 境直接是 用 来 实现 的 ， 因此将 上 述 工作 用 加 以描述 会有 助 于将来 和这些 环境形 成 一个 统一 的 整 体 ， 是 十分有意义 的 下 面建 立 一个用 表示 的 特征 详 画 在 这 里 ， 是 项 ， 是 约束 变 量 ， 是命题 类 型 ， 一 是 由 决定 的 ， 城 即为又 ， 有形 式 囚 ， 呷 定义 了序偶类型 ， 和 分别对应前面 的兀 峋和 峋类 型 和 则代表和类型 与积类型 的规则集 在 中可 以作 为一种 抽象证 明状态类 型 上 的集合来对待 ， 状态 提

Vol.20 No.6 蔡家楣等：基于ECC的程序规范描述 ·589· 供一个操作的有穷集，证明状态的子目标被从1开始编号，把某个规则使用于子目标i即产生 一个新状态. 定义一个公式类型fom 再定义目标和状态类型： (包括原子公式、连接公式和量词公式)： datatype form Pred of string term list Conn of string form list type goal form list form Quant of string string form datatype state State of goal list form int 如果一个状态序列用state Seq,T来表示的话，那么一个规则就有类型：state→stateSeq,T. 5结论 ECC提供了一种肯有很强逻辑能力和结构化机制的类型理论方法，把这种方法应用于 程序的形式化表示，不但可以解决一阶逻辑固有的不可判定的困难，并且因为它的结构化模 块化机制，也使程序规范说明简单可行，当然，要实现用ECC来开发一个程序规范并进行程 序版本演化和正确性证明，还需要解决规范的组合、分解和参数化等问题.对此另文讨论， 参考文献 1 Matin Lof.Constructive Mamatics and Computer Programming.In:Logic,Methodology and Philosophy of Science (VI),1982 2 Simon Thompson.Type Theory and Functional Programming.New York:Addison Wesley Publishing Company,1991.339~346 3 Zhaohui L.ECC,an Extended Calculus of Constructions.In Proc of Fourth Ann.Symp on Logic in Computer Science.Califomia:Asilomat,1989.387 4 Paulson C.ML for the Working Programmer.Cambridge:Cambridge University Press,1991.235 5蔡家楣，复合抽象数据类型的构造型说明.浙江工业大学学报，1996(2)：108 Development of Specification of Program Based on ECC Cai Jiamei)Du Guwi 1)Institute of Information,Zhejiang University of Technology,Hangzhou 310014 2)Applied Science School,UDT Beijing,Beijing 100083 ABSTRACT A Extended Calculus of Constructions(ECC)is introduced.The description of specification for abstract data type with loose semantics and a implementation at the functional language ML are also discussed. KEY WORDS extended calculus of constructions(ECC);specification;functional language

蔡家嵋等 基于 的程序规范描述 · · 供一个操作 的有 穷集 ， 证明状态 的子 目标被从 开始编号 ， 把某 个规则 使用于 子 目标 即产生 一个新状态 定 义一 个公 式类 型 再定义 目标和 状 态类 型 包括 原子公 式 、 连接公 式和量 词公 式 助 如果 一个状态序列 用 来表示 的话 ， 那么一个规则就有类型 卜 结论 提供 了一 种肯有很 强 逻 辑能力和 结 构化机 制 的类 型 理 论方 法 ， 把这 种 方 法 应用 于 程序 的形 式化 表示 ， 不但可 以解 决 一 阶逻辑 固有 的不 可判 定 的 困难 ， 并且 因为它 的结 构化模 块 化机制 ， 也使程 序规范说 明简单可 行 当然 ， 要 实现 用 来 开 发一 个程序规范并 进行程 序版本演化和正确性证 明 ， 还需要解决规范 的组合 、 分解和参数化等问题 对此 另文讨论 参 考 文 献 田的 比口 助 ， ， 娜 吐口 陇 ， 一 毛 ， 】 助 权 山 ， 蔡家媚 复合抽象数据类型 的构造型说明 浙江工 业大学学报 ， ’ ， 产 ， ，卜巨 ， 飞 ， 伪