What does HackerNews think of prusti-dev?
A static verifier for Rust, based on the Viper verification infrastructure.
Language:
Rust
#79
in
Rust
You might be interested in the Prusti project, which statically checks for absence of reachable panics, overflows etc. It also allows user-defined specifications such as pre and post-conditions, loop body invariants, termination checking and so on.
For contract-based programming, I'm personally planning on experimenting with Prusti: https://github.com/viperproject/prusti-dev
The withdraw example would look something like
impl Account {
#[requires(amount <= self.balance)]
#[ensures(self.balance >= 0)]
pub fn withdraw(&mut self, amount: uint) { ... }
}
You might be interested in Prusti: https://github.com/viperproject/prusti-dev
I am the main author of the tool. Vytautas has helped me get the Rust compiler integration set up :-)
The closer relation would be to Prusti [1] which is Vytautas' project on verifying Rust codebases. We use the same IR emitted by the Rust compiler.
There are some things that attempt to come close.
Prusti by ETH Zurich is maybe the closest.
https://github.com/viperproject/prusti-dev
https://www.pm.inf.ethz.ch/research/prusti.html
extern crate prusti_contracts;
use prusti_contracts::*;
#[requires(something)]
#[ensures(result >= a && result >= b)]
#[ensures(result == a || result == b)]
fn max(a: i32, b: i32) -> i32 {
if a > b {
a
} else {
b
}
}