Since a lot of programming is math, a lot of code proofs involve mathematical proofs. Dafny uses Z3 to prove things, and Z3 knows a lot about math, so often Dafny will just "get" a lot of mathematical assertions you make. But sometimes you may write something that seems obvious that Dafny can't prove. In this case, it's useful to include one or more of the files from Libraries/Math and invoke one of the many fundamental mathematical theorems we've already found a way to convince Dafny of. For instance, if you want to use the fact that x * (y + z) == (x * y) + (x * z) , then you can just invoke
lemma_mul_is_distributive_add(x, y, z);

Last edited Oct 15, 2014 at 12:09 AM by howell, version 3

Comments

No comments yet.