0
# Contract System
1
2
CrossHair's contract system enables contract-based programming and verification through preconditions and postconditions. It supports multiple contract formats and provides enforcement mechanisms for runtime validation.
3
4
## Capabilities
5
6
### Contract Registration
7
8
Register contracts for functions to enable verification and enforcement.
9
10
```python { .api }
11
def register_contract(fn, *, pre=None, post=None, sig=None, skip_body=True):
12
"""
13
Register contract for function.
14
15
Parameters:
16
- fn: Function to register contract for
17
- pre: Optional precondition function that takes same args as fn
18
- post: Optional postcondition function that takes fn args plus result
19
- sig: Optional function signature or list of signatures
20
- skip_body: Whether to skip function body during analysis (default True)
21
22
Returns:
23
True if registration successful, False otherwise
24
25
Registers preconditions and postconditions for a function, enabling
26
CrossHair to verify the contracts during symbolic execution.
27
"""
28
29
def clear_contract_registrations():
30
"""
31
Clear all registered contracts.
32
33
Removes all previously registered contracts, useful for testing
34
or when dynamically changing contract configurations.
35
"""
36
37
def get_contract(fn):
38
"""
39
Get contract for function.
40
41
Parameters:
42
- fn: Function to get contract for
43
44
Returns:
45
ContractOverride instance if contract exists, None otherwise
46
47
Retrieves the registered contract information for a function,
48
including preconditions, postconditions, and signature overrides.
49
"""
50
51
def register_modules(*modules):
52
"""
53
Register contracts from modules.
54
55
Parameters:
56
- *modules: Module objects to scan for contract annotations
57
58
Automatically discovers and registers contracts from modules that
59
use supported contract annotation formats (PEP316, icontract, etc.).
60
"""
61
```
62
63
**Usage Examples:**
64
65
```python
66
from crosshair.register_contract import register_contract, clear_contract_registrations
67
68
def sqrt_precondition(x):
69
"""Precondition: input must be non-negative"""
70
return x >= 0
71
72
def sqrt_postcondition(x, result):
73
"""Postcondition: result squared should approximately equal input"""
74
return abs(result * result - x) < 1e-10
75
76
import math
77
78
# Register contract for math.sqrt
79
register_contract(
80
math.sqrt,
81
pre=sqrt_precondition,
82
post=sqrt_postcondition
83
)
84
85
# Clear all contracts when done
86
clear_contract_registrations()
87
```
88
89
### Contract Enforcement
90
91
Runtime enforcement of contracts with specialized exception types.
92
93
```python { .api }
94
class PreconditionFailed(BaseException):
95
"""
96
Exception for precondition failures.
97
98
Raised when a function is called with arguments that violate
99
the registered precondition. Inherits from BaseException to
100
avoid being caught by general exception handlers.
101
"""
102
103
class PostconditionFailed(BaseException):
104
"""
105
Exception for postcondition failures.
106
107
Raised when a function returns a value that violates the
108
registered postcondition. Inherits from BaseException to
109
ensure contract violations are not silently ignored.
110
"""
111
112
class EnforcedConditions:
113
"""
114
Module for enforcing conditions during execution.
115
116
Provides tracing and enforcement mechanisms to ensure contracts
117
are checked at runtime, with proper exception handling and
118
reporting of contract violations.
119
"""
120
121
def WithEnforcement(fn):
122
"""
123
Ensure conditions are enforced on callable.
124
125
Parameters:
126
- fn: Function to enforce conditions on
127
128
Returns:
129
Wrapped function that checks contracts on every call
130
131
Decorator that enables runtime contract checking for a function,
132
raising PreconditionFailed or PostconditionFailed when contracts
133
are violated.
134
"""
135
```
136
137
**Usage Examples:**
138
139
```python
140
from crosshair.enforce import WithEnforcement, PreconditionFailed, PostconditionFailed
141
142
@WithEnforcement
143
def divide(a: float, b: float) -> float:
144
"""
145
pre: b != 0
146
post: __return__ == a / b
147
"""
148
return a / b
149
150
try:
151
result = divide(10.0, 0.0) # Will raise PreconditionFailed
152
except PreconditionFailed as e:
153
print(f"Precondition violation: {e}")
154
155
try:
156
# Hypothetical function with buggy implementation
157
result = buggy_divide(10.0, 2.0) # Might raise PostconditionFailed
158
except PostconditionFailed as e:
159
print(f"Postcondition violation: {e}")
160
```
161
162
### Contract Annotation Formats
163
164
Support for multiple contract specification formats used in the Python ecosystem.
165
166
**PEP 316 Style (Docstring Contracts):**
167
168
```python
169
def factorial(n: int) -> int:
170
"""
171
Calculate factorial of n.
172
173
pre: n >= 0
174
post: __return__ >= 1
175
post: n == 0 or __return__ == n * factorial(n - 1)
176
"""
177
if n == 0:
178
return 1
179
return n * factorial(n - 1)
180
```
181
182
**icontract Library Integration:**
183
184
```python
185
import icontract
186
187
@icontract.require(lambda x: x >= 0)
188
@icontract.ensure(lambda result: result >= 1)
189
@icontract.ensure(lambda x, result: x == 0 or result == x * factorial(x - 1))
190
def factorial(x: int) -> int:
191
if x == 0:
192
return 1
193
return x * factorial(x - 1)
194
```
195
196
**deal Library Integration:**
197
198
```python
199
import deal
200
201
@deal.pre(lambda x: x >= 0)
202
@deal.post(lambda result: result >= 1)
203
def factorial(x: int) -> int:
204
if x == 0:
205
return 1
206
return x * factorial(x - 1)
207
```
208
209
### Contract Verification Workflow
210
211
Complete workflow for contract verification and analysis.
212
213
```python { .api }
214
class ContractOverride:
215
"""
216
Container for contract override information.
217
218
Stores preconditions, postconditions, signature information,
219
and other metadata needed for contract verification during
220
symbolic execution.
221
"""
222
223
class AnalysisMessage:
224
"""
225
Message reporting analysis results.
226
227
Contains information about contract verification results,
228
including counterexamples, error details, and execution
229
context for failed contracts.
230
"""
231
232
def run_checkables(fn_info, options):
233
"""
234
Run contract checking on function.
235
236
Parameters:
237
- fn_info: FunctionInfo containing function metadata
238
- options: AnalysisOptions configuration
239
240
Returns:
241
Generator of AnalysisMessage results
242
243
Performs symbolic execution to verify contracts, yielding
244
messages for each contract verification attempt.
245
"""
246
```
247
248
**Advanced Contract Registration Example:**
249
250
```python
251
from crosshair.register_contract import register_contract
252
from inspect import Signature, Parameter
253
254
def complex_precondition(data, threshold, options=None):
255
"""Complex precondition with multiple parameters"""
256
if not isinstance(data, list):
257
return False
258
if len(data) == 0:
259
return False
260
if threshold <= 0:
261
return False
262
return True
263
264
def complex_postcondition(data, threshold, options, result):
265
"""Complex postcondition checking result properties"""
266
if result is None:
267
return False
268
if not isinstance(result, dict):
269
return False
270
return 'processed_count' in result
271
272
# Create custom signature for overloaded function
273
custom_sig = Signature([
274
Parameter('data', Parameter.POSITIONAL_OR_KEYWORD, annotation=list),
275
Parameter('threshold', Parameter.POSITIONAL_OR_KEYWORD, annotation=float),
276
Parameter('options', Parameter.KEYWORD_ONLY, default=None, annotation=dict)
277
])
278
279
register_contract(
280
complex_data_processor,
281
pre=complex_precondition,
282
post=complex_postcondition,
283
sig=custom_sig,
284
skip_body=False # Analyze function body as well
285
)
286
```
287
288
### Contract Analysis Results
289
290
Understanding and interpreting contract verification results.
291
292
```python { .api }
293
class MessageType(enum.Enum):
294
"""
295
Types of analysis messages from contract verification.
296
297
- CONFIRMED: Contract violation confirmed with counterexample
298
- CANNOT_CONFIRM: Unable to find violation within time limits
299
- PRE_UNSAT: Precondition is unsatisfiable (always false)
300
- POST_FAIL: Postcondition fails with satisfiable precondition
301
- POST_ERR: Error occurred while checking postcondition
302
- EXEC_ERR: Error occurred during function execution
303
- SYNTAX_ERR: Syntax error in contract specification
304
- IMPORT_ERR: Error importing required modules
305
"""
306
CONFIRMED = "confirmed"
307
CANNOT_CONFIRM = "cannot_confirm"
308
PRE_UNSAT = "pre_unsat"
309
POST_FAIL = "post_fail"
310
POST_ERR = "post_err"
311
EXEC_ERR = "exec_err"
312
SYNTAX_ERR = "syntax_err"
313
IMPORT_ERR = "import_err"
314
```
315
316
**Interpreting Analysis Results:**
317
318
```python
319
from crosshair.core_and_libs import run_checkables
320
from crosshair.options import AnalysisOptions
321
322
options = AnalysisOptions()
323
324
for message in run_checkables(function_info, options):
325
if message.message_type == MessageType.CONFIRMED:
326
print(f"Contract violation found: {message.message}")
327
print(f"Counterexample: {message.test_fn}")
328
elif message.message_type == MessageType.CANNOT_CONFIRM:
329
print(f"No violation found within time limit")
330
elif message.message_type == MessageType.PRE_UNSAT:
331
print(f"Precondition is unsatisfiable: {message.message}")
332
```
333
334
### Contract Testing Integration
335
336
Integration with testing frameworks for contract-based testing.
337
338
**Generating Contract Tests:**
339
340
```python
341
# CrossHair can generate tests that verify contracts
342
def test_contract_compliance():
343
"""Generated test ensuring contract compliance"""
344
# Test case that satisfies preconditions
345
result = sqrt(4.0)
346
# Verify postcondition manually
347
assert abs(result * result - 4.0) < 1e-10
348
```
349
350
**Property-Based Testing Integration:**
351
352
```python
353
from hypothesis import given, strategies as st
354
355
@given(st.floats(min_value=0.0, max_value=1000.0))
356
def test_sqrt_contract(x):
357
"""Property-based test for sqrt contract"""
358
try:
359
result = sqrt(x)
360
# Verify postcondition holds
361
assert abs(result * result - x) < 1e-10
362
except PreconditionFailed:
363
# This should not happen with valid inputs
364
assert False, f"Precondition failed for valid input {x}"
365
```