diff options
author | rustanleino <unknown> | 2011-03-26 01:58:19 +0000 |
---|---|---|
committer | rustanleino <unknown> | 2011-03-26 01:58:19 +0000 |
commit | c16176d2993c2df6b8b1b136c28a76cac3165b57 (patch) | |
tree | e9d4aacde97bece06d720bebcfaea7a1ab9f1e84 /Binaries/DafnyRuntime.cs | |
parent | 6eb6941181eeffa85828eca3a1effa33f72628b5 (diff) |
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
Diffstat (limited to 'Binaries/DafnyRuntime.cs')
-rw-r--r-- | Binaries/DafnyRuntime.cs | 27 |
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;
+ }
+ }
}
|