You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: README.md
+14-13Lines changed: 14 additions & 13 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -25,7 +25,7 @@ anodized = "0.1.0"
25
25
26
26
**2. Add contracts to your functions.**
27
27
28
-
Use the `#[contract]` attribute to attach `requires` (precondition), `ensures` (postcondition), and `maintains` (invariant) _clauses_. Each clause contains a standard Rust expression that evaluates to `bool`, called a _predicate_. In an `ensures` clause, the function's return value is available as `output`.
28
+
Use the `#[contract]` attribute to attach `requires` (precondition), `ensures` (postcondition), and `maintains` (invariant) _clauses_. Each clause contains a standard Rust expression that evaluates to `bool`, called a _condition_. In an `ensures` clause, the function's return value is available as `output`.
29
29
30
30
```rust
31
31
useanodized::contract;
@@ -75,24 +75,25 @@ Anodized aims to support a wide spectrum of correctness tools, enabling you to c
75
75
76
76
The `#[contract]` attribute provides a powerful and ergonomic way to define contracts.
77
77
78
-
### Contracts, Clauses, and Predicates
78
+
### Contracts, Clauses, and Conditions
79
79
80
80
Contracts are built from three flavors of clauses:
81
81
82
-
-`requires: <predicate>`: Defines a **precondition**. This predicate must be true when the function is called.
82
+
-`requires: <condition>`: Defines a **precondition**. This condition must be true when the function is called.
83
83
84
-
-`ensures: <predicate>`: Defines a **postcondition**. This predicate must be true when the function returns.
84
+
-`ensures: <condition>`: Defines a **postcondition**. This condition must be true when the function returns.
85
85
86
-
-`maintains: <predicate>`: Defines an **invariant**. A convenience to add a predicate as both a pre- and a postcondition. It's most useful for expressing properties of `self` that a method must preserve.
86
+
-`maintains: <condition>`: Defines an **invariant**. A convenience to add a condition as both a pre- and a postcondition. It's most useful for expressing properties of `self` that a method must preserve.
87
87
88
-
A predicate is a `bool`-valued Rust expression; as simple as that. This is a non-trivial design choice, so its benefits are explained in the section below: [Why Predicates Are Rust Expressions](#why-predicates-are-rust-expressions).
88
+
A condition is a `bool`-valued Rust expression; as simple as that. This is a non-trivial design choice, so its benefits are explained in the section below: [Why Conditions Are Rust Expressions](#why-conditions-are-rust-expressions).
89
89
90
90
You can include zero, one, or many clauses of each flavor. In terms of meaning (semantics), multiple clauses of the same flavor are combined with a logical **AND** (`&&`).
91
91
92
92
```rust
93
93
#[contract(
94
+
// These two `requires` clauses are equivalent to one with `self.is_initialized && !self.is_locked`
94
95
requires: self.is_initialized,
95
-
requires:!self.is_locked,// equivalent to `self.is_initialized && !self.is_locked`
96
+
requires:!self.is_locked,
96
97
maintains: self.len() <= self.capacity(),
97
98
)]
98
99
fnpush(&mutself, value:T) { /* ... */ }
@@ -121,7 +122,7 @@ If the name `output` collides with an existing identifier, you can rename it in
121
122
fnincrement(old_value:i32) ->i32 { old_value+1 }
122
123
```
123
124
124
-
**2. Per-Clause Override**: Use a closure-style syntax on a specific `ensures` clause. This has the highest precedence and only affects that single clause.
125
+
**2. Per-Clause Override**: Use a closure-style syntax in a specific `ensures` clause. This has the highest precedence and only affects that single clause.
**3. Multiple Overrides**: When used together, the per-clause override always takes precedence for its specific clause, while other clauses fall back to the global override.
137
138
138
139
```rust
139
-
// A function where 'output' is an argument name, requiring a global override.
140
+
// A function where 'output' is an argument name, requiring overrides.
A core design principle of Anodized is that a predicate is written as a **standard Rust expression** that evaluates to `bool`. This is a deliberate choice that provides key benefits over using a custom language.
154
+
A core design principle of Anodized is that a condition is written as a **standard Rust expression** that evaluates to `bool`. This is a deliberate choice that provides key benefits over using a custom language.
154
155
155
-
-**The Language You Already Know**: No need to learn yet another language to write the contract predicates. Write them in the one you already know: standard Rust. Call functions, macros (like `matches!`), or write `if` and `match` expressions, and so on. As long as it all evaluates to a `bool`, you're good to go.
156
+
-**The Language You Already Know**: No need to learn yet another language to write the contract conditions. Write them in the one you already know: standard Rust. Call functions, macros (like `matches!`), or write `if` and `match` expressions, and so on. As long as it all evaluates to a `bool`, you're good to go.
156
157
157
-
-**An Integral Part of Your Code**: Contract predicates aren't special comments or strings; they are real Rust expressions, fully integrated with your code. The Rust compiler checks every predicate for syntax and type errors, just like any other part of your code. If you misspell a variable, compare incompatible types, or make any other mistake, you'll get a familiar compiler error pointing directly to the predicate that needs fixing.
158
+
-**An Integral Part of Your Code**: Contract conditions aren't special comments or strings; they are real Rust expressions, fully integrated with your code. The Rust compiler checks every condition for syntax and type errors, just like any other part of your code. If you misspell a variable, compare incompatible types, or make any other mistake, you'll get a familiar compiler error pointing directly to the condition that needs fixing.
0 commit comments