区块链智能合约形式化表达

前言 

本标准依据GB/T 1.1-2020给出的规则起草。

本标准由北京科技大学提出。

本标准由中国电子学会区块链分会技术归口。

本标准拟起草单位：北京科技大学，北京大学，北京市经济与信息化局，北京市社会公信建设促进会，天津蛟图信息科技有限责任公司，北京航天航空大学，北京文章无忧信息科技有限公司。

本标准拟主要起草人：朱岩、秦博涵、何啸、宋伟静、王迪、郭倩、王晟典、孙贻滋、刘国伟、冯荣权、张韬、徐双泉、韩心慧、英伟、胡凯。

引言 

本文件的发布机构提请注意，声明符合本文件时，可能涉及到第8章与智能法律合约语法相关的专利的使用。本文件的发布机构对于该专利的真实性、有效性和范围无任何立场。

该专利持有人已向本文件的发布机构承诺，他愿意同任何申请人在合理无歧视的条款和条件下，就专利授权许可进行谈判。该专利持有人的声明已在本文件的发布机构备案。相关信息可以通过以下联系方式获得：

专利：202010381549.5 一种法律合约的智能可执行合约构造与执行方法和系统

专利持有人姓名：北京科技大学

地址：北京市海淀区学院路30号

请注意除上述专利外，本文件的某些内容仍可能涉及专利。本文件的发布机构不承担识别专利的责任。

范围

本标准规定了智能合约有关的术语和定义，以及智能合约语言的结构、语法及示例（见附录A）。

本标准适用于通用智能合约设计、开发和使用，也可为区块链厂商和用户提供智能合约平台构建的技术标准参考。

规范性引用文件

下列文件对于本文件的应用是必不可少的。凡是注日期的引用文件，仅注日期的版本适用于本文件。凡是未注日期的引用文件，其最新版本（包括所有的修改单）适用于本文件。

GB/T 1.1-2020 标准化工作导则 第1部分：标准化文件的结构和起草规则

术语和定义

智能合约 Smart Contract

智能合约是一种旨在以数字方式传播、验证或执行多方之间约定的计算机程序和协议。

区块链智能合约 Blockchain Smart Contract

区块链智能合约是部署在区块链上并可在满足预定合约条款和履行条件时自动执行的计算机代码。

适用法律的智能合约 Smart Contract Applied to Legal

适用法律的智能合约是指一种含有合同构成要素、涵盖合同缔约方依据要约和承诺达成履行约定的计算机协议，本文中在不加区别时简称智能法律合约。

智能合约语言 Smart Contract Language

智能合约语言是一种为实现智能合约而创建的编程语言，包含规范智能合约撰写的语法规则。

适用法律的智能合约语言 Smart Contract Language Applied to Legal

适用法律的智能合约语言是指一种为实现适用法律的智能合约而创建的编程语言。

智能合约平台 Smart Contract Platform

智能合约平台是一种支持智能合约可执行程序开发、生成、部署、运行、验证的信息网络系统。

账户 Account

账户是指具有一定的格式和结构，用于描述当事人、操作和反映标的等智能法律合约要素的增减变化情况及结果的载体。账户类型包括用户账户和合约账户，其中，当事人拥有用户账户，智能法律合约拥有智能合约平台上的合约账户。

合同 Legal Agreement

合同是指民事主体之间设立、变更、终止民事法律关系的协议。

数据电文 Digital Message

数据电文是指以电子、光学、磁或者类似手段生成、发送、接收或者储存的信息。

合同条款 Contractual Terms

合同条款是合同条件的表现和固定化，是确定合同当事人权利和义务的根据。即从法律文书而言，合同的内容是指合同的各项条款。

术语间关联

适用法律的智能合约在形式上是一种介于现实法律合同与可执行区块链智能合约之间的过渡性法律文档。其中，现实法律合同以自然语言为载体，它可翻译成为由适用法律的智能合约语言撰写的智能法律合约，进而转化为由智能合约语言编写的区块链智能合约。

符号和缩略语

符号

下面符号适用于本文件：

      @@              中文意思表示

      ::=                 表示定义，即“被定义为”

      ?                   前置关键词任选

      |                    用于表示同级元素的“或”

      { } ( )             包含语句集合

      .                    语句结束符

      +                  零条或多条语句

      //                  注释符

   ‘ ’, “”     字符串类型

      0x                 十六进制数（用于区块链地址表示）

      ，空格          用于表示同级元素的并列与分割

缩略语

智能法律合约表示形式

智能法律合约采用书面形式订立合同，属于书面合同。当事人订立智能法律合约，采取要约、承诺方式。

智能法律合约遵循《民法典》《电子签名法》及有关法律法规相关条文，具有与现实法律合同相同的法律效力，对各文本使用的词句推定具有相同含义。各文本使用的词句不一致的，应当根据合同的相关条款、性质、目的以及诚信原则等予以解释。

