4 ms·
If you want a small stepping stone toward Versus, you can add Rust debug_assert for preconditions and postconditions; the Rust compiler strips these out of prod
by jph 2y ago
If you want a small stepping stone toward Versus, you can add Rust debug_assert for preconditions and postconditions; the Rust compiler strips these out of production builds by default.
Example from the Versus tutorial with verification:
fn octuple(x1: i8) -> (x8: i8)
requires
-16 <= x1,
x1 < 16,
ensures
x8 == 8 * x1,
{
let x2 = x1 + x1;
let x4 = x2 + x2;
x4 + x4
}
Example using debug_assert with runtime checks:
fn octuple(x1: i8) -> i8 {
debug_assert(-16 <= x1);
debug_assert(x1 < 16);
let x2 = x1 + x1;
let x4 = x2 + x2;
let x8 = x4 + x4;
debug_assert(x8 == 8 * x1);
x8
}
- diarrhea 2y agoI wish more people used asserts like that. Such a wonderful tool for documentation. It complements the type system and testing really well.
- zozbot234 2y agoOne issue with the existing Verus syntax is that it requires wrapping the whole code in a proc-macro. Other Rust proof/verification/DbC tools such as Creusot use attribute-based syntax instead, which generally seems to be a bit more lightweight and idiomatic for Rust. Hopefully it will become available in future Verus releases.
- lkrubner 2y agoYour Versus example is how I write my Clojure code, with post and pre conditions on most of the functions. And the JVM has a flag that makes it easy to strip that out for production builds.
- thesuperbigfrog 2y agoYou could also try the "contracts" crate: https://docs.rs/contracts/latest/contracts/ https://docs.rs/contracts/latest/contracts/
- nextaccountic 2y agoand you can use MIRAI, that takes the contracts defined by this crate and check them at compile time or, use prusti, that has contracts with a similar syntax checked at compile time as well