diff options
| -rw-r--r-- | Source/Dafny/Resolver.ssc | 8 | ||||
| -rw-r--r-- | Source/Dafny/Translator.ssc | 7 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny0/Refinement.dfy | 78 |
4 files changed, 89 insertions, 6 deletions
diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc index 3c206066..96ae33c6 100644 --- a/Source/Dafny/Resolver.ssc +++ b/Source/Dafny/Resolver.ssc @@ -173,7 +173,6 @@ namespace Microsoft.Dafny { }
decl.Refined = (ClassDecl!) a;
// TODO: copy over remaining members of a
- // TODO: extend with type parameters for refinements
}
}
@@ -469,6 +468,13 @@ namespace Microsoft.Dafny { }
void ResolveTypeParameters(List<TypeParameter!>! tparams, bool emitErrors, TypeParameter.ParentType! parent) {
+ // push type arguments of the refined class
+ if (parent is ClassRefinementDecl) {
+ ClassDecl refined = ((ClassRefinementDecl)parent).Refined;
+ assert refined != null;
+ ResolveTypeParameters(refined.TypeArgs, false, refined);
+ }
+
// push non-duplicated type parameter names
foreach (TypeParameter tp in tparams) {
if (emitErrors) {
diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc index f6fc5142..ff88c67f 100644 --- a/Source/Dafny/Translator.ssc +++ b/Source/Dafny/Translator.ssc @@ -1797,12 +1797,13 @@ namespace Microsoft.Dafny { // assume I($Heap, $Heap)
builder.Add(new Bpl.AssumeCmd(m.tok, TrCouplingInvariant(m, heap, "this", heap, that)));
- // assign input formals of m
+ // assign input formals of m (except "this")
for (int i = 0; i < m.Ins.Count; i++) {
Bpl.LocalVariable arg = new Bpl.LocalVariable(m.tok, new Bpl.TypedIdent(m.tok, m.Ins[i].UniqueName, TrType(m.Ins[i].Type)));
localVariables.Add(arg);
- assert inParams[i+1] != null;
- builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, arg), new Bpl.IdentifierExpr(m.tok, inParams[i+1])));
+ Bpl.Variable var = inParams[i+1];
+ assert var != null;
+ builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, arg), new Bpl.IdentifierExpr(m.tok, var)));
}
// call inlined m;
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index c56c2aeb..3de8e9e9 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -450,4 +450,4 @@ Dafny program verifier finished with 5 verified, 0 errors -------------------- Refinement.dfy --------------------
-Dafny program verifier finished with 39 verified, 0 errors
+Dafny program verifier finished with 54 verified, 0 errors
diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy index c70df916..205f3b6c 100644 --- a/Test/dafny0/Refinement.dfy +++ b/Test/dafny0/Refinement.dfy @@ -1,5 +1,5 @@ // Concrete language syntax for a Dafny extension with refinement. -// Counter example. +// IntegerCounter example. // 6/28/2010 class A { @@ -112,6 +112,82 @@ class CCalc refines ACalc { } } +// Sequence refined to a singly linked list +// 6/22/2010: Kuat Yessenov + +class List<T> { + var rep: seq<T>; + method Clear() + modifies this; + { + rep := []; + } + + method Append(x: T) + modifies this; + { + rep := rep + [x]; + } + + method Prepend(x: T) + modifies this; + { + rep := [x] + rep; + } + + method Insert(i: int, x: T) + requires 0 <= i && i < |rep|; + modifies this; + { + rep := rep[i:=x]; + } +} + +class Node<T> { + var data: T; + var next: Node<T>; +} + +class LinkedList refines List { + var first: Node<T>; + ghost var nodes: set<Node<T>>; + + function Abstraction(n: Node<T>, nodes: set<Node<T>>, rep: seq<T>) : bool + decreases nodes; + reads n, nodes; + { + if (n == null) then + rep == [] && + nodes == {} + else + |rep| >= 1 && + n.data == rep[0] && + n in nodes && + n.next in nodes + {null} && + Abstraction(n.next, nodes - {n}, rep[1..]) + } + + replaces rep by Abstraction(first, nodes, rep); + + refines Clear() + modifies this; + { + first := null; + nodes := {}; + } + + refines Prepend(x: T) + modifies this; + { + var n := new Node<T>; + n.data := x; + n.next := first; + first := n; + nodes := {n} + nodes; + assert nodes - {n} == old(nodes); //set extensionality + } +} + |