3 ms·

So, with projects like this, once you've got the specification verified, how do you then make sure your implementation fits the specification?

skybrian 2y ago
I'm guessing it's the same way you ensure that your code implements a specification written in English. But at least you know the specification is consistent.
sriram_malhar 2y ago
Some projects make it possible for you to generate verified code from the specification. There is usefulness to these tools even if the implementation is a separate beast. At a minimum, they allow you to test drive your ideas in particularly thorny areas such as concurrency and security. Forcing you to think hard about a secure kernel or a library of data structures is a good thing in and of itself. You only have to give such core libraries this kind of anal attention, not to the layers built atop.
sirwhinesalot 2y ago
Some model checkers like CBMC annotate C code directly. Others can generate piles of tests. But usually just knowing your requirements are consistent and exactly how the algorithm has to behave to work as intended goes a long way!
bugarela 2y ago
If you have a specification that resembles your implementation well enough (which is not naturally the case, as keeping specifications on a higher level is almost always better, but can be done), you can use Model-Based Testing (MBT) techniques to increase confidence that your implementation matches the specification. For example, you can ask Quint to generate a bunch of traces (executions) for you in JSON and then parse those to run tests in the implementation. If your trace is [{action: deposit(10), result: ok}, {action: withdraw(20), result: Error}], you can have an sort of integration test for your implementation that asserts that calling deposit(10) should result in ok and then calling withdraw(20) subsequently should result in an error. There is one example for this as a Rust test: https://github.com/informalsystems/quint-sandbox/blob/main/SimpleBank/tests/bank_mbt.rs https://github.com/informalsystems/quint-sandbox/blob/main/S...
hwayne 2y ago
In addition to what everybody else is saying about the value of having a spec at all, there's a lot of exciting developments now in using a spec to generate a test suite, which is way simpler than using a spec to generate production code. Example: https://arxiv.org/abs/2006.00915 https://arxiv.org/abs/2006.00915

skybrian 2y ago

I'm guessing it's the same way you ensure that your code implements a specification written in English. But at least you know the specification is consistent.

sriram_malhar 2y ago

Some projects make it possible for you to generate verified code from the specification. There is usefulness to these tools even if the implementation is a separate beast. At a minimum, they allow you to test drive your ideas in particularly thorny areas such as concurrency and security. Forcing you to think hard about a secure kernel or a library of data structures is a good thing in and of itself. You only have to give such core libraries this kind of anal attention, not to the layers built atop.

sirwhinesalot 2y ago

Some model checkers like CBMC annotate C code directly. Others can generate piles of tests. But usually just knowing your requirements are consistent and exactly how the algorithm has to behave to work as intended goes a long way!

bugarela 2y ago

If you have a specification that resembles your implementation well enough (which is not naturally the case, as keeping specifications on a higher level is almost always better, but can be done), you can use Model-Based Testing (MBT) techniques to increase confidence that your implementation matches the specification. For example, you can ask Quint to generate a bunch of traces (executions) for you in JSON and then parse those to run tests in the implementation. If your trace is [{action: deposit(10), result: ok}, {action: withdraw(20), result: Error}], you can have an sort of integration test for your implementation that asserts that calling deposit(10) should result in ok and then calling withdraw(20) subsequently should result in an error. There is one example for this as a Rust test: https://github.com/informalsystems/quint-sandbox/blob/main/SimpleBank/tests/bank_mbt.rs https://github.com/informalsystems/quint-sandbox/blob/main/S...

hwayne 2y ago

In addition to what everybody else is saying about the value of having a spec at all, there's a lot of exciting developments now in using a spec to generate a test suite, which is way simpler than using a spec to generate production code. Example: https://arxiv.org/abs/2006.00915 https://arxiv.org/abs/2006.00915