There are a few more interesting options here. For example, take a look at Section 4 of “Using lightweight formal methods to validate a key-value storage node in Amazon S3”. From 4.1:
To check that the implementation satisfies the reference model specification, we use property-based testing, which generates inputs to a test case and checks that a user-provided property holds when that test is run.
and
We frame this check as a property-based test that takes as input a sequence of operations drawn from an alphabet we define. For each operation in the sequence, the test case applies the operation to both reference model and implementation, compares the output of each for equivalence, and then checks invariants that relate the two systems.
This approach allows using the specification directly as a “test driver” for property-based testing (when combined with deterministic simulation, a systems testing approach that’s exploding in popularity right now).
Another approach is to look at is the one taken by languages like Dafny (https://dafny.org/), where the language generates the implementation in a way that ensures that it refines the specification. Dafny can generate code in languages like Java and Go, and the Dafny language isn’t particularly esoteric itself. Code level tools like Kani (https://github.com/model-checking/kani) also provide a solution to this divergence problem, again by bringing the specification and code together.
There’s some cool work going on into completely different approaches to this too, but the ones I know of are as-yet unpublished so I can’t talk about them.
This approach allows using the specification directly as a “test driver” for property-based testing (when combined with deterministic simulation, a systems testing approach that’s exploding in popularity right now).
This is the approach that I have a lot of stock in at the moment. First, most people don’t need proof their system works, so that puts us into the testing realm. Testing for properties is still way more powerful than creating examples, so it sits somewhere in between that and proof.
But specifically in terms of specification, what I also like about this approach is that you get an executable specification. This begins to have value outside of testing - for example, instead of spinning up an entire end-to-end environment to see how the application behaves, you can just “ask” the model by running it with your inputs.
Finally, writing an executable model helps with writing the spec itself, since lots of people struggle to come up with abstract properties of their system.
executable specification. This begins to have value outside of testing - for example, instead of spinning up an entire end-to-end environment to see how the application behaves, you can just “ask” the model by running it with your inputs.
This doesn’t work for all domains, but sometimes it can be useful to ask: can the model be the implementation? For example, a model typically doesn’t persist data to stable storage, so a power cycle would erase all data, but if you journal all inputs (aka command sourcing) you get persistence.
There are a few more interesting options here. For example, take a look at Section 4 of “Using lightweight formal methods to validate a key-value storage node in Amazon S3”. From 4.1:
and
This approach allows using the specification directly as a “test driver” for property-based testing (when combined with deterministic simulation, a systems testing approach that’s exploding in popularity right now).
Another approach is to look at is the one taken by languages like Dafny (https://dafny.org/), where the language generates the implementation in a way that ensures that it refines the specification. Dafny can generate code in languages like Java and Go, and the Dafny language isn’t particularly esoteric itself. Code level tools like Kani (https://github.com/model-checking/kani) also provide a solution to this divergence problem, again by bringing the specification and code together.
There’s some cool work going on into completely different approaches to this too, but the ones I know of are as-yet unpublished so I can’t talk about them.
This is the approach that I have a lot of stock in at the moment. First, most people don’t need proof their system works, so that puts us into the testing realm. Testing for properties is still way more powerful than creating examples, so it sits somewhere in between that and proof.
But specifically in terms of specification, what I also like about this approach is that you get an executable specification. This begins to have value outside of testing - for example, instead of spinning up an entire end-to-end environment to see how the application behaves, you can just “ask” the model by running it with your inputs.
Finally, writing an executable model helps with writing the spec itself, since lots of people struggle to come up with abstract properties of their system.
This doesn’t work for all domains, but sometimes it can be useful to ask: can the model be the implementation? For example, a model typically doesn’t persist data to stable storage, so a power cycle would erase all data, but if you journal all inputs (aka command sourcing) you get persistence.