智能法律合约可转化为数据电文表示的可执行程序，经智能法律合约签订过程（参见附录B）进而在智能合约平台加以自动化实施。

智能法律合约可以采用中文和英文联合编写形式，根据具体应用不同可选择使用。

智能法律合约构成要素

本标准可涵盖以下内容：当事人信息、标的、数量、质量、价款或者报酬、履行期限和方式、违约责任、解决争议的方法等。在智能法律合约语法中，本标准由包含在合约框架内的智能法律合约构成要素组成，包括：合约名称、当事人描述、标的、合约条款、合约订立、附加信息等，其中，合约条款包括：一般条款、违约条款、仲裁条款等。此外，智能法律合约编写过程中涉及权利和义务、资产操作、表达式、时间表示等语法规范。上述要素之间关系如下图所示。

智能法律合约语法

合约框架

智能法律合约包括：合约名称及合约内容，合约内容包括：当事人描述、资产描述、合约条款、附加信息、合约订立。

Contract ::= Title{ Parties+  Assets+ Terms+  Additional+  Signs+}

合约名称

合约名称包含：合约标题和合约序号。语法如下：

@@合约标题：合约序号

Title ::= contract Cname (: serial Chash)?

解读：合约序号是指本智能法律合约所求取的唯一性编号。

例：

@@买卖合同：0x827198…ab193

contract purchase: serial 0x827198…ab193

当事人描述

当事人描述包含当事人的名称或者姓名和住所，以及当事人所拥有的属性及特征描述（包含常量和变量），可通过身份认证技术保证当事人身份唯一性。语法如下：

@@当事人 群体？名称 {属性域+ }

Parties ::=  party group? Pname {field+ }

其中，属性域用于宣称当事人所拥有的属性及特征，由冒号分割的二元组表示，左部为属性名称，右部为属性值，表示如下：

@@ 属性：（常量|类型）

field ::= attribute : ( constant | type )

解读：属性值可为常量或类型声明，当属性值为类型声明时，属性值为空。

实体的属性值引用采取Entity:: attribute形式，其结果为该属性的值。

例1：

@@当事人信息：卖家，登记信息包括：当事人账号：0x7c84e8…2934；姓名：张三。

party Seller { account: 0x7c84e8…2934  name: ‘Zhang San’  }

解读：当事人账号指该当事人在区块链中所拥有的用户账户地址，可用于鉴别身份，通常由哈希值表示。

例2：

@@群组当事人信息：竞标人，登记信息包括：当事人账号。

party group Voters{ account: Integer }

解读：群组当事人可表示为动态加入的当事人列表。

标的

合约标的指当事人之间存在的权利义务关系，一般分为物、行为、智力成果等，是智能法律合约成立的必要条件。在智能法律合约中标的用资产来表示，在区块链中应存在该资产的描述，表示如下：

@@资产 资产名称 {资产描述{属性域+ } 资产权属{属性域+ }}

Assets ::= asset Aname{ info{ field+ }  right{ field+ }}

解读：资产的定义包含资产的名称，资产的属性及对资产的权利。

info用以唯一标识该资产和表述合约条款所涉及的属性，right用于明确资产的权属，通常包括：所有权（ownership）、使用权（useRight）、占有权（possessRight）、收益权（usufruct）、处分权（disposeRight），可作为类型使用，用户可根据实际需要自行添加权属。

例1：

@@合约标的：房屋，属性信息包括：产权编号：0x71a2f8…78d93；面积：50；用途：商业；价格：货币资产；权属信息包括：收益权、使用权

asset House{

info{ serial: 0x71a2f8…78d93  area : 50  usage : “business”  price : Money }

right{ houseBenefitRight: usufruct houseUse : useRight }

}

解读：usufruct与useRight类型用于记录权属信息；Money用于表示货币资产。

例2：

@@本金的120%

$ 120%* principal

解读：本金为Money类型的资产。

      资产表达式（也被称为资产表示）被用于在条款中使用该资产，定义如下：

      @@资产表达式：$（具体数量）？（具体权属）？资产名称

AssetExpression ::= $ (amount)? (right of)? Aname

解读：Aname为智能法律合约中声明的资产，权属（right）是指该资产中宣称的权属，如果不添加权属说明，则默认为所有权或权属定义中的第一个权属。

例3：

@@20元。

$ 20 RMB

解读：系统中预定义的货币资产包括：人民币（RMB）、美元（USD）等。

例4：

@@在智能法律合约中声明房屋资产。

$ House

例5：

@@在智能法律合约中声明资产House的50%所有权。

$ 50% ownership of House

合约条款

合约条款类型包括一般条款、违约条款、仲裁条款。

Terms ::= generalTerm | breachTerm | arbitrationTerm

一般条款

