昨天，我们发布了【Facebook的Diem团队梦碎，但成果留存：谈谈Move的编程魅力（上）】，向大家介绍了Move的部分概况。今日，将为大家分享剩余的内容，包括Move的另一关键特性：形式化验证，及该特性为Move所带来的优势和弊端。
深度资源
一个资源是一个只有key和store能力的结构体。在Move中，一个账号每种类型的资源只能持有一个。资源不能被复制或丢弃，这使得资源适合直接代表价值的物品，例如coin。
账户与其资源之间的直接关联，使得编写某些「不好的」代码也变得更加困难，例如导致价值意外损失的代码。
但是，不正确的计算以及与资源有关的那些更微妙的逻辑错误还是有可能会出现。这就是为什么我们强烈建议进行智能合约审计来增强安全保障。
区块链上全局存储的编程接口执行了一个限制——每个账户最多只能持有每个资源的一个副本。
一个程序可以使用以下操作在全局存储中创建、读取、更新和删除资源：
为了避免资源的伪造及其他不当操作，Move执行严格的数据封装（encapsulation of data）。Move的代码和类型声明被分组为module。代码作为module的一部分被部署到一个账户中。
当一个结构类型在一个模块中被声明时，只有在同一模块中定义的函数可以访问该结构类型的字段或创建该结构类型的value。Move结构声明被视为抽象数据类型，对其module以外的代码隐藏其内部工作原理。module中的函数默认为私有，只能在模块内调用。它们可以被声明为public，这使得它们可以被外部代码访问。module可以有friend，也就是他们信任的其他module，并且可以声明个别non-public方法以供friend访问。
References
Reference是pointer的一种类型，包括对其使用方式的限制。使用pointer的语言中，一个常见问题是悬挂引用（dangling references）：指向已被重新用于其他目的或被取消分配的内存或存储。
例如，如果你为一个向量的最后一个元素创建了一个reference，然后缩小了向量，则该reference现在就指向了无效的内存或存储。悬挂引用和其他与不受限制的pointer相关的问题历来是导致大多数软件安全漏洞的原因。
Move处理reference的方式与Rust处理reference的方式类似。它包括类型检查规则，以确保reference的生命周期不长于原始数据的生命周期。当代码创建一个reference时，该reference并没有取得数据的所有权。相反，代码借用了读取或写入数据的能力。
在阅读Move代码时，名称中带有“borrow”一词的操作就会产生reference。
Move语言的定义中并不包含对reference checking的完整描述（"borrow checker"，它确保borrow的reference不会存留太长时间）。
不过，今年有一份详细的技术论文被发表（https://arxiv.org/abs/2205.05181），该定义中的两个关键规则是：
①不允许对reference的reference，而且reference不能存储在结构中。这意味着，当一个函数被调用并带有一个reference参数时，尽管它可以返回reference，但也不能将reference存储在一个长期存在的数据结构中。一个函数调用并不会延长reference的生命周期。
②对局部变量或局部变量字段的reference不能超过局部变量的作用域的终点。
类Rust语法
Move有一种类似于Rust的语法，在某些地方与C风格的语言有些不同。在此，我们总结了一些重要的语法规则，以便更轻松地浏览Move代码。
使用let声明变量：
类型注释：type和initializer=e是可选的。当它们被省略时，Move使用类型推理来确定变量的类型。
下图是一些变量声明的例子：
Move有典型的表达式，用于算术、移位操作、函数调用、赋值等，用于流程控制的有if、while、for、break和continue等表达式。
函数是使用以下语法声明的：
其中id是函数的名称，parameter-list声明参数，return-type是返回类型。还有一些必要的注释，如acquires注释。这些注释列出了函数从全局存储中访问的资源，还有关于可见性的注解。如前所述，函数可以是公共的、私有的，或者可以被friend module访问。
形式化验证
智能合约安全和正确地运行至关重要，因为其往往持有巨额的资产。形式化验证是确保一个程序（如智能合约）执行其预期操作的最佳技术之一。
在形式化验证中，工程师编写规范，并以数学方式表达代码的预期行为。然后使用工具尝试检查代码是否符合规范。
我们可以将这种检查视为测试，但这其中有一个关键的区别：它不是检查代码在某些特定情况下的行为，而是检查代码在所有可能情况下的行为。
如果检查通过，则说明该工具找不到代码违反规范的用例。不过这并不意味着代码100%不存在违反规范的情况，因为工具或编译器的漏洞还是有可能导致错误的发生。但这依旧使得其比运行一组测试用例提供了更严格的规范保证。
对于一些代码，特别是复杂的代码，工具可能无法自动检查代码是否符合规范。因此工程师也许需要为一小部分的代码添加具体化的规范，直到检查器能够成功运行为止。工程师甚至可能需要写证明规则，然后该工具会根据数学原理检查代码是否符合这些证明规则。
因为确保智能合约的安全是至关重要的，一些智能合约编程语言会原生就提供对形式化验证的支持。就像Solidity编译器提供的SMTChecker工具，它假设requires子句始终为真，然后试图证明assert子句永远不会失败。
Move也对形式化验证技术进行了集成支持。它含有丰富的用于形式化验证的规范语言，能够规范比Solidity的requires和assert子句更复杂的属性，并且有目的地删除了会对形式化验证造成问题的语言结构。Move的开发环境中就包括一个名为“Move Prover”的检查器。
CertiK由两位常春藤盟校的计算机科学教授所创立。作为区块链安全领域的先驱，CertiK运用的正是目前最先进的形式化验证技术。创办CertiK的两位教授均是形式化验证方面的专家，并创建了CertiKOS——世界上第一个也是唯一一个完全被验证的并发式多核操作系统和管理程序。CertiK致力于通过将形式化验证技术应用于安全审计以确保智能合约的安全。
因此，CertiK安全专家自然而然地就注意到了Move这一集成了形式化验证技术的编程语言。
下方是一个double函数及其规范的简单示例。double函数的功能是将一个64位无符号整数（unsigned integer）进行翻倍计算。由spec double给出的double 规范从数学上描述了预期的结果。
规范语言是Move的一个集成部分。规范被分离成spec block。spec block指定了函数的前置条件（requirements）和后置条件（ensures）。
前置条件需要在函数被调用之前必须为真，以便该函数能够正常运行。而后置条件则是指当函数返回时必须为真。
此外，spec block还指定了失败条件（aborts_if）。规范语言支持大多数常规Move语法。它还支持用于指定程序行为的重要附加功能，包括forall、exists和implies。
下方是spec block的示例：
Move Prover将规范和程序语义转换为了逻辑表达式。然后将它们传递给可满足性模理论（SMT）求解器，例如Z3和CVC5，以证明或反驳。以下大幅简化的图表说明了这一点：
形式化验证有其优势也有弊端。
形式化验证被认为是构建可靠程序的“黄金标准”，并被用于许多如NASA这样的关键任务系统。编写系统行为的形式化规范可以暴露出逻辑上的不一致或思维的不清晰。
然而即使是对于专家来说，将相对简单的系统进行形式化规范也是困难且耗时的。
除此之外，在处理更复杂的程序或规范时，检察员也会遇到阻碍，并且可能会需要极长的时间来将其解决。
在CertiK接下来发布的文章中，我们将更深入地探究Move形式化验证的潜力和其所面临的挑战。
由于形式化验证的复杂性，CertiK在此建议如有需求的用户应当寻找一个在形式化验证方向有所建树的安全机构来进行合约审计或是协助对合约的形式化验证。
写在最后
我们希望这篇文章可为想要了解Move语言的读者提供足够的参考价值。
Move确实引入了新的方法来解决可扩展性问题以及提高安全性。然而，没有一种语言可以100%保证安全，非可扩展的或不正确的代码仍有机会干扰Move的内置功能。
如同Web3.0，兔子洞的存在是永远数之不尽的。
如果你想了解关于Move技术特点的更多信息，那么建议复制链接（https://move-language.github.io/move/introduction.html）至浏览器访问这些值得参考的开发人员文档，并持续关注我们对Move Prover（一个用Move编写的智能合约的形式化验证工具）进行的技术深入研究。
