4 ms·
Try playing with Why3. http://why3.lri.fr/ http://why3.lri.fr/ It's slightly idiosyncratic, and it has its own programming language that is ML-like. But it allo
by tomsmeding 5y ago
Try playing with Why3. http://why3.lri.fr/ http://why3.lri.fr/ It's slightly idiosyncratic, and it has its own programming language that is ML-like. But it allows you to write arbitrary code in that language, and then prove statements about that code using SMT solvers as helpers. I haven't used it in practice yet, just played with an example, but it felt quite powerful if you get to know its capabilities.
- dwohnitmok 5y agoI haven't used Why3, but I have used other SMT solver-based frameworks such as Dafny and TLAPS for TLA+ and they all seem focused on proving function behavior, rather than function runtime or memory usage. I suspect there's a way to encode runtime and memory usage theorems, but I don't have a clear conception of the best way of doing so without polluting function definitions.