• Need to reason about residuals. Try Rustans axioms from krml178. Problem: need additional axioms like
    (forall a:int, b:int :: (((a%n)-b)%n==(a-b)%n));
    (forall a:int, b:int :: ((0==(a-b)%n && 0≤a && 0≤b && a<n && b<n) ⇒ a==b));
    to prove lemmas needed for invariance of transitions from A to B. But introduction of those axioms leads to divergence of Z3 on other lemmas needed for invariance of transitions from A to B.
    Solution: Use axioms that partially describe what a%n means for absolute values of a between -3n and 4n, since the proof does not require more.
  • Some lemmas need auxiliary forall statements. Solution: use call forall.
    Note: call forall allows writing manual induction. For example:
    procedure TwoPowerXIsPositive(a:int)
    requires 0≤a;
    ensures TwoPowerX(a)>0;
    {
      if(0<a) { call forall TwoPowerXIsPositive(a-1); }
    }
    procedure TwoPowerXIsMonotone(a:int,b:int)
    requires 0≤a && 0≤b && a<b;
    ensures TwoPowerX(a)<TwoPowerX(b);
    {
      if(a>0) { call forall TwoPowerXIsMonotone(a-1,b-1); }
      else { call forall TwoPowerXIsPositive(b-1); }
    }
  • Boogie program verifier, version 2011-03-17, finished in 1.7 seconds.
  • Boogie program verifier, version 2.2.30705.1126, distributed on 2012-10-22, refused to accept the reminder after division % syntactically. We changed % to Mod. This version finished in 1.03 seconds on an Intel® Core™ i5-3320M CPU clocked at 2.6 GHz with 8 GB DDR3 RAM clocked at 1600 MHz.