王迪 秦博涵 宋偉靜 朱巖

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

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

中圖分類號： TP312 ? ? ? ? ?文獻(xiàn)標(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è)計(jì)、部署及運(yùn)行的新構(gòu)架，由于具有按照參與方約定自動(dòng)執(zhí)行的能力，也被認(rèn)為是第二代區(qū)塊鏈的核心技術(shù)。更為重要的是，智能合約技術(shù)[2]通過支持更加強(qiáng)大的編程語言和運(yùn)行環(huán)境，允許開發(fā)者在其上面開發(fā)任意價(jià)值交換相關(guān)的應(yīng)用，成功地解決了區(qū)塊鏈應(yīng)用開發(fā)困難的問題，代表著未來區(qū)塊鏈技術(shù)發(fā)展的方向。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

SPESC中的參與方有四個(gè)特點(diǎn)：

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

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

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

（4）參與方代表的用戶是可以變動(dòng)的。

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

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

作為一種法律文書，SPESC語言的主體和內(nèi)容是通過合約的各項(xiàng)條款（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)成，用以表達(dá)某個(gè)或幾個(gè)合約參與方在什么條件下需要或可能履行的行為。從SPESC語法上講，在參與方聲明一個(gè)動(dòng)作之后，該動(dòng)作何時(shí)（必須或可以）履行則需要通過使用合同條款來進(jìn)行規(guī)范。

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

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

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

（3）動(dòng)作：條款中的動(dòng)作;

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

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

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

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

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

term name ： party （must|may） action

（when preCondition）？

（while transactions+）？

（where postCondition）？ .

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

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

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

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

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

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

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

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

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

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

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

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

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

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

5 SPESC中時(shí)間表達(dá)式規(guī)范

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

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

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

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

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

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

（4）動(dòng)作完成時(shí)間查詢表示某個(gè)角色完成某項(xiàng)動(dòng)作的時(shí)間。

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

（all | first | this）？ party did action

它的返回值為一個(gè)時(shí)間點(diǎn)。

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

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

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

（1）量詞all表示所有用戶個(gè)體都完成該動(dòng)作的時(shí)間，如all Voters did Vote。

（2）量詞first表示第一個(gè)用戶個(gè)體完成該動(dòng)作時(shí)間，如first bidders did Bid。

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

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

（before | after） timepoint

其中，timepoint表示前面定義的時(shí)間點(diǎn)，before和after分別表示在這個(gè)時(shí)間點(diǎn)之前和時(shí)間點(diǎn)之后，例如before BiddingStopTime、after all Voters did Vote。

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

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

（after buyer did pay） and

（before buyer did pay + 3 day）

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

（within）？ boundary （before | after） base

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

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

（1）邏輯表達(dá)式，包含and（與）、or（或）、not（非）以及implies（蘊(yùn)含）。

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

（3）運(yùn)算表達(dá)式，包含+、-、*、/、**（乘方）。

（4）常量表達(dá)式，包含整型常量、浮點(diǎn)常量、布爾常量等。

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

6 SPESC中的貨幣支付功能

為了支持智能合約中交易的支付款功能，SPESC提供了一種簡單的貨幣支付功能，能夠與現(xiàn)有區(qū)塊鏈系統(tǒng)中的數(shù)字貨幣相銜接，實(shí)現(xiàn)簡單而高效的支付款功能。限于智能合約的區(qū)塊鏈功能，在SPESC中所有轉(zhuǎn)賬交易都是通過交易進(jì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是用戶主動(dòng)的行為，是在調(diào)用時(shí)發(fā)生的;而后兩者是按照合約規(guī)定強(qiáng)制執(zhí)行的行為，是在執(zhí)行時(shí)發(fā)生的。因此，后兩者只是按照合約描述執(zhí)行，而deposit應(yīng)作為調(diào)用動(dòng)作時(shí)的限制條件表達(dá)。

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

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

withdraw $amount

transfer $amount to target

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

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

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

7 SPESC實(shí)例應(yīng)用

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

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

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

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

party Seller： address 0x14723…60C {

credentials：String

deliever（）

collectPayment （）

}

party group Buyer{

order（）

confirmReceive（）

}

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

asset Printer： address 0xCA35b…733c {

name： "Printer"

value： 2000 RMB

}

（3）合約條款定義：

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

term no1： Buyer may order

while deposit $ Printer：：value.

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

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為個(gè)體用戶，Buyer為群體用戶，定義用戶時(shí)便聲明其所關(guān)聯(lián)執(zhí)行的動(dòng)作，如Seller相關(guān)聯(lián)動(dòng)作為deliver （）和collectPayment（），動(dòng)作具體內(nèi)容由同名條款進(jìn)行定義。

合同轉(zhuǎn)化后的條款共有4個(gè)，包含兩個(gè)義務(wù)條款term no2： Seller must deliver和term no3： Buyer must confirmReceive，以及兩個(gè)權(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的時(shí)間表達(dá)式對事件發(fā)生時(shí)間進(jìn)行約束。

在term no1中，買方訂購打印機(jī)的同時(shí)需向合約存入訂金，因?yàn)槭琴I方主動(dòng)的行為，采用deposit進(jìn)行存入操作。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ī)范，并以具體實(shí)例的方式介紹了SPESC實(shí)現(xiàn)智能合約基礎(chǔ)功能—貨幣支付的方式。SPESC具有更加接近于現(xiàn)實(shí)合約的特征，也易于非計(jì)算機(jī)專業(yè)人士理解和使用，代表了未來智能合約發(fā)展的趨勢，具有較大的應(yīng)用空間和使用價(jià)值。

基金項(xiàng)目

1.國家科技部重點(diǎn)研發(fā)計(jì)劃（項(xiàng)目編號：2018YFB1402702）;

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

參考文獻(xiàn)

[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] 魏昂，黃忠義，周鳴愛.智能合約安全與實(shí)施規(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.