diff options
| -rw-r--r-- | Binaries/DafnyRuntime.cs | 221 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.ssc | 6 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 3 | ||||
| -rw-r--r-- | Test/dafny0/Modules0.dfy | 16 | ||||
| -rw-r--r-- | Test/dafny0/SumOfCubes.dfy | 2 |
5 files changed, 243 insertions, 5 deletions
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs new file mode 100644 index 00000000..982683b9 --- /dev/null +++ b/Binaries/DafnyRuntime.cs @@ -0,0 +1,221 @@ +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.Add(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;
+ }
+ Dictionary<T, bool> 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;
+ Dictionary<T, bool> 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 class Sequence<T>
+ {
+ T[] elmts;
+ public Sequence() { }
+ 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 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;
+ }
+ }
+}
diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc index e0efaa3c..5b672b17 100644 --- a/Source/Dafny/Resolver.ssc +++ b/Source/Dafny/Resolver.ssc @@ -978,7 +978,7 @@ namespace Microsoft.Dafny { // resolve any local variables declared here
foreach (AutoVarDecl local in s.NewVars) {
// first, fix up the local variables to be ghost variable if the corresponding formal out-parameter is a ghost
- if (callee != null && local.Index < callee.Outs.Count && callee.Outs[local.Index].IsGhost) {
+ if (s.IsGhost || callee != null && local.Index < callee.Outs.Count && callee.Outs[local.Index].IsGhost) {
local.MakeGhost();
}
ResolveStatement(local, specContextOnly, method);
@@ -997,7 +997,7 @@ namespace Microsoft.Dafny { // resolve arguments
int j = 0;
foreach (Expression e in s.Args) {
- bool allowGhost = callee == null || callee.Ins.Count <= j || callee.Ins[j].IsGhost;
+ bool allowGhost = s.IsGhost || callee == null || callee.Ins.Count <= j || callee.Ins[j].IsGhost;
ResolveExpression(e, true, allowGhost);
j++;
}
@@ -1036,7 +1036,7 @@ namespace Microsoft.Dafny { IdentifierExpr lhs = s.Lhs[i];
if (!UnifyTypes((!)lhs.Type, st)) {
Error(s, "incorrect type of method out-parameter {0} (expected {1}, got {2})", i, st, lhs.Type);
- } else if (!specContextOnly && !((!)lhs.Var).IsGhost && callee.Outs[i].IsGhost) {
+ } else if (!specContextOnly && !((!)lhs.Var).IsGhost && (s.IsGhost || callee.Outs[i].IsGhost)) {
Error(s, "actual out-parameter {0} is required to be a ghost variable", i);
}
}
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 7ac8ff37..726a6c13 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -273,7 +273,8 @@ Modules0.dfy(51,6): Error: inter-module calls must follow the module import rela Modules0.dfy(62,6): Error: inter-module calls must follow the module import relation (so module X1 must transitively import X2)
Modules0.dfy(72,6): Error: inter-module calls must follow the module import relation (so module X0 must transitively import X1)
Modules0.dfy(91,4): Error: inter-module calls must follow the module import relation (so module _default must transitively import YY)
-7 resolution/type errors detected in Modules0.dfy
+Modules0.dfy(116,16): Error: ghost variables are allowed only in specification contexts
+8 resolution/type errors detected in Modules0.dfy
-------------------- Modules1.dfy --------------------
Modules1.dfy(55,3): Error: decreases expression must be bounded below by 0
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy index 0e0d3ab3..3e8d1e25 100644 --- a/Test/dafny0/Modules0.dfy +++ b/Test/dafny0/Modules0.dfy @@ -104,3 +104,19 @@ method ProcG(g: ClassG) { call g.T(); // allowed: intra-module call
var t := g.TFunc(); // allowed: intra-module call
}
+
+// ---------------------- some ghost stuff ------------------------
+
+class Ghosty {
+ method Caller() {
+ var x := 3;
+ ghost var y := 3;
+ call Callee(x, y); // fine
+ call Callee(x, x); // fine
+ call Callee(y, x); // error: cannot pass in ghost to a physical formal
+ call Theorem(x); // fine
+ call Theorem(y); // fine, because it's a ghost method
+ }
+ method Callee(a: int, ghost b: int) { }
+ ghost method Theorem(a: int) { }
+}
diff --git a/Test/dafny0/SumOfCubes.dfy b/Test/dafny0/SumOfCubes.dfy index f3359778..e5fe9473 100644 --- a/Test/dafny0/SumOfCubes.dfy +++ b/Test/dafny0/SumOfCubes.dfy @@ -49,7 +49,7 @@ class SumOfCubes { if k == 0 then 0 else GSum(k-1) + k-1
}
- ghost static method Gauss(k: int) returns (r: int)
+ static method Gauss(k: int) returns (r: int)
requires 0 <= k;
ensures r == GSum(k);
{
|