small usability improvement: distinguish invariants in errors

Author: mkovaxx

src/lib.rs

@@ -159,17 +159,21 @@ fn instrument_body(func: &ItemFn, args: &ContractArgs) -> Result<proc_macro2::To
 
     // --- Generate Precondition Checks ---
     let preconditions = args.conditions.iter().filter_map(|c| match c {
-        Condition::Requires { predicate } | Condition::Maintains { predicate } => {
+        Condition::Requires { predicate } => {
             let msg = format!("Precondition failed: {}", predicate.to_token_stream());
             Some(quote! { assert!(#predicate, #msg); })
         }
+        Condition::Maintains { predicate } => {
+            let msg = format!("Pre-invariant failed: {}", predicate.to_token_stream());
+            Some(quote! { assert!(#predicate, #msg); })
+        }
         _ => None,
     });
 
     // --- Generate Postcondition Checks ---
     let postconditions = args.conditions.iter().filter_map(|c| match c {
         Condition::Maintains { predicate } => {
-            let msg = format!("Postcondition failed: {}", predicate.to_token_stream());
+            let msg = format!("Post-invariant failed: {}", predicate.to_token_stream());
             Some(quote! { assert!(#predicate, #msg); })
         }
         Condition::Ensures { predicate } => {

tests/method_with_invariant.rs

@@ -25,11 +25,21 @@ fn test_increment_success() {
 }
 
 #[test]
-#[should_panic(expected = "Postcondition failed: self.count <= self.capacity")]
+#[should_panic(expected = "Post-invariant failed: self.count <= self.capacity")]
 fn test_increment_violates_invariant() {
     let mut c = Counter {
         count: 10,
         capacity: 10,
     };
     c.increment(); // This will make count 11, violating the invariant on exit.
 }
+
+#[test]
+#[should_panic(expected = "Pre-invariant failed: self.count <= self.capacity")]
+fn test_increment_violates_pre_invariant() {
+    let mut c = Counter {
+        count: 11,
+        capacity: 10, // count > capacity, violates pre-invariant
+    };
+    c.increment();
+}