verification of loop invariant

Feb 8, 2016 at 3:16 PM
We are trying to write a program that verifies matrix multiplication using dafny,
we can't understand why it won't verify our code and why the invariant won't hold.
here is the link to our code : http://rise4fun.com/Dafny/Bztr
Thanks!
Feb 10, 2016 at 10:37 AM
Edited Feb 13, 2016 at 11:14 AM
I put an answer on stackoverflow http://stackoverflow.com/a/35313508/72810

The stackoverflow question got deleted so here is the answer on my blog: http://www.lexicalscope.com/blog/2016/02/13/dafny-matrix-mutiplication/