Dafny: Added CC translation of postconditions.

9 files changed, 1258 insertions, 3 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 93860cc6..afab0c1f 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -575,6 +575,7 @@ namespace Microsoft.Dafny {
             wr.WriteLine(")");

             Indent(indent);  wr.WriteLine("{");

             TrReq(m.Req, indent + IndentAmount);

+            TrEns(m.Ens, indent + IndentAmount);

             foreach (Formal p in m.Outs) {

               if (!p.IsGhost) {

                 Indent(indent + IndentAmount);

@@ -2243,6 +2244,25 @@ namespace Microsoft.Dafny {
       }

     }

 

+    void TrEns(List<MaybeFreeExpression/*!*/>/*!*/ ens, int indent)

+    {

+      Contract.Requires(cce.NonNullElements(ens));

+

+      if (DafnyOptions.O.RuntimeChecking)

+      {

+        foreach (MaybeFreeExpression e in ens)

+        {

+          if (!e.IsFree)

+          {

+            Indent(indent);

+            wr.Write("Contract.Ensures(");

+            TrExpr(e.E);

+            wr.WriteLine(");");

+          }

+        }

+      }

+    }

+

     #endregion

 

     #region Runtime checking helper methods

diff --git a/Test/dafnyRuntimeChecking/Answer b/Test/dafnyRuntimeChecking/Answer
index 18a96d8f..6bda12af 100644
--- a/Test/dafnyRuntimeChecking/Answer
+++ b/Test/dafnyRuntimeChecking/Answer
@@ -3609,3 +3609,1210 @@ public class @_default {
     b.Main();

   }

 }

+

+-------------------- Postcondition0 --------------------

+Compiled program written to Postcondition0.cs

+Compiled assembly into Postcondition0.exe

+Rewrote assembly into Postcondition0.exe

+// Dafny program Postcondition0.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.Ensures(true);

+  }

+  public static void Main(string[] args) {

+    @_default b = new @_default();

+    b.Main();

+  }

+}

+

+-------------------- Postcondition1 --------------------

+Compiled program written to Postcondition1.cs

+Compiled assembly into Postcondition1.exe

+Rewrote assembly into Postcondition1.exe

+// Dafny program Postcondition1.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 BigInteger @x = new BigInteger(0);

+  public BigInteger @y = new BigInteger(0);

+  public void @Main()

+  {

+    Contract.Ensures((new BigInteger(0)) <= ((this).@x));

+    Contract.Ensures(((this).@y) <= (new BigInteger(0)));

+    (this).@x = new BigInteger(2);

+    (this).@y = (new BigInteger(0)) - (new BigInteger(7));

+  }

+  public static void Main(string[] args) {

+    @_default b = new @_default();

+    b.Main();

+  }

+}

diff --git a/Test/dafnyRuntimeChecking/AnswerNoRuntimeChecking b/Test/dafnyRuntimeChecking/AnswerNoRuntimeChecking
index 8bc5937f..6fffd815 100644
--- a/Test/dafnyRuntimeChecking/AnswerNoRuntimeChecking
+++ b/Test/dafnyRuntimeChecking/AnswerNoRuntimeChecking
@@ -16,3 +16,9 @@ Compiled assembly into Precondition0.exe
 

 -------------------- Precondition1 --------------------

 Compiled assembly into Precondition1.exe

+

+-------------------- Postcondition0 --------------------

+Compiled assembly into Postcondition0.exe

+

+-------------------- Postcondition1 --------------------

+Compiled assembly into Postcondition1.exe

diff --git a/Test/dafnyRuntimeChecking/AnswerRuntimeChecking b/Test/dafnyRuntimeChecking/AnswerRuntimeChecking
index 56f57f20..860dc843 100644
--- a/Test/dafnyRuntimeChecking/AnswerRuntimeChecking
+++ b/Test/dafnyRuntimeChecking/AnswerRuntimeChecking
@@ -22,3 +22,11 @@ Rewrote assembly into Precondition0.exe
 -------------------- Precondition1 --------------------

 Compiled assembly into Precondition1.exe

 Rewrote assembly into Precondition1.exe

+

+-------------------- Postcondition0 --------------------

+Compiled assembly into Postcondition0.exe

+Rewrote assembly into Postcondition0.exe

+

+-------------------- Postcondition1 --------------------

+Compiled assembly into Postcondition1.exe

+Rewrote assembly into Postcondition1.exe

diff --git a/Test/dafnyRuntimeChecking/Postcondition0.dfy b/Test/dafnyRuntimeChecking/Postcondition0.dfy
new file mode 100644
index 00000000..5b61988c
--- /dev/null
+++ b/Test/dafnyRuntimeChecking/Postcondition0.dfy
@@ -0,0 +1,3 @@
+method Main()

+  ensures true;

+{}

diff --git a/Test/dafnyRuntimeChecking/Postcondition1.dfy b/Test/dafnyRuntimeChecking/Postcondition1.dfy
new file mode 100644
index 00000000..0969c51d
--- /dev/null
+++ b/Test/dafnyRuntimeChecking/Postcondition1.dfy
@@ -0,0 +1,11 @@
+var x: int;

+var y: int;

+

+method Main()

+  modifies this`x, this`y;

+  ensures 0 <= x;

+  ensures y <= 0;

+{

+  x := 2;

+  y := -7;

+}

diff --git a/Test/dafnyRuntimeChecking/runtest.bat b/Test/dafnyRuntimeChecking/runtest.bat
index f874624f..3e434f49 100644
--- a/Test/dafnyRuntimeChecking/runtest.bat
+++ b/Test/dafnyRuntimeChecking/runtest.bat
@@ -6,7 +6,7 @@ set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
 set BPLEXE=%BOOGIEDIR%\Boogie.exe

 

 for %%f in (AssumeStmt0 AssumeStmt1 AssertStmt0 AssertStmt1

-    Precondition0 Precondition1) do (

+    Precondition0 Precondition1 Postcondition0 Postcondition1) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 /spillTargetCode:1 %* %%f.dfy

diff --git a/Test/dafnyRuntimeChecking/runtestNoRuntimeChecking.bat b/Test/dafnyRuntimeChecking/runtestNoRuntimeChecking.bat
index 3edaf517..e336e022 100644
--- a/Test/dafnyRuntimeChecking/runtestNoRuntimeChecking.bat
+++ b/Test/dafnyRuntimeChecking/runtestNoRuntimeChecking.bat
@@ -6,7 +6,7 @@ set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
 set BPLEXE=%BOOGIEDIR%\Boogie.exe

 

 for %%f in (AssumeStmt0 AssumeStmt1 AssertStmt0 AssertStmt1

-    Precondition0 Precondition1) do (

+    Precondition0 Precondition1 Postcondition0 Postcondition1) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy

diff --git a/Test/dafnyRuntimeChecking/runtestRuntimeChecking.bat b/Test/dafnyRuntimeChecking/runtestRuntimeChecking.bat
index 07f7fb57..6b086f6f 100644
--- a/Test/dafnyRuntimeChecking/runtestRuntimeChecking.bat
+++ b/Test/dafnyRuntimeChecking/runtestRuntimeChecking.bat
@@ -6,7 +6,7 @@ set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
 set BPLEXE=%BOOGIEDIR%\Boogie.exe

 

 for %%f in (AssumeStmt0 AssumeStmt1 AssertStmt0 AssertStmt1

-    Precondition0 Precondition1) do (

+    Precondition0 Precondition1 Postcondition0 Postcondition1) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy