Assumptions weaken properties
16 hours ago
- Property/test strength is defined through logical implication: a stronger property guarantees a weaker one.
- Adding assumptions to a specification always makes the resulting property weaker, formalized as Prop => (Assumption => Prop).
- Systems with fewer assumptions are more robust and work in a broader set of cases (e.g., a Unicode JSON parser vs. an ASCII-only one).
- Three common reasons to rely on assumptions: the strong property is impossible, too costly, or too difficult to verify directly.
- Most assumptions concern external 'exoprogram' factors (environment, hardware, user input), making their verification a distinct and often harder challenge than verifying system logic.