开云·娱乐官方网址(中国)官方网站-区块链系统和智能合约的形式验证101：形式化要求

在我们的四部分系列的第二部分中，我们将辩论对系统拒绝展开一般化的过程，以及如何使其适合于区块链系统和智能合约的形式检验的更大范围。回忆起一下，月检验就是要告诉我们的系统构建（例如区块链系统/智能合约）否符合我们的系统拒绝。今天的文章是关于将我们的市场需求文档切换为等价的一般化、数学化市场需求规范的过程。英语是现代商业的通用语。

因此从不奇怪的是我们常常把市场需求写非常简单的英文文档。意外的是，出于月的检验目的，英语文档过于不准确，一般来说不会掩饰最重要的构建细节。基于这个原因（我们将在后面看见），我们一般来说必须月的检验专家来协助我们将英语市场需求文档改写为月的数学拒绝规范。

例如，假设我们正在设计一个构建公开发表竞价拍卖会的智能合约。我们可以将拍卖会合约的拒绝写如下：英语语言拒绝每个拍卖会都有一个主物，一个有效期，一个低于竞标，一个附加的最低竞标者（配置文件为无）和无限数量的竞标者。在拍卖会展开中，投标人可以按顺序展开投标。

如果开价小于低于开价，则将其记录为新的低于开价，同时将开价者记录为最低开价者。否则，开价将被忽视。拍卖会完结时，除非开价人没开价，否则将从开价人的帐户中扣减相等最低开价人开价的金额并将其移往到拍卖会主物。

因此现在我们要将英语叙述切换为月的数学叙述。为此我们将自由选择合适传达我们所须要属性的数学逻辑。就像英语一样，还有多种语言一样。法文 中文; 等等...，我们可以用于有所不同的数学逻辑。

一些少见的自由选择还包括：方程式逻辑，一阶逻辑，集合论，网卓新闻网，高阶逻辑/类型论，改写逻辑或可达性逻辑。我们如何告诉要用于哪个？事实证明，在（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 hoststart 10 /startend 20 /endhighestBidder None /highestBidderminBid 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 hoststart 10 /startend 20 /endcurrentTime 5 /currentTimehighestBidder None /highestBidderminBid 15 /minBid叙述了仍未开始的拍卖会。

我们还必须回应其他问题，例如数字必需为零或正数，因为我们不期望货币或时间为负数。拍卖会合约拒绝（规则）可达性逻辑规则的形式为：rule Configuration1 = Configuration2 requires A ensures B可以将其解读为：正处于配备1所叙述的状态且满足条件A的系统必需演进为配备2所叙述的保证条件B的系统。

为便利起见，我们将假设并未提到的配备部分会发生变化。现在让我们看一些示例规则。格式准确的持续时间立刻想起一个非常简单的规则：对于任何持续时间，我们都必须（a）持续时间是静态的，即恒定；（b）开始于完结之前。可以通过以下形式的规则来叙述：rule start S /startend E /end =start S /startend E /end requires SE（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 /endcurTime C /curTimehighestBidder B /highestBidderminBid M /minBid =end E /endcurTime C’ /curTimehighestBidder B /highestBidderminBid M /minBid requires E = C此规则完全符合我们的拒绝。

从以上叙述中，您可能会以为智能合约检验并不是那么无以。意外的是，为了修改说明，我们隐蔽了检验问题的大部分复杂性。现在让我们拉开帷幕，想到检验现实智能合约的复杂性。

在实践中：1. 们的系统语法/配备实质上叙述了整个区块链系统，例如我们的语法和配备将是以太坊虚拟机（EVM）字节字节的语法和配备;2. 我们的规则将辩论特定的EVM字节码拍卖会智能合约如何演进。该合约将牵涉到我们上面提及的状态组件的变量，即它将有一个拍卖会主机的星型主机，即地址，拍卖会开始时间的星型接续，等等。（1）-（2）的结果是，在实践中，我们推理小说的源代码程序（无论是智能合约还是区块链系统代码）仅有间接叙述了我们要设计的系统，即我们没去设计全新的语言从头开始专门叙述我们的问题。

这意味著我们月拒绝的同构必需辩论与我们整体所需的系统不道德几乎不相关的概念，例如EVM详细信息与拍卖会几乎牵涉到，例如EVM指令和内存方位。我们早已看见了如何用于K将英语拒绝同构到一般化数学拒绝的阐述，并侧重检验区块链系统和智能合约。

此外我们看见形式检验问题更为了解。它必须同时（i）逻辑专家（例如可达性逻辑）和；（ii）系统专家（例如以太坊）。幸运地的是，不存在许多逻辑工具（例如K框架）和教科书，可以协助系统专家通晓解决问题形式检验所需的数学逻辑技能。您的公司或的组织否用于形式检验来加快研发过程并减低潜在的设计风险？您否必须一个有一点信赖的合作伙伴来协助您解决问题环绕区块链系统设计，智能合约语言或智能合约实行的问题？如果是这样，我们很乐意为您获取协助。

本文来源：开云·娱乐官方网址-www.xingdoushangmao.com