Skip to content

Commit 273bff6

Browse files
raj-jain-awsraj-jain-aws
authored
Property Based Testing Extension (awslabs#119)
1 parent 6eb6c25 commit 273bff6

2 files changed

Lines changed: 303 additions & 0 deletions

File tree

‎aidlc-rules/aws-aidlc-rule-details/extensions/testing/property-based/property-based-testing.md‎

Lines changed: 284 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,284 @@
1+
# Property-Based Testing Rules
2+
3+
## Overview
4+
5+
These property-based testing (PBT) rules are cross-cutting constraints that apply across applicable AI-DLC phases. They ensure that code with identifiable properties is tested using property-based techniques, complementing (not replacing) traditional example-based tests.
6+
7+
Property-based testing defines invariants that must hold for all valid inputs, then uses a framework to generate random inputs and search for counterexamples. When a failure is found, the framework shrinks the input to a minimal reproducing case. This approach uncovers edge cases and subtle bugs that example-based testing routinely misses.
8+
9+
**Enforcement**: At each applicable stage, the model MUST verify compliance with these rules before presenting the stage completion message to the user.
10+
11+
### Blocking PBT Finding Behavior
12+
13+
A **blocking PBT finding** means:
14+
1. The finding MUST be listed in the stage completion message under a "PBT Findings" section with the PBT rule ID and description
15+
2. The stage MUST NOT present the "Continue to Next Stage" option until all blocking findings are resolved
16+
3. The model MUST present only the "Request Changes" option with a clear explanation of what needs to change
17+
4. The finding MUST be logged in `aidlc-docs/audit.md` with the PBT rule ID, description, and stage context
18+
19+
If a PBT rule is not applicable to the current project or unit (e.g., PBT-06 when no stateful components exist), mark it as **N/A** in the compliance summary — this is not a blocking finding.
20+
21+
### Default Enforcement
22+
23+
All rules in this document are **blocking** by default. If any rule's verification criteria are not met, it is a blocking PBT finding — follow the blocking finding behavior defined above.
24+
25+
### Partial Enforcement Mode
26+
27+
If the user selected **Partial** enforcement during opt-in, only rules PBT-02, PBT-03, PBT-07, PBT-08, and PBT-09 are enforced. All other rules are treated as advisory (non-blocking). Log the enforcement mode in `aidlc-docs/aidlc-state.md` under `## Extension Configuration`.
28+
29+
### Verification Criteria Format
30+
31+
Verification items in this document are plain bullet points describing compliance checks. Each item should be evaluated as compliant or non-compliant during review.
32+
33+
---
34+
35+
## Rule PBT-01: Property Identification During Design
36+
37+
**Rule**: Every unit containing business logic, data transformations, or algorithmic operations MUST be analyzed for testable properties during the Functional Design stage. The analysis MUST identify which of the following property categories apply:
38+
39+
| Category | Description | Example |
40+
|---|---|---|
41+
| Round-trip | An operation paired with its inverse yields the original value | serialize → deserialize = identity |
42+
| Invariant | A transformation preserves some measurable characteristic | sort preserves collection size and elements |
43+
| Idempotence | Applying an operation twice yields the same result as once | dedup(dedup(list)) = dedup(list) |
44+
| Commutativity | Different operation orderings produce the same result | add(a, b) = add(b, a) |
45+
| Oracle | A reference implementation or simplified model can verify results | optimized algorithm vs brute-force |
46+
| Induction | A property proven for smaller inputs extends to larger ones | recursive structures, divide-and-conquer |
47+
| Easy verification | The result is hard to compute but easy to check | maze solver output can be walked to verify |
48+
49+
The identified properties MUST be documented in the functional design artifacts for the unit, and carried forward into code generation as PBT test requirements.
50+
51+
**Verification**:
52+
- Functional design artifacts include a "Testable Properties" section listing identified properties per component
53+
- Each identified property references one of the categories above
54+
- Components with no identifiable properties are explicitly marked as "No PBT properties identified" with a brief rationale
55+
- The property list is referenced during code generation planning
56+
57+
---
58+
59+
## Rule PBT-02: Round-Trip Properties
60+
61+
**Rule**: Any operation that has a logical inverse MUST have a property-based test verifying the round-trip. This includes but is not limited to:
62+
- Serialization / deserialization (JSON, XML, Protobuf, binary formats)
63+
- Encoding / decoding (Base64, URL encoding, compression)
64+
- Parsing / formatting (date parsing, number formatting, template rendering with structured input)
65+
- Encryption / decryption (where key is available)
66+
- Database write / read (for the data transformation layer, not the I/O itself)
67+
- Any pair of functions where `f_inverse(f(x)) = x` for all valid `x`
68+
69+
The property-based test MUST generate random valid inputs using a domain-appropriate generator (see PBT-07) and assert that the round-trip produces a value equal to the original input.
70+
71+
**Verification**:
72+
- Every serialization/deserialization pair has a round-trip property test
73+
- Every encoding/decoding pair has a round-trip property test
74+
- Every parsing/formatting pair has a round-trip property test (or documents why the transformation is lossy)
75+
- Round-trip tests use generated inputs, not hardcoded examples
76+
- Lossy transformations (e.g., float formatting with precision loss) document the acceptable deviation and test within tolerance
77+
78+
---
79+
80+
## Rule PBT-03: Invariant Properties
81+
82+
**Rule**: Functions with documented invariants MUST have property-based tests verifying those invariants hold across generated inputs. Common invariants include:
83+
- **Size preservation**: output collection has the same size as input (e.g., map, sort)
84+
- **Element preservation**: output contains exactly the same elements as input, possibly reordered (e.g., sort, shuffle)
85+
- **Ordering guarantees**: output satisfies an ordering constraint (e.g., sort produces non-decreasing order)
86+
- **Range constraints**: output values fall within a defined range (e.g., normalize produces values in [0, 1])
87+
- **Type preservation**: output type matches expected type for all valid inputs
88+
- **Business rule invariants**: domain-specific rules that must always hold (e.g., "account balance never goes negative after a valid transaction", "discount never exceeds item price")
89+
90+
**Verification**:
91+
- Each documented invariant has a corresponding property-based test
92+
- Invariant tests generate a wide range of inputs including boundary values
93+
- Business rule invariants identified in functional design are covered by PBT
94+
- Invariant tests do not duplicate exact assertions from example-based tests — they test the general rule, not specific cases
95+
96+
---
97+
98+
## Rule PBT-04: Idempotency Properties
99+
100+
**Rule**: Any operation that claims or requires idempotency MUST have a property-based test proving it. The test MUST verify that `f(f(x)) = f(x)` for all valid generated inputs. This applies to:
101+
- API endpoints documented as idempotent (PUT, DELETE)
102+
- Data normalization or sanitization functions
103+
- Cache population operations
104+
- Deduplication logic
105+
- Configuration application (applying config twice should not change state)
106+
- Message processing in at-least-once delivery systems
107+
108+
**Verification**:
109+
- Every operation documented as idempotent has a PBT asserting `f(f(x)) = f(x)`
110+
- Idempotency tests use domain-appropriate generators (not just primitives)
111+
- For stateful operations, the test verifies observable state equivalence after single vs repeated application
112+
113+
---
114+
115+
## Rule PBT-05: Oracle and Model-Based Testing
116+
117+
**Rule**: When a reference implementation, simplified model, or known-correct algorithm exists, property-based tests MUST compare the system under test against the oracle. This applies to:
118+
- Optimized algorithms replacing a known brute-force version
119+
- Refactored code replacing legacy implementations
120+
- Parallel/concurrent implementations compared against sequential versions
121+
- Custom implementations of well-known algorithms (sorting, searching, graph traversal)
122+
- New query engines compared against a reference database
123+
124+
The property-based test MUST generate random valid inputs and assert that the system under test produces equivalent results to the oracle for all generated inputs.
125+
126+
**Verification**:
127+
- When a reference implementation exists (or can be trivially written), an oracle PBT is present
128+
- Oracle tests generate diverse inputs covering normal, boundary, and adversarial cases
129+
- Equivalence is defined precisely (exact equality, structural equality, or documented tolerance)
130+
- If no oracle exists, this rule is marked N/A with rationale
131+
132+
---
133+
134+
## Rule PBT-06: Stateful Property Testing
135+
136+
**Rule**: Components that manage mutable state MUST be evaluated for stateful property testing. Stateful PBT generates random sequences of commands (operations) against the system and verifies that invariants hold after each step. This applies to:
137+
- In-memory caches and data stores
138+
- State machines and workflow engines
139+
- Queue and buffer implementations
140+
- Session management systems
141+
- Shopping carts, order pipelines, and similar stateful business objects
142+
- Any component where the result of an operation depends on prior operations
143+
144+
Stateful PBT MUST:
145+
- Define a simplified model (reference state) that mirrors the system under test
146+
- Generate random sequences of valid commands (add, remove, update, query, etc.)
147+
- Execute each command against both the real system and the model
148+
- Assert that observable state or query results match between system and model after each command
149+
- Test sequences of varying lengths, including empty sequences
150+
151+
**Verification**:
152+
- Stateful components identified in functional design have stateful PBT or document why it is not applicable
153+
- A simplified model is defined for comparison
154+
- Command generators produce valid operation sequences with realistic parameter distributions
155+
- Invariants are checked after each command in the sequence, not just at the end
156+
- If no stateful components exist, this rule is marked N/A
157+
158+
---
159+
160+
## Rule PBT-07: Generator Quality
161+
162+
**Rule**: Property-based tests MUST use domain-specific generators that produce realistic, structured inputs — not just primitive types. Poor generators (e.g., random strings for email fields, unbounded integers for age fields) produce meaningless test cases and miss real bugs.
163+
164+
Generator requirements:
165+
- **Domain types**: Custom generators MUST be created for domain objects (e.g., User, Order, Transaction) that respect business constraints (valid email format, positive amounts, valid date ranges)
166+
- **Constrained primitives**: Numeric generators MUST be constrained to realistic ranges where the domain requires it
167+
- **Structured data**: Generators for complex inputs (nested objects, lists of domain objects) MUST produce structurally valid data
168+
- **Edge case inclusion**: Generators SHOULD be configured to include boundary values (empty collections, zero, maximum values, Unicode strings) alongside normal values
169+
- **Reusability**: Domain generators SHOULD be defined as reusable test utilities, not duplicated across test files
170+
171+
**Verification**:
172+
- No PBT uses only raw primitive generators (e.g., `st.integers()` alone) for domain-typed parameters
173+
- Custom generators exist for domain objects used in PBT
174+
- Generators respect documented business constraints (e.g., positive amounts, valid formats)
175+
- Generator definitions are centralized and reusable where multiple tests share the same domain types
176+
177+
---
178+
179+
## Rule PBT-08: Shrinking and Reproducibility
180+
181+
**Rule**: All property-based tests MUST support shrinking and deterministic reproducibility.
182+
183+
- **Shrinking**: When a property fails, the PBT framework MUST automatically reduce the failing input to a minimal reproducing case. Tests MUST NOT disable or bypass the framework's shrinking mechanism unless there is a documented technical reason (e.g., shrinking is incompatible with external service calls in integration tests).
184+
- **Reproducibility**: Every PBT run MUST be reproducible via a seed value. The seed MUST be logged on failure so that the exact failing scenario can be replayed. CI configurations MUST either use a fixed seed for deterministic runs or log the random seed on every run for post-failure reproduction.
185+
- **CI integration**: PBT MUST be included in the project's CI pipeline. Flaky PBT failures (tests that pass on retry without code changes) MUST be investigated, not suppressed.
186+
187+
**Verification**:
188+
- PBT framework's shrinking is enabled (not overridden or disabled)
189+
- Test output on failure includes the seed value and the shrunk minimal failing input
190+
- CI configuration logs the seed for every PBT run or uses a fixed seed
191+
- No PBT is excluded from CI without documented justification
192+
- Flaky PBT failures are tracked and investigated, not silently retried
193+
194+
---
195+
196+
## Rule PBT-09: Framework Selection
197+
198+
**Rule**: The project MUST select and configure an appropriate property-based testing framework for its primary language(s). The framework MUST support:
199+
- Custom generators / strategies for domain types
200+
- Automatic shrinking of failing cases
201+
- Seed-based reproducibility
202+
- Integration with the project's existing test runner
203+
204+
Recommended frameworks by language (non-exhaustive):
205+
206+
| Language | Framework | Notes |
207+
|---|---|---|
208+
| Python | Hypothesis | Mature, excellent shrinking, Django integration |
209+
| JavaScript / TypeScript | fast-check | Integrates with Jest, Vitest, Mocha |
210+
| Java | jqwik | JUnit 5 integration, stateful testing support |
211+
| Kotlin | Kotest Property Testing | Kotest framework integration |
212+
| Scala | ScalaCheck | SBT integration, widely adopted |
213+
| Rust | proptest | Macro-based, good shrinking |
214+
| Go | rapid | Lightweight, idiomatic Go |
215+
| Haskell | QuickCheck | The original PBT framework |
216+
| C# / .NET | FsCheck | Works with xUnit, NUnit |
217+
| Erlang / Elixir | PropEr / StreamData | OTP-aware, stateful testing |
218+
219+
The selected framework MUST be documented in the tech stack decisions and included as a project dependency.
220+
221+
**Verification**:
222+
- A PBT framework is selected and documented in tech stack decisions
223+
- The framework is included in project dependencies (package.json, pom.xml, requirements.txt, etc.)
224+
- The framework supports custom generators, shrinking, and seed-based reproducibility
225+
- If the project uses multiple languages, each language with PBT-applicable code has a framework selected
226+
227+
---
228+
229+
## Rule PBT-10: Complementary Testing Strategy
230+
231+
**Rule**: Property-based tests MUST complement, not replace, example-based tests. The two approaches serve different purposes:
232+
233+
- **Example-based tests**: Document specific known scenarios, regression cases, and business-critical edge cases with explicit expected values. They serve as executable documentation of concrete behavior.
234+
- **Property-based tests**: Verify general invariants across a wide input space. They find unknown edge cases and validate that properties hold universally.
235+
236+
Requirements:
237+
- Critical business scenarios identified in user stories or requirements MUST have explicit example-based tests, even if a PBT covers the same property
238+
- PBT MUST NOT be the sole test for any business-critical path — at least one example-based test must pin the expected behavior for key scenarios
239+
- When a PBT discovers a failing case, the shrunk minimal example SHOULD be added as a permanent example-based regression test
240+
- Test documentation MUST clearly distinguish between example-based and property-based tests (separate test files, test classes, or clearly named test functions)
241+
242+
**Verification**:
243+
- Business-critical paths have both example-based and property-based tests
244+
- PBT is not used as the only test coverage for any critical feature
245+
- Test files or test classes clearly separate or label PBT vs example-based tests
246+
- Regression tests from PBT-discovered failures are captured as permanent example-based tests
247+
248+
---
249+
250+
## Enforcement Integration
251+
252+
These rules are cross-cutting constraints that apply to the following AI-DLC stages:
253+
254+
| Stage | Applicable Rules | Enforcement |
255+
|---|---|---|
256+
| Functional Design | PBT-01 | Property identification must appear in design artifacts |
257+
| NFR Requirements | PBT-09 | Framework selection must be included in tech stack decisions |
258+
| Code Generation (Planning) | PBT-01 through PBT-10 | Code generation plan must include PBT test steps for identified properties |
259+
| Code Generation (Generation) | PBT-02 through PBT-08, PBT-10 | Generated tests must include PBT alongside example-based tests |
260+
| Build and Test | PBT-08 | Test execution instructions must include PBT with seed logging and CI integration |
261+
262+
At each applicable stage:
263+
- Evaluate all PBT rule verification criteria against the artifacts produced
264+
- Include a "PBT Compliance" section in the stage completion summary listing each rule as compliant, non-compliant, or N/A
265+
- If any rule is non-compliant, this is a blocking PBT finding — follow the blocking finding behavior defined in the Overview
266+
- Include PBT rule references in design documentation and test instructions
267+
268+
---
269+
270+
## Appendix: Property Category Quick Reference
271+
272+
For developers and AI models identifying properties during Functional Design (PBT-01):
273+
274+
| Pattern Name | Formal Term | Test Shape | When to Use |
275+
|---|---|---|---|
276+
| There and back again | Invertible function | `f_inv(f(x)) == x` | Serialization, encoding, parsing |
277+
| Some things never change | Invariant | `measure(f(x)) == measure(x)` | Sort, map, filter, transform |
278+
| The more things change, the more they stay the same | Idempotence | `f(f(x)) == f(x)` | Normalization, dedup, cache writes |
279+
| Different paths, same destination | Commutativity | `f(g(x)) == g(f(x))` | Arithmetic, set operations, independent transforms |
280+
| Solve a smaller problem first | Structural induction | Property on `x` implies property on `x + element` | Recursive structures, lists, trees |
281+
| Hard to prove, easy to verify | Verification | `verify(solve(x)) == true` | Solvers, optimizers, search algorithms |
282+
| The test oracle | Reference comparison | `f(x) == oracle(x)` | Optimized vs brute-force, refactored vs legacy |
283+
284+
Source: Property category taxonomy adapted from Scott Wlaschin's "Choosing properties for property-based testing" ([fsharpforfunandprofit.com](https://fsharpforfunandprofit.com/posts/property-based-testing-2/)).

‎aidlc-rules/aws-aidlc-rule-details/extensions/testing/property-based/property-based-testing.opt-in.md‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
# Property-Based Testing — Opt-In
2+
3+
**Extension**: Property-Based Testing
4+
5+
## Opt-In Prompt
6+
7+
The following question is automatically included in the Requirements Analysis clarifying questions when this extension is loaded:
8+
9+
```markdown
10+
## Question: Property-Based Testing Extension
11+
Should property-based testing (PBT) rules be enforced for this project?
12+
13+
A) Yes — enforce all PBT rules as blocking constraints (recommended for projects with business logic, data transformations, serialization, or stateful components)
14+
B) Partial — enforce PBT rules only for pure functions and serialization round-trips (suitable for projects with limited algorithmic complexity)
15+
C) No — skip all PBT rules (suitable for simple CRUD applications, UI-only projects, or thin integration layers with no significant business logic)
16+
X) Other (please describe after [Answer]: tag below)
17+
18+
[Answer]:
19+
```

0 commit comments

Comments
 (0)