SPESC:面向法律的智能合約設(shè)計與實踐

王迪 秦博涵 宋偉靜 朱巖

摘 ? 要：智能合約是近年來隨著區(qū)塊鏈技術(shù)興起而發(fā)展起來的一種程序設(shè)計、部署及運行的新構(gòu)架，但目前仍缺少較為完備的面向法律智能合約語言。據(jù)此，文章對一種面向法律的智能合約描述語言—SPESC的規(guī)范化方法進行了詳細(xì)介紹，它以類似于現(xiàn)實合同的結(jié)構(gòu)、類似自然語言的語法設(shè)計實現(xiàn)智能合約的編撰，明確定義了當(dāng)事人的義務(wù)和權(quán)利，制定了時間表達式規(guī)范及加密貨幣的交易規(guī)則，達到了提高合約法律性、便于法律人士與計算機人員協(xié)作合約開發(fā)、易于理解和使用的目的。

關(guān)鍵詞：智能法律合約;SPESC;規(guī)范;區(qū)塊鏈

中圖分類號： TP312 ? ? ? ? ?文獻標(biāo)識碼：A

Abstract： Smart contract is presented as a new infrastructure for programming， deployment and execution with the rapid pace of blockchain technology in recent years. However， there is still a lack of more comprehensive languages for law-oriented smart contract. This paper introduces a formalized method to specify law-oriented smart contract description languages， called SPESC. This method supports the composition of smart contracts with structure similar to real-world contract and grammar similar to natural language. Moreover， the proposed SPESC clearly defines the obligations and rights of the contracting parties， the time expression specifications and the transaction rules for cryptocurrencies. Based on them， our work improves the legality of the SPESC contract， facilitates the cooperation development between legal specialists and computer experts， and makes the contract easy to understand and use.

Key words： smart legal contracts; SPESC; specification; blockchain

1 引言

智能合約是近年來隨著區(qū)塊鏈技術(shù)[1]興起而發(fā)展起來的一種程序設(shè)計、部署及運行的新構(gòu)架，由于具有按照參與方約定自動執(zhí)行的能力，也被認(rèn)為是第二代區(qū)塊鏈的核心技術(shù)。更為重要的是，智能合約技術(shù)[2]通過支持更加強大的編程語言和運行環(huán)境，允許開發(fā)者在其上面開發(fā)任意價值交換相關(guān)的應(yīng)用，成功地解決了區(qū)塊鏈應(yīng)用開發(fā)困難的問題，代表著未來區(qū)塊鏈技術(shù)發(fā)展的方向。

目前幾乎所有的區(qū)塊鏈技術(shù)公司都已在其產(chǎn)品中支持智能合約產(chǎn)品。例如，以太坊基于虛擬機的智能合約平臺、基于Bitcoin區(qū)塊鏈的RSK平臺、IBM公司提出的企業(yè)級HyperLeger Fabric平臺等，這些產(chǎn)品的推出極大的豐富了智能合約技術(shù)的內(nèi)涵和范圍，為區(qū)塊鏈技術(shù)在不同領(lǐng)域的現(xiàn)實應(yīng)用奠定了基礎(chǔ)，也代表了區(qū)塊鏈未來發(fā)展的方向[3]。

在智能合約語言方面，大多數(shù)智能合約語言皆從計算機編程人員的角度出發(fā)進行定義[4]，其合約的創(chuàng)建與維護需要依賴于計算機專業(yè)領(lǐng)域人士方能完成，對于跨學(xué)科領(lǐng)域的用戶缺乏易讀性、友好性[5]，也同時限制了智能合約在多領(lǐng)域協(xié)作中的應(yīng)用。近年來高級智能合約語言（ASCL）已被一些學(xué)者提出來解決上述問題，如文獻[6，7]重點在于驗證智能合約的代碼驗證和語義確認(rèn)，文獻[8～10]從法律角度討論智能合約，文獻[10]從自然語言的角度分析了智能合約。

針對目前缺少較為完備的面向法律智能合約語言的現(xiàn)狀，本文改進了智能合約描述語言（SPESC）[11]使其成為一種更加接近于法律合同的高級智能合約語言，給出了從傳統(tǒng)靜態(tài)文本合同到動態(tài)可自動執(zhí)行的計算機程序的語法規(guī)范。它包含以提高合約法律性、便于法律人士與計算機人員協(xié)作合約開發(fā)、易于理解和使用為目的智能合約規(guī)范。SPESC語言采用了與現(xiàn)實合同類似的結(jié)構(gòu)來規(guī)范智能合約，并使用了類似自然語言的語法，明確定義了當(dāng)事人的義務(wù)和權(quán)利、加密貨幣的交易規(guī)則，對于促進智能合約法律化和協(xié)作開發(fā)智能合約具有很大的潛力。

