A set of macros for design by contact in Rust. The design of this library was inspired by D's contract programming facilities. Here's a quick example:
use std::i32;
contract! {
fn add_one_to_odd(x: i32) -> i32 {
post(y) {
assert!(y - 1 == x, "reverse operation did not produce input");
}
body {
x + 1
}
pre {
assert!(x != i32::MAX, "cannot add one to input at max of number range");
assert!(x % 2 != 0, "evens ain't appropriate here");
}
}
}
assert!(add_one_to_odd(3) == 4);
assert!(add_one_to_odd(5) == 6);
assert_that!(add_one_to_odd(2), panics);
assert_that!(add_one_to_odd(i32::MAX), panics);
In the above example, pre
runs before body
, and post
, which has the
return value of this function bound to y
, runs after. We can also define
checks with the double_check
block, which will be checked before and
after body
has run:
struct Counter {
count: u32,
max: u32
}
contract! {
fn increment_counter(c: &mut Counter) -> () { // Unfortunately, the () return type is necessary for now (see issue #12)
double_check {
assert!(c.count <= c.max, "counter max has been exceeded");
}
body {
c.count += 1;
}
}
}
let mut counter = Counter { count: 0, max: 3 };
macro_rules! assert_incremented_eq {
($e: expr) => ({
increment_counter(&mut counter);
assert!(counter.count == $e, format!("expected counter to be {}, got {}", $e, counter.count));
})
}
assert_incremented_eq!(1);
assert_incremented_eq!(2);
assert_incremented_eq!(3);
assert_incremented_eq!(4); // panics!
When every contract block is being utilized, the order of the checks inserted into the contract definition are as follows:
pre
double_check
body
double_check
post
More examples can be found in:
- The examples directory
- The test suite for this library
This library is called "Adhesion" in reference to a particular type of contract called a "contract of adhesion", also known as a "take-it-or-leave-it" contract. Assertions in programming are definitely "take it or leave it" -- if an assertion is failing, you either have to fix the conditions of the assertion, or change the assertion itself. It sounded appropriate!
After the v0.2.0 release, @eternaleye pointed out in this Reddit thread
that technically an "invariant" connotes a strong guarantee that must be
rigorously maintained between ALL operations in code. This sort of guarantee is
NOT provided by the behavior D's invariant
block, as demonstrated by the
link that
@eternaleye provided.
Semantics are important, especially in systems that attempt to introduce more
rigor to software development like design by contract. For this reason, the
combined pre- and post-check block that D calls invariant
is called
double_check
in this library.
This project is dual-licensed under your choice of the MIT license or the Apache 2.0 license.
- Adhesion uses a modified version of components from the rust-parse-generics project. Both the original and modified versions here use the same dual license as this project.
- @ErichDonGubler, original author
- @dzamlo, for providing assistance with various important features.
- @DanielKeep, for his incredible help making it possible for generics to be parsed and used in macros generally, and for his mentoring during Adhesion's development of its features involving generics.
- @eternaleye, for bringing some security expertise to bear and motivating
the
double_check
divergence from D'sinvariant
.