MIRAI Annotations

此crate提供一组宏，可以用于替换标准RUST assert和debug_assert宏。它们通过允许MIRAI

• 区分路径条件和验证条件
• 区分它应该假设为真的条件和它应该验证的条件
• 在编译时检查那些因为成本太高而不应在运行时检查的条件

从这些考虑中，我们得到了这些宏家族

• 假设宏
• 后置条件宏（如verify where定义和like assume for callers）
• 前置条件宏（如assume where定义和like verify for callers）
• 验证宏

这些宏都有三种类型

• 仅在编译时检查 ('macro' 中包含 {assume, precondition, verify} 中的宏)
• 始终在运行时检查 ('checked_macro')
• 仅对调试构建在运行时检查 ('debug_checked_macro')

此外，运行时检查的类型还提供 eq 和 ne 变体，因此对于 assume 我们有

• assume!
• checked_assume!
• checked_assume_eq!
• checked_assume_ne!
• debug_checked_assume!
• debug_checked_assume_eq!
• debug_checked_assume_ne!

同样对于 postcondition! 和 precondition! 以及 verify!

此外，我们还有

• assumed_postcondition!，它是在定义站点处的假设，而不是验证。
• assume_preconditions!，它假设调用者已经满足下一个调用所有（推断的）前置条件。
• assume_unreachable!，它假设由于MIRAI无法推理的原因不可达。
• unrecoverable!，它与panic!相同，但明确表示这并不是到达这里的编程错误。
• verify_unreachable!，它要求MIRAI验证它不可达。

此外，此crate还提供用于描述和约束仅对MIRAI有意义的抽象状态的宏。这些是

• abstract_value!
• add_tag!
• does_not_have_tag!
• get_model_field!
• has_tag!
• result!
• 设置模型字段！

请参阅文档了解如何使用这些功能。