2 SPESC語言整體結(jié)構(gòu)

SPESC語言是介于現(xiàn)實法律合約與現(xiàn)有智能合約通用語言之間的一種過渡性語言，因此，在SPESC語言中智能合約被視為計算機技術(shù)、法律與金融的結(jié)合性文檔。在語法結(jié)構(gòu)上，SPESC語言既有法律合約的結(jié)構(gòu)和語法，同時又具有一定的計算機形式化語言的特征，從而避免自然語言所有的二義性和不確定性。

SPESC語言結(jié)構(gòu)和實例如圖1所示，合約分為合約框架、合約參與方、合約條款和附加信息四部分。SPESC合約采用英文進行寫作，合約框架用于規(guī)范合約名稱、合約簽名、簽約時間等信息;合約參與方則對所有合約參與方進行說明（以關(guān)鍵字party表示）;合約條款則按照現(xiàn)實合約形式表達各參與方的行為、權(quán)力和義務(wù)（以關(guān)鍵字term表示）;附加信息則對合約涉及的其它信息進行定義（以關(guān)鍵字type表示）和說明。

在圖1中商品買賣合約例子中，所定義條款對下面行為進行了規(guī)范：

（1）先由賣家創(chuàng)建合約，在買家下訂單后通過調(diào)用post（）動作進行郵寄;

（2）買家通過調(diào)用pay（）動作將資金轉(zhuǎn)到合約中作為貨款;

（3）當(dāng)買家調(diào)用receive（）動作表示已收到貨物，賣家才可調(diào)用collect獲取前述資金。

從圖1中不難看出，SPESC語言具有結(jié)構(gòu)簡單、表述上易于理解、代碼量低等特點。而且，與傳統(tǒng)通用編程語言相比，該語言具有全新定義的時序邏輯以及情態(tài)動詞，用于更準(zhǔn)確地表述合約參與方的行為。此外，SPESC語言還包含合約中需要記錄的重要屬性，如被出售貨物的數(shù)量和價格等。

在SPESC語言執(zhí)行上，由SPESC語言編寫的智能合約并不限定具體的智能合約編程語言和實現(xiàn)環(huán)境，可支持將其轉(zhuǎn)化為任何現(xiàn)有區(qū)塊鏈智能合約語言程序代碼和平臺上運行。需要說明的是，SPESC語言編寫的合約并不與最終的可執(zhí)行合約程序完全等價，SPESC語言是智能合約的高層且抽象表示，它重點對合同中的當(dāng)事人、貨幣支付流程、時間序列等進行轉(zhuǎn)換，其余補充信息亦可由計算機人員進行后期編程補充。

因此，高級智能合約語言作為一種面向法律規(guī)范的智能合約高層語言，它的語言結(jié)構(gòu)和計算機本身的硬件以及指令系統(tǒng)無關(guān)，它的可閱讀性更強，能夠方便地表達合約功能和權(quán)利與義務(wù)表述。同時，所編寫的智能合約也更容易被理解，也更方便被初學(xué)者所掌握和學(xué)習(xí)。

3 SPESC合約參與方規(guī)范

在SPESC語言中合約參與方被定義在合約框架的前部，這與現(xiàn)實合約相似。合約參與方將逐一被定義，每一名參與方由party結(jié)構(gòu)進行定義，它由一個作為標(biāo)識的名稱、一些當(dāng)事人屬性和動作構(gòu)成，其中，這些屬性和行為是必須記錄在區(qū)塊鏈上的信息和一組動作組成。

SPESC中的參與方有四個特點：

（1）一個合約中可以有多個參與方;

（2）一個用戶個體可以屬于多種參與方;

（3）一個參與方可以包含多個用戶個體（被稱為群組）;

（4）參與方代表的用戶是可以變動的。

