Dafny:

* Recoded frame axioms to be more goal directed
* Added Main test driver to Test/VSI-Benchmarks/b2.dfy

6 files changed, 103 insertions, 10 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 04da0993..d9ff2f63 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -227,6 +227,10 @@ const unique alloc: Field bool;
 function DeclType<T>(Field T) returns (ClassName);

 

 function $HeapSucc(HeapType, HeapType) returns (bool);

+axiom (forall<alpha> h: HeapType, r: ref, f: Field alpha, x: alpha :: { h[r,f:=x] }

+  $HeapSucc(h, h[r,f:=x]));

+axiom (forall a,b,c: HeapType :: { $HeapSucc(a,b), $HeapSucc(b,c) }

+  $HeapSucc(a,b) && $HeapSucc(b,c) ==> $HeapSucc(a,c));

 axiom (forall h: HeapType, k: HeapType :: { $HeapSucc(h,k) }

   $HeapSucc(h,k) ==> (forall o: ref :: { k[o,alloc] } h[o,alloc] ==> k[o,alloc]));

 

diff --git a/Dafny/Compiler.ssc b/Dafny/Compiler.ssc
index decbcdaa..155927c4 100644
--- a/Dafny/Compiler.ssc
+++ b/Dafny/Compiler.ssc
@@ -76,7 +76,7 @@ namespace Microsoft.Dafny {
           } else {

             ClassDecl cl = (ClassDecl)d;

             Indent(indent);

-            wr.Write("public class {0}", cl.IsDefaultClass ? "_DefaultClass" : cl.Name);

+            wr.Write("public class {0}", cl.Name);

             if (cl.TypeArgs.Count != 0) {

               wr.Write("<{0}>", TypeParameters(cl.TypeArgs));

             }

diff --git a/Dafny/Translator.ssc b/Dafny/Translator.ssc
index 763ed8c9..9b17d628 100644
--- a/Dafny/Translator.ssc
+++ b/Dafny/Translator.ssc
@@ -827,6 +827,7 @@ namespace Microsoft.Dafny {
       builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, frame), lambda));

     }

         

+#if OLD_FRAME_AXIOM

     /// <summary>

     /// Generates:

     ///   axiom (forall h0: HeapType, h1: HeapType, formals... ::

@@ -863,7 +864,7 @@ namespace Microsoft.Dafny {
       

       Bpl.Expr wellFormed = Bpl.Expr.And(

         FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran0.HeapExpr),

-        FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran0.HeapExpr));

+        FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran1.HeapExpr));

       

       Bpl.TypeVariable alpha = new Bpl.TypeVariable(f.tok, "alpha");

       Bpl.BoundVariable oVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$o", predef.RefType));

@@ -927,6 +928,99 @@ namespace Microsoft.Dafny {
         Bpl.Expr.Imp(Bpl.Expr.And(q0, q1), eq)));

       sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax, "frame axiom for " + f.FullName));

     }

+#else

+    /// <summary>

+    /// Generates:

+    ///   axiom (forall h0: HeapType, h1: HeapType, formals... ::

+    ///        { HeapSucc(h0,h1), F(h1,formals) }

+    ///        heaps are well-formed and formals are allocated AND

+    ///        HeapSucc(h0,h1)

+    ///        AND

+    ///        (forall(alpha) o: ref, f: Field alpha ::

+    ///            o != null AND h0[o,alloc] AND h1[o,alloc] AND

+    ///            o in reads clause of formals in h0

+    ///            IMPLIES h0[o,f] == h1[o,f])

+    ///        IMPLIES

+    ///        F(h0,formals) == F(h1,formals)

+    ///      );

+    ///

+    /// If the function is a "use" function, then "F "in the last line is replaced by "F#alt".

+    /// </summary>

+    void AddFrameAxiom(Function! f)

+      requires sink != null && predef != null;

+    {

+      Bpl.BoundVariable h0Var = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$h0", predef.HeapType));

+      Bpl.BoundVariable h1Var = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$h1", predef.HeapType));

+      Bpl.Expr h0 = new Bpl.IdentifierExpr(f.tok, h0Var);

+      Bpl.Expr h1 = new Bpl.IdentifierExpr(f.tok, h1Var);

+      ExpressionTranslator etran0 = new ExpressionTranslator(this, predef, h0);

+      ExpressionTranslator etran1 = new ExpressionTranslator(this, predef, h1);

+      

+      Bpl.Expr wellFormed = Bpl.Expr.And(

+        FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran0.HeapExpr),

+        FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran1.HeapExpr));

+      

+      Bpl.TypeVariable alpha = new Bpl.TypeVariable(f.tok, "alpha");

+      Bpl.BoundVariable oVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$o", predef.RefType));

+      Bpl.Expr o = new Bpl.IdentifierExpr(f.tok, oVar);

+      Bpl.BoundVariable fieldVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$f", predef.FieldName(f.tok, alpha)));

+      Bpl.Expr field = new Bpl.IdentifierExpr(f.tok, fieldVar);

+      Bpl.Expr oNotNull = Bpl.Expr.Neq(o, predef.Null);

+      Bpl.Expr oNotNullAlloced = Bpl.Expr.And(oNotNull, Bpl.Expr.And(etran0.IsAlloced(f.tok, o), etran1.IsAlloced(f.tok, o)));

