New feature:

* Added "comethod" declarations and support for writing manual co-inductive proofs (but currently blindly assume comethod postconditions to, in positive positions, only have copredicates and codatatype equalities--other cases still need to be dealt with)
Code restructuring:
* New set of Boogie procedure stubs generated for each other
* Start of improvements around TrSplitExpr

1 files changed, 25 insertions, 1 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 3550ddb2..cec40977 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1126,7 +1126,7 @@ namespace Microsoft.Dafny {
     // TODO: One could imagine having a precondition on datatype constructors

     public DatatypeDecl EnclosingDatatype;  // filled in during resolution

     public SpecialField QueryField;  // filled in during resolution

-    public List<SpecialField/*may be null*/> Destructors = new List<SpecialField/*may be null*/>();  // contents filled in during resolution

+    public List<SpecialField> Destructors = new List<SpecialField>();  // contents filled in during resolution; includes both implicit (not mentionable in source) and explicit destructors

 

     public DatatypeCtor(IToken/*!*/ tok, string/*!*/ name, [Captured] List<Formal/*!*/>/*!*/ formals, Attributes attributes)

       : base(tok, name, attributes) {

@@ -1794,6 +1794,30 @@ namespace Microsoft.Dafny {
     }

   }

 

+  public class CoMethod : Method

+  {

+    public CoMethod(IToken tok, string name,

+                  bool isStatic,

+                  List<TypeParameter/*!*/>/*!*/ typeArgs,

+                  List<Formal/*!*/>/*!*/ ins, [Captured] List<Formal/*!*/>/*!*/ outs,

+                  List<MaybeFreeExpression/*!*/>/*!*/ req, [Captured] Specification<FrameExpression>/*!*/ mod,

+                  List<MaybeFreeExpression/*!*/>/*!*/ ens,

+                  Specification<Expression>/*!*/ decreases,

+                  BlockStmt body,

+                  Attributes attributes, bool signatureOmitted)

+      : base(tok, name, isStatic, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureOmitted) {

+      Contract.Requires(tok != null);

+      Contract.Requires(name != null);

+      Contract.Requires(cce.NonNullElements(typeArgs));

+      Contract.Requires(cce.NonNullElements(ins));

+      Contract.Requires(cce.NonNullElements(outs));

+      Contract.Requires(cce.NonNullElements(req));

+      Contract.Requires(mod != null);

+      Contract.Requires(cce.NonNullElements(ens));

+      Contract.Requires(decreases != null);

+    }

+  }

+

   // ------------------------------------------------------------------------------------------------------

 

   public abstract class Statement {