Property-based testing

[treiher]

Basis: Hypothesis

Property-Based Test for Model Parser

• Generate model
• Convert to specification
• Parse specification
• Compare models

To be tested entities:

• [x] ModularInteger
• [x] RangeInteger
• [x] Enumeration
• [x] Message
• [x] Refinement

Property-Based Test for Expression Parser

• Generate expression
• Convert to specification
• Parse specification
• Compare expressions

To be tested entities:

• [x] TRUE
• [x] FALSE
• [x] And
• [x] Or
• [x] Add
• [x] Mul
• [x] Sub
• [x] Div
• [x] Number
• [x] Variable
• [x] Length
• [x] First
• [x] Last
• [x] Aggregate
• [x] Less
• [x] LessEqual
• [x] Equal
• [x] GreaterEqual
• [x] Greater
• [x] NotEqual

Property-Based Test for SPARK Code Generator

• Generate model
• Generate SPARK code
• Compile generated code
• Prove generated code

Property-Based Test for Expression Conversion (RecordFlux ⇿ Ada)

• [ ] Complete tested expressions

Found Issues

#298, #305, #309, #310, #311, #312, #313, #314, #315, #316, #317, #319, #320

[treiher]

It is now possible to integrate icontract with Hypothesis: icontract-hypothesis. The most interesting part is the automatic inference of Hypothesis strategies based on contracts, i.e. test cases for a function can be generated automatically based on its preconditions.