Attributes
#[spec] 作用在方法上
spec属性用于表明某个函数属于规范范畴。
当spec属性赋值给名为<函数名称>_spec的函数时，移动证明器在验证调用<函数名称>的其他函数时，会使用该规格说明，而非原始函数。
在这种情况下，spec 函数必须：
- 其名称与原始函数相同，但会在末尾添加
_spec——若情况并非如此，则该spec仅用于检查特定场景（详情见下文） - 与原始函数具有相同的签名
- 调用原始函数——根据规范返回的值通常就是原始函数所返回的值，但并非必须如此。
#[spec] as a spec of a scenario
#[spec] 属性可用于指定一个可由 Move 验证器进行验证的场景。在这种情况下，对 spec 函数的名称和签名没有限制。
#[spec(prove)]
#[spec(prove)] 这个属性用于指定一个函数是需要由 Move 验证器进行验证的规范。没有 prove 关键字的规范不会被验证器进行检查，但在作为其他函数证明的一部分被调用时，它会被使用——请参阅 我们的常见问题解答中关于规范如何组合的说明 。
在规格说明/场景中添加focus属性（使用形式为 #[spec(prove, focus)]）会使验证者仅尝试验证此特定的规格说明。而focus属性还可同时用于多个规格说明。
#[spec_only]
与 test_only 类似，spec_only 使得任何带有注释的代码（模块、函数等）仅对证明者可见。该代码不会出现在常规编译过程中，也不会在测试模式下出现。