Dafny:

* Added arrays
* Beefed up set axiomatization to know more things about set displays
* Added a simple heuristic that can infer some simple decreases clauses for loops
* Added Dafny solutions to a couple of VACID benchmarks

1 files changed, 82 insertions, 12 deletions

diff --git a/Source/Dafny/Compiler.ssc b/Source/Dafny/Compiler.ssc
index 155927c4..c7dc73eb 100644
--- a/Source/Dafny/Compiler.ssc
+++ b/Source/Dafny/Compiler.ssc
@@ -386,6 +386,9 @@ namespace Microsoft.Dafny {
         return "BigInteger";

       } else if (type is ObjectType) {

         return "object";

+      } else if (type.IsArrayType) {

+        Type elType = UserDefinedType.ArrayElementType(type);

+        return TypeName(elType) + "[]";

       } else if (type is UserDefinedType) {

         UserDefinedType udt = (UserDefinedType)type;

         string s = udt.Name;

@@ -507,13 +510,54 @@ namespace Microsoft.Dafny {
         wr.WriteLine("return;");

       } else if (stmt is AssignStmt) {

         AssignStmt s = (AssignStmt)stmt;

-        Indent(indent);

-        TrExpr(s.Lhs);

-        if (!(s.Rhs is HavocRhs)) {

-          wr.Write(" = ");

-          TrAssignmentRhs(s.Rhs);

+        if (s.Lhs is SeqSelectExpr && !((SeqSelectExpr)s.Lhs).SelectOne) {

+          SeqSelectExpr sel = (SeqSelectExpr)s.Lhs;

+          // Generate the following:

+          //   tmpArr = sel.Seq;

+          //   tmpLow = sel.E0;  // or 0 if sel.E0==null

+          //   tmpHigh = sel.Eq;  // or arr.Length if sel.E1==null

+          //   tmpRhs = s.Rhs;

+          //   for (int tmpI = tmpLow; tmpI < tmpHigh; tmpI++) {

+          //     tmpArr[tmpI] = tmpRhs;

+          //   }

+          string arr = "_arr" + tmpVarCount;

+          string low = "_low" + tmpVarCount;

+          string high = "_high" + tmpVarCount;

+          string rhs = "_rhs" + tmpVarCount;

+          string i = "_i" + tmpVarCount;

+          tmpVarCount++;

+          Indent(indent);  wr.Write("{0} {1} = ", TypeName((!)sel.Seq.Type), arr);  TrExpr(sel.Seq);  wr.WriteLine(";");

+          Indent(indent);  wr.Write("int {0} = ", low);

+          if (sel.E0 == null) {

+            wr.Write("0");

+          } else {

+            TrExpr(sel.E0);

+          }

+          wr.WriteLine(";");

+          Indent(indent);  wr.Write("int {0} = ", high);

+          if (sel.E1 == null) {

+            wr.Write("new BigInteger(arr.Length)");

+          } else {

+            TrExpr(sel.E1);

+          }

+          wr.WriteLine(";");

+          Indent(indent);  wr.Write("{0} {1} = ", TypeName((!)sel.Type), rhs);  TrAssignmentRhs(s.Rhs);  wr.WriteLine(";");

+          Indent(indent);

+          wr.WriteLine("for (BigInteger {0} = {1}; {0} < {2}; {0}++) {{", i, low, high);

+          Indent(indent + IndentAmount);

+          wr.WriteLine("{0}[(int)({1})] = {2};", arr, i, rhs);

+          Indent(indent);

+          wr.WriteLine(";");

+

+        } else {

+          Indent(indent);

+          TrExpr(s.Lhs);

+          if (!(s.Rhs is HavocRhs)) {

+            wr.Write(" = ");

+            TrAssignmentRhs(s.Rhs);

+          }

+          wr.WriteLine(";");

         }

-        wr.WriteLine(";");

         

       } else if (stmt is VarDecl) {

         TrVarDecl((VarDecl)stmt, true, indent);

@@ -686,7 +730,21 @@ namespace Microsoft.Dafny {
         

       } else {

         TypeRhs tp = (TypeRhs)rhs;

-        wr.Write("new {0}()", TypeName(tp.Type));

+        if (tp.ArraySize == null) {

+          wr.Write("new {0}()", TypeName(tp.EType));

+        } else {

+          if (tp.EType is IntType || tp.EType.IsTypeParameter) {

+            // Because the default constructor for BigInteger does not generate a valid BigInteger, we have

+            // to excplicitly initialize the elements of an integer array.  This is all done in a helper routine.

+            wr.Write("Dafny.Helpers.InitNewArray<{0}>(", TypeName(tp.EType));

+            TrExpr(tp.ArraySize);

+            wr.Write(")");

+          } else {

+            wr.Write("new {0}[(int)", TypeName(tp.EType));

+            TrExpr(tp.ArraySize);

+            wr.Write("]");

+          }

+        }

       }

     }

     

@@ -827,9 +885,15 @@ namespace Microsoft.Dafny {
       } else if (expr is SeqSelectExpr) {

         SeqSelectExpr e = (SeqSelectExpr)expr;

         TrParenExpr(e.Seq);

-        if (e.SelectOne) {

-          assert e.E0 != null;

-          assert e.E1 == null;

+        assert e.Seq.Type != null;

+        if (e.Seq.Type.IsArrayType) {

+          assert e.SelectOne;

+          assert e.E0 != null && e.E1 == null;

+          wr.Write("[(int)");

+          TrParenExpr(e.E0);

+          wr.Write("]");

+        } else if (e.SelectOne) {

+          assert e.E0 != null && e.E1 == null;

           TrParenExpr(".Select", e.E0);

         } else {

           if (e.E1 != null) {

@@ -902,8 +966,14 @@ namespace Microsoft.Dafny {
             TrParenExpr(e.E);

             break;

           case UnaryExpr.Opcode.SeqLength:

-            TrParenExpr(e.E);

-            wr.Write(".Length");

+            if (((!)e.E.Type).IsArrayType) {

+              wr.Write("new BigInteger(");

+              TrParenExpr(e.E);

+              wr.Write(".Length)");

+            } else {

+              TrParenExpr(e.E);

+              wr.Write(".Length");

+            }

             break;

           default:

             assert false;  // unexpected unary expression