合約參與人中定義的每項動作都代表該合約當(dāng)事人可以或必須履行的某項行為。每個動作通過后面的括號進行聲明，例如圖1中的post（）表示銷售方發(fā)貨行為，pay（）表示購買方的付款行為等，這些行為在現(xiàn)實合約中可存在多種實現(xiàn)方法，并已能被合約參與方接受的情況下無需在合約中予以進一步說明。圖2展示了三個比較簡單的合約參與人的例子：賣家（Seller）、買家（Buyer）和投票者（Voters）。賣家可以行使放棄abort和收集資金collect兩個行為;買家具有付款pay和接收receive兩個行為;在選舉合約中，投票者的定義使用了關(guān)鍵詞group表示該參與方對應(yīng)不止一個個體（由多個個體構(gòu)成的成員列表表示），且每個投票者包含一個字符串類型的名字屬性，還有一個屬于投票者的動作—投票。上述定義的參與方及其屬性和行為將可在后續(xù)合約條款中被使用。

4 SPESC合約條款規(guī)范

作為一種法律文書，SPESC語言的主體和內(nèi)容是通過合約的各項條款（Contract Terms）體現(xiàn)的，在法律上合約條款是當(dāng)事人合意的產(chǎn)物、合同內(nèi)容的表現(xiàn)形式，是確定合同當(dāng)事人權(quán)利義務(wù)的根據(jù)。合約條款也是合同條件的表現(xiàn)和固定化，是確定合同當(dāng)事人權(quán)利和義務(wù)的根據(jù)。因此，合約條款定義在SPESC語言中具有核心性地位。

在SPESC規(guī)范中，合約條款是由關(guān)鍵字term、條款名稱，以及其后跟隨的一組語句構(gòu)成，用以表達某個或幾個合約參與方在什么條件下需要或可能履行的行為。從SPESC語法上講，在參與方聲明一個動作之后，該動作何時（必須或可以）履行則需要通過使用合同條款來進行規(guī)范。

一條SPESC合約條款涉及一個參與方和該參與方的動作，并包含該動作執(zhí)行的前置、后置條件和資產(chǎn)轉(zhuǎn)移。具體而言，一條條款包含的元素為：

（1）角色：條款內(nèi)容描述的參與方;

（2）分類：這條條款是屬于權(quán)利還是義務(wù);

（3）動作：條款中的動作;

（4）前置條件：描述角色在什么條件下可以執(zhí)行條款;

（5）資產(chǎn)轉(zhuǎn)移：動作的執(zhí)行時伴隨的資產(chǎn)轉(zhuǎn)移情況;

（6）后置條件：執(zhí)行結(jié)果需要滿足的要求。

盡管對計算機人員而言，合約條款的定義通?？梢灶惐葹橛嬎銠C語言中過程或函數(shù)的定義，但SPESC中條款定義更加抽象化和明確化，只用于規(guī)范資產(chǎn)的轉(zhuǎn)移條件和過程;另一方面，對法律人員而言，SPESC中條款的定義采用計算機中形式化模型加以描述，更加規(guī)范化和標(biāo)準(zhǔn)化。

為了增加可讀性，SPESC采用類似自然語言的語法來定義合同條款。條款的具體語法在EBNF中定義為：

term name ： party （must|may） action

（when preCondition）？

（while transactions+）？

（where postCondition）？ .

其中，在SPESC的初始模型中定義的概念以斜體顯示，關(guān)鍵字以粗體顯示。

按照動作的履行方式，SPESC條款分為權(quán)利條款和義務(wù)條款兩類。

（1）義務(wù)條款：規(guī)定參與方在一定先決條件下必須執(zhí)行該動作，通過條款中動作前的關(guān)鍵字must加以定義。

（2）權(quán)利條款：定義了參與方在一定先決條件下可以執(zhí)行該動作，通過條款中動作前關(guān)鍵字may加以定義。

需要說明的是，當(dāng)執(zhí)行時條件不成立，兩類條款中參與方都不能實施該行動。

條款中行為所需要滿足的條件可由前置、后置和伴隨條件來表達，具體為：

（1）PreCondition表示執(zhí)行條款的前置條件;

（2）TransferOperation表示執(zhí)行該條款的過程中伴隨的資產(chǎn)轉(zhuǎn)移;

（3）PostCondition表示該條款執(zhí)行結(jié)束后該滿足的后置條件。

圖3給出了三條SPESC條款的示例，具體內(nèi)容為：

（1）第一個條款（no1）是買賣中的例子，意思是賣家可以在買家確認(rèn)購買前終止合約，并取回自己購買商品兩倍價格的保證金。

（2）第二個條款（no2）是投票中的例子，意思是投票者在投票開始后，如果他還沒進行過投票，那么他可以委托別人代他投票，并且將他標(biāo)記為已投票狀態(tài)。

