diff options
| -rw-r--r-- | Binaries/DafnyRuntime.cs | 506 | ||||
| -rw-r--r-- | Source/Dafny/DafnyOptions.cs | 12 | ||||
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 13 | ||||
| -rw-r--r-- | Test/irondafny0/optimize0.dfy | 6 | ||||
| -rw-r--r-- | Test/irondafny0/optimize0.dfy.expect | 6 |
5 files changed, 485 insertions, 58 deletions
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index fd680a0b..7d3799d8 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -4,39 +4,430 @@ using System.Numerics; namespace Dafny
{
using System.Collections.Generic;
+// set this option if you want to use System.Collections.Immutable and if you know what you're doing.
+#if DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE
+ using System.Collections.Immutable;
+ using System.Linq;
public class Set<T>
{
- Dictionary<T, bool> dict;
- Set(Dictionary<T, bool> d) {
+ readonly ImmutableHashSet<T> setImpl;
+ Set(ImmutableHashSet<T> d) {
+ this.setImpl = d;
+ }
+ public static readonly Set<T> Empty = new Set<T>(ImmutableHashSet<T>.Empty);
+ public static Set<T> FromElements(params T[] values) {
+ return FromElements((IEnumerable<T>)values);
+ }
+ public static Set<T> FromElements(IEnumerable<T> values) {
+ var d = ImmutableHashSet<T>.Empty.ToBuilder();
+ foreach (T t in values)
+ d.Add(t);
+ return new Set<T>(d.ToImmutable());
+ }
+ public static Set<T> FromCollection(ICollection<T> values) {
+ var d = ImmutableHashSet<T>.Empty.ToBuilder();
+ foreach (T t in values)
+ d.Add(t);
+ return new Set<T>(d.ToImmutable());
+ }
+ public int Length {
+ get { return this.setImpl.Count; }
+ }
+ public long LongLength {
+ get { return this.setImpl.Count; }
+ }
+ public IEnumerable<T> Elements {
+ get {
+ return this.setImpl;
+ }
+ }
+ /// <summary>
+ /// This is an inefficient iterator for producing all subsets of "this". Each set returned is the same
+ /// Set<T> object (but this Set<T> object is fresh; in particular, it is not "this").
+ /// </summary>
+ public IEnumerable<Set<T>> AllSubsets {
+ get {
+ // Start by putting all set elements into a list
+ var elmts = new List<T>();
+ elmts.AddRange(this.setImpl);
+ var n = elmts.Count;
+ var which = new bool[n];
+ var s = ImmutableHashSet<T>.Empty.ToBuilder();
+ while (true) {
+ yield return new Set<T>(s.ToImmutable());
+ // "add 1" to "which", as if doing a carry chain. For every digit changed, change the membership of the corresponding element in "s".
+ int i = 0;
+ for (; i < n && which[i]; i++) {
+ which[i] = false;
+ s.Remove(elmts[i]);
+ }
+ if (i == n) {
+ // we have cycled through all the subsets
+ break;
+ }
+ which[i] = true;
+ s.Add(elmts[i]);
+ }
+ }
+ }
+ public bool Equals(Set<T> other) {
+ return this.setImpl.Equals(other.setImpl);
+ }
+ public override bool Equals(object other) {
+ var otherSet = other as Set<T>;
+ return otherSet != null && Equals(otherSet);
+ }
+ public override int GetHashCode() {
+ var hashCode = 1;
+ foreach (var t in this.setImpl) {
+ hashCode = hashCode * (t.GetHashCode()+3);
+ }
+ return hashCode;
+ }
+ public override string ToString() {
+ var s = "{";
+ var sep = "";
+ foreach (var t in this.setImpl) {
+ s += sep + t.ToString();
+ sep = ", ";
+ }
+ return s + "}";
+ }
+ public bool IsProperSubsetOf(Set<T> other) {
+ return IsProperSubsetOf(other);
+ }
+ public bool IsSubsetOf(Set<T> other) {
+ return IsSubsetOf(other);
+ }
+ public bool IsSupersetOf(Set<T> other) {
+ return other.IsSupersetOf(this);
+ }
+ public bool IsProperSupersetOf(Set<T> other) {
+ return other.IsProperSupersetOf(this);
+ }
+ public bool IsDisjointFrom(Set<T> other) {
+ ImmutableHashSet<T> a, b;
+ if (this.setImpl.Count < other.setImpl.Count) {
+ a = this.setImpl; b = other.setImpl;
+ } else {
+ a = other.setImpl; b = this.setImpl;
+ }
+ foreach (T t in a) {
+ if (b.Contains(t))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(T t) {
+ return this.setImpl.Contains(t);
+ }
+ public Set<T> Union(Set<T> other) {
+ return new Set<T>(this.setImpl.Union(other.setImpl));
+ }
+ public Set<T> Intersect(Set<T> other) {
+ return new Set<T>(this.setImpl.Intersect(other.setImpl));
+ }
+ public Set<T> Difference(Set<T> other) {
+ return new Set<T>(this.setImpl.Except(other.setImpl));
+ }
+ }
+ public partial class MultiSet<T>
+ {
+
+ readonly ImmutableDictionary<T, int> dict;
+ MultiSet(ImmutableDictionary<T, int> d) {
dict = d;
}
+ public static readonly MultiSet<T> Empty = new MultiSet<T>(ImmutableDictionary<T, int>.Empty);
+ public static MultiSet<T> FromElements(params T[] values) {
+ var d = ImmutableDictionary<T, int>.Empty.ToBuilder();
+ 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.ToImmutable());
+ }
+ public static MultiSet<T> FromCollection(ICollection<T> values) {
+ var d = ImmutableDictionary<T, int>.Empty.ToBuilder();
+ 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.ToImmutable());
+ }
+ public static MultiSet<T> FromSeq(Sequence<T> values) {
+ var d = ImmutableDictionary<T, int>.Empty.ToBuilder();
+ 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.ToImmutable());
+ }
+ public static MultiSet<T> FromSet(Set<T> values) {
+ var d = ImmutableDictionary<T, int>.Empty.ToBuilder();
+ foreach (T t in values.Elements) {
+ d[t] = 1;
+ }
+ return new MultiSet<T>(d.ToImmutable());
+ }
+
+ 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() {
+ var hashCode = 1;
+ foreach (var kv in dict) {
+ var key = kv.Key.GetHashCode();
+ key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode();
+ hashCode = hashCode * (key + 3);
+ }
+ return hashCode;
+ }
+ public override string ToString() {
+ var s = "multiset{";
+ var sep = "";
+ foreach (var kv in dict) {
+ var t = kv.Key.ToString();
+ for (int i = 0; i < kv.Value; i++) {
+ s += sep + t.ToString();
+ sep = ", ";
+ }
+ }
+ return s + "}";
+ }
+ 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 = ImmutableDictionary<T, int>.Empty.ToBuilder();
+ 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.ToImmutable());
+ }
+ public MultiSet<T> Intersect(MultiSet<T> other) {
+ if (dict.Count == 0)
+ return this;
+ else if (other.dict.Count == 0)
+ return other;
+ var r = ImmutableDictionary<T, int>.Empty.ToBuilder();
+ foreach (T t in dict.Keys) {
+ if (other.dict.ContainsKey(t)) {
+ r[t] = other.dict[t] < dict[t] ? other.dict[t] : dict[t];
+ }
+ }
+ return new MultiSet<T>(r.ToImmutable());
+ }
+ 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 = ImmutableDictionary<T, int>.Empty.ToBuilder();
+ foreach (T t in dict.Keys) {
+ if (!other.dict.ContainsKey(t)) {
+ r[t] = dict[t];
+ } else if (other.dict[t] < dict[t]) {
+ r[t] = dict[t] - other.dict[t];
+ }
+ }
+ return new MultiSet<T>(r.ToImmutable());
+ }
+ public IEnumerable<T> Elements {
+ get {
+ foreach (T t in dict.Keys) {
+ int n;
+ dict.TryGetValue(t, out n);
+ for (int i = 0; i < n; i ++) {
+ yield return t;
+ }
+ }
+ }
+ }
+ }
+
+ public partial class Map<U, V>
+ {
+ readonly ImmutableDictionary<U, V> dict;
+ Map(ImmutableDictionary<U, V> d) {
+ dict = d;
+ }
+ public static readonly Map<U, V> Empty = new Map<U, V>(ImmutableDictionary<U, V>.Empty);
+ public static Map<U, V> FromElements(params Pair<U, V>[] values) {
+ var d = ImmutableDictionary<U, V>.Empty.ToBuilder();
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d.ToImmutable());
+ }
+ public static Map<U, V> FromCollection(List<Pair<U, V>> values) {
+ var d = ImmutableDictionary<U, V>.Empty.ToBuilder();
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d.ToImmutable());
+ }
+ public int Length {
+ get { return dict.Count; }
+ }
+ public long LongLength {
+ get { return dict.Count; }
+ }
+ 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() {
+ var hashCode = 1;
+ foreach (var kv in dict) {
+ var key = kv.Key.GetHashCode();
+ key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode();
+ hashCode = hashCode * (key + 3);
+ }
+ return hashCode;
+ }
+ public override string ToString() {
+ var s = "map[";
+ var sep = "";
+ foreach (var kv in dict) {
+ s += sep + kv.Key.ToString() + " := " + kv.Value.ToString();
+ sep = ", ";
+ }
+ return s + "]";
+ }
+ 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) {
+ return new Map<U, V>(dict.SetItem(index, val));
+ }
+ public IEnumerable<U> Domain {
+ get {
+ return dict.Keys;
+ }
+ }
+ }
+#else // !def DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE
+ public class Set<T>
+ {
+ HashSet<T> set;
+ Set(HashSet<T> s) {
+ this.set = s;
+ }
public static Set<T> Empty {
get {
- return new Set<T>(new Dictionary<T, bool>(0));
+ return new Set<T>(new HashSet<T>());
}
}
public static Set<T> FromElements(params T[] values) {
- Dictionary<T, bool> d = new Dictionary<T, bool>(values.Length);
+ var s = new HashSet<T>();
foreach (T t in values)
- d[t] = true;
- return new Set<T>(d);
+ s.Add(t);
+ return new Set<T>(s);
}
public static Set<T> FromCollection(ICollection<T> values) {
- Dictionary<T, bool> d = new Dictionary<T, bool>();
+ HashSet<T> s = new HashSet<T>();
foreach (T t in values)
- d[t] = true;
- return new Set<T>(d);
+ s.Add(t);
+ return new Set<T>(s);
}
public int Length {
- get { return dict.Count; }
+ get { return this.set.Count; }
}
public long LongLength {
- get { return dict.Count; }
+ get { return this.set.Count; }
}
public IEnumerable<T> Elements {
get {
- return dict.Keys;
+ return this.set;
}
}
/// <summary>
@@ -47,36 +438,36 @@ namespace Dafny get {
// Start by putting all set elements into a list
var elmts = new List<T>();
- elmts.AddRange(dict.Keys);
+ elmts.AddRange(this.set);
var n = elmts.Count;
var which = new bool[n];
- var s = new Set<T>(new Dictionary<T, bool>(0));
+ var s = new Set<T>(new HashSet<T>());
while (true) {
yield return s;
// "add 1" to "which", as if doing a carry chain. For every digit changed, change the membership of the corresponding element in "s".
int i = 0;
for (; i < n && which[i]; i++) {
which[i] = false;
- s.dict.Remove(elmts[i]);
+ s.set.Remove(elmts[i]);
}
if (i == n) {
// we have cycled through all the subsets
break;
}
which[i] = true;
- s.dict.Add(elmts[i], true);
+ s.set.Add(elmts[i]);
}
}
}
public bool Equals(Set<T> other) {
- return dict.Count == other.dict.Count && IsSubsetOf(other);
+ return this.set.Count == other.set.Count && IsSubsetOf(other);
}
public override bool Equals(object other) {
return other is Set<T> && Equals((Set<T>)other);
}
public override int GetHashCode() {
var hashCode = 1;
- foreach (var t in dict.Keys) {
+ foreach (var t in this.set) {
hashCode = hashCode * (t.GetHashCode()+3);
}
return hashCode;
@@ -84,20 +475,20 @@ namespace Dafny public override string ToString() {
var s = "{";
var sep = "";
- foreach (var t in dict.Keys) {
+ foreach (var t in this.set) {
s += sep + t.ToString();
sep = ", ";
}
return s + "}";
}
public bool IsProperSubsetOf(Set<T> other) {
- return dict.Count < other.dict.Count && IsSubsetOf(other);
+ return this.set.Count < other.set.Count && IsSubsetOf(other);
}
public bool IsSubsetOf(Set<T> other) {
- if (other.dict.Count < dict.Count)
+ if (other.set.Count < this.set.Count)
return false;
- foreach (T t in dict.Keys) {
- if (!other.dict.ContainsKey(t))
+ foreach (T t in this.set) {
+ if (!other.set.Contains(t))
return false;
}
return true;
@@ -109,66 +500,66 @@ namespace Dafny 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;
+ HashSet<T> a, b;
+ if (this.set.Count < other.set.Count) {
+ a = this.set; b = other.set;
} else {
- a = other.dict; b = dict;
+ a = other.set; b = this.set;
}
- foreach (T t in a.Keys) {
- if (b.ContainsKey(t))
+ foreach (T t in a) {
+ if (b.Contains(t))
return false;
}
return true;
}
public bool Contains(T t) {
- return dict.ContainsKey(t);
+ return this.set.Contains(t);
}
public Set<T> Union(Set<T> other) {
- if (dict.Count == 0)
+ if (this.set.Count == 0)
return other;
- else if (other.dict.Count == 0)
+ else if (other.set.Count == 0)
return this;
- Dictionary<T, bool> a, b;
- if (dict.Count < other.dict.Count) {
- a = dict; b = other.dict;
+ HashSet<T> a, b;
+ if (this.set.Count < other.set.Count) {
+ a = this.set; b = other.set;
} else {
- a = other.dict; b = dict;
+ a = other.set; b = this.set;
}
- 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;
+ var r = new HashSet<T>();
+ foreach (T t in b)
+ r.Add(t);
+ foreach (T t in a)
+ r.Add(t);
return new Set<T>(r);
}
public Set<T> Intersect(Set<T> other) {
- if (dict.Count == 0)
+ if (this.set.Count == 0)
return this;
- else if (other.dict.Count == 0)
+ else if (other.set.Count == 0)
return other;
- Dictionary<T, bool> a, b;
- if (dict.Count < other.dict.Count) {
- a = dict; b = other.dict;
+ HashSet<T> a, b;
+ if (this.set.Count < other.set.Count) {
+ a = this.set; b = other.set;
} else {
- a = other.dict; b = dict;
+ a = other.set; b = this.set;
}
- var r = new Dictionary<T, bool>();
- foreach (T t in a.Keys) {
- if (b.ContainsKey(t))
- r.Add(t, true);
+ var r = new HashSet<T>();
+ foreach (T t in a) {
+ if (b.Contains(t))
+ r.Add(t);
}
return new Set<T>(r);
}
public Set<T> Difference(Set<T> other) {
- if (dict.Count == 0)
+ if (this.set.Count == 0)
return this;
- else if (other.dict.Count == 0)
+ else if (other.set.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);
+ var r = new HashSet<T>();
+ foreach (T t in this.set) {
+ if (!other.set.Contains(t))
+ r.Add(t);
}
return new Set<T>(r);
}
@@ -447,6 +838,7 @@ namespace Dafny }
}
}
+#endif
public class Sequence<T>
{
T[] elmts;
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index a6827d5f..125ab11e 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -55,6 +55,7 @@ namespace Microsoft.Dafny public bool ignoreAutoReq = false;
public bool AllowGlobals = false;
public bool CountVerificationErrors = true;
+ public bool Optimize = false;
protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {
var args = ps.args; // convenient synonym
@@ -180,6 +181,11 @@ namespace Microsoft.Dafny return true;
}
+ case "optimize": {
+ Optimize = true;
+ return true;
+ }
+
default:
break;
}
@@ -270,6 +276,12 @@ namespace Microsoft.Dafny of verification errors.
1 (default) - If preprocessing succeeds, set exit code to the number of
verification errors.
+ /optimize Produce optimized C# code, meaning:
+ - selects optimized C# prelude by passing
+ /define:DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE to csc.exe (requires
+ System.Collections.Immutable.dll in the source directory to successfully
+ compile).
+ - passes /optimize flag to csc.exe.
");
base.Usage(); // also print the Boogie options
}
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index a769b829..cf464754 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -15,6 +15,8 @@ namespace Microsoft.Dafny using System.Collections.Generic;
using System.Diagnostics.Contracts;
using System.IO;
+ using System.Reflection;
+
using Microsoft.Boogie;
using Bpl = Microsoft.Boogie;
@@ -330,7 +332,7 @@ namespace Microsoft.Dafny }
else
{
- var provider = CodeDomProvider.CreateProvider("CSharp");
+ var provider = CodeDomProvider.CreateProvider("CSharp", new Dictionary<string, string> { { "CompilerVersion", "v4.0" } });
var cp = new System.CodeDom.Compiler.CompilerParameters();
cp.GenerateExecutable = hasMain;
if (DafnyOptions.O.RunAfterCompile) {
@@ -344,6 +346,15 @@ namespace Microsoft.Dafny }
cp.CompilerOptions = "/debug /nowarn:0164 /nowarn:0219"; // warning CS0164 complains about unreferenced labels, CS0219 is about unused variables
cp.ReferencedAssemblies.Add("System.Numerics.dll");
+ cp.ReferencedAssemblies.Add("System.Core.dll");
+ cp.ReferencedAssemblies.Add("System.dll");
+
+ if (DafnyOptions.O.Optimize) {
+ var libPath = Path.GetDirectoryName(dafnyProgramName);
+ cp.CompilerOptions += string.Format(" /optimize /define:DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE /lib:{0}", libPath);
+ cp.ReferencedAssemblies.Add("System.Collections.Immutable.dll");
+ cp.ReferencedAssemblies.Add("System.Runtime.dll");
+ }
var cr = provider.CompileAssemblyFromSource(cp, csharpProgram);
var assemblyName = Path.GetFileName(cr.PathToAssembly);
diff --git a/Test/irondafny0/optimize0.dfy b/Test/irondafny0/optimize0.dfy new file mode 100644 index 00000000..865d8707 --- /dev/null +++ b/Test/irondafny0/optimize0.dfy @@ -0,0 +1,6 @@ +// RUN: %dafny /compile:3 /optimize /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Main() {
+ print "o hai!";
+}
diff --git a/Test/irondafny0/optimize0.dfy.expect b/Test/irondafny0/optimize0.dfy.expect new file mode 100644 index 00000000..6b3e13c5 --- /dev/null +++ b/Test/irondafny0/optimize0.dfy.expect @@ -0,0 +1,6 @@ +
+Dafny program verifier finished with 2 verified, 0 errors
+Program compiled successfully
+Running...
+
+o hai!
\ No newline at end of file |