Interesting! I am curious how it develops. Another option (addon) would be to use commented invariants like in SPARK which are tested against the code by an au

Interesting! I am curious how it develops. Another option (addon) would be to use commented invariants like in SPARK which are tested against the code by an automatic verification system even before compile time. To get an impression what it means, please read: http://www.adacore.com/home/products/sparkpro/tokeneer/discovery/lesson_contracts/ http://www.adacore.com/home/products/sparkpro/tokeneer/disco...