Dafny: compile quantifiers

Dafny: allow {:induction} attribute to take an explicit list of bound variables on which to apply induction
Dafny: split expressions when proving function postconditions
Boogie and BVD: updated copyright year ranges

1 files changed, 27 insertions, 0 deletions

diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index 982683b9..f32cc85a 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -218,4 +218,31 @@ namespace Dafny
       this.Cdr = b;

     }

   }

+  public partial class Helpers {

+    public static bool QuantBool(bool frall, System.Predicate<bool> pred) {

+      if (frall) {

+        return pred(false) && pred(true);

+      } else {

+        return pred(false) || pred(true);

+      }

+    }

+    public static bool QuantInt(BigInteger lo, BigInteger hi, bool frall, System.Predicate<BigInteger> pred) {

+      for (BigInteger i = lo; i < hi; i++) {

+        if (pred(i) != frall) { return !frall; }

+      }

+      return frall;

+    }

+    public static bool QuantSet<T>(Dafny.Set<T> set, bool frall, System.Predicate<T> pred) {

+      foreach (var t in set.Elements) {

+        if (pred(t) != frall) { return !frall; }

+      }

+      return frall;

+    }

+    public static bool QuantSeq<T>(Dafny.Sequence<T> seq, bool frall, System.Predicate<T> pred) {

+      foreach (var t in seq.Elements) {

+        if (pred(t) != frall) { return !frall; }

+      }

+      return frall;

+    }

+  }

 }