diff options
| author |  chmaria <unknown> | 2012-06-05 11:26:39 +0200 |
|---|---|---|
| committer | chmaria <unknown> | 2012-06-05 11:26:39 +0200 |
| commit | c2178326f725a39d825b4b2d25e0a30519d7055e (patch) | |
| tree | ed29c11a98bc11064d6160c265e28ada22219a53 | |
| parent | 8f7fdc817875de6ba2a68f853c970b7d841d38e2 (diff) | |
Dafny: Added runtime checking tests.
| -rw-r--r-- | Test/dafnyRuntimeChecking/Answer | 3624 | ||||
| -rw-r--r-- | Test/dafnyRuntimeChecking/AssertStmt0.dfy | 4 | ||||
| -rw-r--r-- | Test/dafnyRuntimeChecking/AssertStmt1.dfy | 4 | ||||
| -rw-r--r-- | Test/dafnyRuntimeChecking/AssumeStmt0.dfy | 4 | ||||
| -rw-r--r-- | Test/dafnyRuntimeChecking/AssumeStmt1.dfy | 4 | ||||
| -rw-r--r-- | Test/dafnyRuntimeChecking/Precondition0.dfy | 3 | ||||
| -rw-r--r-- | Test/dafnyRuntimeChecking/Precondition1.dfy | 9 | ||||
| -rw-r--r-- | Test/dafnyRuntimeChecking/runtest.bat | 15 | ||||
| -rw-r--r-- | Test/dafnytests.txt | 15 |
9 files changed, 3675 insertions, 7 deletions
diff --git a/Test/dafnyRuntimeChecking/Answer b/Test/dafnyRuntimeChecking/Answer new file mode 100644 index 00000000..900a0dca --- /dev/null +++ b/Test/dafnyRuntimeChecking/Answer @@ -0,0 +1,3624 @@ +
+-------------------- AssumeStmt0 --------------------
+
+Dafny program verifier finished with 2 verified, 0 errors
+Compiled program written to AssumeStmt0.cs
+Compiled assembly into AssumeStmt0.exe
+Rewrote assembly into AssumeStmt0.exe
+// Dafny program AssumeStmt0.dfy compiled into C#
+
+using System.Diagnostics.Contracts;
+using System.Numerics;
+using System.Collections.Generic;
+
+namespace Dafny
+{
+ public class Set<T>
+ {
+ Dictionary<T, bool> dict;
+ public Set() { }
+ Set(Dictionary<T, bool> d) {
+ dict = d;
+ }
+ public static Set<T> Empty {
+ get {
+ return new Set<T>(new Dictionary<T, bool>(0));
+ }
+ }
+ public static Set<T> FromElements(params T[] values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>(values.Length);
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+ public static Set<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>();
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+
+ public IEnumerable<T> Elements {
+ get {
+ return dict.Keys;
+ }
+ }
+ public bool Equals(Set<T> other) {
+ return dict.Count == other.dict.Count && IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is Set<T> && Equals((Set<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(Set<T> other) {
+ return dict.Count < other.dict.Count && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(Set<T> other) {
+ if (other.dict.Count < dict.Count)
+ return false;
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(Set<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(Set<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(Set<T> other) {
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public Set<T> Union(Set<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ Dictionary<T, bool> r = new Dictionary<T, bool>();
+ foreach (T t in b.Keys)
+ r[t] = true;
+ foreach (T t in a.Keys)
+ r[t] = true;
+ return new Set<T>(r);
+ }
+ public Set<T> Intersect(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ var r = new Dictionary<T, bool>();
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public Set<T> Difference(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, bool>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public T Choose() {
+ foreach (T t in dict.Keys) {
+ // return the first one
+ return t;
+ }
+ return default(T);
+ }
+ }
+ public class MultiSet<T>
+ {
+ Dictionary<T, int> dict;
+ public MultiSet() { }
+ MultiSet(Dictionary<T, int> d) {
+ dict = d;
+ }
+ public static MultiSet<T> Empty {
+ get {
+ return new MultiSet<T>(new Dictionary<T, int>(0));
+ }
+ }
+ public static MultiSet<T> FromElements(params T[] values) {
+ Dictionary<T, int> d = new Dictionary<T, int>(values.Length);
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSeq(Sequence<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSet(Set<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ d[t] = 1;
+ }
+ return new MultiSet<T>(d);
+ }
+
+ public bool Equals(MultiSet<T> other) {
+ return other.IsSubsetOf(this) && this.IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is MultiSet<T> && Equals((MultiSet<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(MultiSet<T> other) {
+ return !Equals(other) && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t])
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(MultiSet<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(MultiSet<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t))
+ return false;
+ }
+ foreach (T t in other.dict.Keys) {
+ if (dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public MultiSet<T> Union(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + dict[t];
+ }
+ foreach (T t in other.dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + other.dict[t];
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Intersect(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t)) {
+ r.Add(t, other.dict[t] < dict[t] ? other.dict[t] : dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Difference(MultiSet<T> other) { // \result == this - other
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t)) {
+ r.Add(t, dict[t]);
+ } else if (other.dict[t] < dict[t]) {
+ r.Add(t, dict[t] - other.dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public IEnumerable<T> Elements {
+ get {
+ List<T> l = new List<T>();
+ foreach (T t in dict.Keys) {
+ int n;
+ dict.TryGetValue(t, out n);
+ for (int i = 0; i < n; i ++) {
+ l.Add(t);
+ }
+ }
+ return l;
+ }
+ }
+ }
+
+ public class Map<U, V>
+ {
+ Dictionary<U, V> dict;
+ public Map() { }
+ Map(Dictionary<U, V> d) {
+ dict = d;
+ }
+ public static Map<U, V> Empty {
+ get {
+ return new Map<U, V>(new Dictionary<U,V>());
+ }
+ }
+ public static Map<U, V> FromElements(params Pair<U, V>[] values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Length);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public static Map<U, V> FromCollection(List<Pair<U, V>> values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Count);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public bool Equals(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ V v1, v2;
+ if (!dict.TryGetValue(u, out v1)) {
+ return false; // this shouldn't happen
+ }
+ if (!other.dict.TryGetValue(u, out v2)) {
+ return false; // other dictionary does not contain this element
+ }
+ if (!v1.Equals(v2)) {
+ return false;
+ }
+ }
+ foreach (U u in other.dict.Keys) {
+ if (!dict.ContainsKey(u)) {
+ return false; // this shouldn't happen
+ }
+ }
+ return true;
+ }
+ public override bool Equals(object other) {
+ return other is Map<U, V> && Equals((Map<U, V>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsDisjointFrom(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ if (other.dict.ContainsKey(u))
+ return false;
+ }
+ foreach (U u in other.dict.Keys) {
+ if (dict.ContainsKey(u))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(U u) {
+ return dict.ContainsKey(u);
+ }
+ public V Select(U index) {
+ return dict[index];
+ }
+ public Map<U, V> Update(U index, V val) {
+ Dictionary<U, V> d = new Dictionary<U, V>(dict);
+ d[index] = val;
+ return new Map<U, V>(d);
+ }
+ public IEnumerable<U> Domain {
+ get {
+ return dict.Keys;
+ }
+ }
+ }
+ public class Sequence<T>
+ {
+ T[] elmts;
+ public Sequence() { }
+ public Sequence(T[] ee) {
+ elmts = ee;
+ }
+ public static Sequence<T> Empty {
+ get {
+ return new Sequence<T>(new T[0]);
+ }
+ }
+ public static Sequence<T> FromElements(params T[] values) {
+ return new Sequence<T>(values);
+ }
+ public BigInteger Length {
+ get { return new BigInteger(elmts.Length); }
+ }
+ public T[] Elements {
+ get {
+ return elmts;
+ }
+ }
+ public IEnumerable<T> UniqueElements {
+ get {
+ var st = Set<T>.FromElements(elmts);
+ return st.Elements;
+ }
+ }
+ public T Select(BigInteger index) {
+ return elmts[(int)index];
+ }
+ public Sequence<T> Update(BigInteger index, T t) {
+ T[] a = (T[])elmts.Clone();
+ a[(int)index] = t;
+ return new Sequence<T>(a);
+ }
+ public bool Equals(Sequence<T> other) {
+ int n = elmts.Length;
+ return n == other.elmts.Length && EqualUntil(other, n);
+ }
+ public override bool Equals(object other) {
+ return other is Sequence<T> && Equals((Sequence<T>)other);
+ }
+ public override int GetHashCode() {
+ return elmts.GetHashCode();
+ }
+ bool EqualUntil(Sequence<T> other, int n) {
+ for (int i = 0; i < n; i++) {
+ if (!elmts[i].Equals(other.elmts[i]))
+ return false;
+ }
+ return true;
+ }
+ public bool IsProperPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n < other.elmts.Length && EqualUntil(other, n);
+ }
+ public bool IsPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n <= other.elmts.Length && EqualUntil(other, n);
+ }
+ public Sequence<T> Concat(Sequence<T> other) {
+ if (elmts.Length == 0)
+ return other;
+ else if (other.elmts.Length == 0)
+ return this;
+ T[] a = new T[elmts.Length + other.elmts.Length];
+ System.Array.Copy(elmts, 0, a, 0, elmts.Length);
+ System.Array.Copy(other.elmts, 0, a, elmts.Length, other.elmts.Length);
+ return new Sequence<T>(a);
+ }
+ public bool Contains(T t) {
+ int n = elmts.Length;
+ for (int i = 0; i < n; i++) {
+ if (t.Equals(elmts[i]))
+ return true;
+ }
+ return false;
+ }
+ public Sequence<T> Take(BigInteger n) {
+ int m = (int)n;
+ if (elmts.Length == m)
+ return this;
+ T[] a = new T[m];
+ System.Array.Copy(elmts, a, m);
+ return new Sequence<T>(a);
+ }
+ public Sequence<T> Drop(BigInteger n) {
+ if (n.IsZero)
+ return this;
+ int m = (int)n;
+ T[] a = new T[elmts.Length - m];
+ System.Array.Copy(elmts, m, a, 0, elmts.Length - m);
+ return new Sequence<T>(a);
+ }
+ }
+ public struct Pair<A, B>
+ {
+ public readonly A Car;
+ public readonly B Cdr;
+ public Pair(A a, B b) {
+ this.Car = a;
+ this.Cdr = b;
+ }
+ }
+ public partial class Helpers {
+ // Computing forall/exists quantifiers
+ 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<U>(Dafny.Set<U> set, bool frall, System.Predicate<U> pred) {
+ foreach (var u in set.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantMap<U,V>(Dafny.Map<U,V> map, bool frall, System.Predicate<U> pred) {
+ foreach (var u in map.Domain) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantSeq<U>(Dafny.Sequence<U> seq, bool frall, System.Predicate<U> pred) {
+ foreach (var u in seq.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ // Enumerating other collections
+ public delegate Dafny.Set<T> ComprehensionDelegate<T>();
+ public delegate Dafny.Map<U, V> MapComprehensionDelegate<U, V>();
+ public static IEnumerable<bool> AllBooleans {
+ get {
+ yield return false;
+ yield return true;
+ }
+ }
+ // pre: b != 0
+ // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) {
+ if (0 <= a.Sign) {
+ if (0 <= b.Sign) {
+ // +a +b: a/b
+ return BigInteger.Divide(a, b);
+ } else {
+ // +a -b: -(a/(-b))
+ return BigInteger.Negate(BigInteger.Divide(a, BigInteger.Negate(b)));
+ }
+ } else {
+ if (0 <= b.Sign) {
+ // -a +b: -((-a-1)/b) - 1
+ return BigInteger.Negate(BigInteger.Divide(BigInteger.Negate(a) - 1, b)) - 1;
+ } else {
+ // -a -b: ((-a-1)/(-b)) + 1
+ return BigInteger.Divide(BigInteger.Negate(a) - 1, BigInteger.Negate(b)) + 1;
+ }
+ }
+ }
+ // pre: b != 0
+ // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) {
+ var bp = BigInteger.Abs(b);
+ if (0 <= a.Sign) {
+ // +a: a % b'
+ return BigInteger.Remainder(a, bp);
+ } else {
+ // c = ((-a) % b')
+ // -a: b' - c if c > 0
+ // -a: 0 if c == 0
+ var c = BigInteger.Remainder(BigInteger.Negate(a), bp);
+ return c.IsZero ? c : BigInteger.Subtract(bp, c);
+ }
+ }
+ public static Sequence<T> SeqFromArray<T>(T[] array) {
+ return new Sequence<T>(array);
+ }
+ // In .NET version 4.5, it it possible to mark a method with "AggressiveInlining", which says to inline the
+ // method if possible. Method "ExpressionSequence" would be a good candidate for it:
+ // [System.Runtime.CompilerServices.MethodImpl(System.Runtime.CompilerServices.MethodImplOptions.AggressiveInlining)]
+ public static U ExpressionSequence<T, U>(T t, U u)
+ {
+ return u;
+ }
+ }
+}
+namespace Dafny {
+ public partial class Helpers {
+ public static T[] InitNewArray1<T>(BigInteger size0) {
+ int s0 = (int)size0;
+ T[] a = new T[s0];
+ BigInteger[] b = a as BigInteger[];
+ if (b != null) {
+ BigInteger z = new BigInteger(0);
+ for (int i0 = 0; i0 < s0; i0++)
+ b[i0] = z;
+ }
+ return a;
+ }
+ }
+}
+
+public class @_default {
+ public void @Main()
+ {
+ Contract.Assume((new BigInteger(2)) < (new BigInteger(10)));
+ }
+ public static void Main(string[] args) {
+ @_default b = new @_default();
+ b.Main();
+ }
+}
+
+-------------------- AssumeStmt1 --------------------
+
+Dafny program verifier finished with 2 verified, 0 errors
+Compiled program written to AssumeStmt1.cs
+Compiled assembly into AssumeStmt1.exe
+Rewrote assembly into AssumeStmt1.exe
+// Dafny program AssumeStmt1.dfy compiled into C#
+
+using System.Diagnostics.Contracts;
+using System.Numerics;
+using System.Collections.Generic;
+
+namespace Dafny
+{
+ public class Set<T>
+ {
+ Dictionary<T, bool> dict;
+ public Set() { }
+ Set(Dictionary<T, bool> d) {
+ dict = d;
+ }
+ public static Set<T> Empty {
+ get {
+ return new Set<T>(new Dictionary<T, bool>(0));
+ }
+ }
+ public static Set<T> FromElements(params T[] values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>(values.Length);
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+ public static Set<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>();
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+
+ public IEnumerable<T> Elements {
+ get {
+ return dict.Keys;
+ }
+ }
+ public bool Equals(Set<T> other) {
+ return dict.Count == other.dict.Count && IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is Set<T> && Equals((Set<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(Set<T> other) {
+ return dict.Count < other.dict.Count && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(Set<T> other) {
+ if (other.dict.Count < dict.Count)
+ return false;
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(Set<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(Set<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(Set<T> other) {
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public Set<T> Union(Set<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ Dictionary<T, bool> r = new Dictionary<T, bool>();
+ foreach (T t in b.Keys)
+ r[t] = true;
+ foreach (T t in a.Keys)
+ r[t] = true;
+ return new Set<T>(r);
+ }
+ public Set<T> Intersect(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ var r = new Dictionary<T, bool>();
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public Set<T> Difference(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, bool>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public T Choose() {
+ foreach (T t in dict.Keys) {
+ // return the first one
+ return t;
+ }
+ return default(T);
+ }
+ }
+ public class MultiSet<T>
+ {
+ Dictionary<T, int> dict;
+ public MultiSet() { }
+ MultiSet(Dictionary<T, int> d) {
+ dict = d;
+ }
+ public static MultiSet<T> Empty {
+ get {
+ return new MultiSet<T>(new Dictionary<T, int>(0));
+ }
+ }
+ public static MultiSet<T> FromElements(params T[] values) {
+ Dictionary<T, int> d = new Dictionary<T, int>(values.Length);
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSeq(Sequence<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSet(Set<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ d[t] = 1;
+ }
+ return new MultiSet<T>(d);
+ }
+
+ public bool Equals(MultiSet<T> other) {
+ return other.IsSubsetOf(this) && this.IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is MultiSet<T> && Equals((MultiSet<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(MultiSet<T> other) {
+ return !Equals(other) && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t])
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(MultiSet<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(MultiSet<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t))
+ return false;
+ }
+ foreach (T t in other.dict.Keys) {
+ if (dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public MultiSet<T> Union(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + dict[t];
+ }
+ foreach (T t in other.dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + other.dict[t];
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Intersect(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t)) {
+ r.Add(t, other.dict[t] < dict[t] ? other.dict[t] : dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Difference(MultiSet<T> other) { // \result == this - other
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t)) {
+ r.Add(t, dict[t]);
+ } else if (other.dict[t] < dict[t]) {
+ r.Add(t, dict[t] - other.dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public IEnumerable<T> Elements {
+ get {
+ List<T> l = new List<T>();
+ foreach (T t in dict.Keys) {
+ int n;
+ dict.TryGetValue(t, out n);
+ for (int i = 0; i < n; i ++) {
+ l.Add(t);
+ }
+ }
+ return l;
+ }
+ }
+ }
+
+ public class Map<U, V>
+ {
+ Dictionary<U, V> dict;
+ public Map() { }
+ Map(Dictionary<U, V> d) {
+ dict = d;
+ }
+ public static Map<U, V> Empty {
+ get {
+ return new Map<U, V>(new Dictionary<U,V>());
+ }
+ }
+ public static Map<U, V> FromElements(params Pair<U, V>[] values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Length);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public static Map<U, V> FromCollection(List<Pair<U, V>> values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Count);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public bool Equals(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ V v1, v2;
+ if (!dict.TryGetValue(u, out v1)) {
+ return false; // this shouldn't happen
+ }
+ if (!other.dict.TryGetValue(u, out v2)) {
+ return false; // other dictionary does not contain this element
+ }
+ if (!v1.Equals(v2)) {
+ return false;
+ }
+ }
+ foreach (U u in other.dict.Keys) {
+ if (!dict.ContainsKey(u)) {
+ return false; // this shouldn't happen
+ }
+ }
+ return true;
+ }
+ public override bool Equals(object other) {
+ return other is Map<U, V> && Equals((Map<U, V>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsDisjointFrom(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ if (other.dict.ContainsKey(u))
+ return false;
+ }
+ foreach (U u in other.dict.Keys) {
+ if (dict.ContainsKey(u))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(U u) {
+ return dict.ContainsKey(u);
+ }
+ public V Select(U index) {
+ return dict[index];
+ }
+ public Map<U, V> Update(U index, V val) {
+ Dictionary<U, V> d = new Dictionary<U, V>(dict);
+ d[index] = val;
+ return new Map<U, V>(d);
+ }
+ public IEnumerable<U> Domain {
+ get {
+ return dict.Keys;
+ }
+ }
+ }
+ public class Sequence<T>
+ {
+ T[] elmts;
+ public Sequence() { }
+ public Sequence(T[] ee) {
+ elmts = ee;
+ }
+ public static Sequence<T> Empty {
+ get {
+ return new Sequence<T>(new T[0]);
+ }
+ }
+ public static Sequence<T> FromElements(params T[] values) {
+ return new Sequence<T>(values);
+ }
+ public BigInteger Length {
+ get { return new BigInteger(elmts.Length); }
+ }
+ public T[] Elements {
+ get {
+ return elmts;
+ }
+ }
+ public IEnumerable<T> UniqueElements {
+ get {
+ var st = Set<T>.FromElements(elmts);
+ return st.Elements;
+ }
+ }
+ public T Select(BigInteger index) {
+ return elmts[(int)index];
+ }
+ public Sequence<T> Update(BigInteger index, T t) {
+ T[] a = (T[])elmts.Clone();
+ a[(int)index] = t;
+ return new Sequence<T>(a);
+ }
+ public bool Equals(Sequence<T> other) {
+ int n = elmts.Length;
+ return n == other.elmts.Length && EqualUntil(other, n);
+ }
+ public override bool Equals(object other) {
+ return other is Sequence<T> && Equals((Sequence<T>)other);
+ }
+ public override int GetHashCode() {
+ return elmts.GetHashCode();
+ }
+ bool EqualUntil(Sequence<T> other, int n) {
+ for (int i = 0; i < n; i++) {
+ if (!elmts[i].Equals(other.elmts[i]))
+ return false;
+ }
+ return true;
+ }
+ public bool IsProperPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n < other.elmts.Length && EqualUntil(other, n);
+ }
+ public bool IsPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n <= other.elmts.Length && EqualUntil(other, n);
+ }
+ public Sequence<T> Concat(Sequence<T> other) {
+ if (elmts.Length == 0)
+ return other;
+ else if (other.elmts.Length == 0)
+ return this;
+ T[] a = new T[elmts.Length + other.elmts.Length];
+ System.Array.Copy(elmts, 0, a, 0, elmts.Length);
+ System.Array.Copy(other.elmts, 0, a, elmts.Length, other.elmts.Length);
+ return new Sequence<T>(a);
+ }
+ public bool Contains(T t) {
+ int n = elmts.Length;
+ for (int i = 0; i < n; i++) {
+ if (t.Equals(elmts[i]))
+ return true;
+ }
+ return false;
+ }
+ public Sequence<T> Take(BigInteger n) {
+ int m = (int)n;
+ if (elmts.Length == m)
+ return this;
+ T[] a = new T[m];
+ System.Array.Copy(elmts, a, m);
+ return new Sequence<T>(a);
+ }
+ public Sequence<T> Drop(BigInteger n) {
+ if (n.IsZero)
+ return this;
+ int m = (int)n;
+ T[] a = new T[elmts.Length - m];
+ System.Array.Copy(elmts, m, a, 0, elmts.Length - m);
+ return new Sequence<T>(a);
+ }
+ }
+ public struct Pair<A, B>
+ {
+ public readonly A Car;
+ public readonly B Cdr;
+ public Pair(A a, B b) {
+ this.Car = a;
+ this.Cdr = b;
+ }
+ }
+ public partial class Helpers {
+ // Computing forall/exists quantifiers
+ 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<U>(Dafny.Set<U> set, bool frall, System.Predicate<U> pred) {
+ foreach (var u in set.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantMap<U,V>(Dafny.Map<U,V> map, bool frall, System.Predicate<U> pred) {
+ foreach (var u in map.Domain) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantSeq<U>(Dafny.Sequence<U> seq, bool frall, System.Predicate<U> pred) {
+ foreach (var u in seq.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ // Enumerating other collections
+ public delegate Dafny.Set<T> ComprehensionDelegate<T>();
+ public delegate Dafny.Map<U, V> MapComprehensionDelegate<U, V>();
+ public static IEnumerable<bool> AllBooleans {
+ get {
+ yield return false;
+ yield return true;
+ }
+ }
+ // pre: b != 0
+ // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) {
+ if (0 <= a.Sign) {
+ if (0 <= b.Sign) {
+ // +a +b: a/b
+ return BigInteger.Divide(a, b);
+ } else {
+ // +a -b: -(a/(-b))
+ return BigInteger.Negate(BigInteger.Divide(a, BigInteger.Negate(b)));
+ }
+ } else {
+ if (0 <= b.Sign) {
+ // -a +b: -((-a-1)/b) - 1
+ return BigInteger.Negate(BigInteger.Divide(BigInteger.Negate(a) - 1, b)) - 1;
+ } else {
+ // -a -b: ((-a-1)/(-b)) + 1
+ return BigInteger.Divide(BigInteger.Negate(a) - 1, BigInteger.Negate(b)) + 1;
+ }
+ }
+ }
+ // pre: b != 0
+ // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) {
+ var bp = BigInteger.Abs(b);
+ if (0 <= a.Sign) {
+ // +a: a % b'
+ return BigInteger.Remainder(a, bp);
+ } else {
+ // c = ((-a) % b')
+ // -a: b' - c if c > 0
+ // -a: 0 if c == 0
+ var c = BigInteger.Remainder(BigInteger.Negate(a), bp);
+ return c.IsZero ? c : BigInteger.Subtract(bp, c);
+ }
+ }
+ public static Sequence<T> SeqFromArray<T>(T[] array) {
+ return new Sequence<T>(array);
+ }
+ // In .NET version 4.5, it it possible to mark a method with "AggressiveInlining", which says to inline the
+ // method if possible. Method "ExpressionSequence" would be a good candidate for it:
+ // [System.Runtime.CompilerServices.MethodImpl(System.Runtime.CompilerServices.MethodImplOptions.AggressiveInlining)]
+ public static U ExpressionSequence<T, U>(T t, U u)
+ {
+ return u;
+ }
+ }
+}
+namespace Dafny {
+ public partial class Helpers {
+ public static T[] InitNewArray1<T>(BigInteger size0) {
+ int s0 = (int)size0;
+ T[] a = new T[s0];
+ BigInteger[] b = a as BigInteger[];
+ if (b != null) {
+ BigInteger z = new BigInteger(0);
+ for (int i0 = 0; i0 < s0; i0++)
+ b[i0] = z;
+ }
+ return a;
+ }
+ }
+}
+
+public class @_default {
+ public void @Main()
+ {
+ Contract.Assume((new BigInteger(10)) < (new BigInteger(2)));
+ }
+ public static void Main(string[] args) {
+ @_default b = new @_default();
+ b.Main();
+ }
+}
+
+-------------------- AssertStmt0 --------------------
+
+Dafny program verifier finished with 2 verified, 0 errors
+Compiled program written to AssertStmt0.cs
+Compiled assembly into AssertStmt0.exe
+Rewrote assembly into AssertStmt0.exe
+// Dafny program AssertStmt0.dfy compiled into C#
+
+using System.Diagnostics.Contracts;
+using System.Numerics;
+using System.Collections.Generic;
+
+namespace Dafny
+{
+ public class Set<T>
+ {
+ Dictionary<T, bool> dict;
+ public Set() { }
+ Set(Dictionary<T, bool> d) {
+ dict = d;
+ }
+ public static Set<T> Empty {
+ get {
+ return new Set<T>(new Dictionary<T, bool>(0));
+ }
+ }
+ public static Set<T> FromElements(params T[] values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>(values.Length);
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+ public static Set<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>();
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+
+ public IEnumerable<T> Elements {
+ get {
+ return dict.Keys;
+ }
+ }
+ public bool Equals(Set<T> other) {
+ return dict.Count == other.dict.Count && IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is Set<T> && Equals((Set<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(Set<T> other) {
+ return dict.Count < other.dict.Count && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(Set<T> other) {
+ if (other.dict.Count < dict.Count)
+ return false;
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(Set<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(Set<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(Set<T> other) {
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public Set<T> Union(Set<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ Dictionary<T, bool> r = new Dictionary<T, bool>();
+ foreach (T t in b.Keys)
+ r[t] = true;
+ foreach (T t in a.Keys)
+ r[t] = true;
+ return new Set<T>(r);
+ }
+ public Set<T> Intersect(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ var r = new Dictionary<T, bool>();
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public Set<T> Difference(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, bool>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public T Choose() {
+ foreach (T t in dict.Keys) {
+ // return the first one
+ return t;
+ }
+ return default(T);
+ }
+ }
+ public class MultiSet<T>
+ {
+ Dictionary<T, int> dict;
+ public MultiSet() { }
+ MultiSet(Dictionary<T, int> d) {
+ dict = d;
+ }
+ public static MultiSet<T> Empty {
+ get {
+ return new MultiSet<T>(new Dictionary<T, int>(0));
+ }
+ }
+ public static MultiSet<T> FromElements(params T[] values) {
+ Dictionary<T, int> d = new Dictionary<T, int>(values.Length);
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSeq(Sequence<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSet(Set<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ d[t] = 1;
+ }
+ return new MultiSet<T>(d);
+ }
+
+ public bool Equals(MultiSet<T> other) {
+ return other.IsSubsetOf(this) && this.IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is MultiSet<T> && Equals((MultiSet<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(MultiSet<T> other) {
+ return !Equals(other) && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t])
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(MultiSet<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(MultiSet<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t))
+ return false;
+ }
+ foreach (T t in other.dict.Keys) {
+ if (dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public MultiSet<T> Union(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + dict[t];
+ }
+ foreach (T t in other.dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + other.dict[t];
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Intersect(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t)) {
+ r.Add(t, other.dict[t] < dict[t] ? other.dict[t] : dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Difference(MultiSet<T> other) { // \result == this - other
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t)) {
+ r.Add(t, dict[t]);
+ } else if (other.dict[t] < dict[t]) {
+ r.Add(t, dict[t] - other.dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public IEnumerable<T> Elements {
+ get {
+ List<T> l = new List<T>();
+ foreach (T t in dict.Keys) {
+ int n;
+ dict.TryGetValue(t, out n);
+ for (int i = 0; i < n; i ++) {
+ l.Add(t);
+ }
+ }
+ return l;
+ }
+ }
+ }
+
+ public class Map<U, V>
+ {
+ Dictionary<U, V> dict;
+ public Map() { }
+ Map(Dictionary<U, V> d) {
+ dict = d;
+ }
+ public static Map<U, V> Empty {
+ get {
+ return new Map<U, V>(new Dictionary<U,V>());
+ }
+ }
+ public static Map<U, V> FromElements(params Pair<U, V>[] values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Length);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public static Map<U, V> FromCollection(List<Pair<U, V>> values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Count);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public bool Equals(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ V v1, v2;
+ if (!dict.TryGetValue(u, out v1)) {
+ return false; // this shouldn't happen
+ }
+ if (!other.dict.TryGetValue(u, out v2)) {
+ return false; // other dictionary does not contain this element
+ }
+ if (!v1.Equals(v2)) {
+ return false;
+ }
+ }
+ foreach (U u in other.dict.Keys) {
+ if (!dict.ContainsKey(u)) {
+ return false; // this shouldn't happen
+ }
+ }
+ return true;
+ }
+ public override bool Equals(object other) {
+ return other is Map<U, V> && Equals((Map<U, V>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsDisjointFrom(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ if (other.dict.ContainsKey(u))
+ return false;
+ }
+ foreach (U u in other.dict.Keys) {
+ if (dict.ContainsKey(u))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(U u) {
+ return dict.ContainsKey(u);
+ }
+ public V Select(U index) {
+ return dict[index];
+ }
+ public Map<U, V> Update(U index, V val) {
+ Dictionary<U, V> d = new Dictionary<U, V>(dict);
+ d[index] = val;
+ return new Map<U, V>(d);
+ }
+ public IEnumerable<U> Domain {
+ get {
+ return dict.Keys;
+ }
+ }
+ }
+ public class Sequence<T>
+ {
+ T[] elmts;
+ public Sequence() { }
+ public Sequence(T[] ee) {
+ elmts = ee;
+ }
+ public static Sequence<T> Empty {
+ get {
+ return new Sequence<T>(new T[0]);
+ }
+ }
+ public static Sequence<T> FromElements(params T[] values) {
+ return new Sequence<T>(values);
+ }
+ public BigInteger Length {
+ get { return new BigInteger(elmts.Length); }
+ }
+ public T[] Elements {
+ get {
+ return elmts;
+ }
+ }
+ public IEnumerable<T> UniqueElements {
+ get {
+ var st = Set<T>.FromElements(elmts);
+ return st.Elements;
+ }
+ }
+ public T Select(BigInteger index) {
+ return elmts[(int)index];
+ }
+ public Sequence<T> Update(BigInteger index, T t) {
+ T[] a = (T[])elmts.Clone();
+ a[(int)index] = t;
+ return new Sequence<T>(a);
+ }
+ public bool Equals(Sequence<T> other) {
+ int n = elmts.Length;
+ return n == other.elmts.Length && EqualUntil(other, n);
+ }
+ public override bool Equals(object other) {
+ return other is Sequence<T> && Equals((Sequence<T>)other);
+ }
+ public override int GetHashCode() {
+ return elmts.GetHashCode();
+ }
+ bool EqualUntil(Sequence<T> other, int n) {
+ for (int i = 0; i < n; i++) {
+ if (!elmts[i].Equals(other.elmts[i]))
+ return false;
+ }
+ return true;
+ }
+ public bool IsProperPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n < other.elmts.Length && EqualUntil(other, n);
+ }
+ public bool IsPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n <= other.elmts.Length && EqualUntil(other, n);
+ }
+ public Sequence<T> Concat(Sequence<T> other) {
+ if (elmts.Length == 0)
+ return other;
+ else if (other.elmts.Length == 0)
+ return this;
+ T[] a = new T[elmts.Length + other.elmts.Length];
+ System.Array.Copy(elmts, 0, a, 0, elmts.Length);
+ System.Array.Copy(other.elmts, 0, a, elmts.Length, other.elmts.Length);
+ return new Sequence<T>(a);
+ }
+ public bool Contains(T t) {
+ int n = elmts.Length;
+ for (int i = 0; i < n; i++) {
+ if (t.Equals(elmts[i]))
+ return true;
+ }
+ return false;
+ }
+ public Sequence<T> Take(BigInteger n) {
+ int m = (int)n;
+ if (elmts.Length == m)
+ return this;
+ T[] a = new T[m];
+ System.Array.Copy(elmts, a, m);
+ return new Sequence<T>(a);
+ }
+ public Sequence<T> Drop(BigInteger n) {
+ if (n.IsZero)
+ return this;
+ int m = (int)n;
+ T[] a = new T[elmts.Length - m];
+ System.Array.Copy(elmts, m, a, 0, elmts.Length - m);
+ return new Sequence<T>(a);
+ }
+ }
+ public struct Pair<A, B>
+ {
+ public readonly A Car;
+ public readonly B Cdr;
+ public Pair(A a, B b) {
+ this.Car = a;
+ this.Cdr = b;
+ }
+ }
+ public partial class Helpers {
+ // Computing forall/exists quantifiers
+ 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<U>(Dafny.Set<U> set, bool frall, System.Predicate<U> pred) {
+ foreach (var u in set.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantMap<U,V>(Dafny.Map<U,V> map, bool frall, System.Predicate<U> pred) {
+ foreach (var u in map.Domain) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantSeq<U>(Dafny.Sequence<U> seq, bool frall, System.Predicate<U> pred) {
+ foreach (var u in seq.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ // Enumerating other collections
+ public delegate Dafny.Set<T> ComprehensionDelegate<T>();
+ public delegate Dafny.Map<U, V> MapComprehensionDelegate<U, V>();
+ public static IEnumerable<bool> AllBooleans {
+ get {
+ yield return false;
+ yield return true;
+ }
+ }
+ // pre: b != 0
+ // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) {
+ if (0 <= a.Sign) {
+ if (0 <= b.Sign) {
+ // +a +b: a/b
+ return BigInteger.Divide(a, b);
+ } else {
+ // +a -b: -(a/(-b))
+ return BigInteger.Negate(BigInteger.Divide(a, BigInteger.Negate(b)));
+ }
+ } else {
+ if (0 <= b.Sign) {
+ // -a +b: -((-a-1)/b) - 1
+ return BigInteger.Negate(BigInteger.Divide(BigInteger.Negate(a) - 1, b)) - 1;
+ } else {
+ // -a -b: ((-a-1)/(-b)) + 1
+ return BigInteger.Divide(BigInteger.Negate(a) - 1, BigInteger.Negate(b)) + 1;
+ }
+ }
+ }
+ // pre: b != 0
+ // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) {
+ var bp = BigInteger.Abs(b);
+ if (0 <= a.Sign) {
+ // +a: a % b'
+ return BigInteger.Remainder(a, bp);
+ } else {
+ // c = ((-a) % b')
+ // -a: b' - c if c > 0
+ // -a: 0 if c == 0
+ var c = BigInteger.Remainder(BigInteger.Negate(a), bp);
+ return c.IsZero ? c : BigInteger.Subtract(bp, c);
+ }
+ }
+ public static Sequence<T> SeqFromArray<T>(T[] array) {
+ return new Sequence<T>(array);
+ }
+ // In .NET version 4.5, it it possible to mark a method with "AggressiveInlining", which says to inline the
+ // method if possible. Method "ExpressionSequence" would be a good candidate for it:
+ // [System.Runtime.CompilerServices.MethodImpl(System.Runtime.CompilerServices.MethodImplOptions.AggressiveInlining)]
+ public static U ExpressionSequence<T, U>(T t, U u)
+ {
+ return u;
+ }
+ }
+}
+namespace Dafny {
+ public partial class Helpers {
+ public static T[] InitNewArray1<T>(BigInteger size0) {
+ int s0 = (int)size0;
+ T[] a = new T[s0];
+ BigInteger[] b = a as BigInteger[];
+ if (b != null) {
+ BigInteger z = new BigInteger(0);
+ for (int i0 = 0; i0 < s0; i0++)
+ b[i0] = z;
+ }
+ return a;
+ }
+ }
+}
+
+public class @_default {
+ public void @Main()
+ {
+ Contract.Assert((new BigInteger(2)) < (new BigInteger(10)));
+ }
+ public static void Main(string[] args) {
+ @_default b = new @_default();
+ b.Main();
+ }
+}
+
+-------------------- AssertStmt1 --------------------
+AssertStmt1.dfy(3,13): Error: assertion violation
+
+Dafny program verifier finished with 1 verified, 1 error
+Compiled program written to AssertStmt1.cs
+Compiled assembly into AssertStmt1.exe
+Rewrote assembly into AssertStmt1.exe
+// Dafny program AssertStmt1.dfy compiled into C#
+
+using System.Diagnostics.Contracts;
+using System.Numerics;
+using System.Collections.Generic;
+
+namespace Dafny
+{
+ public class Set<T>
+ {
+ Dictionary<T, bool> dict;
+ public Set() { }
+ Set(Dictionary<T, bool> d) {
+ dict = d;
+ }
+ public static Set<T> Empty {
+ get {
+ return new Set<T>(new Dictionary<T, bool>(0));
+ }
+ }
+ public static Set<T> FromElements(params T[] values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>(values.Length);
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+ public static Set<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>();
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+
+ public IEnumerable<T> Elements {
+ get {
+ return dict.Keys;
+ }
+ }
+ public bool Equals(Set<T> other) {
+ return dict.Count == other.dict.Count && IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is Set<T> && Equals((Set<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(Set<T> other) {
+ return dict.Count < other.dict.Count && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(Set<T> other) {
+ if (other.dict.Count < dict.Count)
+ return false;
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(Set<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(Set<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(Set<T> other) {
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public Set<T> Union(Set<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ Dictionary<T, bool> r = new Dictionary<T, bool>();
+ foreach (T t in b.Keys)
+ r[t] = true;
+ foreach (T t in a.Keys)
+ r[t] = true;
+ return new Set<T>(r);
+ }
+ public Set<T> Intersect(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ var r = new Dictionary<T, bool>();
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public Set<T> Difference(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, bool>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public T Choose() {
+ foreach (T t in dict.Keys) {
+ // return the first one
+ return t;
+ }
+ return default(T);
+ }
+ }
+ public class MultiSet<T>
+ {
+ Dictionary<T, int> dict;
+ public MultiSet() { }
+ MultiSet(Dictionary<T, int> d) {
+ dict = d;
+ }
+ public static MultiSet<T> Empty {
+ get {
+ return new MultiSet<T>(new Dictionary<T, int>(0));
+ }
+ }
+ public static MultiSet<T> FromElements(params T[] values) {
+ Dictionary<T, int> d = new Dictionary<T, int>(values.Length);
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSeq(Sequence<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSet(Set<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ d[t] = 1;
+ }
+ return new MultiSet<T>(d);
+ }
+
+ public bool Equals(MultiSet<T> other) {
+ return other.IsSubsetOf(this) && this.IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is MultiSet<T> && Equals((MultiSet<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(MultiSet<T> other) {
+ return !Equals(other) && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t])
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(MultiSet<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(MultiSet<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t))
+ return false;
+ }
+ foreach (T t in other.dict.Keys) {
+ if (dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public MultiSet<T> Union(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + dict[t];
+ }
+ foreach (T t in other.dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + other.dict[t];
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Intersect(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t)) {
+ r.Add(t, other.dict[t] < dict[t] ? other.dict[t] : dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Difference(MultiSet<T> other) { // \result == this - other
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t)) {
+ r.Add(t, dict[t]);
+ } else if (other.dict[t] < dict[t]) {
+ r.Add(t, dict[t] - other.dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public IEnumerable<T> Elements {
+ get {
+ List<T> l = new List<T>();
+ foreach (T t in dict.Keys) {
+ int n;
+ dict.TryGetValue(t, out n);
+ for (int i = 0; i < n; i ++) {
+ l.Add(t);
+ }
+ }
+ return l;
+ }
+ }
+ }
+
+ public class Map<U, V>
+ {
+ Dictionary<U, V> dict;
+ public Map() { }
+ Map(Dictionary<U, V> d) {
+ dict = d;
+ }
+ public static Map<U, V> Empty {
+ get {
+ return new Map<U, V>(new Dictionary<U,V>());
+ }
+ }
+ public static Map<U, V> FromElements(params Pair<U, V>[] values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Length);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public static Map<U, V> FromCollection(List<Pair<U, V>> values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Count);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public bool Equals(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ V v1, v2;
+ if (!dict.TryGetValue(u, out v1)) {
+ return false; // this shouldn't happen
+ }
+ if (!other.dict.TryGetValue(u, out v2)) {
+ return false; // other dictionary does not contain this element
+ }
+ if (!v1.Equals(v2)) {
+ return false;
+ }
+ }
+ foreach (U u in other.dict.Keys) {
+ if (!dict.ContainsKey(u)) {
+ return false; // this shouldn't happen
+ }
+ }
+ return true;
+ }
+ public override bool Equals(object other) {
+ return other is Map<U, V> && Equals((Map<U, V>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsDisjointFrom(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ if (other.dict.ContainsKey(u))
+ return false;
+ }
+ foreach (U u in other.dict.Keys) {
+ if (dict.ContainsKey(u))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(U u) {
+ return dict.ContainsKey(u);
+ }
+ public V Select(U index) {
+ return dict[index];
+ }
+ public Map<U, V> Update(U index, V val) {
+ Dictionary<U, V> d = new Dictionary<U, V>(dict);
+ d[index] = val;
+ return new Map<U, V>(d);
+ }
+ public IEnumerable<U> Domain {
+ get {
+ return dict.Keys;
+ }
+ }
+ }
+ public class Sequence<T>
+ {
+ T[] elmts;
+ public Sequence() { }
+ public Sequence(T[] ee) {
+ elmts = ee;
+ }
+ public static Sequence<T> Empty {
+ get {
+ return new Sequence<T>(new T[0]);
+ }
+ }
+ public static Sequence<T> FromElements(params T[] values) {
+ return new Sequence<T>(values);
+ }
+ public BigInteger Length {
+ get { return new BigInteger(elmts.Length); }
+ }
+ public T[] Elements {
+ get {
+ return elmts;
+ }
+ }
+ public IEnumerable<T> UniqueElements {
+ get {
+ var st = Set<T>.FromElements(elmts);
+ return st.Elements;
+ }
+ }
+ public T Select(BigInteger index) {
+ return elmts[(int)index];
+ }
+ public Sequence<T> Update(BigInteger index, T t) {
+ T[] a = (T[])elmts.Clone();
+ a[(int)index] = t;
+ return new Sequence<T>(a);
+ }
+ public bool Equals(Sequence<T> other) {
+ int n = elmts.Length;
+ return n == other.elmts.Length && EqualUntil(other, n);
+ }
+ public override bool Equals(object other) {
+ return other is Sequence<T> && Equals((Sequence<T>)other);
+ }
+ public override int GetHashCode() {
+ return elmts.GetHashCode();
+ }
+ bool EqualUntil(Sequence<T> other, int n) {
+ for (int i = 0; i < n; i++) {
+ if (!elmts[i].Equals(other.elmts[i]))
+ return false;
+ }
+ return true;
+ }
+ public bool IsProperPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n < other.elmts.Length && EqualUntil(other, n);
+ }
+ public bool IsPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n <= other.elmts.Length && EqualUntil(other, n);
+ }
+ public Sequence<T> Concat(Sequence<T> other) {
+ if (elmts.Length == 0)
+ return other;
+ else if (other.elmts.Length == 0)
+ return this;
+ T[] a = new T[elmts.Length + other.elmts.Length];
+ System.Array.Copy(elmts, 0, a, 0, elmts.Length);
+ System.Array.Copy(other.elmts, 0, a, elmts.Length, other.elmts.Length);
+ return new Sequence<T>(a);
+ }
+ public bool Contains(T t) {
+ int n = elmts.Length;
+ for (int i = 0; i < n; i++) {
+ if (t.Equals(elmts[i]))
+ return true;
+ }
+ return false;
+ }
+ public Sequence<T> Take(BigInteger n) {
+ int m = (int)n;
+ if (elmts.Length == m)
+ return this;
+ T[] a = new T[m];
+ System.Array.Copy(elmts, a, m);
+ return new Sequence<T>(a);
+ }
+ public Sequence<T> Drop(BigInteger n) {
+ if (n.IsZero)
+ return this;
+ int m = (int)n;
+ T[] a = new T[elmts.Length - m];
+ System.Array.Copy(elmts, m, a, 0, elmts.Length - m);
+ return new Sequence<T>(a);
+ }
+ }
+ public struct Pair<A, B>
+ {
+ public readonly A Car;
+ public readonly B Cdr;
+ public Pair(A a, B b) {
+ this.Car = a;
+ this.Cdr = b;
+ }
+ }
+ public partial class Helpers {
+ // Computing forall/exists quantifiers
+ 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<U>(Dafny.Set<U> set, bool frall, System.Predicate<U> pred) {
+ foreach (var u in set.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantMap<U,V>(Dafny.Map<U,V> map, bool frall, System.Predicate<U> pred) {
+ foreach (var u in map.Domain) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantSeq<U>(Dafny.Sequence<U> seq, bool frall, System.Predicate<U> pred) {
+ foreach (var u in seq.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ // Enumerating other collections
+ public delegate Dafny.Set<T> ComprehensionDelegate<T>();
+ public delegate Dafny.Map<U, V> MapComprehensionDelegate<U, V>();
+ public static IEnumerable<bool> AllBooleans {
+ get {
+ yield return false;
+ yield return true;
+ }
+ }
+ // pre: b != 0
+ // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) {
+ if (0 <= a.Sign) {
+ if (0 <= b.Sign) {
+ // +a +b: a/b
+ return BigInteger.Divide(a, b);
+ } else {
+ // +a -b: -(a/(-b))
+ return BigInteger.Negate(BigInteger.Divide(a, BigInteger.Negate(b)));
+ }
+ } else {
+ if (0 <= b.Sign) {
+ // -a +b: -((-a-1)/b) - 1
+ return BigInteger.Negate(BigInteger.Divide(BigInteger.Negate(a) - 1, b)) - 1;
+ } else {
+ // -a -b: ((-a-1)/(-b)) + 1
+ return BigInteger.Divide(BigInteger.Negate(a) - 1, BigInteger.Negate(b)) + 1;
+ }
+ }
+ }
+ // pre: b != 0
+ // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) {
+ var bp = BigInteger.Abs(b);
+ if (0 <= a.Sign) {
+ // +a: a % b'
+ return BigInteger.Remainder(a, bp);
+ } else {
+ // c = ((-a) % b')
+ // -a: b' - c if c > 0
+ // -a: 0 if c == 0
+ var c = BigInteger.Remainder(BigInteger.Negate(a), bp);
+ return c.IsZero ? c : BigInteger.Subtract(bp, c);
+ }
+ }
+ public static Sequence<T> SeqFromArray<T>(T[] array) {
+ return new Sequence<T>(array);
+ }
+ // In .NET version 4.5, it it possible to mark a method with "AggressiveInlining", which says to inline the
+ // method if possible. Method "ExpressionSequence" would be a good candidate for it:
+ // [System.Runtime.CompilerServices.MethodImpl(System.Runtime.CompilerServices.MethodImplOptions.AggressiveInlining)]
+ public static U ExpressionSequence<T, U>(T t, U u)
+ {
+ return u;
+ }
+ }
+}
+namespace Dafny {
+ public partial class Helpers {
+ public static T[] InitNewArray1<T>(BigInteger size0) {
+ int s0 = (int)size0;
+ T[] a = new T[s0];
+ BigInteger[] b = a as BigInteger[];
+ if (b != null) {
+ BigInteger z = new BigInteger(0);
+ for (int i0 = 0; i0 < s0; i0++)
+ b[i0] = z;
+ }
+ return a;
+ }
+ }
+}
+
+public class @_default {
+ public void @Main()
+ {
+ Contract.Assert((new BigInteger(10)) < (new BigInteger(2)));
+ }
+ public static void Main(string[] args) {
+ @_default b = new @_default();
+ b.Main();
+ }
+}
+
+-------------------- Precondition0 --------------------
+
+Dafny program verifier finished with 2 verified, 0 errors
+Compiled program written to Precondition0.cs
+Compiled assembly into Precondition0.exe
+Rewrote assembly into Precondition0.exe
+// Dafny program Precondition0.dfy compiled into C#
+
+using System.Diagnostics.Contracts;
+using System.Numerics;
+using System.Collections.Generic;
+
+namespace Dafny
+{
+ public class Set<T>
+ {
+ Dictionary<T, bool> dict;
+ public Set() { }
+ Set(Dictionary<T, bool> d) {
+ dict = d;
+ }
+ public static Set<T> Empty {
+ get {
+ return new Set<T>(new Dictionary<T, bool>(0));
+ }
+ }
+ public static Set<T> FromElements(params T[] values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>(values.Length);
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+ public static Set<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>();
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+
+ public IEnumerable<T> Elements {
+ get {
+ return dict.Keys;
+ }
+ }
+ public bool Equals(Set<T> other) {
+ return dict.Count == other.dict.Count && IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is Set<T> && Equals((Set<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(Set<T> other) {
+ return dict.Count < other.dict.Count && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(Set<T> other) {
+ if (other.dict.Count < dict.Count)
+ return false;
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(Set<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(Set<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(Set<T> other) {
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public Set<T> Union(Set<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ Dictionary<T, bool> r = new Dictionary<T, bool>();
+ foreach (T t in b.Keys)
+ r[t] = true;
+ foreach (T t in a.Keys)
+ r[t] = true;
+ return new Set<T>(r);
+ }
+ public Set<T> Intersect(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ var r = new Dictionary<T, bool>();
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public Set<T> Difference(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, bool>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public T Choose() {
+ foreach (T t in dict.Keys) {
+ // return the first one
+ return t;
+ }
+ return default(T);
+ }
+ }
+ public class MultiSet<T>
+ {
+ Dictionary<T, int> dict;
+ public MultiSet() { }
+ MultiSet(Dictionary<T, int> d) {
+ dict = d;
+ }
+ public static MultiSet<T> Empty {
+ get {
+ return new MultiSet<T>(new Dictionary<T, int>(0));
+ }
+ }
+ public static MultiSet<T> FromElements(params T[] values) {
+ Dictionary<T, int> d = new Dictionary<T, int>(values.Length);
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSeq(Sequence<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSet(Set<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ d[t] = 1;
+ }
+ return new MultiSet<T>(d);
+ }
+
+ public bool Equals(MultiSet<T> other) {
+ return other.IsSubsetOf(this) && this.IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is MultiSet<T> && Equals((MultiSet<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(MultiSet<T> other) {
+ return !Equals(other) && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t])
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(MultiSet<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(MultiSet<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t))
+ return false;
+ }
+ foreach (T t in other.dict.Keys) {
+ if (dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public MultiSet<T> Union(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + dict[t];
+ }
+ foreach (T t in other.dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + other.dict[t];
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Intersect(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t)) {
+ r.Add(t, other.dict[t] < dict[t] ? other.dict[t] : dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Difference(MultiSet<T> other) { // \result == this - other
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t)) {
+ r.Add(t, dict[t]);
+ } else if (other.dict[t] < dict[t]) {
+ r.Add(t, dict[t] - other.dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public IEnumerable<T> Elements {
+ get {
+ List<T> l = new List<T>();
+ foreach (T t in dict.Keys) {
+ int n;
+ dict.TryGetValue(t, out n);
+ for (int i = 0; i < n; i ++) {
+ l.Add(t);
+ }
+ }
+ return l;
+ }
+ }
+ }
+
+ public class Map<U, V>
+ {
+ Dictionary<U, V> dict;
+ public Map() { }
+ Map(Dictionary<U, V> d) {
+ dict = d;
+ }
+ public static Map<U, V> Empty {
+ get {
+ return new Map<U, V>(new Dictionary<U,V>());
+ }
+ }
+ public static Map<U, V> FromElements(params Pair<U, V>[] values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Length);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public static Map<U, V> FromCollection(List<Pair<U, V>> values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Count);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public bool Equals(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ V v1, v2;
+ if (!dict.TryGetValue(u, out v1)) {
+ return false; // this shouldn't happen
+ }
+ if (!other.dict.TryGetValue(u, out v2)) {
+ return false; // other dictionary does not contain this element
+ }
+ if (!v1.Equals(v2)) {
+ return false;
+ }
+ }
+ foreach (U u in other.dict.Keys) {
+ if (!dict.ContainsKey(u)) {
+ return false; // this shouldn't happen
+ }
+ }
+ return true;
+ }
+ public override bool Equals(object other) {
+ return other is Map<U, V> && Equals((Map<U, V>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsDisjointFrom(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ if (other.dict.ContainsKey(u))
+ return false;
+ }
+ foreach (U u in other.dict.Keys) {
+ if (dict.ContainsKey(u))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(U u) {
+ return dict.ContainsKey(u);
+ }
+ public V Select(U index) {
+ return dict[index];
+ }
+ public Map<U, V> Update(U index, V val) {
+ Dictionary<U, V> d = new Dictionary<U, V>(dict);
+ d[index] = val;
+ return new Map<U, V>(d);
+ }
+ public IEnumerable<U> Domain {
+ get {
+ return dict.Keys;
+ }
+ }
+ }
+ public class Sequence<T>
+ {
+ T[] elmts;
+ public Sequence() { }
+ public Sequence(T[] ee) {
+ elmts = ee;
+ }
+ public static Sequence<T> Empty {
+ get {
+ return new Sequence<T>(new T[0]);
+ }
+ }
+ public static Sequence<T> FromElements(params T[] values) {
+ return new Sequence<T>(values);
+ }
+ public BigInteger Length {
+ get { return new BigInteger(elmts.Length); }
+ }
+ public T[] Elements {
+ get {
+ return elmts;
+ }
+ }
+ public IEnumerable<T> UniqueElements {
+ get {
+ var st = Set<T>.FromElements(elmts);
+ return st.Elements;
+ }
+ }
+ public T Select(BigInteger index) {
+ return elmts[(int)index];
+ }
+ public Sequence<T> Update(BigInteger index, T t) {
+ T[] a = (T[])elmts.Clone();
+ a[(int)index] = t;
+ return new Sequence<T>(a);
+ }
+ public bool Equals(Sequence<T> other) {
+ int n = elmts.Length;
+ return n == other.elmts.Length && EqualUntil(other, n);
+ }
+ public override bool Equals(object other) {
+ return other is Sequence<T> && Equals((Sequence<T>)other);
+ }
+ public override int GetHashCode() {
+ return elmts.GetHashCode();
+ }
+ bool EqualUntil(Sequence<T> other, int n) {
+ for (int i = 0; i < n; i++) {
+ if (!elmts[i].Equals(other.elmts[i]))
+ return false;
+ }
+ return true;
+ }
+ public bool IsProperPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n < other.elmts.Length && EqualUntil(other, n);
+ }
+ public bool IsPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n <= other.elmts.Length && EqualUntil(other, n);
+ }
+ public Sequence<T> Concat(Sequence<T> other) {
+ if (elmts.Length == 0)
+ return other;
+ else if (other.elmts.Length == 0)
+ return this;
+ T[] a = new T[elmts.Length + other.elmts.Length];
+ System.Array.Copy(elmts, 0, a, 0, elmts.Length);
+ System.Array.Copy(other.elmts, 0, a, elmts.Length, other.elmts.Length);
+ return new Sequence<T>(a);
+ }
+ public bool Contains(T t) {
+ int n = elmts.Length;
+ for (int i = 0; i < n; i++) {
+ if (t.Equals(elmts[i]))
+ return true;
+ }
+ return false;
+ }
+ public Sequence<T> Take(BigInteger n) {
+ int m = (int)n;
+ if (elmts.Length == m)
+ return this;
+ T[] a = new T[m];
+ System.Array.Copy(elmts, a, m);
+ return new Sequence<T>(a);
+ }
+ public Sequence<T> Drop(BigInteger n) {
+ if (n.IsZero)
+ return this;
+ int m = (int)n;
+ T[] a = new T[elmts.Length - m];
+ System.Array.Copy(elmts, m, a, 0, elmts.Length - m);
+ return new Sequence<T>(a);
+ }
+ }
+ public struct Pair<A, B>
+ {
+ public readonly A Car;
+ public readonly B Cdr;
+ public Pair(A a, B b) {
+ this.Car = a;
+ this.Cdr = b;
+ }
+ }
+ public partial class Helpers {
+ // Computing forall/exists quantifiers
+ 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<U>(Dafny.Set<U> set, bool frall, System.Predicate<U> pred) {
+ foreach (var u in set.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantMap<U,V>(Dafny.Map<U,V> map, bool frall, System.Predicate<U> pred) {
+ foreach (var u in map.Domain) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantSeq<U>(Dafny.Sequence<U> seq, bool frall, System.Predicate<U> pred) {
+ foreach (var u in seq.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ // Enumerating other collections
+ public delegate Dafny.Set<T> ComprehensionDelegate<T>();
+ public delegate Dafny.Map<U, V> MapComprehensionDelegate<U, V>();
+ public static IEnumerable<bool> AllBooleans {
+ get {
+ yield return false;
+ yield return true;
+ }
+ }
+ // pre: b != 0
+ // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) {
+ if (0 <= a.Sign) {
+ if (0 <= b.Sign) {
+ // +a +b: a/b
+ return BigInteger.Divide(a, b);
+ } else {
+ // +a -b: -(a/(-b))
+ return BigInteger.Negate(BigInteger.Divide(a, BigInteger.Negate(b)));
+ }
+ } else {
+ if (0 <= b.Sign) {
+ // -a +b: -((-a-1)/b) - 1
+ return BigInteger.Negate(BigInteger.Divide(BigInteger.Negate(a) - 1, b)) - 1;
+ } else {
+ // -a -b: ((-a-1)/(-b)) + 1
+ return BigInteger.Divide(BigInteger.Negate(a) - 1, BigInteger.Negate(b)) + 1;
+ }
+ }
+ }
+ // pre: b != 0
+ // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) {
+ var bp = BigInteger.Abs(b);
+ if (0 <= a.Sign) {
+ // +a: a % b'
+ return BigInteger.Remainder(a, bp);
+ } else {
+ // c = ((-a) % b')
+ // -a: b' - c if c > 0
+ // -a: 0 if c == 0
+ var c = BigInteger.Remainder(BigInteger.Negate(a), bp);
+ return c.IsZero ? c : BigInteger.Subtract(bp, c);
+ }
+ }
+ public static Sequence<T> SeqFromArray<T>(T[] array) {
+ return new Sequence<T>(array);
+ }
+ // In .NET version 4.5, it it possible to mark a method with "AggressiveInlining", which says to inline the
+ // method if possible. Method "ExpressionSequence" would be a good candidate for it:
+ // [System.Runtime.CompilerServices.MethodImpl(System.Runtime.CompilerServices.MethodImplOptions.AggressiveInlining)]
+ public static U ExpressionSequence<T, U>(T t, U u)
+ {
+ return u;
+ }
+ }
+}
+namespace Dafny {
+ public partial class Helpers {
+ public static T[] InitNewArray1<T>(BigInteger size0) {
+ int s0 = (int)size0;
+ T[] a = new T[s0];
+ BigInteger[] b = a as BigInteger[];
+ if (b != null) {
+ BigInteger z = new BigInteger(0);
+ for (int i0 = 0; i0 < s0; i0++)
+ b[i0] = z;
+ }
+ return a;
+ }
+ }
+}
+
+public class @_default {
+ public void @Main()
+ {
+ Contract.Requires(true);
+ }
+ public static void Main(string[] args) {
+ @_default b = new @_default();
+ b.Main();
+ }
+}
+
+-------------------- Precondition1 --------------------
+
+Dafny program verifier finished with 4 verified, 0 errors
+Compiled program written to Precondition1.cs
+Compiled assembly into Precondition1.exe
+Rewrote assembly into Precondition1.exe
+// Dafny program Precondition1.dfy compiled into C#
+
+using System.Diagnostics.Contracts;
+using System.Numerics;
+using System.Collections.Generic;
+
+namespace Dafny
+{
+ public class Set<T>
+ {
+ Dictionary<T, bool> dict;
+ public Set() { }
+ Set(Dictionary<T, bool> d) {
+ dict = d;
+ }
+ public static Set<T> Empty {
+ get {
+ return new Set<T>(new Dictionary<T, bool>(0));
+ }
+ }
+ public static Set<T> FromElements(params T[] values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>(values.Length);
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+ public static Set<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, bool> d = new Dictionary<T, bool>();
+ foreach (T t in values)
+ d[t] = true;
+ return new Set<T>(d);
+ }
+
+ public IEnumerable<T> Elements {
+ get {
+ return dict.Keys;
+ }
+ }
+ public bool Equals(Set<T> other) {
+ return dict.Count == other.dict.Count && IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is Set<T> && Equals((Set<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(Set<T> other) {
+ return dict.Count < other.dict.Count && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(Set<T> other) {
+ if (other.dict.Count < dict.Count)
+ return false;
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(Set<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(Set<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(Set<T> other) {
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public Set<T> Union(Set<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ Dictionary<T, bool> r = new Dictionary<T, bool>();
+ foreach (T t in b.Keys)
+ r[t] = true;
+ foreach (T t in a.Keys)
+ r[t] = true;
+ return new Set<T>(r);
+ }
+ public Set<T> Intersect(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ Dictionary<T, bool> a, b;
+ if (dict.Count < other.dict.Count) {
+ a = dict; b = other.dict;
+ } else {
+ a = other.dict; b = dict;
+ }
+ var r = new Dictionary<T, bool>();
+ foreach (T t in a.Keys) {
+ if (b.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public Set<T> Difference(Set<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, bool>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t))
+ r.Add(t, true);
+ }
+ return new Set<T>(r);
+ }
+ public T Choose() {
+ foreach (T t in dict.Keys) {
+ // return the first one
+ return t;
+ }
+ return default(T);
+ }
+ }
+ public class MultiSet<T>
+ {
+ Dictionary<T, int> dict;
+ public MultiSet() { }
+ MultiSet(Dictionary<T, int> d) {
+ dict = d;
+ }
+ public static MultiSet<T> Empty {
+ get {
+ return new MultiSet<T>(new Dictionary<T, int>(0));
+ }
+ }
+ public static MultiSet<T> FromElements(params T[] values) {
+ Dictionary<T, int> d = new Dictionary<T, int>(values.Length);
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromCollection(ICollection<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSeq(Sequence<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ var i = 0;
+ if (!d.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ d[t] = i + 1;
+ }
+ return new MultiSet<T>(d);
+ }
+ public static MultiSet<T> FromSet(Set<T> values) {
+ Dictionary<T, int> d = new Dictionary<T, int>();
+ foreach (T t in values.Elements) {
+ d[t] = 1;
+ }
+ return new MultiSet<T>(d);
+ }
+
+ public bool Equals(MultiSet<T> other) {
+ return other.IsSubsetOf(this) && this.IsSubsetOf(other);
+ }
+ public override bool Equals(object other) {
+ return other is MultiSet<T> && Equals((MultiSet<T>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsProperSubsetOf(MultiSet<T> other) {
+ return !Equals(other) && IsSubsetOf(other);
+ }
+ public bool IsSubsetOf(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t])
+ return false;
+ }
+ return true;
+ }
+ public bool IsSupersetOf(MultiSet<T> other) {
+ return other.IsSubsetOf(this);
+ }
+ public bool IsProperSupersetOf(MultiSet<T> other) {
+ return other.IsProperSubsetOf(this);
+ }
+ public bool IsDisjointFrom(MultiSet<T> other) {
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t))
+ return false;
+ }
+ foreach (T t in other.dict.Keys) {
+ if (dict.ContainsKey(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
+ }
+ public MultiSet<T> Union(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return other;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + dict[t];
+ }
+ foreach (T t in other.dict.Keys) {
+ var i = 0;
+ if (!r.TryGetValue(t, out i)) {
+ i = 0;
+ }
+ r[t] = i + other.dict[t];
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Intersect(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t)) {
+ r.Add(t, other.dict[t] < dict[t] ? other.dict[t] : dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public MultiSet<T> Difference(MultiSet<T> other) { // \result == this - other
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return this;
+ var r = new Dictionary<T, int>();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t)) {
+ r.Add(t, dict[t]);
+ } else if (other.dict[t] < dict[t]) {
+ r.Add(t, dict[t] - other.dict[t]);
+ }
+ }
+ return new MultiSet<T>(r);
+ }
+ public IEnumerable<T> Elements {
+ get {
+ List<T> l = new List<T>();
+ foreach (T t in dict.Keys) {
+ int n;
+ dict.TryGetValue(t, out n);
+ for (int i = 0; i < n; i ++) {
+ l.Add(t);
+ }
+ }
+ return l;
+ }
+ }
+ }
+
+ public class Map<U, V>
+ {
+ Dictionary<U, V> dict;
+ public Map() { }
+ Map(Dictionary<U, V> d) {
+ dict = d;
+ }
+ public static Map<U, V> Empty {
+ get {
+ return new Map<U, V>(new Dictionary<U,V>());
+ }
+ }
+ public static Map<U, V> FromElements(params Pair<U, V>[] values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Length);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public static Map<U, V> FromCollection(List<Pair<U, V>> values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Count);
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public bool Equals(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ V v1, v2;
+ if (!dict.TryGetValue(u, out v1)) {
+ return false; // this shouldn't happen
+ }
+ if (!other.dict.TryGetValue(u, out v2)) {
+ return false; // other dictionary does not contain this element
+ }
+ if (!v1.Equals(v2)) {
+ return false;
+ }
+ }
+ foreach (U u in other.dict.Keys) {
+ if (!dict.ContainsKey(u)) {
+ return false; // this shouldn't happen
+ }
+ }
+ return true;
+ }
+ public override bool Equals(object other) {
+ return other is Map<U, V> && Equals((Map<U, V>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsDisjointFrom(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ if (other.dict.ContainsKey(u))
+ return false;
+ }
+ foreach (U u in other.dict.Keys) {
+ if (dict.ContainsKey(u))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(U u) {
+ return dict.ContainsKey(u);
+ }
+ public V Select(U index) {
+ return dict[index];
+ }
+ public Map<U, V> Update(U index, V val) {
+ Dictionary<U, V> d = new Dictionary<U, V>(dict);
+ d[index] = val;
+ return new Map<U, V>(d);
+ }
+ public IEnumerable<U> Domain {
+ get {
+ return dict.Keys;
+ }
+ }
+ }
+ public class Sequence<T>
+ {
+ T[] elmts;
+ public Sequence() { }
+ public Sequence(T[] ee) {
+ elmts = ee;
+ }
+ public static Sequence<T> Empty {
+ get {
+ return new Sequence<T>(new T[0]);
+ }
+ }
+ public static Sequence<T> FromElements(params T[] values) {
+ return new Sequence<T>(values);
+ }
+ public BigInteger Length {
+ get { return new BigInteger(elmts.Length); }
+ }
+ public T[] Elements {
+ get {
+ return elmts;
+ }
+ }
+ public IEnumerable<T> UniqueElements {
+ get {
+ var st = Set<T>.FromElements(elmts);
+ return st.Elements;
+ }
+ }
+ public T Select(BigInteger index) {
+ return elmts[(int)index];
+ }
+ public Sequence<T> Update(BigInteger index, T t) {
+ T[] a = (T[])elmts.Clone();
+ a[(int)index] = t;
+ return new Sequence<T>(a);
+ }
+ public bool Equals(Sequence<T> other) {
+ int n = elmts.Length;
+ return n == other.elmts.Length && EqualUntil(other, n);
+ }
+ public override bool Equals(object other) {
+ return other is Sequence<T> && Equals((Sequence<T>)other);
+ }
+ public override int GetHashCode() {
+ return elmts.GetHashCode();
+ }
+ bool EqualUntil(Sequence<T> other, int n) {
+ for (int i = 0; i < n; i++) {
+ if (!elmts[i].Equals(other.elmts[i]))
+ return false;
+ }
+ return true;
+ }
+ public bool IsProperPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n < other.elmts.Length && EqualUntil(other, n);
+ }
+ public bool IsPrefixOf(Sequence<T> other) {
+ int n = elmts.Length;
+ return n <= other.elmts.Length && EqualUntil(other, n);
+ }
+ public Sequence<T> Concat(Sequence<T> other) {
+ if (elmts.Length == 0)
+ return other;
+ else if (other.elmts.Length == 0)
+ return this;
+ T[] a = new T[elmts.Length + other.elmts.Length];
+ System.Array.Copy(elmts, 0, a, 0, elmts.Length);
+ System.Array.Copy(other.elmts, 0, a, elmts.Length, other.elmts.Length);
+ return new Sequence<T>(a);
+ }
+ public bool Contains(T t) {
+ int n = elmts.Length;
+ for (int i = 0; i < n; i++) {
+ if (t.Equals(elmts[i]))
+ return true;
+ }
+ return false;
+ }
+ public Sequence<T> Take(BigInteger n) {
+ int m = (int)n;
+ if (elmts.Length == m)
+ return this;
+ T[] a = new T[m];
+ System.Array.Copy(elmts, a, m);
+ return new Sequence<T>(a);
+ }
+ public Sequence<T> Drop(BigInteger n) {
+ if (n.IsZero)
+ return this;
+ int m = (int)n;
+ T[] a = new T[elmts.Length - m];
+ System.Array.Copy(elmts, m, a, 0, elmts.Length - m);
+ return new Sequence<T>(a);
+ }
+ }
+ public struct Pair<A, B>
+ {
+ public readonly A Car;
+ public readonly B Cdr;
+ public Pair(A a, B b) {
+ this.Car = a;
+ this.Cdr = b;
+ }
+ }
+ public partial class Helpers {
+ // Computing forall/exists quantifiers
+ 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<U>(Dafny.Set<U> set, bool frall, System.Predicate<U> pred) {
+ foreach (var u in set.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantMap<U,V>(Dafny.Map<U,V> map, bool frall, System.Predicate<U> pred) {
+ foreach (var u in map.Domain) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ public static bool QuantSeq<U>(Dafny.Sequence<U> seq, bool frall, System.Predicate<U> pred) {
+ foreach (var u in seq.Elements) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
+ // Enumerating other collections
+ public delegate Dafny.Set<T> ComprehensionDelegate<T>();
+ public delegate Dafny.Map<U, V> MapComprehensionDelegate<U, V>();
+ public static IEnumerable<bool> AllBooleans {
+ get {
+ yield return false;
+ yield return true;
+ }
+ }
+ // pre: b != 0
+ // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) {
+ if (0 <= a.Sign) {
+ if (0 <= b.Sign) {
+ // +a +b: a/b
+ return BigInteger.Divide(a, b);
+ } else {
+ // +a -b: -(a/(-b))
+ return BigInteger.Negate(BigInteger.Divide(a, BigInteger.Negate(b)));
+ }
+ } else {
+ if (0 <= b.Sign) {
+ // -a +b: -((-a-1)/b) - 1
+ return BigInteger.Negate(BigInteger.Divide(BigInteger.Negate(a) - 1, b)) - 1;
+ } else {
+ // -a -b: ((-a-1)/(-b)) + 1
+ return BigInteger.Divide(BigInteger.Negate(a) - 1, BigInteger.Negate(b)) + 1;
+ }
+ }
+ }
+ // pre: b != 0
+ // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) {
+ var bp = BigInteger.Abs(b);
+ if (0 <= a.Sign) {
+ // +a: a % b'
+ return BigInteger.Remainder(a, bp);
+ } else {
+ // c = ((-a) % b')
+ // -a: b' - c if c > 0
+ // -a: 0 if c == 0
+ var c = BigInteger.Remainder(BigInteger.Negate(a), bp);
+ return c.IsZero ? c : BigInteger.Subtract(bp, c);
+ }
+ }
+ public static Sequence<T> SeqFromArray<T>(T[] array) {
+ return new Sequence<T>(array);
+ }
+ // In .NET version 4.5, it it possible to mark a method with "AggressiveInlining", which says to inline the
+ // method if possible. Method "ExpressionSequence" would be a good candidate for it:
+ // [System.Runtime.CompilerServices.MethodImpl(System.Runtime.CompilerServices.MethodImplOptions.AggressiveInlining)]
+ public static U ExpressionSequence<T, U>(T t, U u)
+ {
+ return u;
+ }
+ }
+}
+namespace Dafny {
+ public partial class Helpers {
+ public static T[] InitNewArray1<T>(BigInteger size0) {
+ int s0 = (int)size0;
+ T[] a = new T[s0];
+ BigInteger[] b = a as BigInteger[];
+ if (b != null) {
+ BigInteger z = new BigInteger(0);
+ for (int i0 = 0; i0 < s0; i0++)
+ b[i0] = z;
+ }
+ return a;
+ }
+ }
+}
+
+public class @_default {
+ public void @foo(BigInteger @x, BigInteger @y)
+ {
+ Contract.Requires((new BigInteger(0)) <= (@x));
+ Contract.Requires((@y) <= (new BigInteger(0)));
+ }
+ public void @Main()
+ {
+ (this).@foo(new BigInteger(2), (new BigInteger(0)) - (new BigInteger(7)));
+ }
+ public static void Main(string[] args) {
+ @_default b = new @_default();
+ b.Main();
+ }
+}
diff --git a/Test/dafnyRuntimeChecking/AssertStmt0.dfy b/Test/dafnyRuntimeChecking/AssertStmt0.dfy new file mode 100644 index 00000000..5596e9e9 --- /dev/null +++ b/Test/dafnyRuntimeChecking/AssertStmt0.dfy @@ -0,0 +1,4 @@ +method Main()
+{
+ assert 2 < 10;
+}
diff --git a/Test/dafnyRuntimeChecking/AssertStmt1.dfy b/Test/dafnyRuntimeChecking/AssertStmt1.dfy new file mode 100644 index 00000000..2730e87c --- /dev/null +++ b/Test/dafnyRuntimeChecking/AssertStmt1.dfy @@ -0,0 +1,4 @@ +method Main()
+{
+ assert 10 < 2;
+}
diff --git a/Test/dafnyRuntimeChecking/AssumeStmt0.dfy b/Test/dafnyRuntimeChecking/AssumeStmt0.dfy new file mode 100644 index 00000000..13f58deb --- /dev/null +++ b/Test/dafnyRuntimeChecking/AssumeStmt0.dfy @@ -0,0 +1,4 @@ +method Main()
+{
+ assume 2 < 10;
+}
diff --git a/Test/dafnyRuntimeChecking/AssumeStmt1.dfy b/Test/dafnyRuntimeChecking/AssumeStmt1.dfy new file mode 100644 index 00000000..7a749f51 --- /dev/null +++ b/Test/dafnyRuntimeChecking/AssumeStmt1.dfy @@ -0,0 +1,4 @@ +method Main()
+{
+ assume 10 < 2;
+}
diff --git a/Test/dafnyRuntimeChecking/Precondition0.dfy b/Test/dafnyRuntimeChecking/Precondition0.dfy new file mode 100644 index 00000000..73733bbb --- /dev/null +++ b/Test/dafnyRuntimeChecking/Precondition0.dfy @@ -0,0 +1,3 @@ +method Main()
+ requires true;
+{}
diff --git a/Test/dafnyRuntimeChecking/Precondition1.dfy b/Test/dafnyRuntimeChecking/Precondition1.dfy new file mode 100644 index 00000000..1732b0bc --- /dev/null +++ b/Test/dafnyRuntimeChecking/Precondition1.dfy @@ -0,0 +1,9 @@ +method foo(x: int, y: int)
+ requires 0 <= x;
+ requires y <= 0;
+{}
+
+method Main()
+{
+ foo(2, -7);
+}
diff --git a/Test/dafnyRuntimeChecking/runtest.bat b/Test/dafnyRuntimeChecking/runtest.bat new file mode 100644 index 00000000..5def269e --- /dev/null +++ b/Test/dafnyRuntimeChecking/runtest.bat @@ -0,0 +1,15 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+for %%f in (AssumeStmt0 AssumeStmt1 AssertStmt0 AssertStmt1
+ Precondition0 Precondition1) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /nologo /errorTrace:0 /runtimeChecking:1 /compile:2 /spillTargetCode:1 %* %%f.dfy
+ type %%f.cs
+ del %%f.cs %%f.exe %%f.pdb %%f.pdb.original
+)
diff --git a/Test/dafnytests.txt b/Test/dafnytests.txt index 2b457c91..ebb51203 100644 --- a/Test/dafnytests.txt +++ b/Test/dafnytests.txt @@ -1,7 +1,8 @@ -dafny0 Use Dafny functionality tests
-dafny1 Use Various Dafny examples
-dafny2 Use More Dafny examples
-VSI-Benchmarks Use Solutions to Verified Software Initiative verification challenges
-vacid0 Use Dafny attempts to VACID Edition 0 benchmarks
-vstte2012 Use Dafny solutions for the VSTTE 2012 program verification competition
-VSComp2010 Use Dafny solutions to VSComp (verified software competition) problems
+dafny0 Use Dafny functionality tests
+dafny1 Use Various Dafny examples
+dafny2 Use More Dafny examples
+dafnyRuntimeChecking Use Dafny runtime checking tests
+VSI-Benchmarks Use Solutions to Verified Software Initiative verification challenges
+vacid0 Use Dafny attempts to VACID Edition 0 benchmarks
+vstte2012 Use Dafny solutions for the VSTTE 2012 program verification competition
+VSComp2010 Use Dafny solutions to VSComp (verified software competition) problems
|