依赖

• rustc1.12.0-nightly(2016-08-12).

• z3

您需要将 z3 的安装路径添加到您的 PATH 中，以便 rustproof 可以正常工作。

支持的 Rust 语言特性

• 整数算术
  • isize 和 usize 是 不支持的
• 布尔表达式、变量和字面量
• 断言（整数/布尔型）
  • assert_eq!() 是 不支持的
• if 语句

使用

将 Rustproof 包含到您的项目中

在 Cargo.toml 中添加 rustproof 作为依赖项

[dependencies]
rustproof = { git = "https://github.com/Rust-Proof/rustproof.git" }

使用 Rustproof

#![plugin(rustproof)] 在每个使用 rustproof 的文件中都是必需的。通常，这会被放置在文件的开始处。

Rustproof 使用自定义属性 condition 允许在函数上声明前置/后置条件。

该属性提供为： #[condition(pre=" ", post=" ")] 并且必须在函数定义之前提供。

有关属性系统的详细说明，请参阅 USAGE。

请参阅 EXAMPLES 以查看具有条件属性的示例函数。

此外，#![plugin(rustproof(debug))] 会打印出每个使用 #[condition(..)] 注释的函数的基本块，以及生成验证条件的逐步视图。

贡献者

Matthew Slocum
Sami Sahli
Vincent Schuster
Michael Salter
Bradley Rasmussen
Drew Gohman
Matthew O'Brien

报告问题

请将所有问题报告到 github 问题跟踪器。

许可

Rustproof 在 MIT 许可证和 Apache 许可证（版本 2.0）的条款下分发。

有关详细信息，请参阅 LICENSE-APACHE、LICENSE-MIT 和 COPYRIGHT。