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