今天的文章是關於將我們的需求文件轉換為等價的形式化、數學化需求規範的過程。
英語是現代商業的通用語。因此毫不奇怪的是我們經常把需求寫成簡單的英文文件。不幸的是，出於正式的驗證目的，英語文件太不精確，通常會掩蓋重要的實現細節。基於這個原因（我們將在後面看到），我們通常需要正式的驗證專家來幫助我們將英語需求文件重寫為正式的數學要求規範。例如，假設我們正在設計一個實現公開競價拍賣的智慧合約。我們可以將拍賣合同的要求寫成如下：
英語語言要求
每個拍賣都有一個主物，一個有效期，一個最低競標，一個可選的最高競標者（預設為無）和無限數量的競標者。在拍賣進行中，投標人可以按順序進行投標。如果出價大於最低出價，則將其記錄為新的最低出價，同時將出價者記錄為最高出價者。否則，出價將被忽略。拍賣結束時，除非出價人沒有出價，否則將從出價人的帳戶中扣除等於最高出價人出價的金額並將其轉移到拍賣主物。
因此現在我們要將英語描述轉換為正式的數學描述。為此我們將選擇適合表達我們所需屬性的數學邏輯。就像英語一樣，還有多種語言一樣。法文 中文; 等等...，我們可以使用不同的數學邏輯。一些常見的選擇包括：方程式邏輯，一階邏輯，集合論，高階邏輯/型別論，重寫邏輯或可達性邏輯。我們如何知道要使用哪個？事實證明，在（a）形式化我們的要求，（b）我們的定理證明者和（c）我們的形式語義中使用的邏輯都需要整合在一起，因此我們如何對過程的一部分做出選擇將影響其他。
為了我們的目的，我們將使用可達性邏輯（這也是K框架使用的邏輯），因為它（1）使我們能夠非常自然地形式化對演化系統的需求，以及（2）具有強大的工具支援。因此這意味著我們將系統描述為可達性邏輯理論。可達性邏輯理論具有（a）描述我們系統狀態的語法和配置；（b）描述我們系統要求的可達性規則。現在我們發明一些語法和配置來定義拍賣合同狀態。為此我們將使用K語言提供的語法架構。
拍賣狀態（語法/配置）
syntax Address ::= (Letter | Number)*
syntax MaybeAddress ::= Address | “None”
configuration <host> Address </host>
<start> Number </start>
<end> Number </end>
<highestBidder> Address </highestBidder>
<minBid> Number </minBid>
使用此語法和配置，我們可以編寫如下的具體拍賣狀態：
<host> ab2r3f <host>
<start> 10 </start>
<end> 20 </end>
<highestBidder> None </highestBidder>
<minBid> 15 </minBid>
希望該配置的含義很清楚：拍賣在時間unit 10開始，在時間unit 20結束，由地址為ab2r3f的帳戶所有者主持，尚無可行的出價，且最低出價為15個令牌。現在這個簡單的語法描述已經有可能幫助我們發現問題——特別是，它可以幫助我們瞭解系統狀態描述是否不完整。實際上我們的拍賣配置缺少一個關鍵要素：當前時間！這種遺漏是有道理的，因為在我們原始的合約說明中從未直接提及時間，而只是間接提及了時間。因此修改後的拍賣合約狀態配置將如下所示：
configuration <host> Address </host>
<start> Number </start>
<end> Number </end>
<currentTime> Number </currentTime>
<highestBidder> Address </highestBidder>
<minBid> Number </minBid>
現在我們知道拍賣何時開始。例如拍賣配置：
<host> ab2r3f <host>
<start> 10 </start>
<end> 20 </end>
<currentTime> 5 </currentTime>
<highestBidder> None </highestBidder>
<minBid> 15 </minBid>
描述了尚未開始的拍賣。我們還需要澄清其他問題，例如數字必須為零或正數，因為我們不希望貨幣或時間為負數。
拍賣合同要求（規則）
可達性邏輯規則的形式為：
rule Configuration1 => Configuration2 requires A ensures B
可以將其理解為：處於配置1所描述的狀態且滿足條件A的系統必須演變為配置2所描述的確保條件B的系統。為方便起見，我們將假定未提及的配置部分不會發生變化。現在讓我們看一些示例規則。
格式正確的持續時間
立即想到一個簡單的規則：對於任何持續時間，我們都需要（a）持續時間是靜態的，即不變；（b）開始於結束之前。可以透過以下形式的規則來描述：
rule <start> S </start>
<end> E </end>
=>
<start> S </start>
<end> E </end>
requires S < E
（a）滿足以下條件：開始時間和結束時間不受此規則的影響；要求（b）包含在require子句中。
時間和出價的單調性
在除了最奇特的物理學研究之外的所有研究中，時間總是在向前發展。讓我們將該要求編碼為規則：
rule <curTime> C </curTime>
=>
<curTime> C’ </curTime>
requires C <= C’
該規則是說當前時間C必須演變為某個時間C'（可能不同），以使C小於或等於C'。
我們有一條几乎相同的規則，規定最低出價必須始終增加價值或保持不變（以防萬一沒有新的出價）：
rule <minBid> M </minBid>
=>
<minBid> M’ </minBid>
requires M <= M’
拍賣結束
最終規則規定，拍賣狀態在拍賣結束後不得更改。我們可以這樣寫：
rule <end> E </end>
<curTime> C </curTime>
<highestBidder> B </highestBidder>
<minBid> M </minBid>
=>
<end> E </end>
<curTime> C’ </curTime>
<highestBidder> B </highestBidder>
<minBid> M </minBid>
requires E <= C
此規則完全符合我們的要求。
從以上描述中，您可能會以為智慧合約驗證並不是那麼難。不幸的是，為了簡化解釋，我們隱藏了驗證問題的大部分複雜性。現在讓我們拉開帷幕，看看驗證真實智慧合約的複雜性。在實踐中：
1. 們的系統語法/配置實際上描述了整個區塊鏈系統，例如我們的語法和配置將是以太坊虛擬機器（EVM）位元組碼的語法和配置;
2. 我們的規則將討論特定的EVM位元組碼拍賣智慧合約如何演變。該合同將涉及我們上面提到的狀態元件的變數，即它將有一個拍賣主機的可變主機，即地址，拍賣開始時間的可變起始，等等。
（1）-（2）的結果是，在實踐中，我們推理的原始碼程式（無論是智慧合約還是區塊鏈系統程式碼）僅間接描述了我們要設計的系統，即我們沒有去設計全新的語言從頭開始專門描述我們的問題。這意味著我們正式要求的對映必須討論與我們整體所需的系統行為完全不相關的概念，例如EVM詳細資訊與拍賣完全無關，例如EVM指令和記憶體位置。
我們已經看到了如何使用K將英語要求對映到形式化數學要求的概述，並著眼於驗證區塊鏈系統和智慧合約。此外我們看到形式驗證問題更加深入。它需要同時（i）邏輯專家（例如可達性邏輯）和；（ii）系統專家（例如以太坊）。幸運的是，存在許多邏輯工具（例如K框架）和教科書，可以幫助系統專家精通解決形式驗證所需的數學邏輯技能。
您的公司或組織是否使用形式驗證來加速開發過程並減輕潛在的設計風險？您是否需要一個值得信賴的合作伙伴來幫助您解決圍繞區塊鏈系統設計，智慧合約語言或智慧合約實施的問題？如果是這樣，我們很樂意為您提供幫助。
