AdaCore / RecordFlux

Formal specification and generation of verifiable binary parsers, message generators and protocol state machines

Apache License 2.0

103 stars 6 forks source link

Property-based testing #229

Open treiher opened 4 years ago

treiher commented 4 years ago

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 commented 3 years ago

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.