（3）第三個條款（no3）是拍賣中的例子，意思是競拍者在主持人開啟競拍且在競拍結(jié)束前可以競拍，同時要向合約賬戶轉(zhuǎn)入比目前最高價高的價格，然后把當(dāng)前最高價返還給當(dāng)前最高者，最后記錄這個競拍者及新的最高價。

由此可見，SPESC條款具有較強而簡潔的當(dāng)事人行為表達能力。

5 SPESC中時間表達式規(guī)范

SPESC中表達式是指由數(shù)字、算符、符號、變量等已有意義排列方法所得的組合，它是構(gòu)成語句的基礎(chǔ)。SPESC語言表達式大致分為五類：邏輯表達式、關(guān)系表達式、運算表達式、常數(shù)表達式、時間表達式。前四類與其它程序語言大致相同，但具有特有的時間表達式來描述合約中行為/動作之間的相互時序關(guān)系，下面將重點對時間表達式規(guī)范加以介紹。

在現(xiàn)實合約中，條款中的權(quán)利與義務(wù)往往是通過時間限制的，比如，買家必須在簽訂合約后的三天內(nèi)付款。所以時間表達對于合約條款條件的限定是非常重要的，因此，SPESC中建立了一系列時間表達式來更方便以及更準(zhǔn)確地表達時序關(guān)系。更嚴(yán)格地說，在SPESC語言中時間表達式是為了支持前置條件、后置條件和資產(chǎn)轉(zhuǎn)移的表達，并包含時間常量、動作完成時間、當(dāng)時時間等形式。

首先，SPESC智能合約語言在定義時間點（timepoint）的表示基礎(chǔ)上將時間表達式分為四種，分別為時間變量、時間常量、全局查詢、動作完成時間查詢四類：

（1）時間變量指類型為時間（date/time）的變量。

（2）時間常量指一些固定的時間的值，比如3小時20分鐘。

（3）全局查詢指對系統(tǒng)和合約中某一時間相關(guān)信息的獲取，比如，獲取合約創(chuàng)建時間（start）、獲取當(dāng)前時間（now）（有時限于區(qū)塊鏈而只能獲取當(dāng)前區(qū)塊的時間）。

（4）動作完成時間查詢表示某個角色完成某項動作的時間。

對動作完成時間查詢而言，由于被查詢方（被稱為角色）可能表示一個或多個當(dāng)事人，情況相對復(fù)雜，因此定義其表達式格式為：

（all | first | this）？ party did action

它的返回值為一個時間點。

具體而言，動作完成時間查詢根據(jù)當(dāng)事人的角色不同，可分為兩種情況。

首先，如果角色屬于單個個體，即只有一個當(dāng)事人，那么假如這個當(dāng)事人沒有完成這項動作，表達式將返回一個無限大的值;當(dāng)這個當(dāng)事人完成了這個動作，表達式返回這個角色完成這項動作的時間。

其次，如果角色是一組人的話，那么需要在動作時間查詢表達式中使用全稱或特稱量詞，這種量詞分為all、first、this三種：

（1）量詞all表示所有用戶個體都完成該動作的時間，如all Voters did Vote。

（2）量詞first表示第一個用戶個體完成該動作時間，如first bidders did Bid。

（3）量詞this表示當(dāng)前用戶完成時間，如this bidders did Bid。

除了時間表達式之外，SPESC中定義了兩個基本的時間謂詞：before和after來限制當(dāng)事人行為完成的時間范圍并定義事件觸發(fā)的時間條件，其中，謂詞返回值是布爾值—真或假。上述兩個時間量詞定義為：

（before | after） timepoint

其中，timepoint表示前面定義的時間點，before和after分別表示在這個時間點之前和時間點之后，例如before BiddingStopTime、after all Voters did Vote。

時間謂詞表達式可轉(zhuǎn)化為關(guān)系表達式，before timepoint等價于now < timepoint，after timepoint等價于now > timepoint，其中，now為當(dāng)前時間。

謂詞表達式和其它表達式相結(jié)合可以組成時間范圍，例如，在買家付款后的三天內(nèi)可以表示為：

（after buyer did pay） and

（before buyer did pay + 3 day）

其中，時間點可進行簡單的代數(shù)運算。但這種表達比較冗雜，既不方便書寫也不方便閱讀。SPESC拓展了時間范圍謂詞的表達方式，定義為：

（within）？ boundary （before | after） base

