Attribute Macro contract

#[contract]

contract is a procedural macro that checks if a given invariant holds true before and after a method call. If the invariant does not hold, the macro will cause the program to panic with a specified message.

Arguments

• invariant: A struct method identifier that returns a boolean. This is the invariant that needs to be checked.
• check_time: An optional string literal that specifies when the invariant should be checked.
  • "require" - The invariant is checked before the operation.
  • "ensure" - The invariant is checked after the operation.
  • "require_and_ensure" - The invariant is checked both before and after the operation.

Example

use eiffel_macros_gen::contract;
 
struct MyClass {
    // Fields
    a: i32,
};

impl MyClass {
    fn my_invariant(&self) -> bool {
        // Your invariant checks here
        true
    }

    #[contract(my_invariant)]
    fn my_method(&self) {
        // Method body
        println!("Method body {:?}", self.a);
    }

    // Only check the invariant before the method call
    #[contract(my_invariant, "require")]
    fn my_other_method(&self) {
        // Method body
        println!("Method body {:?}", self.a);
    }

    // Only check the invariant after the method call
    #[contract(my_invariant, "ensure")]
    fn my_other_method_after(&self) {
        // Method body
        println!("Method body {:?}", self.a);
    }

    // Only check the invariant before and after (default)
    #[contract(my_invariant, "require_and_ensure")]
    fn my_other_method_before_and_after(&self) {
        // Method body
        println!("Method body {:?}", self.a);
    }

}       

Test

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_my_method() {
        let my_class = MyClass;
        my_class.my_method(); // This should not panic as the invariant is true
    }
}