mirror of https://codeberg.org/topola/topola.git
138 lines
3.1 KiB
Rust
138 lines
3.1 KiB
Rust
/* This Source Code Form is subject to the terms of the Mozilla Public
|
|
* License, v. 2.0. If a copy of the MPL was not distributed with this
|
|
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */
|
|
|
|
//! Testing of methods and `impl`-blocks.
|
|
|
|
use contracts::*;
|
|
|
|
#[cfg(feature = "mirai_assertions")]
|
|
mod mirai_assertion_mocks;
|
|
|
|
#[test]
|
|
fn methods() {
|
|
fn is_even(x: usize) -> bool {
|
|
x % 2 == 0
|
|
}
|
|
|
|
struct EvenAdder {
|
|
count: usize,
|
|
}
|
|
|
|
impl EvenAdder {
|
|
#[invariant(is_even(self.count))]
|
|
#[ensures(self.count == old(self.count) + 2)]
|
|
fn next_even(&mut self) {
|
|
self.count += 2;
|
|
}
|
|
|
|
// Manually express the invariant in terms of `ret` since `self.count` is mutably borrowed.
|
|
#[requires(is_even(self.count))]
|
|
#[ensures(is_even(*ret))]
|
|
#[ensures(*ret == old(self.count) + 2)]
|
|
fn next_even_and_get<'a>(&'a mut self) -> &'a mut usize {
|
|
self.count += 2;
|
|
&mut self.count
|
|
}
|
|
|
|
#[invariant(is_even(self.count))]
|
|
#[requires(self.count >= 2)]
|
|
#[ensures(self.count == old(self.count) - 2)]
|
|
fn prev_even(&mut self) {
|
|
self.count -= 2;
|
|
}
|
|
|
|
#[invariant(is_even(self.count))]
|
|
fn this_var_collision(&mut self) -> usize {
|
|
#[allow(unused_variables)]
|
|
let (this, this__) = (42, 42);
|
|
self.count
|
|
}
|
|
}
|
|
|
|
let mut adder = EvenAdder { count: 0 };
|
|
|
|
adder.next_even();
|
|
adder.next_even();
|
|
|
|
adder.prev_even();
|
|
adder.prev_even();
|
|
|
|
assert_eq!(*adder.next_even_and_get(), 2);
|
|
}
|
|
|
|
#[test]
|
|
fn impl_invariant() {
|
|
fn is_even(x: usize) -> bool {
|
|
x % 2 == 0
|
|
}
|
|
|
|
struct EvenAdder {
|
|
count: usize,
|
|
}
|
|
|
|
#[invariant(is_even(self.count), "Count has to always be even")]
|
|
impl EvenAdder {
|
|
const fn step() -> usize {
|
|
2
|
|
}
|
|
|
|
fn new() -> Self {
|
|
EvenAdder { count: 0 }
|
|
}
|
|
|
|
#[ensures(self.count == old(self.count) + 2)]
|
|
fn next_even(&mut self) {
|
|
self.count += Self::step();
|
|
}
|
|
|
|
#[requires(self.count >= 2)]
|
|
#[ensures(self.count == old(self.count) - 2)]
|
|
fn prev_even(&mut self) {
|
|
self.count -= Self::step();
|
|
}
|
|
}
|
|
|
|
let mut adder = EvenAdder::new();
|
|
|
|
adder.next_even();
|
|
adder.next_even();
|
|
|
|
adder.prev_even();
|
|
adder.prev_even();
|
|
}
|
|
|
|
#[test]
|
|
fn test_self_macro_hygiene() {
|
|
struct S {
|
|
value: i32,
|
|
}
|
|
|
|
// Use a macro to generate the function impl
|
|
// This requires strict hygiene of the `self` receiver
|
|
macro_rules! __impl {
|
|
(
|
|
$(#[$metas:meta])*
|
|
fn $function:ident(&mut $this:ident, $value:ident: $ty:ty)
|
|
$body:block
|
|
) => {
|
|
$(#[$metas])*
|
|
fn $function(&mut $this, $value: $ty)
|
|
$body
|
|
};
|
|
}
|
|
|
|
impl S {
|
|
__impl! {
|
|
#[ensures(self.value == old(value))]
|
|
fn set_value(&mut self, value: i32) {
|
|
self.value = value;
|
|
}
|
|
}
|
|
}
|
|
|
|
let mut s = S { value: 24 };
|
|
s.set_value(42);
|
|
assert_eq!(s.value, 42);
|
|
}
|