通过Archetype验证智能合约-Coinmonks
原型是一种简单的高级语言，用于在Tezos区块链上开发智能合约。它可以通过将合约转码为Why3来正式验证合约。有关原型语言的更多信息，请点击以下链接：
在本文中，我们开发，指定和正式验证智能合约；通过正式验证，我们可以发现并修复错误，并确保其符合规范。
下面的视频是演示的放映（25分钟）：
以下是该演示的文本版本。
该演示的目的是为链上忠诚度计划开发智能合约。该合约记录有两个入口点的里程和里程所有者：添加和消费。
合约资产
英里所有者通过地址值标识，并且拥有数英里（可能为零）。英里由唯一的字符串ID和有效期标识，因此，在有效期后不能消费任何英里。
下面的模式说明了数据的基本建模：
优化已添加到上述模型中。用数量值增加英里，以用相同的到期日期收集几英里。例如，将具有相同到期日期的3英里合并为1英里，并将数量值设置为3：
具有相同到期日期的3英里……已合并为一项资产。
以下代码片段是合约数据的原型实现：
请注意，里程的收集类型（第11行）是分区的：这是指定一英里归一个所有者所有，并且只有一个所有者。例如，这可以防止直接将英里添加或删除到英里集合中。它必须经过所有者的里程收集。
在将里程添加到所有者的里程集合时，将测试该里程是否已存在；如果是这样，则添加指令失败。
这是通过单个里程集合实现的，而Miles字段则实现为里程标识符的列表，而不是里程列表。
动作
add操作具有两个参数：所有者地址和要添加到该所有者的新里程：
上方的所有者（第4行）是所有所有者的集合。使用get方法可以从其地址（即所有者标识符）中检索一个所有者。
add方法（第5行）用于将资产添加到集合（此处为o.miles）。
消费操作有两个参数：所有者的地址ow以及该所有者消费qty的里程数：
消费动作的实现不是那么简单，因为每英里承载着数量字段：
- 使用select方法创建所有者有效里程的集合（第4行）
- 删除英里，直到删除的英里数等于数量；为此，将迭代每个有效英里：如果当前英里的数量少于要删除的剩余英里数（第9行），则该英里将被删除（第11行），剩余值将减少其数量；否则，将减少当前英里的数量（第14行），并将剩余数字设置为0（第13行）
此实现有2个错误：您可以发现它们吗？以下部分中提供的验证将有助于检测和修复它们。
请注意，英里资产的数量字段的类型为int（即，上面资产部分的整数行6），可以为负数。但是，数量等于或小于零是没有意义的。我们想对数量字段指定一些约束，特别是应该严格保持数量为正。
可以使用资产不变性来指定这样的约束（下面的第5至7行）：
这将为所有操作（添加和消耗）生成相应的证明义务。
我们希望从一个地址操作合约，也就是说，每个操作只能由该地址调用。原型提供了一个专用的“修饰符”，由（第4行）调用：
安全谓词only_by_role（下面的第2行）可以在安全性部分中使用，以指定任何操作都应在admin上使用被调用者by修饰符：
no_storage_fail谓词（上面的第3行）对于指出某个操作（在此为add操作）不应失败（对于“找不到键”或“键存在”异常）而言很有用。通常最好的做法是不要对逻辑异常进行编程，无论是显式的（使用try…catch机制）还是隐式的，例如在发生故障时具有回滚机制的智能合约中。最好使用if控件来显式打开执行分支。异常仅应用于硬件，网络…故障，也就是说，程序本身无法控制的任何事物。
显然，这不是添加操作的情况，添加操作将失败，例如，如果ow与任何现有的记录所有者都不对应。
这些安全谓词生成证明义务，如下面的验证部分所述。可用的安全谓词列表可以在这里找到。
最后，我们要确保消耗操作的实施符合删除qty里程的基本要求。提出这种要求的方法是在执行动作之前和执行之后之间建立存储状态之间的算术关系：
后置条件p1（上面的第5行）从字面上读取“执行消耗之后的数量字段的总和等于执行之前的总和减去值qty”。
回顾一下，这是验证之前的完整合约代码：
在本节中，我们验证上一节中定义的4个谓词：
- s0：任何操作只能由管理员角色调用
- s1：访问存储时，添加操作不会失败
- p0：消费操作消耗了正数里程
- i0：任何英里的数量值严格为正
VS Code原型扩展提供了一个左侧面板，该面板列出了谓词，并允许在要验证的每个谓词上调用why3 ide：