Add property testing of denotational correctness of TinyRAM spec

Orbis-Tertius / osl

Apache License 2.0

2 stars 2 forks source link

Add property testing of denotational correctness of TinyRAM spec #15

Open morganthomas opened 2 years ago

morganthomas commented 2 years ago

Given a valid TinyRAM trace, check that it is in the denotation of the spec. Given an invalid TinyRAM trace, check that it is not in the denotation of the spec.