本系列文檔翻譯版權(quán)歸FireStack團(tuán)隊(duì)所有帆竹，轉(zhuǎn)載請(qǐng)注明來源合砂。
智能合約通過一種去中心化的目胡、拜占庭容錯(cuò)的分布式賬本锯七，很好地展現(xiàn)了區(qū)塊鏈的計(jì)算形式。智能合約的出現(xiàn)誉己，讓開發(fā)者構(gòu)建去中心化應(yīng)用（Dapps）成為可能眉尸。這些應(yīng)用的運(yùn)行及業(yè)務(wù)邏輯皆可編寫為智能合約，放到去中心化的區(qū)塊鏈網(wǎng)絡(luò)上運(yùn)行巨双。
在去中心化網(wǎng)絡(luò)上運(yùn)行應(yīng)用噪猾，使得受信任中心節(jié)點(diǎn)、定制化服務(wù)器的需求不復(fù)存在筑累。如今智能合約非常受歡迎袱蜡，在諸如眾籌、游戲慢宗、去中心化外匯交易坪蚁、支付處理等場(chǎng)景，智能合約有力推動(dòng)了現(xiàn)實(shí)經(jīng)濟(jì)環(huán)境的發(fā)展镜沽。
然而敏晤，從過去幾年的經(jīng)歷來看，智能合約的實(shí)踐催生了一些游走于邊緣的行為缅茉，這偏離了開發(fā)人員關(guān)于智能合約的最初理念嘴脾。這種分歧導(dǎo)致了對(duì)智能合約的重大攻擊事件，例如對(duì)DAO合約和Parity錢包的攻擊宾舅。正因?yàn)閰^(qū)塊鏈的不可篡改性统阿，智能合約無法獲得直接升級(jí)修復(fù)，這使得問題日益嚴(yán)重筹我。因此，確保智能合約的安全運(yùn)行至關(guān)重要帆离。
事實(shí)證明蔬蕊，形式化證明和模型檢驗(yàn)等方法在提高其他領(lǐng)域的軟件系統(tǒng)的安全性方面是非常有效的。所以我們很自然會(huì)想到將其用于探索提高智能合約的可讀性和安全性哥谷。另外岸夯，這些方法也能嚴(yán)格保證合約行為的規(guī)范性。
然而们妥，使用現(xiàn)有語(yǔ)言（如Solidity）在形式化證明工具上進(jìn)行應(yīng)用并不是一件容易的事猜扮。因?yàn)榈湫偷膱D靈完備語(yǔ)言有其非常特別的表達(dá)形式。誠(chéng)然监婶，在讓語(yǔ)言更易于理解旅赢、易于驗(yàn)證齿桃、易于表達(dá)三者之間是存在著權(quán)衡的。例如煮盼，比特幣的腳本語(yǔ)言具有易于理解的特點(diǎn)短纵，并且對(duì)有狀態(tài)對(duì)象不作處理。而圖靈完備的語(yǔ)言（如Solidity）具有易于表達(dá)的特點(diǎn)僵控。
Scilla是一種新的（中級(jí)水平的）智能合約香到，旨在同時(shí)實(shí)現(xiàn)易于表達(dá)的形式及可追蹤性”ㄆ疲基于前述有關(guān)合約行為的論證悠就，Scilla設(shè)定的設(shè)計(jì)原理如下：
計(jì)算與通信的分離
Scilla中的合約會(huì)被構(gòu)造為通信自動(dòng)機(jī)：每個(gè)合約內(nèi)計(jì)算（例如改變賬戶余額或運(yùn)算函數(shù)值）會(huì)通過一種具有獨(dú)立原子性轉(zhuǎn)換（transition）的過程來實(shí)現(xiàn)。也就是說充易，這個(gè)過程不涉及到第三方梗脾。每當(dāng)進(jìn)行類似操作時(shí)（例如，向第三方轉(zhuǎn)移控制權(quán)）蔽氨，轉(zhuǎn)換（transition）會(huì)通過發(fā)送/接收消息這種顯式通信來表示結(jié)束藐唠。自動(dòng)機(jī)架構(gòu)使得區(qū)塊鏈上的通信（如發(fā)送/接收資金和消息）能直接解決某類合約糾紛（如transitions），這種清晰鹉究、合理的機(jī)制有利于撰寫合約及保護(hù)不動(dòng)產(chǎn)宇立。
有效性和純計(jì)算之間的分離
轉(zhuǎn)換（transition）中發(fā)生的任何合約內(nèi)計(jì)算必須可終止，并且合約狀態(tài)和執(zhí)行過程可預(yù)測(cè)自赔。為了實(shí)現(xiàn)這一目標(biāo)妈嘹，Scilla從函數(shù)式編程思想中取其精華，將純表達(dá)式（如原生數(shù)據(jù)類型和映射）绍妨、不完全本地狀態(tài)管理（如讀/寫合約字段）和區(qū)塊鏈反射（如讀取當(dāng)前區(qū)塊編號(hào)）區(qū)分開來润脸。通過介于純語(yǔ)言和不純語(yǔ)言之間交叉語(yǔ)義的嚴(yán)謹(jǐn)設(shè)計(jì)，Scilla確保了許多合約轉(zhuǎn)換（如進(jìn)程和類型保護(hù)）的基本性質(zhì)不變他去，同時(shí)讓它們適合通過獨(dú)立工具進(jìn)行交互式和/或自動(dòng)化驗(yàn)證毙驯。
調(diào)用與持續(xù)之間的分離
合約構(gòu)建作為一種自動(dòng)化通信系統(tǒng)，它是一種僅允許尾調(diào)用的計(jì)算模型灾测，即每次對(duì)外部函數(shù)（如另一個(gè)合約）的調(diào)用都必須是最后的完成指令爆价。
