设计-by-合同 for Rust

使用“合同”注释函数和方法，使用 不变性、前置条件 和 后置条件。

设计-by-合同 是一种流行的通过形式接口规范增强代码的方法。这些规范用于通过在运行时检查它们来提高代码的正确性。

pub struct Library {
    available: HashSet<String>,
    lent: HashSet<String>,
}

impl Library {
    fn book_exists(&self, book_id: &str) -> bool {
        self.available.contains(book_id)
            || self.lent.contains(book_id)
    }

    #[debug_requires(!self.book_exists(book_id), "Book IDs are unique")]
    #[debug_ensures(self.available.contains(book_id), "Book now available")]
    #[ensures(self.available.len() == old(self.available.len()) + 1)]
    #[ensures(self.lent.len() == old(self.lent.len()), "No lent change")]
    pub fn add_book(&mut self, book_id: &str) {
        self.available.insert(book_id.to_string());
    }

    #[debug_requires(self.book_exists(book_id))]
    #[ensures(ret -> self.available.len() == old(self.available.len()) - 1)]
    #[ensures(ret -> self.lent.len() == old(self.lent.len()) + 1)]
    #[debug_ensures(ret -> self.lent.contains(book_id))]
    #[debug_ensures(!ret -> self.lent.contains(book_id), "Book already lent")]
    pub fn lend(&mut self, book_id: &str) -> bool {
        if self.available.contains(book_id) {
            self.available.remove(book_id);
            self.lent.insert(book_id.to_string());
            true
        } else {
            false
        }
    }

    #[debug_requires(self.lent.contains(book_id), "Can't return a non-lent book")]
    #[ensures(self.lent.len() == old(self.lent.len()) - 1)]
    #[ensures(self.available.len() == old(self.available.len()) + 1)]
    #[debug_ensures(!self.lent.contains(book_id))]
    #[debug_ensures(self.available.contains(book_id), "Book available again")]
    pub fn return_book(&mut self, book_id: &str) {
        self.lent.remove(book_id);
        self.available.insert(book_id.to_string());
    }
}

属性

此crate公开了 requires、ensures 和 invariant 属性。

• requires 在函数/方法执行之前进行检查。
• ensures 在函数/方法运行完成后进行检查
• invariant 在函数/方法运行之前和之后都进行检查。

此外，所有这些属性都有不同“模式”的版本。请参阅下面的 模式部分。

对于 trait 和 trait impl，可以使用 contract_trait 属性。

更具体的信息可以在crate文档中找到。

伪函数和运算符

old() 函数

此crate提供的独特功能之一是 old() 伪函数，允许在函数调用之前使用参数的值进行检查。这仅适用于 ensures 属性。

#[ensures(*x == old(*x) + 1, "after the call `x` was incremented")]
fn incr(x: &mut usize) {
    *x += 1;
}

-> 运算符

对于更复杂的函数，使用逻辑蕴涵表达行为可能很有用。因为Rust没有蕴涵运算符，此crate为此目的添加了此运算符。

#[ensures(person_name.is_some() -> ret.contains(person_name.unwrap()))]
fn geeting(person_name: Option<&str>) -> String {
    let mut s = String::from("Hello");
    if let Some(name) = person_name {
        s.push(' ');
        s.push_str(name);
    }
    s.push('!');
    s
}

此运算符是右结合的。

注意：由于 syn 的设计，添加需要解析的自定义操作符比较棘手，因此这个crate通过重写 TokenStream 来实现。重写方法是将表达式分为两部分：一部分在 -> 操作符左侧，另一部分在右侧。这意味着 if a -> b { c } else { d } 不会生成预期的代码。可以通过使用括号或花括号进行显式分组来避免这种情况。

模式

所有属性（requires，ensures，invariant）都有 debug_* 和 test_* 版本。

• debug_requires/debug_ensures/debug_invariant 内部使用 debug_assert! 而不是 assert!

• test_requires/test_ensures/test_invariant 使用一个 if cfg!(test) 来保护 assert!。这通常用于表示与“慢但明显正确”的替代实现或检查的等价性。

  例如，一个归并排序的实现可能看起来像这样

  #[test_ensures(is_sorted(input))]
  fn merge_sort<T: Ord + Copy>(input: &mut [T]) {
      // ...
  }
  

设置

要安装最新版本，请将 contracts 添加到 Cargo.toml 文件的依赖项部分。

[dependencies]
contracts = "0.6.3"

然后，您可以通过在所有计划使用合约属性的文件中添加 use contracts::*; 来将所有过程宏引入作用域。

或者使用“旧式”导入宏，使它们在整个项目中可用。

#[macro_use]
extern crate contracts;

配置

此crate公开了一些功能标志，用于配置断言行为。

• disable_contracts - 禁用所有检查和断言。
• override_debug - 将所有合约（除 test_ 之外）更改为 debug_* 版本
• override_log - 如果条件违反，将所有合约（除 test_ 之外）更改为 log::error!() 调用。不会发生中止。
• mirai_assertions - 而不是常规的 assert! 样式宏，生成由 MIRAI 静态分析器使用的宏。有关此使用的更多文档，请参阅 MIRAI 仓库。

待办事项

• 为特质实现更多合约。
• 添加一个类似于SPARK的静态分析器，以在项目范围内使用合约进行静态断言。