一般条款包含条款名、条款当事人、当事人必须、可以或禁止履行的行为、条款执行条件、条款执行过程中资产的转移、以及条款执行后应满足的结果。语法如下：

@@条款名：当事人 （必须|可以|禁止） 行为（属性域+）

（执行所需的前置条件）？

（伴随的资产操作+）？

（执行后需满足的后置条件）？

generalTerm ::= term Tname: Pname (must|can|cannot) action(field+)

(when preCondition)?

  (while transactions+)?

       (where postCondition)?.

      解读：条款声称某当事人在何种条件下必须、可以或禁止采取何种行为，同时伴随着何种资产操作，完成后应满足何种条件，具体包括：

1）  preCondition是由表示前置条件的表达式组成，在当事人执行动作之前进行检测，如果前置条件转化布尔表达式后值为真，则可以执行条款；如果值为假，不能执行条款。

2）  transactions是表示资产操作，描述条款执行过程中伴随的资产操作情况。

3）  postCondition是由表示后置条件的表达式组成，用于描述条款执行完成后应满足的条件，如果满足，则本条款执行成功。

行为是对其后属性列表的操作，它由智能合约平台的程序实现，后置条件用于检查该行为结果是否正确。

      例：

@@条款1：竞拍者（角色）可以（权利）在竞拍开始后（前置条件）出价竞拍（动作），向合约账户转入大于当前最高价的资金（资产操作），出价最高者为得主（后置条件）。

term no1: bidder can bid()

when after bidBegin

while deposit value > highestPrice

where winner = this bidder.

违约条款

违约条款是指双方约定的当事人不履行智能法律合约中规定的义务时或履行义务不符合约定时，应当承担的法律责任。即在指定条款的后置条件未得满足且此违约条件的前置条件得以满足时，当事人必须或可以执行违约处理，同时伴随某种资产转移，执行后应满足某种状态。

@@违约条款 条款名 （针对 条款名+）？：当事人 （必须|可以） 违约处理（属性域+）

（执行所需的前置条件）？

（伴随的资产操作+）？

（执行后需满足的后置条件）？

breachTerm ::= breach term Bname (against Tname+)? : Pname (must|can) action(field+)

(when preCondition)?

 (while transactions+)?

       (where postCondition)?.

      解读：违约条款通常可规定违约者必须执行的动作或受害者可以执行的动作。

例：

@@如果买家在预定了购买房屋之后，房屋主人（角色）把房屋租出去了（前置条件），那么房屋主人应该（权利）赔偿（动作）买家违约金（资金转移）。

breach term no6 against no4 : houseOwner must compensate()

                  when houseOwner did lend after buyer did order

               while transfer default to buyer.

仲裁条款

智能法律合约中以仲裁条款形式规定解决争议的方法，具体争议可由自然语言陈述，并可指定仲裁机构，语法如下：

@@（所声明之争议）？由某仲裁机构进行裁决。

arbitrationTerm ::= arbitration term : (The statement of any controversy)?

administered by institution : instName.

例：

@@凡因本智能法律合约引起的或与其有关的一切劳动争议，均由北京劳动仲裁委员会按照有效仲裁规则进行裁决。

arbitration term : Any labor controversy or claim arising out of or relating to this contract, or the breach thereof, shall be settled by arbitration administered by institution : Beijing Labor Arbitration Commission.

解读：仲裁机构可选择为区块链网络中具有司法管辖权的节点。

权利和义务

当事人在条款中有两种行为限制，分别是权利与义务。

权利

权利限制使用关键词can，用于当事人在满足前置条件的基础下可以选择执行某动作的条款，当事人也可以选择不执行。

例：

@@条款2：投票者（角色）可以（权利）在主席发表提案后（前置条件）开始投票（动作）。

term no2: voter can vote (target)

when after chairPerson did propose.

解读：投票属于权利，投票者可以行使自己的权利为提案投票，也可以不行使自己的权利，放弃投票。

义务

义务限制包括应当限制与禁止限制。

1）  应当限制使用关键词must，用于当事人在规定条件内必须执行某动作的条款。

例1：

@@条款3：借贷者（角色）需要（权利）在借贷后两年内（前置条件）归还（动作）借款。

term no3: borrower must return (loan)

when within 2 year after borrower did lend.

解读：归还属于义务，当事人需要在规定期限内履行自己的义务。

2）  禁止限制使用关键词cannot，用于当事人在一定情况下不应该执行某动作的条款。

例1：

@@条款4：房屋所有者（角色）在买家预定后（前置条件），不能（权利）再把房屋租出去（动作）。

term no4: houseOwner cannot rent()

when after buyer did order.

对于一条禁止条款可以有多种限制方式，可以按执行条件进行限制，也可以直接对执行结果进行限制，如对于“投票者不可以给自己投票”，如果直接投票给候选人，可以有如下两种表述方式：

例2：

@@条款5_1：如果选举人（角色）的投票对象是自己（执行条件），选举人不能（权利）执行投票（动作）。

