3 ms·

> the checks could be run-time or disabled overall, enabled just for testing If you do not require proofs, how is that different from C-like asserts and unit t

• krcz 8y ago
  you could have mix of assertions and proofs, obtaining something that you could call gradual verification - you wouldn't have to prove everything from axioms, you could base on assertions. the difference from asserts and unit testing is that you could match post-contract from one function with pre-contract of another one, as in: fun sort(l: List[Int]): SortedList[Int] fun minusReverse(l: SortedList[Int]): SortedList[Int] = l.map(el => -el) fun f(l: List[Int]): SortedList[Int] = minusReverse(sort(l)) when you have sort and minusReverse functions unit-tested, you could use proof system to prove that f is correct (assuming that sort and minusReverse are). while looking for similar concepts in existing programming languages I have found that SPARK 2014 [1] (subset of Ada 2012 with static verification) follows such philosophy: you can prove some parts of the code and unit test the rest. [1] https://www.adacore.com/about-spark https://www.adacore.com/about-spark [2] http://docs.adacore.com/spark2014-docs/html/lrm/introduction.html#combining-formal-verification-and-testing http://docs.adacore.com/spark2014-docs/html/lrm/introduction...