其中，boundary表示其邊界范圍，例如，within 3 day after buyer did pay。

此外，SPESC語言所支持其它表達式形式簡單定義為：

（1）邏輯表達式，包含and（與）、or（或）、not（非）以及implies（蘊含）。

（2）關(guān)系表達式，包含>、>=、<、<=、=、！=和belong to（屬于）。

（3）運算表達式，包含+、-、*、/、**（乘方）。

（4）常量表達式，包含整型常量、浮點常量、布爾常量等。

總之，通過上述SPESC語言的表達式規(guī)范，可以對合約中各方行為加以限定，達到易于表達和理解的目的。

6 SPESC中的貨幣支付功能

為了支持智能合約中交易的支付款功能，SPESC提供了一種簡單的貨幣支付功能，能夠與現(xiàn)有區(qū)塊鏈系統(tǒng)中的數(shù)字貨幣相銜接，實現(xiàn)簡單而高效的支付款功能。限于智能合約的區(qū)塊鏈功能，在SPESC中所有轉(zhuǎn)賬交易都是通過交易進行的，不存在用戶與用戶之間直接的轉(zhuǎn)賬操作。

SPESC智能合約語言中的交易分為三種操作：

（1）deposit：調(diào)用者向合約賬戶存入一定量資產(chǎn)。

（2）withdraw：按照合約中的規(guī)則，合約賬戶向調(diào)用者轉(zhuǎn)一定資產(chǎn)。

（3）transfer：按照合約中的規(guī)則，合約賬戶向某賬戶轉(zhuǎn)一定資產(chǎn)。

與后兩者不同，deposit是用戶主動的行為，是在調(diào)用時發(fā)生的;而后兩者是按照合約規(guī)定強制執(zhí)行的行為，是在執(zhí)行時發(fā)生的。因此，后兩者只是按照合約描述執(zhí)行，而deposit應(yīng)作為調(diào)用動作時的限制條件表達。

具體而言，三種資產(chǎn)轉(zhuǎn)移行為的語法：

deposit （= | > | >= | < | <=）？ $amount

withdraw $amount

transfer $amount to target

為了理解上述語句的使用方法，圖4給出了三種資產(chǎn)轉(zhuǎn)移行為交易條款的兩個示例，并在語句中使用了前述中時間表達式。

第一個條款表示，如果買家收到貨了要調(diào)用接收（receive）操作解凍貨款轉(zhuǎn)給賣家，并取回保證金。

第二個條款表示，如果過了發(fā)貨后15天后買家仍沒有確認(rèn)到貨且沒有申訴（其它條款表示），就按未收到貨物處理，賣家就可將買家定金從合約中解凍返還給買家，并取走合約中的余額，即他自己的定金和貨款。

7 SPESC實例應(yīng)用

為了驗證SPESC語言的有效性，本節(jié)將綜合應(yīng)用前述SPESC語法規(guī)范，以“打印機售賣合同”為例，展現(xiàn)SPESC語言在編寫面向法律合同所具有的便捷性、易用性以及可讀性。

（1）合約當(dāng)事人定義：包括買方和賣方。

賣方擁有一個作為唯一標(biāo)識的地址，并且可以執(zhí)行獲取交易收益、郵寄打印機的動作。

買方為群體用戶，可以執(zhí)行訂購打印機、確認(rèn)接收打印機的動作。

party Seller： address 0x14723…60C {

credentials：String

deliever（）

collectPayment （）

}

party group Buyer{

order（）

confirmReceive（）

}

（2）資產(chǎn)描述：一臺價值2000元人民幣的打印機。

asset Printer： address 0xCA35b…733c {

name： "Printer"

value： 2000 RMB

}

（3）合約條款定義：

條款1：買方可以向賣方訂購一臺打印機，并向合約存入訂金。

term no1： Buyer may order

while deposit $ Printer：：value.

條款2：如果買方向賣方訂購了一臺打印機，合約生效，賣方應(yīng)該在7天內(nèi)將打印機寄送給買方。

term no2： Seller must deliver

when within 7 days after Buyer did order.

條款3：到貨后買方應(yīng)在7天內(nèi)確認(rèn)收貨。

term no3： Buyer must confirmReceive

when within 7 days after Buyer did receive.

條款4：在買方確認(rèn)收貨后，賣方可以獲取收益并結(jié)束交易。

term no4： Seller may CollectPayment

when after Buyer did confirmReceive

while withdraw $ Printer：：value.

