@@ -72,12 +72,12 @@ $(H2 $(LNAME2 pre_post_contracts, Pre and Post Contracts))
72
72
73
73
$(P The expression form is:)
74
74
------
75
- in(expression)
76
- in(expression, "failure string")
77
- out(identifier; expression)
78
- out(identifier; expression, "failure string")
79
- out(; expression)
80
- out(; expression, "failure string")
75
+ in (expression)
76
+ in (expression, "failure string")
77
+ out (identifier; expression)
78
+ out (identifier; expression, "failure string")
79
+ out (; expression)
80
+ out (; expression, "failure string")
81
81
{
82
82
...function body...
83
83
}
131
131
132
132
------
133
133
int fun(ref int a, int b)
134
- in (a > 0)
135
- in (b >= 0, "b cannot be negative!")
136
- out(r; r > 0, "return must be positive")
137
- out(; a != 0)
134
+ in (a > 0)
135
+ in (b >= 0, "b cannot be negative!")
136
+ out (r; r > 0, "return must be positive")
137
+ out (; a != 0)
138
138
{
139
139
// function body
140
140
}
145
145
assert(a > 0);
146
146
assert(b >= 0, "b cannot be negative!");
147
147
}
148
- out(r)
148
+ out (r)
149
149
{
150
150
assert(r > 0, "return must be positive");
151
151
assert(a != 0);
@@ -219,8 +219,8 @@ class Date
219
219
)
220
220
221
221
------
222
- invariant(1 <= day && day <= 31);
223
- invariant(0 <= hour && hour < 24, "hour out of bounds");
222
+ invariant (1 <= day && day <= 31);
223
+ invariant (0 <= hour && hour < 24, "hour out of bounds");
224
224
------
225
225
226
226
$(P The invariant is a contract saying that the `assert`s must hold true.
0 commit comments