CodePlexProject Hosting for Open Source Software

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