（4）合約附加信息Additional定義—添加兩方當(dāng)事人簽名。

SellerSignature ： String

BuyerSignature ： String

綜上，形成售賣合同對應(yīng)的SPESC程序如圖5所示。在合約中，Seller為個體用戶，Buyer為群體用戶，定義用戶時便聲明其所關(guān)聯(lián)執(zhí)行的動作，如Seller相關(guān)聯(lián)動作為deliver （）和collectPayment（），動作具體內(nèi)容由同名條款進行定義。

合同轉(zhuǎn)化后的條款共有4個，包含兩個義務(wù)條款term no2： Seller must deliver和term no3： Buyer must confirmReceive，以及兩個權(quán)力條款term no1： Buyer may order和term no4： Seller may collectPayment，并依照第4節(jié)所述，定義其各自的前置、后置和伴隨條件。

此外，在term no2中，規(guī)定賣家必須在買家下單后7天內(nèi)執(zhí)行寄出操作，此處使用when表示條款前置條件，并使用within 7 days after Buyer did order的時間表達式對事件發(fā)生時間進行約束。

在term no1中，買方訂購打印機的同時需向合約存入訂金，因為是買方主動的行為，采用deposit進行存入操作。term no4中規(guī)定買方確認(rèn)收貨后，賣方可以獲取收益，此處是指當(dāng)前置條件成立后，按照合約中的規(guī)則，合約賬戶向調(diào)用者轉(zhuǎn)移資產(chǎn)，因此使用withdraw關(guān)鍵詞表示貨幣支付。

8 結(jié)束語

本文介紹了一種類自然語言的高級智能合約語言SPESC，系統(tǒng)介紹了SPESC的整體結(jié)構(gòu)和語法規(guī)則，詳述了參與方和條款的撰寫規(guī)范，并以具體實例的方式介紹了SPESC實現(xiàn)智能合約基礎(chǔ)功能—貨幣支付的方式。SPESC具有更加接近于現(xiàn)實合約的特征，也易于非計算機專業(yè)人士理解和使用，代表了未來智能合約發(fā)展的趨勢，具有較大的應(yīng)用空間和使用價值。

基金項目

1.國家科技部重點研發(fā)計劃（項目編號：2018YFB1402702）;

2.國家自然科學(xué)基金（項目編號：61972032）。

參考文獻

[1] Nakamoto S. A peer-to-peer electronic cash system[J]. Bitcoin.–URL： https：//bitcoin. org/bitcoin. pdf， 2008.

[2] Szabo N. Smart contracts in essays on smart contracts， commercial controls and security （1994）[J]. URL： http：//www. fon. hum. uva. nl/rob/Courses/InformationInSpeech/CDROM/Literature/LOTwinterschool2006/szabo. best. vwh. net/smart. contracts. html.

[3] 魏昂，黃忠義，周鳴愛.智能合約安全與實施規(guī)范研究[J].網(wǎng)絡(luò)空間安全，2020，11（03）：44-49.

[4] Coblenz M . Obsidian： A Safer Blockchain Programming Language[C] In proceedings of 2017 IEEE/ACM 39th International Conference on Software Engineering Companion （ICSE-C）. ACM， 2017.

[5] Bhargavan K， Delignat-Lavaud A， Fournet C， et al. Formal verification of smart contracts： Short paper[C]//Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security. ACM， 2016： 91-96.

[6] Hirai Y. Defining the ethereum virtual machine for interactive theorem provers[C]//International Conference on Financial Cryptography and Data Security. Springer， Cham， 2017： 520-535.

[7] Kasprzyk K. The Concept of Smart Contracts from the Legal Perspective[J]. Review of Comparative Law， 2018， 34（3）.

[8] Goldenfein J， Leiter A. Legal Engineering on the Blockchain：‘Smart Contracts as Legal Conduct[J]. Law and Critique， 2018， 29（2）： 141-149.

[9] Gomes S S. Smart Contracts： legal frontiers and insertion into the Creative Economy[J]. Brazilian Journal of Operations & Production Management， 2018， 15（3）： 376-385.

[10] Allen J G. Wrapped and Stacked：‘Smart Contracts and the Interaction of Natural and Formal Language[J]. European Review of Contract Law， 2018， 14（4）： 307-343.

[11] He X， Qin B， Zhu Y， et al. Spesc： A specification language for smart contracts[C]//2018 IEEE 42nd Annual Computer Software and Applications Conference （COMPSAC）. IEEE， 2018， 1： 132-137.