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