term no5_1: voter cannot elect ( target)

when target = this voter.

例3：

@@条款5_2：如果选举人（角色）投票结果是使自己选票加一（执行结果），选举人不能（权利）投票（动作）。

term no5_2: voter cannot elect( target)

where this voter:: candidate = this voter :: origin candidate + 1.

解读：对条款5_1，如果投票者将选票给代理人，再由代理人投给投票者，这种行为将被许可；而用条款5_2直接对执行结果进行限制则可避免上述行为。

资产操作

资产操作是指智能法律合约执行过程中对资产的不同操作方式，通常用来实现标的物在不同账户之间的转移，资产操作分为三种：

1）存入deposit：当事人主动由其用户账户向合约账户存入资产，作为条款的执行条件使用，可以直接指定存入的资产或根据价值关系进行限制，后者在关系满足时才能转移指定的资产，语法如下：

@@存入（满足某种价值关系的）？ 资产描述

Deposit ::= deposit (value RelationOperator)? AssetExpression

例1：

@@存入大于当前最高价的金额

deposit value > highestPrice

解读：在竞拍条款中要求存入金额大于目前最高价才能执行竞拍操作，其中highestPrice表示当前最高价，为货币类型（Money）资产。

例2：

@@存入大于10元的金额

deposit value > $10 RMB

2）取回withdraw：当事人执行条款过程中从合约账户中取回一定资产，语法如下：

@@取回 指定资产。

Withdraw ::= withdraw AssetExpression

例3：

@@取回本金和利息（资产表达式中数额*（1+息率））

withdraw principal * (1+rate)

解读：在执行取款条款时，可以取回本金和利息。

3）转移transfer：当事人执行条款过程中从当前合约账户向其他当事人转移一定资产，语法如下：

@@转移指定资产到某当事人。

Transfer ::= transfer AssetExpression to target

例4：

@@向卖家转移保证金。

transfer welfare to seller

解读：welfare是买家事先存入的保证金，为Money类型，在买方确认收货时，会将事先存入合约账户的保证金转给卖家。

条款可以有多条资产操作语句：

例5：

@@条款6：借贷者（角色）可以（权利）抵押自己的房子（动作），将房屋的所有权存入合约账户，同时取出约定好的资金（资产操作）。

term no6: borrower can mortgage ()

while deposit $House and withdraw HousePrice.

表达式

智能法律合约中支持采用表达式规范条款条件以及用于构成智能法律合约中其他要素，条款条件（包括前置条件与后置条件）中的表达式结果应可直接转化为布尔值。表达式中的符号包括：

1）   逻辑符号，包括：and、or、not、implies；

2）   关系符号，包括：>、>=、<、<=、=、!=、belongsTo；

3）  算术符号，包括：+、−、∗、/；

4）   常量符号，包括：数字、字符串、true、false；

5）   时间符号，包括：month、day、year、hour、minute、second、now；

6）   类型符号，包括：String、Money、Date、Integer、Float、Boolean、Right、Time。

时间表示

时间表示由时间点表达式和时间段表达式构成。

时间点表达式

时间点表达式分为四种：时间变量、时间常量、全局查询、动作完成时间查询。

1） 时间变量是指日期（Date）类型的变量。

2） 时间常量是指固定时间的值，比如2019年11月18日。

3） 全局查询是指获取与智能法律合约运行相关的时间数值，如获取区块链智能合约生效时间（effective_date）、获取当前时间（now），它是由智能合约平台提供接口加以实现的。

4）  动作完成时间查询是指某个角色完成某项动作的时间，其表达式语法如下：

@@动作完成时间查询:（任意|存在|当前）？当事人做某动作的时间。

ActionEnforcedTimeQuery ::= (all|some|this)? party did action

解读：根据当事人为个体或群体情况，可将时间查询分为如下两种情况：

当事人为个体时，无须添加冠词all、some、this。

例：

@@买家支付完成的时刻。

buyer did pay

当事人为群体时，可通过添加冠词all、some、this查询特定时间。

1）   冠词all：表示群体当事人中最后一个完成某动作的时间，若存在任意个体未完成，则查询结果为未完成。

例1：

@@所有投票者投票完成的时刻。

all voter did vote

2）   冠词some：表示群体当事人最近一个完成某动作的时间，若所有个体都未完成，则查询结果为未完成。

例2：

@@竞标者群体中最近一个完成拍卖动作的时刻。

some bidder did bid

3）   冠词this：表示当前条款执行方若属于该群体，则查询结果为该个体的完成时间。

例3：

@@本人投票完成的时刻。

this voter did vote

时间段表达式

时间段分为时间变量和时间常量两类。

1)       时间变量是指时间（Time）类型的变量；

2)       时间常量是指固定长度的时间，如1天、2小时等。

时间段表达式定义如下：

