·78 工程科学学报，第44卷.第1期 中若包含违反上述规定的行为，现实合约将自动 条件，将其转换为可执行代码，并提供了一种将业 失效，与此对应的智能法律合约、代码、链码也将 务规则表示为模块化独立单元的方法，兼有使用 自动视为无效合同，从而可以保证满足原则3)的 优先级和覆盖谓词来解决冲突的能力.在论文[38] 要求. 进一步研究了使用道义逻辑来表达合约语义的需 针对原则2)，现实合约具有法律约束力，其中 要，并提出了使用可废止逻辑对模态逻辑算子和 规定了全部的合同条款和各方的权利和义务，而 道义逻辑算子的进一步扩展.在论文[39]中提出 代码和链码皆具有极强的专业性和领域性，在涉 了一个用来表示和推理电子合约的架构(DR 及其意思解读时会带来第三方理解的误差或困 CONTRACT).在道义逻辑的基础上增加了可废止 难，难以验证 逻辑，使用道义可废止逻辑(Deontic defeasible 综上，在智能法律合约充当现实合约和智能 logic)来处理合同违约情况. 合约（代码）、链码之间桥梁的基础上，其意思表示 2015年，Idelberger等o提出基于逻辑的智能 一致是智能合约具有法律效力的必要条件，因此 合约语言以替代过程式语言(Procedural language). 在合同订立过程中，必须保证它们间相互转化关 当合约中执行复杂逻辑时，用过程式语言描述合 系是可经过检验求证的，且当事人签订时需知晓 约会使程序更加笨重且易错，同时因为逻辑约束 且同意其互证关系， 的动作执行顺序直接影响程序状态，导致合约不 5智能法律合约研究进展 易维护和监测.而基于逻辑的语言可以避免这个 问题，其规则的顺序不影响程序执行，并且语句声 智能法律合约虽然是一个较新的词汇，但其 明将会更加简洁 涉及到的法律合约逻辑、智能合约形式化表达等 2016年Frantz和Nowostawskil基于捕捉法 基础探索和相关研究在很久前便已经开始了，现 律基本特征的制度语法(ADICO)2提出了将人机 行研究工作主要分为两个方向：合约的逻辑模型 可读的合同半自动翻译成智能合约的方法，支持 研究与智能法律合约语言模型研究.下面分别就 将ADICO组件映射为相应的Solidity结构，包括 这两方面研究进展予以介绍与分析， 生成合约地址、修饰器名称、函数框架，但是尚未 5.1合约逻辑模型研究 实现函数主体和Solidity表达式的转换 在早期论文中，I952年，von Wright发表论文 Denotic logic!3,被视为现代道义逻辑的开端，他将 2019年王璞巍等以承诺(Commitment)作为 义务、允许和禁止的规范概念与量化词一所有、 基本元素构建了面向合同的智能合约形式化语言， 某些、否，以及模态词一一必要、可能、不可能联 承诺表示为C(xy,P,r,tc,代表承诺人x向被承诺人 系起来，基于经典命题逻辑形成了标准道义逻辑 y做出承诺，如果前提p达成，就产生结果r,tc表 (SDL)的基础，可谓是形式化研究的开端.1988 示该承诺的有效期限，tc为true时承诺才会有效 年，Lee时对道义逻辑(Deontic logic)给出了更加详 上述工作表明合约逻辑模型日趋完善，并正朝着 细的描述和扩充，提出了一种强调合约时序性、道 与现实法律相融合的方向发展 义性和行为性的逻辑合约模型，成为最突出的合 5.2智能法律合约语言模型研究 同正式化范式之一 文献[44提出了一种被称为Simplicity的功能 在此基础上，2001年Grosof等B使用谦虚逻 性语言，该语言通过对抽象机器上操作语义的评 辑编程(Courteous logic program,CLP)给出了有关 估，计算空间和时间资源消耗的上限，在执行之前 知识表示的新的形式化表示，通过增加冲突的优 计算出比特币脚本和以太坊虚拟机中的资源消耗 先处理，扩展自说明性的普通逻辑，并开发了一个 费用，有利于解决智能合约的预付费问题 可以翻译任何CLP程序到语义相等的OLP程序 文献[45)提出了一种声明式智能合约语言 的编译器 (Findel)),着重从金融的角度描述了合约的资金转 Governatori等在连续多年的研究中对道义逻 移动作及乘法、逻辑、时序表达式.Findel通过两 辑表示合同的应用给出了更多的可行方案.作者 种资金转移动作与乘法、逻辑、时序3类表达式的 在论文[3刀中利用谦虚逻辑编程开发了使用 组合编写合约，使用该语言可以将某借款合约体 RuleML(Rule markup language)语言表达的商务合 现为一个表达式，记为ccb其合约最终体现为一 同的推理机，以机器可读语言来明确合同的所有 个表达式，如下所示：中若包含违反上述规定的行为，现实合约将自动 失效，与此对应的智能法律合约、代码、链码也将 自动视为无效合同，从而可以保证满足原则 3）的 要求. 针对原则 2），现实合约具有法律约束力，其中 规定了全部的合同条款和各方的权利和义务，而 代码和链码皆具有极强的专业性和领域性，在涉 及其意思解读时会带来第三方理解的误差或困 难，难以验证. 综上，在智能法律合约充当现实合约和智能 合约（代码）、链码之间桥梁的基础上，其意思表示 一致是智能合约具有法律效力的必要条件，因此 在合同订立过程中，必须保证它们间相互转化关 系是可经过检验求证的，且当事人签订时需知晓 且同意其互证关系. 5    智能法律合约研究进展 智能法律合约虽然是一个较新的词汇，但其 涉及到的法律合约逻辑、智能合约形式化表达等 基础探索和相关研究在很久前便已经开始了，现 行研究工作主要分为两个方向：合约的逻辑模型 研究与智能法律合约语言模型研究. 下面分别就 这两方面研究进展予以介绍与分析. 5.1    合约逻辑模型研究 在早期论文中，1952 年 ，von Wright 发表论文 Denotic logic[34] ，被视为现代道义逻辑的开端，他将 义务、允许和禁止的规范概念与量化词——所有、 某些、否，以及模态词——必要、可能、不可能联 系起来，基于经典命题逻辑形成了标准道义逻辑 （SDL）的基础，可谓是形式化研究的开端. 1988 年，Lee[35] 对道义逻辑（Deontic logic）给出了更加详 细的描述和扩充，提出了一种强调合约时序性、道 义性和行为性的逻辑合约模型，成为最突出的合 同正式化范式之一. 在此基础上，2001 年 Grosof 等[36] 使用谦虚逻 辑编程（Courteous logic program，CLP）给出了有关 知识表示的新的形式化表示，通过增加冲突的优 先处理，扩展自说明性的普通逻辑，并开发了一个 可以翻译任何 CLP 程序到语义相等的 OLP 程序 的编译器. Governatori 等在连续多年的研究中对道义逻 辑表示合同的应用给出了更多的可行方案. 作者 在 论 文 [37] 中利用谦虚逻辑编程开发了使 用 RuleML（Rule markup language）语言表达的商务合 同的推理机，以机器可读语言来明确合同的所有 条件，将其转换为可执行代码，并提供了一种将业 务规则表示为模块化独立单元的方法，兼有使用 优先级和覆盖谓词来解决冲突的能力. 在论文 [38] 进一步研究了使用道义逻辑来表达合约语义的需 要，并提出了使用可废止逻辑对模态逻辑算子和 道义逻辑算子的进一步扩展. 在论文 [39] 中提出 了一个用来表示和推理电子合约的架构 （ DR￾CONTRACT）. 在道义逻辑的基础上增加了可废止 逻 辑 ， 使 用 道 义 可 废 止 逻 辑 （ Deontic  defeasible logic）来处理合同违约情况. 2015 年，Idelberger 等[40] 提出基于逻辑的智能 合约语言以替代过程式语言（Procedural language）. 当合约中执行复杂逻辑时，用过程式语言描述合 约会使程序更加笨重且易错，同时因为逻辑约束 的动作执行顺序直接影响程序状态，导致合约不 易维护和监测. 而基于逻辑的语言可以避免这个 问题，其规则的顺序不影响程序执行，并且语句声 明将会更加简洁. 2016 年 Frantz 和 Nowostawski[41] 基于捕捉法 律基本特征的制度语法（ADICO） [42] 提出了将人机 可读的合同半自动翻译成智能合约的方法，支持 将 ADICO 组件映射为相应的 Solidity 结构，包括 生成合约地址、修饰器名称、函数框架，但是尚未 实现函数主体和 Solidity 表达式的转换. C(x,y,p,r,tc) 2019 年王璞巍等[43] 以承诺（Commitment）作为 基本元素构建了面向合同的智能合约形式化语言， 承诺表示为 ，代表承诺人 x 向被承诺人 y 做出承诺，如果前提 p 达成，就产生结果 r，tc 表 示该承诺的有效期限，tc 为 true 时承诺才会有效. 上述工作表明合约逻辑模型日趋完善，并正朝着 与现实法律相融合的方向发展. 5.2    智能法律合约语言模型研究 文献 [44] 提出了一种被称为 Simplicity 的功能 性语言，该语言通过对抽象机器上操作语义的评 估，计算空间和时间资源消耗的上限，在执行之前 计算出比特币脚本和以太坊虚拟机中的资源消耗 费用，有利于解决智能合约的预付费问题. 文献 [45] 提出了一种声明式智能合约语言 （Findel），着重从金融的角度描述了合约的资金转 移动作及乘法、逻辑、时序表达式. Findel 通过两 种资金转移动作与乘法、逻辑、时序 3 类表达式的 组合编写合约，使用该语言可以将某借款合约体 现为一个表达式，记为 czcb. 其合约最终体现为一 个表达式，如下所示： · 78 · 工程科学学报，第 44 卷，第 1 期