5 ms·
I believe I've read about some languages with invariant using them at compile time to verify the value meets the invariant, if possible. For example, let's say
by jjice 4y ago
I believe I've read about some languages with invariant using them at compile time to verify the value meets the invariant, if possible. For example, let's say a function's invariant guarantees it returns an even integer, and then we pass that into a function that only accepts odd negative integers, it could catch that during compile time. To me, that's the coolest case for invariants.
Again, I believe that this is a PL research topic, but I'm not super well versed in it, so take that with a grain of salt.
- JonChesterfield 4y agoRequires dependent types. And yeah, research is probably a fair characterisation.
- henrikeh 4y agoAda / SPARK can do that. Ada has had some form of that analyses since the first version from 1983. https://learn.adacore.com/courses/intro-to-spark/chapters/03_Proof_Of_Program_Integrity.html#contracts https://learn.adacore.com/courses/intro-to-spark/chapters/03...