Closed dbenn closed 5 months ago
A property based test revealed that a VeLa expression such as 42--4
yielded 42
since --4
was treated as a comment.
Given that #
and --
are both single-line comments, I decided to disallow --
for VeLa comments and just use #
. I changed example and test VeLa scripts that used --
to use #
.
There are a number of places where property-based testing could find hidden bugs in VStar, such as in VeLa and in calculations where invariants or post-conditions can be expressed as properties. Awhile ago I experimented with a few JUnit based property-based tests (PBTs) but dependencies would have required a lot of change to UTs and potentially incompatible licences.
There are a few PBT frameworks/libraries for Java including:
The first 3 are integrated with various versions of JUnit, later than we currently use.
https://github.com/quicktheories/QuickTheories is relatively simple and powerful (includes shrinking all Python hypothesis and some other libraries) DSL-style library under Apache 2.0, so I will start with that.