@@（目标时间）？（是|否）在基础时间点（之前|之后）

TimePredicate ::= (targetTime)? (is | isn’t) (before | after) baseTime

解读：targetTime和baseTime都是时间点，如果没有目标时间，则默认与当前时间进行比较。

例1：

@@本人投过票之后且所有人投票完成之前

(after this voter did vote) and (before all voter did vote)

例2：

@@本人投票完成时刻是在有效期之后。

this voter did vote is after effective_date

     

边界时间段表达式定义如下：

@@边界时间点（之前|之后）一段时间（内）？

BoundedTimePredicate ::= (within)? boundary (before|after) baseTime

解读：boundary为时间段，baseTime为时间点

例3：

@@在拍卖结束前的三天内。

within 3 day before auctionEnd

例4：

@@在拍卖结束前的三天以前。

3 day before auctionEnd

合约订立

@@合约订立 : (所有当事人的约定)?

Signs ::= Contract conclusions : (The statement of all parties.)?

{  Signature of party Pname （当事人签字）:

{   printed-name（打印名）：String,

signature（法定代表人签字）: String,

date（签订日期）: Date

},+

}

例：

@@合约订立：本智能法律合约当事人不得以任何形式修改本合约，除非以书面形式并经双方签字。本合约及其附件构成合约双方的完整协议。本合约对当事各方及其继承人，受让人均具有约束力。通过签署本协议，各方同意上述条款。双方各收到一份本协议，并负责维护其条款。双方同意将本合约转化为智能合约平台的计算机程序，并同意该程序及其执行具有相同法律效力。

Contract conclusions: This contract may not be modified in any manner unless in writing and signed by both parties. This document and any attachments hereto constitute the entire agreement between the parties. This Contract shall be binding upon the parties, their successors and assigns. By signing this agreement, all parties agree to the terms as described above. Each of parties will receive one copy of this agreement, and will be responsible for upholding its terms. Both parties agree with conversion from this contract to computer programs on smart contract platform, and approve that the programs’ implementation has the same legal effect.

Signature of party auctioneer（拍卖人签字）：

{     printed-Name（打印名）：Yao San,

signature（法定代表人签字）：0x2319…8DE393,

date（签订日期）：2020/7/12

}

附加信息

附加信息给出智能法律合约所需的其它补充条件的定义，包括：合约属性、合约标的、当事人签名、保证人信息及签名、附加条款、程序变量、数据结构定义，可置于智能法律合约任何位置，语法如下：

@@属性域 +

Additional ::= field +

解读：附加信息引用采用 (Cname:: ) ? attribute的形式。

例：

@@最高拍卖金额和拍卖停止时间

highestPrice : Money,

biddingStopTime : Date

附录A（资料性） 智能法律合约示例及智能合约示例