+      Bpl.Expr unchanged = Bpl.Expr.Eq(Bpl.Expr.SelectTok(f.tok, h0, o, field), Bpl.Expr.SelectTok(f.tok, h1, o, field));

+      

+      Bpl.Expr heapSucc = FunctionCall(f.tok, BuiltinFunction.HeapSucc, null, h0, h1);

+      Bpl.Expr r0 = InRWClause(f.tok, o, f.Reads, etran0, null, null);

+      Bpl.Expr q0 = new Bpl.ForallExpr(f.tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fieldVar),

+        Bpl.Expr.Imp(Bpl.Expr.And(oNotNullAlloced, r0), unchanged));

+      

+      // bvars:  h0, h1, formals

+      // f0args:  h0, formals

+      // f1args:  h1, formals

+      Bpl.VariableSeq bvars = new Bpl.VariableSeq();

+      Bpl.ExprSeq f0args = new Bpl.ExprSeq();

+      Bpl.ExprSeq f1args = new Bpl.ExprSeq();

+      bvars.Add(h0Var);  bvars.Add(h1Var);

+      f0args.Add(h0);

+      f1args.Add(h1);

+      if (!f.IsStatic) {

+        Bpl.BoundVariable thVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType));

+        Bpl.Expr th = new Bpl.IdentifierExpr(f.tok, thVar);

+        bvars.Add(thVar);

+        f0args.Add(th);

+        f1args.Add(th);

+

+        Type thisType = Resolver.GetThisType(f.tok, (!)f.EnclosingClass);

+        Bpl.Expr wh = Bpl.Expr.And(Bpl.Expr.Neq(th, predef.Null),

+          Bpl.Expr.And(etran0.GoodRef(f.tok, th, thisType), etran1.GoodRef(f.tok, th, thisType)));

+        wellFormed = Bpl.Expr.And(wellFormed, wh);

+      }

+

+      foreach (Formal p in f.Formals) {

+        Bpl.BoundVariable bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));

+        bvars.Add(bv);

+        Bpl.Expr formal = new Bpl.IdentifierExpr(p.tok, bv);

+        f0args.Add(formal);

+        f1args.Add(formal);

+        Bpl.Expr wh = GetWhereClause(p.tok, formal, p.Type, etran0);

+        if (wh != null) { wellFormed = Bpl.Expr.And(wellFormed, wh); }

+        wh = GetWhereClause(p.tok, formal, p.Type, etran1);

+        if (wh != null) { wellFormed = Bpl.Expr.And(wellFormed, wh); }

+      }

+      

+      Bpl.FunctionCall fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.IsUse ? f.FullName + "#alt" : f.FullName, TrType(f.ResultType)));

+      Bpl.Expr F0 = new Bpl.NAryExpr(f.tok, fn, f0args);

+      Bpl.Expr F1 = new Bpl.NAryExpr(f.tok, fn, f1args);

+      Bpl.Expr eq = Bpl.Expr.Eq(F0, F1);

+      Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(heapSucc, F1));

+      

+      Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);

+      Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, bvars, null, tr,

+        Bpl.Expr.Imp(Bpl.Expr.And(wellFormed, heapSucc),

+        Bpl.Expr.Imp(q0, eq)));

+      sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax, "frame axiom for " + f.FullName));

+    }

+#endif

     

     Bpl.Expr! InRWClause(Token! tok, Bpl.Expr! o, List<Expression!>! rw, ExpressionTranslator! etran,

                          Expression receiverReplacement, Dictionary<IVariable,Expression!> substMap)

diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer
index 926a4da3..1efeba04 100644
--- a/Test/VSI-Benchmarks/Answer
+++ b/Test/VSI-Benchmarks/Answer
@@ -5,7 +5,7 @@ Dafny program verifier finished with 10 verified, 0 errors
 

 -------------------- b2.dfy --------------------

 

-Dafny program verifier finished with 8 verified, 0 errors

+Dafny program verifier finished with 12 verified, 0 errors

 

 -------------------- b3.dfy --------------------

 

diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy
index 0cae993a..86c12854 100644
--- a/Test/VSI-Benchmarks/b2.dfy
+++ b/Test/VSI-Benchmarks/b2.dfy
@@ -63,16 +63,12 @@ class Array {
   method Set(i: int, x: int)

     requires 0 <= i && i < |contents|;

     modifies this;

-    ensures |contents| == |old(contents)|;

-    ensures contents[..i] == old(contents[..i]);

-    ensures contents[i] == x;

-    ensures contents[i+1..] == old(contents[i+1..]);

+    ensures contents == old(contents)[i := x];

   {

     contents := contents[i := x];

   }

 }

 

-/******

 method Main() {

   var a := new Array;

   call a.Init(5);

@@ -103,4 +99,3 @@ method TestSearch(a: Array, key: int)
   call r := b.BinarySearch(a, key);

   print "Looking for key=", key, ", result=", r, "\n";

 }

-******/

diff --git a/Test/dafny0/ListContents.dfy b/Test/dafny0/ListContents.dfy
index 62636ce5..7f0085e0 100644
--- a/Test/dafny0/ListContents.dfy
+++ b/Test/dafny0/ListContents.dfy
@@ -5,7 +5,7 @@ class Node<T> {
   var data: T;

   var next: Node<T>;

 

-  function Valid(): bool

+  use function Valid(): bool

     reads this, footprint;

   {

     this in this.footprint && null !in this.footprint &&