What Does Dafny Know?

Mar 13, 2014 at 1:43 AM
How can we know what Dafny knows? i.e., is this specified somewhere? e.g., commented section below not known to Dafny.

Can I teach the commented theorem to Dafny, for example?

method WhatDafnyKnows(s: int, r: int, t: int)
{
//assert g != 0 && a % g == 0 && b % g == 0 ==> (a + b) % g == 0;
assert s * (t + r) == s * t + s * r;
}