Dafny:

* Added some more set axioms that go "inside out" for union and set differences (UnionOne already had such an axiom)
* Fixed bug to, once again, allow multiple .dfy files on the command line (with the effect of them being merged into one program)
* Fixed bug in translation of reads/modifies clauses that mention sequences

4 files changed, 99 insertions, 18 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 13314e29..520f9c77 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -32,10 +32,13 @@ axiom (forall<T> a: Set T, x: T :: { Set#UnionOne(a, x) }
 axiom (forall<T> a: Set T, x: T, y: T :: { Set#UnionOne(a, x), a[y] }

   a[y] ==> Set#UnionOne(a, x)[y]);

 

-

 function Set#Union<T>(Set T, Set T) returns (Set T);

 axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Union(a,b)[o] }

   Set#Union(a,b)[o] <==> a[o] || b[o]);

+axiom (forall<T> a, b: Set T, y: T :: { Set#Union(a, b), a[y] }

+  a[y] ==> Set#Union(a, b)[y]);

+axiom (forall<T> a, b: Set T, y: T :: { Set#Union(a, b), b[y] }

+  b[y] ==> Set#Union(a, b)[y]);

 

 function Set#Intersection<T>(Set T, Set T) returns (Set T);

 axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Intersection(a,b)[o] }

@@ -44,6 +47,8 @@ axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Intersection(a,b)[o] }
 function Set#Difference<T>(Set T, Set T) returns (Set T);

 axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Difference(a,b)[o] }

   Set#Difference(a,b)[o] <==> a[o] && !b[o]);

+axiom (forall<T> a, b: Set T, y: T :: { Set#Difference(a, b), b[y] }

+  b[y] ==> !Set#Difference(a, b)[y] );

 

 function Set#Subset<T>(Set T, Set T) returns (bool);

 axiom(forall<T> a: Set T, b: Set T :: { Set#Subset(a,b) }

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 6b46aa4f..7affe087 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -130,7 +130,18 @@ Dafny
 

      List<MemberDecl!> membersDefaultClass = new List<MemberDecl!>();

      ModuleDecl module;

-     DefaultModuleDecl defaultModule = new DefaultModuleDecl();

+     

+     // to support multiple files, create a default module only if theModules doesn't already contain one

+     DefaultModuleDecl defaultModule = null;

+     foreach (ModuleDecl mdecl in theModules) {

+       defaultModule = mdecl as DefaultModuleDecl;

+       if (defaultModule != null) { break; }

+     }

+     bool defaultModuleCreatedHere = false;

+     if (defaultModule == null) {

+       defaultModuleCreatedHere = true;

+       defaultModule = new DefaultModuleDecl();

+     }

   .)

   { "module"                             (. attrs = null;  theImports = new List<string!>(); .)

     { Attribute<ref attrs> }

@@ -145,8 +156,19 @@ Dafny
   | DatatypeDecl<defaultModule, out dt>  (. defaultModule.TopLevelDecls.Add(dt); .)

   | ClassMemberDecl<membersDefaultClass>

   }

-  (. defaultModule.TopLevelDecls.Add(new DefaultClassDecl(defaultModule, membersDefaultClass));

-     theModules.Add(defaultModule);

+  (. if (defaultModuleCreatedHere) {

+       defaultModule.TopLevelDecls.Add(new DefaultClassDecl(defaultModule, membersDefaultClass));

+       theModules.Add(defaultModule);

+     } else {

+       // find the default class in the default module, then append membersDefaultClass to its member list

+       foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {

+         DefaultClassDecl defaultClass = topleveldecl as DefaultClassDecl;

+         if (defaultClass != null) {

+           defaultClass.Members.AddRange(membersDefaultClass);

+           break;

+         }

+       }

+     }

   .)

   EOF

   .

diff --git a/Source/Dafny/Parser.ssc b/Source/Dafny/Parser.ssc
index 2499821c..3752fd33 100644
--- a/Source/Dafny/Parser.ssc
+++ b/Source/Dafny/Parser.ssc
@@ -152,7 +152,18 @@ public static int Parse (List<ModuleDecl!>! modules) {
 		Attributes attrs;  Token! id;  List<string!> theImports;

 		  List<MemberDecl!> membersDefaultClass = new List<MemberDecl!>();

 		ModuleDecl module;

-		DefaultModuleDecl defaultModule = new DefaultModuleDecl();

+		

+		// to support multiple files, create a default module only if theModules doesn't already contain one

+		DefaultModuleDecl defaultModule = null;

+		foreach (ModuleDecl mdecl in theModules) {

+		  defaultModule = mdecl as DefaultModuleDecl;

+		  if (defaultModule != null) { break; }

+		}

+		bool defaultModuleCreatedHere = false;

+		if (defaultModule == null) {

+		  defaultModuleCreatedHere = true;

+		  defaultModule = new DefaultModuleDecl();

+		}

 		

 		while (StartOf(1)) {

 			if (t.kind == 4) {

@@ -189,8 +200,19 @@ public static int Parse (List<ModuleDecl!>! modules) {
 				ClassMemberDecl(membersDefaultClass);

 			}

 		}

-		defaultModule.TopLevelDecls.Add(new DefaultClassDecl(defaultModule, membersDefaultClass));

-		theModules.Add(defaultModule);

+		if (defaultModuleCreatedHere) {

+		 defaultModule.TopLevelDecls.Add(new DefaultClassDecl(defaultModule, membersDefaultClass));

+		 theModules.Add(defaultModule);

+		} else {

+		  // find the default class in the default module, then append membersDefaultClass to its member list

+		  foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {

+		    DefaultClassDecl defaultClass = topleveldecl as DefaultClassDecl;

+		    if (defaultClass != null) {

+		      defaultClass.Members.AddRange(membersDefaultClass);

+		      break;

+		    }

+		  }

+		}

 		

 		Expect(0);

 	}

diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc
index 27103bd0..1740bf8b 100644
--- a/Source/Dafny/Translator.ssc
+++ b/Source/Dafny/Translator.ssc
@@ -980,14 +980,14 @@ namespace Microsoft.Dafny {
           // old(e)[Box(o)]

           disjunct = etran.TrInSet(tok, o, e, ((SetType)e.Type).Arg);

         } else if (e.Type is SeqType) {

-          // (exists i: int :: 0 <= i && i < Seq#Length(old(e)) ==> Seq#Index(old(e),i) == Box(o))

+          // (exists i: int :: 0 <= i && i < Seq#Length(old(e)) && Seq#Index(old(e),i) == Box(o))

           Bpl.Expr boxO = FunctionCall(tok, BuiltinFunction.Box, null, o);

           Bpl.Variable iVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$i", Bpl.Type.Int));

           Bpl.Expr i = new Bpl.IdentifierExpr(tok, iVar);

           Bpl.Expr iBounds = InSeqRange(tok, i, etran.TrExpr(e), true, null, false);

           Bpl.Expr XsubI = FunctionCall(tok, BuiltinFunction.SeqIndex, predef.BoxType, etran.TrExpr(e), i);

           // TODO: the equality in the next line should be changed to one that understands extensionality

-          disjunct = new Bpl.ExistsExpr(tok, new Bpl.VariableSeq(iVar), Bpl.Expr.Imp(iBounds, Bpl.Expr.Eq(XsubI, boxO)));

+          disjunct = new Bpl.ExistsExpr(tok, new Bpl.VariableSeq(iVar), Bpl.Expr.And(iBounds, Bpl.Expr.Eq(XsubI, boxO)));

         } else {

           // o == old(e)

           disjunct = Bpl.Expr.Eq(o, etran.TrExpr(e));

@@ -1322,11 +1322,13 @@ namespace Microsoft.Dafny {
             if (module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(func)) {

               List<Expression!> contextDecreases = func.Decreases;

               if (contextDecreases.Count == 0) {

-                contextDecreases = ProjectOutSpecificFields(func.Reads);  // use its reads clause instead

+                contextDecreases = new List<Expression!>();

+                contextDecreases.Add(FrameToObjectSet(func.Reads));  // use its reads clause instead

               }

               List<Expression!> calleeDecreases = e.Function.Decreases;

               if (calleeDecreases.Count == 0) {

-                calleeDecreases = ProjectOutSpecificFields(e.Function.Reads);  // use its reads clause instead

+                calleeDecreases = new List<Expression!>();

+                calleeDecreases.Add(FrameToObjectSet(e.Function.Reads));  // use its reads clause instead

               }

               CheckCallTermination(expr.tok, contextDecreases, calleeDecreases, e.Receiver, substMap, etran, builder);

             }

@@ -1432,17 +1434,47 @@ namespace Microsoft.Dafny {
       }

     }

     

-    List<Expression!>! ProjectOutSpecificFields(List<FrameExpression!>! fexprs) {

-      List<Expression!> exprs = new List<Expression!>();

+    Expression! FrameToObjectSet(List<FrameExpression!>! fexprs) {

+      List<Expression!> sets = new List<Expression!>();

+      List<Expression!> singletons = null;

       foreach (FrameExpression fe in fexprs) {

         if (fe.E is WildcardExpr) {

           // drop wildcards altogether

         } else {

-          // keep only fe.E, drop any fe.Field designation

-          exprs.Add(fe.E);

+          Expression e = fe.E;  // keep only fe.E, drop any fe.Field designation

+          assert e.Type != null;  // should have been resolved already

+          if (e.Type.IsRefType) {

+            // e represents a singleton set

+            if (singletons == null) {

+              singletons = new List<Expression!>();

+            }

+            singletons.Add(e);

+          } else {

+            // e is already a set

+            assert e.Type is SetType;

+            sets.Add(e);

+          }

         }

       }

-      return exprs;

+      if (singletons != null) {

+        Expression display = new SetDisplayExpr(singletons[0].tok, singletons);

+        display.Type = new SetType(new ObjectType());  // resolve here

+        sets.Add(display);

+      }

+      if (sets.Count == 0) {

+        Expression emptyset = new SetDisplayExpr(Token.NoToken, new List<Expression!>());

+        emptyset.Type = new SetType(new ObjectType());  // resolve here

+        return emptyset;

+      } else {

+        Expression s = sets[0];

+        for (int i = 1; i < sets.Count; i++) {

+          BinaryExpr union = new BinaryExpr(s.tok, BinaryExpr.Opcode.Add, s, sets[i]);

+          union.ResolvedOp = BinaryExpr.ResolvedOpcode.Union;  // resolve here

+          union.Type = new SetType(new ObjectType());  // resolve here

+          s = union;

+        }

+        return s;

+      }

     }

     

     Bpl.Constant! GetClass(TopLevelDecl! cl)

@@ -3158,7 +3190,7 @@ namespace Microsoft.Dafny {
       public Bpl.Expr! ProperSubset(Token! tok, Bpl.Expr! e0, Bpl.Expr! e1) {

         return Bpl.Expr.And(

           translator.FunctionCall(tok, BuiltinFunction.SetSubset, null, e0, e1),

-          Bpl.Expr.Not(translator.FunctionCall(tok, BuiltinFunction.SetEqual, null, e0, e1)));

+          Bpl.Expr.Not(translator.FunctionCall(tok, BuiltinFunction.SetSubset, null, e1, e0)));

       }

       public Bpl.Expr! ProperPrefix(Token! tok, Bpl.Expr! e0, Bpl.Expr! e1) {

         Bpl.Expr len0 = translator.FunctionCall(tok, BuiltinFunction.SeqLength, null, e0);

@@ -3715,7 +3747,7 @@ namespace Microsoft.Dafny {
       

       yield return expr;

     }

-

+    

     static Expression! Substitute(Expression! expr, Expression receiverReplacement, Dictionary<IVariable,Expression!>! substMap) {

       Expression newExpr = null;  // set to non-null value only if substitution has any effect; if non-null, newExpr will be resolved at end