A.1 智能法律合约示例——网络竞买合同

 1 @@网络竞买合同协议书
 2 contract SimpleAuction{
 3 @@甲方信息：拍卖人，登记信息包括：用户账户信息：0x712379218…C4E80。
 4 party auctioneer{
 5          account : 0x712379218…C4E80
 6 	}
 7 
 8 	@@乙方信息：竞买人，属于群体，登记信息包括：用户账户信息: [0x93A8BCD…793968, 0x48BD38… 92AC93]；账户曾出价累计值：货币资产。
 9 	party group bidders{
10 account : [0x93A8BCD…793968, 0x48BD38…92AC93]
11 		amount : Money
12 	}
13 	
14 @@当前最高价、最高出价的竞拍者、竞拍结束时间。
15 highestPrice : Money
16 highestBidder : bidders
17 biddingStopTime : Date
18     
19 @@标的物：竞拍货品，拍卖人需要提供拍卖物的物品名称、数量等相关信息。
20     asset good{
21 	info{
22 name : Name       //物品名称
23 quantity : Integer    //物品数量
24 price : Money      //价格
25 package : String    //运送包装 
26 }
27    }
28 	@@条款1：拍卖人（角色）可以（权利）发起竞拍（动作），在动作执行后，当前最高价应为拍卖人输入的底价，结束时间为当前时间加上输入的竞拍持续时间（后置条件）。
29 term no1 : auctioneer can StartBidding(reservePrice : Money, auctionDuration : Date)
30      when before auctioneer did StartBidding
31 		where highestPrice = reservePrice and biddingStopTime = auctionDuration + now.
32 
33 @@条款2：竞买人（角色）可以（权利）在拍卖人发起竞拍后至竞拍结束前（前置条件），进行出价（动作），如果出价大于目前所给最高价格（资产操作），则出价成功（后置条件）。
34 	term no2 : bidders can Bid
35 		when after auctioneer did StartBidding and before biddingStopTime
36 		while deposit value > highestPrice
37 where highestPrice = value and highestBidder = this bidder and this bidder::amount = this bidder:: origin amount + value.
38 
39 @@条款3_1：若竞买人（角色）不是最高出价者，且当前合约账户中存有其押金（前置条件），竞买人可以（行为分类）取回无效押金（动作），此后该竞买人押金清零（后置条件）。
40 	term no3_1 : bidders can WithdrawOverbidMoney
41 		when this bidder::amount > 0 and this bidder isn't highestBidder
42 		while withdraw this bidder::amount
43 		where this bidder::amount = 0.
44      
45 @@条款3_2：若竞买人(角色)是当前最高出价者，且当前合约账户中存有其之前的失败押金（前置条件），竞买人可以（行为分类）取回无效押金（动作），并登记成为当前竞拍最高价（后置条件）。
46 	term no3_2 : bidders can WithdrawOverbidMoney
47 		when this bidder::amount > highestPrice and this bidder is highestBidder
48 		while withdraw this bidder::amount - highestPrice
49 		where this bidder::amount = highestPrice.
50      
51 @@条款4：拍卖人（角色）可以（行为分类）在竞拍时间结束后（前置条件），收取拍卖成交款（动作）。
52 	term no4 : auctioneer can StopBidding
53 		when after biddingStopTime and before auctioneer did StopBidding
54 		while withdraw highestPrice.
55      
56 @@仲裁条款：凡因本智能法律合约引起的或与其有关的一切争议，均由北京互联网法院管辖。
57 Arbitration term : Any controversy or claim arising out of or relating to this contract, or the breach thereof, shall be settled by arbitration administered by institution : BeijingIneternetCourt.
58 
59 @@合约订立：本智能法律合约当事人不得以任何形式修改本合约，除非以书面形式并经双方签字。本合约及其附件构成合约双方的完整协议。通过签署本协议，各方同意上述条款。双方各收到一份本协议，并负责维护其条款。双方同意将本合约转化为智能合约平台的计算机程序，并同意该程序及其执行具有相同法律效力。
60 Contract conclusions: This contract may not be modified in any manner unless in writing and signed by both parties. This document and any attachments hereto constitute the entire agreement between the parties. This Contract shall be binding upon the parties, their successors and assigns. By signing this agreement, all parties agree to the terms as described above. Each of parties will receive one copy of this agreement, and will be responsible for upholding its terms. Both parties agree with conversion from this contract to computer programs on smart contract platform, and approve that the programs’ implementation has the same legal effect.
61 
62 Signature of party auctioneer（拍卖人签字）: 
63 {	printed-Name（打印名）：Yao San,
64 signature（法定代表人签字）: 0x23198de…393,
65 date（签订日期）: 2020/7/12
66 }
67 Signature of party bidders（竞拍人签字）: 
68 {	printed-Name（打印名）：柳湾,
69 signature（法定代表人签字）: 0x877238…201,
70 date（签订日期）: 2020/7/12
71 }
72 {	printed-Name（打印名）：秦源,
73 signature（法定代表人签字）: 0x9340593…495,
74 date（签订日期）: 2020/7/12
75 }
76 }

