On Tue, 24 Feb 2015 10:47:19 -0800, Ali Ãehreli wrote: > Some implementation out there are buggy: > > > http://www.reddit.com/r/programming/comments/2wze7z/ proving_that_androids_javas_and_pythons_sorting/ > > Ali
their KeY system is very interesting. i'm very curious what minimal changes can be made for D to integrate something like it into the source code. i.e. turn all that pseudo-comment things that KeY is using into valid D code. compiler can check code semantics, so all contracts are at least syntactically correct. and then KeY-like tool can try to prove the correctness. we already has `in` and `out`, and `invariant` for structs/classes. i believe that `invariant` can be reused for other invariants (like loop invariant)... and it's interesting what complications templates can bring. testing templates is relatively hard now, 'cause programmer must ensure that every path is instantiated (i'm constantly hitting by the bugs in my templates due to missing some codepathes). sorry for derailing the thread.
signature.asc
Description: PGP signature
