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:

• ModularInteger
• RangeInteger
• Enumeration
• Message
• Refinement

Property-Based Test for Expression Parser

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

To be tested entities:

• TRUE
• FALSE
• And
• Or
• Add
• Mul
• Sub
• Div
• Number
• Variable
• Length
• First
• Last
• Aggregate
• Less
• LessEqual
• Equal
• GreaterEqual
• Greater
• 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.