4 ms·
Such runtime asserts[1] are so conceptually simple though -- have enough language constructs to express invariants in the right places, and let the compiler ins
by Dewie3 11y ago
Such runtime asserts[1] are so conceptually simple though -- have enough language constructs to express invariants in the right places, and let the compiler insert asserts in all places where they would be needed. And then perhaps also have pragmas for turning off asserts for more performant but less secure builds of the code. Maybe with custom granularity for what asserts to turn off.
It's too bad that more mainstream languages don't have things like this (except for vanilla `assert` I guess). I would prefer this to something like built in unit tests.
[1] I'm assuming you are not talking about static verification, which I guess would use Spark?
- david-given 11y agoAda's contract stuff is a bit more sophisticated than a simple assertion. You can, for example, do this: procedure increment(v: in out integer) with post => v /= v'old ... (/= is Ada's not-equal-to operator.) This enforces as a postcondition that the value of v must have changed. You can even refer to the old versions of arrays. Plus, the run-time type checking required by more complex type expressions are augmented by compile-time checking. If the compiler can deduce that a conversion will always be correct, it won't emit a check. If it can deduce that it will always be wrong, it'll error out at compile time. It all works really rather well. The only trouble I have with preconditions and postconditions is that you have to declare them in your module's interface, which is public, rather than in the module's implementation, which isn't. So you can only test your module's public interface. If your module doesn't expose a state variable to the outside world, you can't use it in a precondition or postcondition. I find that a very odd design decision.