A.2 智能法律合约示例——房屋租赁合同

 1 @@房屋租赁合同协议书
 2 contract HouseLease{
 3 @@甲方信息：出租人，登记信息包括：用户账户信息：0x82384a68…90e72。
 4 party Renter{
 5      account : 0x82384a68…90e72
 6 	}
 7 
 8 	@@乙方信息：承租人，登记信息包括：用户账户信息：0x9845a6b…73c4e。
 9 party Tenant{
10      account : 0x9845a6b…73c4e
11 	}
12 	
13 @@合约属性：出租人押金、承租人押金、房屋租金、总租金、合约起始时间、合约终止时间、支付租金的时间、租金支付周期。
14 type contractInfo {
15 	renterBail:Money
16 	renantBail:Money
17 	rental:Money
18 	totalRental:Money
19 	startLeasingTime:Date
20 	endLeasingTime:Date
21 	payDate:Date
22 	payDuration:Date
23 	}
24 
25 @@标的物：房屋，出租人应提供产权号、地址、面积、用途、价格等信息。
26 asset House{
27 	info{ /*房屋的具体信息*/
28 		ownershipNumber: Integer
29 		location: Address
30 		area: Integer
31 		usage: String
32 		price: Money
33 	}
34 	right{ /*所有者可对该资产行使的4种权利*/
35 		houseUseright : useRight
36 		houseUsufruct : usufruct
37 		dispositionRight: Right
38 		ossessionRight: Right
39 	}
40 	}
41 	@@条款1：出租人（角色）可以（行为分类）通过交纳出租人押金（资产转移）来注册房屋信息（动作）。
42 	term term1: Renter can registerHouse
43 		while deposit infos::renterBail.
44 
45 	@@条款2：承租人（角色）可以（行为分类）在出租人注册房屋之后（前置条件），通过交纳承租人押金（资产转移）来确认租赁（动作），动作执行之后要求自动记录当前时间为合约的开始时间、且计算截止时间并设置合约执行有效期和承租人支付租金的时间（后置条件）。
46 	term term2: Tenant can confirmLease
47 when after Renter did registerHouse
48 while deposit infos::tenantBail
49 where infos::startLeasingTime = now and infos::endLeasingTime = endLeasingDuration+now
50       and infos::payDate = payDuration+now and infos::payDuration = payDuration.
51 
52 	@@条款3：承租人确认承租7天内（前置条件），出租人（角色）必须（行为分类）将房屋使用权转移给承租人（动作）。
53 	term term3: Renter must transferHouse
54 when within 7 day after Tenant did confirmLease
55 while deposit $ house:: houseUseright.     
56 @@条款4：在承租人确认承租后，在规定的支付租金日期之前（前置条件），承租人（角色）必须（行为分类）支付租金（动作）。
57 	term term4: Tenant must payRent
58 when before infos :: payDate and after Renter did transferHouse
59 while deposit infos ::rental.
60 @@条款5：租赁合约到期后且承租人检查房租之前（前置条件），承租人应当归还房屋（动作），即将房屋使用权转回出租人（后置条件）。
61 	term term5: Tenant must returnHouse
62 when after infos :: endLeasingTime and before Renter did checkHouse
63 while transfer $ house:: houseUseright to Renter.   
64 @@条款6：出租人（角色）在承租人确认归还房屋后（前置条件）可以（行为分类）对房屋进行检查（动作）。
65 	term term6: Renter can checkHouse
66 when after Tenant did returnHouse.
67 @@条款7：出租人（角色）在检查房屋之后的15天内（前置条件），可以（行为分类）收取全部租金（动作），即取出租金（资产转移）。
68 	term term7: Renter can collectRent
69 when within 15 day after Renter did checkHouse
70 while withdraw infos::rental.
71 @@条款8_1：在检查房屋之后的15天内（前置条件），出租人（角色）可以（行为分类）取出出租人押金（动作）。
72 	term term8: Renter can collectBail
73 when within 15 day after Renter did checkHouse
74 while withdraw infos :: renterBail.
75 
76 @@条款8_2：在检查房屋之后的15天内（前置条件），承租人（角色）可以（行为分类）取出承租人押金（动作）。
77 	term term9: Tenant can collectBail
78 when 15 day after Renter did checkHouse
79 while withdraw infos :: tenantBail.
80 
81 @@仲裁条款：凡因本智能法律合约引起的或与其有关的一切争议，均由北京互联网法院管辖。
82 Arbitration term : Any controversy or claim arising out of or relating to this contract, or the breach thereof, shall be settled by arbitration administered by institution : BeijingIneternetCourt.
83 
84 @@合约订立：本智能法律合约当事人不得以任何形式修改本合约，除非以书面形式并经双方签字。本合约及其附件构成合约双方的完整协议。通过签署本协议，各方同意上述条款。双方各收到一份本协议，并负责维护其条款。双方同意将本合约转化为智能合约平台的计算机程序，并同意该程序及其实施具有相同法律效力。
85 Contract conclusions: This contract may not be modified in any manner unless in writing and signed by both parties. This document and any attachments hereto constitute the entire agreement between the parties. This Contract shall be binding upon the parties, their successors and assigns. By signing this agreement, all parties agree to the terms as described above. Each of parties will receive one copy of this agreement, and will be responsible for upholding its terms. Both parties agree with conversion from this contract to computer programs on smart contract platform, and approve that the programs’ implementation has the same legal effect.
86 
87 Signature of party Renter（出租人签字）: 
88 {   printed-Name（打印名）：Mike Micheal,
89 signature（法定代表人签字）: 0x9045f7a…80d4,
90 date（签订日期）: 2020/8/20
91 }
92 
93 Signature of party Tenant（承租人人签字）: 
94 {   printed-Name（打印名）：姜爽,
95 signature（法定代表人签字）: 0x46b9d3e…a983,
96 date（签订日期）: 2020/8/20
97 }
98 }

