Include axioms about $Is and $IsAlloc for traits

4 files changed, 132 insertions, 61 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 299c3abe..b25b8cbe 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1328,9 +1328,8 @@ namespace Microsoft.Dafny
       }

       // Now, we're ready for the other declarations.

       foreach (TopLevelDecl d in declarations) {

-        if (d is TraitDecl && d.TypeArgs.Count > 0)

-        {

-            Error(d, "a trait cannot declare type parameters");

+        if (d is TraitDecl && d.TypeArgs.Count > 0) {

+          Error(d, "sorry, traits with type parameters are not supported");

         }

         allTypeParameters.PushMarker();

         ResolveTypeParameters(d.TypeArgs, false, d);

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 2672258d..aa3e1854 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1299,68 +1299,51 @@ namespace Microsoft.Dafny {
         AddAllocationAxiom(null, c, true);

       }

 

-      /* // Add $Is and $IsAlloc for this class :

-            axiom (forall p: ref, G: Ty ::

-               { $Is(p, TClassA(G), h) }

-               $Is(p, TClassA(G), h) <=> (p == null || dtype(p) == TClassA(G));

-            axiom (forall p: ref, h: Heap, G: Ty ::

-               { $IsAlloc(p, TClassA(G), h) }

-               $IsAlloc(p, TClassA(G), h) => (p == null || h[p, alloc]);

-      */

-

-      if (!(c is TraitDecl))

-      {

-          MapM(Bools, is_alloc =>

-          {

-              List<Bpl.Expr> tyexprs;

-              var vars = MkTyParamBinders(GetTypeParams(c), out tyexprs);

+      // Add $Is and $IsAlloc for this class :

+      //    axiom (forall p: ref, G: Ty ::

+      //       { $Is(p, TClassA(G), h) }

+      //       $Is(p, TClassA(G), h) <=> (p == null || dtype(p) == TClassA(G));

+      //    axiom (forall p: ref, h: Heap, G: Ty ::

+      //       { $IsAlloc(p, TClassA(G), h) }

+      //       $IsAlloc(p, TClassA(G), h) => (p == null || h[p, alloc]);

+      MapM(Bools, is_alloc => {

+        List<Bpl.Expr> tyexprs;

+        var vars = MkTyParamBinders(GetTypeParams(c), out tyexprs);

 

-              var o = BplBoundVar("$o", predef.RefType, vars);

+        var o = BplBoundVar("$o", predef.RefType, vars);

 

-              Bpl.Expr body, is_o;

-              Bpl.Expr o_null = Bpl.Expr.Eq(o, predef.Null);

-              Bpl.Expr o_ty = ClassTyCon(c, tyexprs);

-              string name;

+        Bpl.Expr body, is_o;

+        Bpl.Expr o_null = Bpl.Expr.Eq(o, predef.Null);

+        Bpl.Expr o_ty = ClassTyCon(c, tyexprs);

+        string name;

 

-              if (is_alloc)

-              {

-                  name = c + ": Class $IsAlloc";

-                  var h = BplBoundVar("$h", predef.HeapType, vars);

-                  // $IsAlloc(o, ..)

-                  is_o = MkIsAlloc(o, o_ty, h);

-                  body = BplIff(is_o, BplOr(o_null, IsAlloced(c.tok, h, o)));

-              }

-              else

-              {

-                  name = c + ": Class $Is";

-                  // $Is(o, ..)

-                  is_o = MkIs(o, o_ty);

-                  Bpl.Expr rhs;

-                  if (c == program.BuiltIns.ObjectDecl)

-                  {

-                      rhs = Bpl.Expr.True;

-                  }

-                  else

-                  {

-                      //generating $o == null || implements$J(dtype(x))

-                      if (c is TraitDecl)

-                      {

-                          var t = (TraitDecl)c;

-                          var dtypeFunc = FunctionCall(o.tok, BuiltinFunction.DynamicType, null, o);

-                          Bpl.Expr implementsFunc = FunctionCall(t.tok, "implements$" + t.FullSanitizedName, Bpl.Type.Bool, new List<Expr> { dtypeFunc });

-                          rhs = BplOr(o_null, implementsFunc);

-                      }

-                      else

-                      {

-                          rhs = BplOr(o_null, DType(o, o_ty));

-                      }

-                  }

-                  body = BplIff(is_o, rhs);

-              }

+        if (is_alloc) {

+          name = c + ": Class $IsAlloc";

+          var h = BplBoundVar("$h", predef.HeapType, vars);

+          // $IsAlloc(o, ..)

+          is_o = MkIsAlloc(o, o_ty, h);

+          body = BplIff(is_o, BplOr(o_null, IsAlloced(c.tok, h, o)));

+        } else {

+          name = c + ": Class $Is";

+          // $Is(o, ..)

+          is_o = MkIs(o, o_ty);

+          Bpl.Expr rhs;

+          if (c == program.BuiltIns.ObjectDecl) {

+            rhs = Bpl.Expr.True;

+          } else if (c is TraitDecl) {

+            //generating $o == null || implements$J(dtype(x))

+            var t = (TraitDecl)c;

+            var dtypeFunc = FunctionCall(o.tok, BuiltinFunction.DynamicType, null, o);

+            Bpl.Expr implementsFunc = FunctionCall(t.tok, "implements$" + t.FullSanitizedName, Bpl.Type.Bool, new List<Expr> { dtypeFunc });

+            rhs = BplOr(o_null, implementsFunc);

+          } else {

+            rhs = BplOr(o_null, DType(o, o_ty));

+          }

+          body = BplIff(is_o, rhs);

+        }

 

-              sink.AddTopLevelDeclaration(new Bpl.Axiom(c.tok, BplForall(vars, BplTrigger(is_o), body), name));

-          });

-      }

+        sink.AddTopLevelDeclaration(new Bpl.Axiom(c.tok, BplForall(vars, BplTrigger(is_o), body), name));

+      });

 

       if (c is TraitDecl) {

         //this adds: function implements$J(Ty): bool;

diff --git a/Test/dafny0/Trait/TraitExample.dfy b/Test/dafny0/Trait/TraitExample.dfy
new file mode 100644
index 00000000..be38bfe5
--- /dev/null
+++ b/Test/dafny0/Trait/TraitExample.dfy
@@ -0,0 +1,82 @@
+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+trait Automobile {

+  ghost var Repr: set<object>

+  predicate Valid()

+    reads this //, Repr

+    ensures Valid() ==> this in Repr

+  function method Brand(): string

+  var position: int

+  method Drive()

+    requires Valid()

+    modifies this // Repr

+    ensures old(position) <= position

+}

+

+class Volvo extends Automobile {

+  predicate Valid()

+    reads this //, Repr

+    ensures Valid() ==> this in Repr

+  {

+    this in Repr

+  }

+  constructor()

+    modifies this

+    ensures Valid()

+  {

+    Repr := {this};

+  }

+  function method Brand(): string {

+    "Volvo"

+  }

+  method Drive()

+//    requires Valid()

+    modifies this // Repr

+    ensures old(position) <= position

+  {

+    position := position + 10;

+  }

+}

+

+class Fiat extends Automobile {

+  predicate Valid()

+    reads this // , Repr

+    ensures Valid() ==> this in Repr

+  {

+    this in Repr

+  }

+  constructor()

+    modifies this

+    ensures Valid()

+  {

+    Repr := {this};

+  }

+  function method Brand(): string {

+    "Fiat"

+  }

+  method Drive()

+//    requires Valid()

+    modifies this // Repr

+    ensures old(position) <= position

+  {

+    position := position + 3;

+  }

+}

+

+method Main() {

+  var auto: Automobile;

+  auto := new Volvo();

+  WorkIt(auto);

+  auto := new Fiat();

+  WorkIt(auto);

+}

+

+method WorkIt(auto: Automobile)

+  requires auto != null && auto.Valid()

+  modifies auto // auto.Repr

+{

+  auto.Drive();

+  print auto.Brand(), ": ", auto.position, "\n";

+  auto.position := 0;

+}

diff --git a/Test/dafny0/Trait/TraitExample.dfy.expect b/Test/dafny0/Trait/TraitExample.dfy.expect
new file mode 100644
index 00000000..4fc71fb5
--- /dev/null
+++ b/Test/dafny0/Trait/TraitExample.dfy.expect
@@ -0,0 +1,7 @@
+

+Dafny program verifier finished with 25 verified, 0 errors

+Program compiled successfully

+Running...

+

+Volvo: 10
+Fiat: 3