From fcdeb94c52f39f4fc8dd9dd97db627e81433f5b0 Mon Sep 17 00:00:00 2001 From: Maurice Scheffmacher Date: Fri, 16 Oct 2026 13:22:33 +0200 Subject: [PATCH 1/2] docs: correct specification examples and runtime guidance Extract standalone documentation improvements from #193. Co-authored-by: Slava Barinov --- crates/anodized/README.md | 15 +++++++++++---- crates/anodized/REFERENCE.md | 33 ++++++++++++++++++--------------- 2 files changed, 29 insertions(+), 19 deletions(-) diff --git a/crates/anodized/README.md b/crates/anodized/README.md index bdefd9fc..80dcb2de 100644 --- a/crates/anodized/README.md +++ b/crates/anodized/README.md @@ -80,18 +80,25 @@ fn percentage_10_over_0() { } ``` -Use the `anodized_panic` setting to instrument the code with runtime checks. +Use the `anodized_panic` setting to instrument the code with runtime checks. Add +`anodized_print` to have the failing condition named as well. ```bash -RUSTFLAGS="--cfg anodized_panic" cargo test +RUSTFLAGS="--cfg anodized_print --cfg anodized_panic" cargo test ``` -A spec violation will cause a panic with a descriptive error message: +A spec violation reports the condition, then panics: ```text -thread 'main' panicked at 'Precondition failed: part <= whole', src/main.rs:17:5 +precondition failed: part <= whole +precondition failed: whole > 0.0 +thread 'main' panicked at src/main.rs:3:1: +precondition failed ``` +Conditions are checked independently rather than short-circuiting, so every violated one is +reported before the panic. + For more details and other approaches, see [The Anodized Reference](https://github.com/anodized-rs/anodized/blob/main/crates/anodized/REFERENCE.md). ## Why Anodized diff --git a/crates/anodized/REFERENCE.md b/crates/anodized/REFERENCE.md index 4b86b22b..cdf098ac 100644 --- a/crates/anodized/REFERENCE.md +++ b/crates/anodized/REFERENCE.md @@ -32,7 +32,7 @@ RUSTFLAGS="--cfg anodized_print" cargo test Disable embedding the specs as Rust code. -**Important:** This has **no effect on runtime performance** because the embedded specs are always dead code. On the other hand, it **prevents syntax/type checking** specs, so it may decrease compilation time. +**Important:** Discarding specs removes their generated code and prevents syntax/type checking of their expressions. With no `anodized_*` flags, runtime checks are disabled, but `captures` expressions still execute alongside the function body: a `.clone()` in a capture still runs. The separate `anodized_embed_specs` mode embeds specifications without changing the function body. ### `anodized_embed_specs` @@ -78,7 +78,7 @@ Use `#[cfg]` attributes on individual conditions to control when checks run (see When runtime checks are enabled, use the standard `#[cfg]` attribute to select build configurations under which a condition is checked. ```rust, no_run -use anodized::{spec, types::Spec}; +use anodized::spec; #[spec( // Runtime checks only during `cargo test`. @@ -87,12 +87,12 @@ use anodized::{spec, types::Spec}; // Runtime checks only in debug builds (like `debug_assert!`) #[cfg(debug_assertions)] - ensures: output.is_ok(), + ensures: |ref output| output.is_ok(), )] fn perform_complex_operation(input: i32) -> Result { todo!() } ``` -The `#[cfg]` attribute follows standard Rust semantics: when the configuration predicate is false, the runtime check for the condition is completely omitted. +The `#[cfg]` attribute follows standard Rust semantics: when the configuration predicate is false, the runtime check for the condition is completely omitted. This holds in every build configuration that runs checks, whether or not `anodized_print` is enabled. **Important:** Anodized guarantees that each condition remains syntactically valid and type-correct regardless of its `#[cfg]` settings. This prevents conditions from becoming invalid between different build configurations, and keeps the entire spec always visible to analysis tools. @@ -135,7 +135,7 @@ use anodized::spec; // Invariant: length never exceeds capacity maintains: vec.len() <= vec.capacity(), )] -fn push_checked(vec: &mut Vec, value: T) { todo!() } +fn push_checked(vec: &mut Vec, value: T) { vec.push(value) } ``` ### `captures`: Capture Entry-Time Values @@ -146,6 +146,7 @@ Sometimes postconditions need to compare the function's final state with its ini use anodized::spec; #[spec( + requires: !items.is_empty(), captures: [ // Copy types: captured directly orig_len = items.len(), @@ -207,6 +208,7 @@ reconstructed. use anodized::spec; #[spec( + requires: input < i32::MAX - 1, // Bind the return value to `output` for the entire group of postconditions. ensures: |output| [ output > input, @@ -243,7 +245,7 @@ fn sort_pair(pair: (i32, i32)) -> (i32, i32) { todo!() } use anodized::spec; #[spec( - requires: *balance >= amount, + requires: amount >= 0 && *balance >= amount, maintains: *balance >= 0, captures: initial_balance = *balance, ensures: |(new_balance, receipt_amount)| [ @@ -252,7 +254,7 @@ use anodized::spec; *balance == new_balance, ], )] -fn withdraw(balance: &mut u64, amount: u64) -> (u64, u64) { todo!() } +fn withdraw(balance: &mut i64, amount: i64) -> (i64, i64) { todo!() } ``` ### Loop Specs @@ -270,9 +272,10 @@ Loop specs support the following fields: use anodized::spec; #[spec( - ensures: [ - seq.iter().any(|elem| elem == output), - seq.iter().all(|elem| elem <= output), + requires: !seq.is_empty(), + ensures: |output| [ + seq.iter().any(|elem| *elem == output), + seq.iter().all(|elem| *elem <= output), ], )] fn find_maximum(seq: &[u8]) -> u8 { @@ -298,10 +301,10 @@ use anodized::spec; #[spec( requires: seq.is_sorted(), - ensures: [ - *output <= seq.len(), - seq[0..*output].iter().all(|item| item < value), - seq[*output..].iter().all(|item| item >= value), + ensures: |output| [ + output <= seq.len(), + seq[0..output].iter().all(|item| item < value), + seq[output..].iter().all(|item| item >= value), ], )] fn find_insert_position(seq: &[T], value: &T) -> usize { @@ -343,6 +346,7 @@ trait MonotonicGenerator { fn current(&self) -> i32; #[spec( + requires: self.current() < i32::MAX, captures: old_val = self.current(), ensures: self.current() > old_val, )] @@ -407,7 +411,6 @@ use anodized::spec; Descending(vec) => vec.iter().rev().is_sorted(), } )] -#[allow(unused)] enum MonotonicVec { Ascending(Vec), Descending(Vec), From ed2975614b5d67ed269f54552550836d2fe48600 Mon Sep 17 00:00:00 2001 From: Maurice Scheffmacher Date: Sat, 17 Oct 2026 00:25:46 +0200 Subject: [PATCH 2/2] docs: simplify reference examples per review --- crates/anodized/REFERENCE.md | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/crates/anodized/REFERENCE.md b/crates/anodized/REFERENCE.md index cdf098ac..08f21ae0 100644 --- a/crates/anodized/REFERENCE.md +++ b/crates/anodized/REFERENCE.md @@ -87,7 +87,7 @@ use anodized::spec; // Runtime checks only in debug builds (like `debug_assert!`) #[cfg(debug_assertions)] - ensures: |ref output| output.is_ok(), + ensures: |output| output.is_ok(), )] fn perform_complex_operation(input: i32) -> Result { todo!() } ``` @@ -135,7 +135,7 @@ use anodized::spec; // Invariant: length never exceeds capacity maintains: vec.len() <= vec.capacity(), )] -fn push_checked(vec: &mut Vec, value: T) { vec.push(value) } +fn push_checked(vec: &mut Vec, value: T) { todo!() } ``` ### `captures`: Capture Entry-Time Values @@ -208,7 +208,6 @@ reconstructed. use anodized::spec; #[spec( - requires: input < i32::MAX - 1, // Bind the return value to `output` for the entire group of postconditions. ensures: |output| [ output > input, @@ -245,7 +244,7 @@ fn sort_pair(pair: (i32, i32)) -> (i32, i32) { todo!() } use anodized::spec; #[spec( - requires: amount >= 0 && *balance >= amount, + requires: *balance >= amount, maintains: *balance >= 0, captures: initial_balance = *balance, ensures: |(new_balance, receipt_amount)| [ @@ -254,7 +253,7 @@ use anodized::spec; *balance == new_balance, ], )] -fn withdraw(balance: &mut i64, amount: i64) -> (i64, i64) { todo!() } +fn withdraw(balance: &mut u64, amount: u64) -> (u64, u64) { todo!() } ``` ### Loop Specs