A.3 智能合约（Solidity）代码示例

 1 pragma solidity >=0.5.0 <0.6.0;
 2 
 3 import "./bidders.sol";
 4 import "./auctioneer.sol";
 5 
 6 contract SimpleAuction {
 7 
 8     biddersT bidders;
 9     auctioneerT auctioneer;
10 
11     uint highestPrice;
12     address highestBidder;
13 uint biddingStopTime;
14 
15 
16     constructor() public{
17         bidders = new biddersT();
18         auctioneer = new auctioneerT();
19         auctioneer.regist(msg.sender);
20 auctioneer.name = "Yao San";
21 auctioneer.signature = "0x23198de…393";
22 auctioneer.signDate = 2020/7/12;
23 bidders.add("柳湾","0x877238…201",2020/7/12);
24 bidders.add("秦源", "0x9340593…495", 2020/7/12);
25     }
26 
27     modifier onlybidders{
28         require(bidders.contains(msg.sender));
29         _;
30     }
31 
32     modifier onlyauctioneer{
33         require(auctioneer.getAddress() == msg.sender);
34         _;
35     }
36 
37     function StartBidding(uint reservePrice, uint auctionDuration) onlyauctioneer() public {
38         //RECORD
39         auctioneer.StartBiddingDone();
40         //USER CODE HERE
41         highestPrice = reservePrice;
42         biddingStopTime = auctionDuration + now;
43         //CHECK
44         assert(highestPrice == reservePrice && biddingStopTime == auctionDuration + now);
45     }
46 
47     function Bid() public payable {
48         if(!bidders.contains(msg.sender))
49             bidders.add(msg.sender);
50         //REQUIRE
51         require(now > auctioneer.StartBiddingTime() && now < biddingStopTime);
52         require(msg.value > highestPrice);
53         uint this_bidder_Ori_amount = bidders.getamount(msg.sender);
54         //USER CODE HERE
55         highestPrice = msg.value;
56         highestBidder = msg.sender;
57         bidders.setamount(msg.sender,bidders.getamount(msg.sender) + msg.value);
58         //CHECK
59         assert(highestPrice == msg.value && highestBidder == msg.sender &&
60         bidders.getamount(msg.sender) == this_bidder_Ori_amount + msg.value);
61     }
62 
63     function WithdrawOverbidMoney() onlybidders() public payable {
64         //REQUIRE
65         if(msg.sender != highestBidder && bidders.getamount(msg.sender) > 0){
66             //USER CODE HERE
67             msg.sender.transfer(bidders.getamount(msg.sender));
68             bidders.setamount(msg.sender, 0);
69             //CHECK
70             assert(bidders.getamount(msg.sender) == 0);
71         }
72         //REQUIRE
73         else if(msg.sender == highestBidder && bidders.getamount(msg.sender) > highestPrice) {
74             //USER CODE HERE
75             msg.sender.transfer(bidders.getamount(msg.sender) -  highestPrice);
76             bidders.setamount(msg.sender, highestPrice);
77             //CHECK
78             assert(bidders.getamount(msg.sender) == highestPrice);
79         }
80         else{
81             revert();
82         }
83     }
84 
85     function CollectPayment() onlyauctioneer() public payable {
86         //REQUIRE
87         require(now > biddingStopTime && now < auctioneer.CollectPaymentTime());
88         //RECORD
89         auctioneer.CollectPaymentDone();
90         //USER CODE HERE
91         msg.sender.transfer(highestPrice);
92     }
93 }

附录B（资料性） 智能法律合约签订过程

智能法律合约签订过程是指智能法律合约由生成、部署、签名到履行的处理流程。在智能法律合约经当事人协商撰写完成后，通过翻译器转化为计算机程序语言编写的可执行程序，然后被部署到智能合约平台中并由当事人签名确认，进而进入合同履行阶段。同时，部署后进入履行阶段的区块链智能合约可随时被查阅与审查。

智能法律合约存储结构是指其在生命周期中的各种形态及支持合约签订、部署、运行、监管等阶段的数据存储结构。该存储结构除包含智能法律合约与其演化形态以及用户定义信息外，还包含智能法律合约自身的基本属性与状态信息，如合约地址Address、签名信息Sign、时间戳Time等。

1）  在使用本标准语言编写智能法律合约A时，A中的所有缺省属性值为空；

2）  在由智能法律合约A生成可执行区块链智能合约B时，如果有人工参与，参与人通过签名函数进行签名；

3）  在部署区块链智能合约B时，生成合约地址Address，作为B的唯一编号；部署成功后，合约当事人加入时间戳记录签名时间，并通过签名函数对A和B进行签名；

4）  当事人完成签名后，任何时间可通过调取查用将合约属性填充回智能合约A，生成可浏览的合约形式。

参考文献

[1]      Xiao He, Bohan Qin, Yan Zhu, et al. SPESC: A Specification Language for Smart Contracts[C]. In proceedings of IEEE 42nd Annual Computer Software and Applications Conference (COMPSAC), 2018: 132-137.

[2]      朱岩, 王迪, 秦博涵, 宋伟静. 一种法律合约的智能可执行合约构造与执行方法和系统：202010381549.5 [P]. 2020-05-08.

[3]      朱岩, 秦博涵, 陈娥, 刘国伟. 基于高级智能合约语言的竞买合约设计与实现[J]. 计算机学报, 2020.（网络发表）

[4]      Yan Zhu, Weijing Song, Di Wang, Di Ma, Chu William. TA-SPESC: Towards Asset-driven Smart Contract Language supporting Ownership Transaction and Rule-based Generation on Blockchain[J]. IEEE Transactions on Reliability, 2020.（小修）