rule <curTime> C </curTime>
您的公司或组织是否利用形式验证来加快开拓进程并减轻潜在的设计风险？您是否需要一个值得信赖的相助同伴来辅佐您办理环绕区块链系统设计，智能合约语言或智能合约实施的问题？假如是这样，我们很乐意为您提供辅佐。在除了最怪异的物理学研究之外的所有研究中，时间老是在向前成长。让我们将该要求编码为法则：
<minBid> Number </minBid>
<currentTime> Number </currentTime>
configuration <host> Address </host>
（a）满意以下条件：开始时间和竣事时间不受此法则的影响；要求（b）包括在require子句中。
<curTime> C’ </curTime>
追念一下，正式验证就是要知道我们的系统实现（譬喻区块链系统/智能合约）是否满意我们的系统要求。syntax MaybeAddress ::= Address | “None”
最终法则划定，拍卖状态在拍卖竣事后不得变动。我们可以这样写：
描写了尚未开始的拍卖。我们还需要澄清其他问题，譬喻数字必需为零或正数，因为我们不但愿钱币或时间为负数。
但愿该设置的寄义很清楚：拍卖在时间unit 10开始，在时间unit 20竣事，由地点为ab2r3f的帐户所有者主持，尚无可行的出价，且最低出价为15个令牌。此刻这个简朴的语法描写已经有大概辅佐我们发明问题——出格是，它可以辅佐我们相识系统状态描写是否不完整。实际上我们的拍卖设置缺少一个要害要素：当前时间！这种漏掉是有原理的，因为在我们原始的合约说明中从未直接提实时间，而只是间接提及了时间。因此修改后的拍卖合约状态设置将如下所示：
<minBid> M </minBid>
=>
每个拍卖都有一个主物，一个有效期，一个最低竞标，一个可选的最高竞标者（默认为无）和无限数量的竞标者。在拍卖举办中，投标人可以按顺序举办投标。假如出价大于最低出价，则将其记录为新的最低出价，，同时将出价者记录为最跨越价者。不然，出价将被忽略。拍卖竣事时，除非出价人没有出价，不然将从出价人的帐户中扣除便是最跨越价人出价的金额并将其转移到拍卖主物。
<curTime> C </curTime>
拍卖竣事
<end> Number </end>
<end> E </end>
利用此语法和设置，我们可以编写如下的详细拍卖状态：
rule <end> E </end>
rule <minBid> M </minBid>
英语语言要求
可以将其领略为：处于设置1所描写的状态且满意条件A的系统必需演变为设置2所描写简直保条件B的系统。为利便起见，我们将假定未提及的设置部门不会产生变革。此刻让我们看一些示例法则。
<highestBidder> None </highestBidder>
本日的文章是关于将我们的需求文档转换为等价的形式化、数学化需求类型的进程。
requires S < E<minBid> M’ </minBid>
<host> ab2r3f <host>
该法则是说当前时间C必需演变为某个时间C’（大概差异），以使C小于或便是C’。
1. 们的系统语法/设置实际上描写了整个区块链系统，譬喻我们的语法和设置将是虚拟机（EVM）字节码的语法和设置;
<end> E </end>
2. 我们的法则将接头特定的EVM字节码拍卖智能合约如何演变。该条约将涉及我们上面提到的状态组件的变量，即它将有一个拍卖主机的可变主机，即地点，拍卖开始时间的可变起始，等等。
<end> Number </end>
从以上描写中，您大概会觉得智能合约验证并不是那么难。不幸的是，为了简化表明，我们埋没了验证问题的大部门巨大性。此刻让我们拉开帷幕，看看验证真实智能合约的巨大性。在实践中：
<end> E </end>
rule <start> S </start>
<end> 20 </end>
<minBid> Number </minBid>
requires M <= M’
rule Configuration1 => Configuration2 requires A ensures B
拍卖状态（语法/设置）
<highestBidder> None </highestBidder>
<start> Number </start>
<host> ab2r3f <host>
syntax Address ::= (Letter | Number)*
<highestBidder> B </highestBidder>
=>
<start> Number </start>
<highestBidder> B </highestBidder>
=>
<end> 20 </end>
当即想到一个简朴的法则：对付任何一连时间，我们都需要（a）一连时间是静态的，即稳定；（b）开始于竣事之前。可以通过以下形式的法则来描写：
因此此刻我们要将英语描写转换为正式的数学描写。为此我们将选择适合表达我们所需属性的数学逻辑。就像英语一样，尚有多种语言一样。法文 中文; 等等…，我们可以利用差异的数学逻辑。一些常见的选择包罗：方程式逻辑，一阶逻辑，荟萃论，高阶逻辑/范例论，重写逻辑或可达性逻辑。我们如何知道要利用哪个？事实证明，在（a）形式化我们的要求，（b）我们的定理证明者和（c）我们的形式语义中利用的逻辑都需要整合在一起，因此我们如何对进程的一部门做出选择将影响其他。
英语是现代贸易的通用语。因此绝不奇怪的是我们常常把需求写成简朴的英文文档。不幸的是，出于正式的验证目标，英语文档太不准确，凡是会掩盖重要的实现细节。基于这个原因（我们将在后头看到），我们凡是需要正式的验证专家来辅佐我们将英语需求文档重写为正式的数学要求类型。譬喻，假设我们正在设计一个实现果真竞价拍卖的智能合约。我们可以将拍卖条约的要求写成如下：
可达性逻辑法则的形式为：
<highestBidder> Address </highestBidder>
<start> 10 </start>
<curTime> C’ </curTime>
=>
（1）-（2）的功效是，在实践中，我们推理的源代码措施（无论是智能合约照旧区块链系统代码）仅间接描写了我们要设计的系统，即我们没有去设计全新的语言从新开始专门描写我们的问题。这意味着我们正式要求的映射必需接头与我们整体所需的系统行为完全不相关的观念，譬喻EVM具体信息与拍卖完全无关，譬喻EVM指令和内存位置。
为了我们的目标，我们将利用可达性逻辑（这也是K框架利用的逻辑），因为它（1）使我们可以或许很是自然地形式化对演化系统的需求，以及（2）具有强大的东西支持。因此这意味着我们将系统描写为可达性逻辑理论。可达性逻辑理论具有（a）描写我们系统状态的语法和设置；（b）描写我们系统要求的可达性法则。此刻我们发现一些语法和设置来界说拍卖条约状态。为此我们将利用K语言提供的语法架构。
在我们的四部门系列的第二部门中，我们将接头对系统要求举办形式化的进程，以及如何使其适合于系统和智能合约的形式验证的更大范畴。
此刻我们知道拍卖何时开始。譬喻拍卖设置：
<minBid> M </minBid>
拍卖条约要求（法则）
<currentTime> 5 </currentTime>
我们已经看到了如何利用K将英语要求映射到形式化数学要求的概述，并着眼于验证区块链系统和智能合约。另外我们看到形式验证问题越发深入。它需要同时（i）逻辑专家（譬喻可达性逻辑）和；（ii）系统专家（譬喻以太坊）。幸运的是，存在很多逻辑东西（譬喻K框架）和教科书，可以辅佐系统专家能干办理形式验证所需的数学逻辑技术。
<minBid> 15 </minBid>
<minBid> 15 </minBid>
<start> S </start>
名目正确的一连时间
<start> 10 </start>
时间和出价的单调性
我们有一条险些沟通的法则，划定最低出价必需始终增加代价或保持稳定（以防万一没有新的出价）：
requires C <= C’
此法则完全切合我们的要求。
configuration <host> Address </host>
requires E <= C
郑重声明：本文版权归原作者所有，转载文章仅为传播更多信息之目的，如作者信息标记有误，请第一时间联系我们修改或删除，多谢。
