let mut b = Bar { f1: 0, f2: 10 };
baz(&mut b);
b.f2 = 100;
baz(&mut b);
b.f2 = -5;
// task '<main>' failed at 'invariant entering baz (x.f1 < x.f2)'
// baz(&mut b);
}
Design by contract style assertions for Rust
Simple Rust support for design by contract-style assertions. Supports * preconditions (
precond), * postconditions (
postcond), * invariants (pre and post) (
invariant).
Each macro takes a predicate given as a string parameter. Each macro is available in a
debug_version which only checks the assertion in debug builds, they should be zero overhead in non-debug builds. You can use
resultinside a postcondition to get the value returned by the function.
Preconditions are checked on entry to a function. Postconditions are checked when leaving the function by any path.
(The library is named for Tony, not Graydon. Or rather it is named for the logic which was named after Tony).
You can use libhoare with Cargo by adding
[dependencies.hoare] git = "https://github.com/nick29581/libhoare.git"
to your projects Cargo manifest.
Otherwise, download this repo, build it (see build instructions below), make sure the path to the compiled libhoare is on your library path in some way (one way of doing this is to
export LD_LIBRARY_PATH=/path/to/libhoare/objbefore building).
Then (whether or not you used Cargo), in your crate you will need the following boilerplate:
#![feature(plugin, custom_attribute)]#![plugin(hoare)]
Then you can use the macros as shown below.
#[precond="x > 0"] #[postcond="result > 1"] fn foo(x: int) -> int { let y = 45 / x; y + 1 }struct Bar { f1: int, f2: int }
#[invariant="x.f1 < x.f2"] fn baz(x: &mut Bar) { x.f1 += 10; x.f2 += 10; }
fn main() { foo(12); foo(26); // task '
' failed at 'precondition of foo (x > 0)' // foo(-3); let mut b = Bar { f1: 0, f2: 10 }; baz(&mut b); b.f2 = 100; baz(&mut b); b.f2 = -5; // task '<main>' failed at 'invariant entering baz (x.f1 < x.f2)' // baz(&mut b);
}
You can use contracts on methods as well as functions, but they are not as well tested.
All the code for checking conditions is in
libhoare. Currently, there is only a single file,
lib.rs.
The
testdirectory contains unit tests for the library.
The
egdirectory contains a few examples of how to use the library:
To build libhoare from the top level of your checked out repo run
cargo build
(if using cargo) or
$RUSTC ./libhoare/lib.rs
This will create libhoare.rs in the current directory, you might want to specify an output file using
-o.
To build the examples run
eg.shin the top level and to run the tests run
tests.sh. Both of these assume that you have a sibling directory called
objand that you used
$RUSTC ./libhoare/lib.rs -o "../obj/libhoare.so"
to build libhoare. Examples are created in
../obj
Wish list:
[#invariant="..."]to a struct, enum, etc. and the invariant would be checked on entering and leaving every method defined in any impl for the object).