Added support for automatic generation of function requirements via the :autoReq attribute.

8 files changed, 725 insertions, 7 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index b7ff7a01..994a9d7e 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -169,6 +169,33 @@ namespace Microsoft.Dafny {
       return false;

     }

 

+    /// <summary>

+    /// Checks whether a Boolean attribute has been set on the declaration itself,

+    /// the enclosing class, or any enclosing module.  Settings closer to the declaration

+    /// override those further away.

+    /// </summary>

+    public static bool ContainsBoolAtAnyLevel(MemberDecl decl, string attribName) {

+      bool setting = true;

+      if (Attributes.ContainsBool(decl.Attributes, attribName, ref setting)) {

+        return setting;

+      }

+

+      if (Attributes.ContainsBool(decl.EnclosingClass.Attributes, attribName, ref setting)) {

+        return setting;

+      }

+

+      // Check the entire stack of modules

+      var mod = decl.EnclosingClass.Module;

+      while (mod != null) {

+        if (Attributes.ContainsBool(mod.Attributes, attribName, ref setting)) {

+          return setting;

+        }

+        mod = mod.Module;

+      }

+

+      return false;

+    }

+

     public class Argument

     {

       public readonly IToken Tok;

@@ -3945,6 +3972,24 @@ namespace Microsoft.Dafny {
     }

 

     /// <summary>

+    /// Create a resolved expression for a bool b

+    /// </summary>        

+    public static Expression CreateBoolLiteral(IToken tok, bool b) {

+      Contract.Requires(tok != null);

+      var lit = new LiteralExpr(tok, b);

+      lit.Type = Type.Bool;  // resolve here

+      return lit;

+    }

+

+    public static Expression CreateNot(IToken tok, Expression e) {

+      Contract.Requires(tok != null);

+      Contract.Requires(e.Type == Type.Bool);

+      var un = new UnaryExpr(tok, UnaryExpr.Opcode.Not, e);

+      un.Type = Type.Bool;  // resolve here

+      return un;

+    }

+

+    /// <summary>

     /// Create a resolved expression of the form "e0 LESS e1"

     /// </summary>

     public static Expression CreateLess(Expression e0, Expression e1) {

@@ -4023,6 +4068,102 @@ namespace Microsoft.Dafny {
       ite.Type = e0.type;  // resolve here

       return ite;

     }

+

+    /*  Still under development

+     

+    /// <summary>

+    /// Create a resolved case expression for a match expression

+    /// </summary>

+    public static MatchCaseExpr CreateMatchCase(MatchCaseExpr old_case, Expression new_body) {

+      Contract.Requires(old_case != null);

+      Contract.Requires(new_body != null);   

+      Contract.Ensures(Contract.Result<Expression>() != null);

+      

+      Cloner cloner = new Cloner();

+      var newVars = old_case.Arguments.ConvertAll(cloner.CloneBoundVar);

+      new_body = VarSubstituter(old_case.Arguments, newVars, new_body);

+

+      var new_case = new MatchCaseExpr(old_case.tok, old_case.Id, newVars, new_body);

+

+      new_case.Ctor = old_case.Ctor; // resolve here

+      return new_case;

+    }

+

+    /// <summary>

+    /// Create a match expression with a resolved type 

+    /// </summary>

+    public static Expression CreateMatch(IToken tok, Expression src, List<MatchCaseExpr> cases, Type type) {

+      MatchExpr e = new MatchExpr(tok, src, cases);

+      e.Type = type;  // resolve here

+

+      return e;

+    }

+    */

+

+    /// <summary>

+    /// Create a let expression with a resolved type and fresh variables

+    /// </summary>

+    public static Expression CreateLet(IToken tok, List<BoundVar> vars, List<Expression> RHSs, Expression body, bool exact) {

+      Contract.Requires(tok  != null);

+      Contract.Requires(vars != null && RHSs != null);

+      Contract.Requires(vars.Count == RHSs.Count);

+      Contract.Requires(body != null);

+

+      Cloner cloner = new Cloner();

+      var newVars = vars.ConvertAll(cloner.CloneBoundVar);

+      body = VarSubstituter(vars, newVars, body);

+

+      var let = new LetExpr(tok, newVars, RHSs, body, exact);

+      let.Type = body.Type;  // resolve here

+      return let;

+    }

+

+    /// <summary>

+    /// Create a quantifier expression with a resolved type and fresh variables

+    /// Optionally replace the old body with the supplied argument

+    /// </summary>

+    public static Expression CreateQuantifier(QuantifierExpr expr, bool forall,  Expression body = null) {

+      //(IToken tok, List<BoundVar> vars, Expression range, Expression body, Attributes attribs, Qu) {

+      Contract.Requires(expr != null);

+

+      Cloner cloner = new Cloner();

+      var newVars = expr.BoundVars.ConvertAll(cloner.CloneBoundVar);

+

+      if (body == null) {

+        body = expr.Term;

+      }

+

+      body = VarSubstituter(expr.BoundVars, newVars, body);

+      

+      QuantifierExpr q;

+      if (forall) {

+        q = new ForallExpr(expr.tok, newVars, expr.Range, body, expr.Attributes);

+      } else {

+        q = new ExistsExpr(expr.tok, newVars, expr.Range, body, expr.Attributes);

+      } 

+      q.Type = Type.Bool;

+

+      return q;           

+    }

+

+    private static Expression VarSubstituter(List<BoundVar> oldVars, List<BoundVar> newVars, Expression e) {

+      Contract.Requires(oldVars != null && newVars != null);

+      Contract.Requires(oldVars.Count == newVars.Count);

+      

+      Dictionary<IVariable, Expression/*!*/> substMap = new Dictionary<IVariable, Expression>();

+      Dictionary<TypeParameter, Type> typeMap = new Dictionary<TypeParameter, Type>();

+

+      for (int i = 0; i < oldVars.Count; i++) {

+        var id = new IdentifierExpr(newVars[i].tok, newVars[i].Name);

+        id.Var = newVars[i];    // Resolve here manually

+        id.Type = newVars[i].Type;  // Resolve here manually

+        substMap.Add(oldVars[i], id);

+      }

+

+      Translator.Substituter sub = new Translator.Substituter(null, substMap, typeMap, null);

+      return sub.Substitute(e);

+    }

+

   }

 

   /// <summary>

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 24375f7b..3ca5872c 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -36,6 +36,17 @@ namespace Microsoft.Dafny {
       }

     }

 

+    /*

+    public static string ExtendedExprToString(Expression expr) {

+      Contract.Requires(expr != null);

+      using (var wr = new System.IO.StringWriter()) {

+        var pr = new Printer(wr);

+        pr.PrintExtendedExpr(expr, 0, true, false, false);        

+        return wr.ToString();

+      }

+    }

+     */

+

     public static string IteratorClassToString(IteratorDecl iter) {

       Contract.Requires(iter != null);

       using (var wr = new System.IO.StringWriter()) {

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 1fe84e4e..1fba4170 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -192,6 +192,7 @@ namespace Microsoft.Dafny
       rewriters.Add(refinementTransformer);

       rewriters.Add(new AutoContractsRewriter());

       rewriters.Add(new OpaqueFunctionRewriter());

+      rewriters.Add(new AutoReqFunctionRewriter(this));

 

       systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule, false);

       foreach (var decl in sortedDecls) {

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 26a3a70c..f6460e63 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -523,4 +523,288 @@ namespace Microsoft.Dafny
       }

     }

   }

+

+

+  /// <summary>

+  /// Automatically accumulate requires for function calls within a function body, 

+  /// if requested via {:autoreq}

+  /// </summary>

+  public class AutoReqFunctionRewriter : IRewriter {

+    Function parentFunction;

+    Resolver resolver;

+

+    public AutoReqFunctionRewriter(Resolver r) {

+      this.resolver = r;

+    }

+

+    public void PreResolve(ModuleDefinition m) { 

+    }    

+

+    public void PostResolve(ModuleDefinition m) {

+      var components = m.CallGraph.TopologicallySortedComponents();

+

+      foreach (var scComponent in components) {  // Visit the call graph bottom up, so anything we call already has its prequisites calculated

+        if (scComponent is Function) {

+          Function fn = (Function)scComponent;

+          if (Attributes.ContainsBoolAtAnyLevel(fn, "autoReq")) {

+            parentFunction = fn;  // Remember where the recursion started

+

+            List<Expression> auto_reqs = new List<Expression>();

+

+            // First handle all of the requirements' preconditions

+            foreach (Expression req in fn.Req) {

+              auto_reqs.AddRange(generateAutoReqs(req));

+            }

+

+            // Then the body itself, if any

+            if (fn.Body != null) {

+              auto_reqs.AddRange(generateAutoReqs(fn.Body));

+            }

+           

+            fn.Req.InsertRange(0, auto_reqs);

+            addAutoReqToolTipInfo(fn, auto_reqs);

+          }

+        } 

+      }

+    }

+  

+    public void addAutoReqToolTipInfo(Function f, List<Expression> reqs) {

+      string prefix = "auto requires ";

+      string tip = "";

+

+      foreach (var req in reqs) {

+        //tip += prefix + Printer.ExtendedExprToString(req) + ";\n";

+        tip += prefix + Printer.ExprToString(req) + ";\n";

+      }

+

+      if (!tip.Equals("")) {

+        resolver.ReportAdditionalInformation(f.tok, tip, f.tok.val.Length);

+      }

+    }

+

+    // Stitch a list of expressions together with logical ands

+    Expression andify(Bpl.IToken tok, List<Expression> exprs) {

+      Expression ret = Expression.CreateBoolLiteral(tok, true); 

+

+      foreach (var expr in exprs) {        

+        ret = Expression.CreateAnd(ret, expr);

+      }   

+

+      return ret;

+    }

+   

+    List<Expression> gatherReqs(Function f, List<Expression> args, Expression f_this) {

+      List<Expression> translated_f_reqs = new List<Expression>();

+

+      if (f.Req.Count > 0) {

+        Dictionary<IVariable, Expression/*!*/> substMap = new Dictionary<IVariable,Expression>();

+        Dictionary<TypeParameter, Type> typeMap = new Dictionary<TypeParameter,Type>();

+

+        for (int i = 0; i < f.Formals.Count; i++) {

+          substMap.Add(f.Formals[i], args[i]);

+        }

+

+        foreach (var req in f.Req) {

+          Translator.Substituter sub = new Translator.Substituter(f_this, substMap, typeMap, null);          

+          translated_f_reqs.Add(sub.Substitute(req));         

+        }

+      }

+

+      return translated_f_reqs;

+    }

+

+    List<Expression> generateAutoReqs(Expression expr) {

+      List<Expression> reqs = new List<Expression>();

+

+      if (expr is LiteralExpr) {      

+      } else if (expr is ThisExpr) {

+      } else if (expr is IdentifierExpr) {

+      } else if (expr is SetDisplayExpr) {

+        SetDisplayExpr e = (SetDisplayExpr)expr;

+

+        foreach (var elt in e.Elements) {

+          reqs.AddRange(generateAutoReqs(elt));

+        }

+      } else if (expr is MultiSetDisplayExpr) {

+        MultiSetDisplayExpr e = (MultiSetDisplayExpr)expr;

+        foreach (var elt in e.Elements) {

+          reqs.AddRange(generateAutoReqs(elt));

+        }

+      } else if (expr is SeqDisplayExpr) {

+        SeqDisplayExpr e = (SeqDisplayExpr)expr;

+        foreach (var elt in e.Elements) {

+          reqs.AddRange(generateAutoReqs(elt));

+        }

+      } else if (expr is MapDisplayExpr) {

+        MapDisplayExpr e = (MapDisplayExpr)expr;

+

+        foreach (ExpressionPair p in e.Elements) {

+          reqs.AddRange(generateAutoReqs(p.A));

+          reqs.AddRange(generateAutoReqs(p.B));        

+        }

+      } else if (expr is FieldSelectExpr) {

+        FieldSelectExpr e = (FieldSelectExpr)expr;

+        Contract.Assert(e.Field != null);

+

+        reqs.AddRange(generateAutoReqs(e.Obj));       

+      } else if (expr is SeqSelectExpr) {

+        SeqSelectExpr e = (SeqSelectExpr)expr;

+

+        reqs.AddRange(generateAutoReqs(e.Seq));

+        if (e.E0 != null) {

+          reqs.AddRange(generateAutoReqs(e.E0));

+        }

+

+        if (e.E1 != null) {

+          reqs.AddRange(generateAutoReqs(e.E1));

+        }

+      } else if (expr is SeqUpdateExpr) {

+        SeqUpdateExpr e = (SeqUpdateExpr)expr;

+        reqs.AddRange(generateAutoReqs(e.Seq));

+        reqs.AddRange(generateAutoReqs(e.Index));

+        reqs.AddRange(generateAutoReqs(e.Value));

+      } else if (expr is FunctionCallExpr) {

+        FunctionCallExpr e = (FunctionCallExpr)expr;

+

+        // All of the arguments need to be satisfied

+        foreach (var arg in e.Args) {

+          reqs.AddRange(generateAutoReqs(arg));

+        }

+

+        ModuleDefinition module = e.Function.EnclosingClass.Module;

+        if (module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(parentFunction)) {

+          // We're making a call within the same SCC, so don't descend into this function

+        } else {

+          reqs.AddRange(gatherReqs(e.Function, e.Args, e.Receiver));

+        }

+      } else if (expr is DatatypeValue) {         

+        DatatypeValue dtv = (DatatypeValue)expr;

+        Contract.Assert(dtv.Ctor != null);  // since dtv has been successfully resolved

+        for (int i = 0; i < dtv.Arguments.Count; i++) {

+          Expression arg = dtv.Arguments[i];

+          reqs.AddRange(generateAutoReqs(arg));

+        }              

+      } else if (expr is OldExpr) {  

+      } else if (expr is MatchExpr) {

+        MatchExpr e = (MatchExpr)expr;

+        reqs.AddRange(generateAutoReqs(e.Source));

+        

+        /*  Still under development

+        List<MatchCaseExpr> newMatches = new List<MatchCaseExpr>();

+        foreach (MatchCaseExpr caseExpr in e.Cases) {

+          //MatchCaseExpr c = new MatchCaseExpr(caseExpr.tok, caseExpr.Id, caseExpr.Arguments, andify(caseExpr.tok, generateAutoReqs(caseExpr.Body)));

+          //c.Ctor = caseExpr.Ctor; // resolve here

+          MatchCaseExpr c = Expression.CreateMatchCase(caseExpr, andify(caseExpr.tok, generateAutoReqs(caseExpr.Body)));

+          newMatches.Add(c);

+        }

+        

+        reqs.Add(Expression.CreateMatch(e.tok, e.Source, newMatches, e.Type));

+        */

+      } else if (expr is MultiSetFormingExpr) {

+        MultiSetFormingExpr e = (MultiSetFormingExpr)expr;

+        reqs.AddRange(generateAutoReqs(e.E));

+      } else if (expr is FreshExpr) {

+      } else if (expr is UnaryExpr) {

+        UnaryExpr e = (UnaryExpr)expr;

+        Expression arg = e.E;                

+        reqs.AddRange(generateAutoReqs(arg));

+      } else if (expr is BinaryExpr) {

+        BinaryExpr e = (BinaryExpr)expr;

+  

+        switch (e.ResolvedOp) {

+          case BinaryExpr.ResolvedOpcode.Imp:

+          case BinaryExpr.ResolvedOpcode.And:

+            reqs.AddRange(generateAutoReqs(e.E0));

+            foreach (var req in generateAutoReqs(e.E1)) {

+              // We only care about this req if E0 is true, since And short-circuits              

+              reqs.Add(Expression.CreateImplies(e.E0, req));  

+            }

+            break;

+

+          case BinaryExpr.ResolvedOpcode.Or:

+            reqs.AddRange(generateAutoReqs(e.E0));

+            foreach (var req in generateAutoReqs(e.E1)) {

+              // We only care about this req if E0 is false, since Or short-circuits              

+              reqs.Add(Expression.CreateImplies(Expression.CreateNot(e.E1.tok, e.E0), req));

+            }

+            break;

+

+          default:

+            reqs.AddRange(generateAutoReqs(e.E0));

+            reqs.AddRange(generateAutoReqs(e.E1));

+            break;

+        }   

+      } else if (expr is TernaryExpr) {

+        var e = (TernaryExpr)expr;

+

+        reqs.AddRange(generateAutoReqs(e.E0));

+        reqs.AddRange(generateAutoReqs(e.E1));

+        reqs.AddRange(generateAutoReqs(e.E2));

+      } else if (expr is LetExpr) {

+        var e = (LetExpr)expr;

+

+        if (e.Exact) {

+          foreach (var rhs in e.RHSs) {

+            reqs.AddRange(generateAutoReqs(rhs));

+          }

+          var new_reqs = generateAutoReqs(e.Body);

+          if (new_reqs.Count > 0) {                 

+            reqs.Add(Expression.CreateLet(e.tok, e.Vars, e.RHSs, andify(e.tok, new_reqs), e.Exact));

+          }

+        } else {

+          // TODO: Still need to figure out what the right choice is here:

+          // Given: var x :| g(x); f(x, y) do we:

+          //    1) Update the original statement to be: var x :| g(x) && WP(f(x,y)); f(x, y)

+          //    2) Add forall x :: g(x) ==> WP(f(x, y)) to the function's requirements

+          //    3) Current option -- do nothing.  Up to the spec writer to fix

+        }

+      } else if (expr is NamedExpr) {

+        reqs.AddRange(generateAutoReqs(((NamedExpr)expr).Body));

+      } else if (expr is QuantifierExpr) {

+        QuantifierExpr e = (QuantifierExpr)expr;

+

+        // See LetExpr for issues with the e.Range

+

+        var auto_reqs = generateAutoReqs(e.Term);

+        if (auto_reqs.Count > 0) {

+          reqs.Add(Expression.CreateQuantifier(e, true, andify(e.Term.tok, auto_reqs)));        

+        }

+      } else if (expr is SetComprehension) {

+        var e = (SetComprehension)expr;

+        // Translate "set xs | R :: T" 

+

+        // See LetExpr for issues with the e.Range

+        //reqs.AddRange(generateAutoReqs(e.Range));

+        var auto_reqs = generateAutoReqs(e.Term);

+        if (auto_reqs.Count > 0) {

+          reqs.Add(Expression.CreateQuantifier(new ForallExpr(e.tok, e.BoundVars, e.Range, andify(e.Term.tok, auto_reqs), e.Attributes), true));

+        }      

+      } else if (expr is MapComprehension) {

+        var e = (MapComprehension)expr;

+        // Translate "map x | R :: T" into

+        // See LetExpr for issues with the e.Range

+        //reqs.AddRange(generateAutoReqs(e.Range));        

+        var auto_reqs = generateAutoReqs(e.Term);

+        if (auto_reqs.Count > 0) {

+          reqs.Add(Expression.CreateQuantifier(new ForallExpr(e.tok, e.BoundVars, e.Range, andify(e.Term.tok, auto_reqs), e.Attributes), true));

+        }

+      } else if (expr is StmtExpr) {

+        var e = (StmtExpr)expr;

+        reqs.AddRange(generateAutoReqs(e.E));

+      } else if (expr is ITEExpr) {

+        ITEExpr e = (ITEExpr)expr;

+        reqs.AddRange(generateAutoReqs(e.Test));        

+        reqs.Add(Expression.CreateITE(e.Test, andify(e.Thn.tok, generateAutoReqs(e.Thn)), andify(e.Els.tok, generateAutoReqs(e.Els))));

+      } else if (expr is ConcreteSyntaxExpression) {

+        var e = (ConcreteSyntaxExpression)expr;

+        reqs.AddRange(generateAutoReqs(e.ResolvedExpression));

+      } else {

+        //Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression

+      }

+

+      return reqs;

+    }

+  }

 }

+

+

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 92ce09bc..76180eb5 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -10269,7 +10269,6 @@ namespace Microsoft.Dafny {
       public Substituter(Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap, Dictionary<TypeParameter, Type> typeMap, Translator translator) {

         Contract.Requires(substMap != null);

         Contract.Requires(typeMap != null);

-        Contract.Requires(translator != null);

         this.receiverReplacement = receiverReplacement;

         this.substMap = substMap;

         this.typeMap = typeMap;

@@ -10463,11 +10462,14 @@ namespace Microsoft.Dafny {
               return e;

             }

             var newLet = new LetExpr(e.tok, e.Vars, new List<Expression>{ rhs }, body, e.Exact);

-            Expression d = translator.LetDesugaring(e);

-            newLet.translationDesugaring = Substitute(d);

-            var info = translator.letSuchThatExprInfo[e];

-            translator.letSuchThatExprInfo.Add(newLet, new LetSuchThatExprInfo(info, translator, substMap));

-            newExpr = newLet;

+            if (translator != null)

+            {

+              Expression d = translator.LetDesugaring(e);

+              newLet.translationDesugaring = Substitute(d);

+              var info = translator.letSuchThatExprInfo[e];

+              translator.letSuchThatExprInfo.Add(newLet, new LetSuchThatExprInfo(info, translator, substMap));

+            }

+            newExpr = newLet;         

           }

 

         } else if (expr is MatchExpr) {

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 472932c5..d7996361 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -2043,6 +2043,44 @@ Dafny program verifier finished with 3 verified, 3 errors
 

 Dafny program verifier finished with 2 verified, 0 errors

 

+-------------------- AutoReq.dfy --------------------

+AutoReq.dfy(11,3): Error: possible violation of function precondition

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+AutoReq.dfy(23,3): Error: possible violation of function precondition

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+AutoReq.dfy(36,12): Error: assertion violation

+AutoReq.dfy(29,13): Related location

+AutoReq.dfy(5,5): Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon9_Then

+AutoReq.dfy(36,12): Error: possible violation of function precondition

+Execution trace:

+    (0,0): anon0

+    (0,0): anon9_Then

+AutoReq.dfy(38,12): Error: assertion violation

+AutoReq.dfy(29,27): Related location

+AutoReq.dfy(5,5): Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon10_Then

+AutoReq.dfy(38,12): Error: possible violation of function precondition

+Execution trace:

+    (0,0): anon0

+    (0,0): anon10_Then

+AutoReq.dfy(43,12): Error: assertion violation

+AutoReq.dfy(29,13): Related location

+AutoReq.dfy(5,5): Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon11_Then

+

+Dafny program verifier finished with 37 verified, 7 errors

+

 -------------------- Superposition.dfy --------------------

 

 Verifying CheckWellformed$$_0_M0.C.M ...

diff --git a/Test/dafny0/AutoReq.dfy b/Test/dafny0/AutoReq.dfy
new file mode 100644
index 00000000..9e221900
--- /dev/null
+++ b/Test/dafny0/AutoReq.dfy
@@ -0,0 +1,241 @@
+

+function f(x:int) : bool

+  requires x > 3;

+{

+  x > 7

+}

+

+// Should cause a function-requires failure

+function g(y:int) : bool    

+{

+  f(y)

+}

+

+// Should succeed thanks to auto-generation based on f's requirements

+function {:autoReq} h(y:int) : bool  

+{

+  f(y)

+}

+

+// Should fail based on h's inferred requirements

+function h_tester() : bool

+{

+  h(2)

+}

+

+// Should succeed thanks to auto_reqs

+function {:autoReq} i(y:int, b:bool) : bool

+{

+  if b then f(y + 2) else f(2*y)

+}

+

+method test() 

+{

+  // Function req violations (and assertion violations)

+  if (*) {

+    assert i(1, true);

+  } else if (*) {

+    assert i(0, false);

+  }

+

+  // Make sure function i's reqs can be satisfied

+  if (*) {

+    assert i(3, true);    // False assertion

+  }

+  assert i(7, false);     // True  assertion

+}

+

+module {:autoReq} TwoLayersOfRequires {

+  function f(x:int) : bool

+    requires x > 4;

+  {

+    x > 5

+  }

+

+  function g(y:int) : bool

+    requires y < 50;

+  {

+    f(y)

+  }

+

+  function h(z:int) : bool

+  {

+    g(z)

+  }

+}

+

+module {:autoReq} QuantifierTestsSimple {

+  function byte(x:int) : bool

+  {

+    0 <= x < 256

+  }

+

+  function f_forall(s:seq<int>) : bool

+  {

+    forall i :: 0 <= i < |s| ==> byte(s[i])

+  }

+

+  function f_exists(s:seq<int>) : bool

+  {

+    exists i :: 0 <= i < |s| && byte(s[i])

+  }

+

+  function g_forall(s:seq<int>) : bool

+    requires f_forall(s);

+  {

+    |s| > 2

+  }

+

+  function g_exists(s:seq<int>) : bool

+    requires f_exists(s);

+  {

+    |s| > 2

+  }

+

+  function h(s:seq<int>) : bool

+  {

+    g_forall(s) && g_exists(s)

+  }

+}

+

+module {:autoReq} QuantifierTestsHard {

+  function byte(x:int) : bool

+    requires 0 <= x < 256;

+  { true }

+

+  function f_forall(s:seq<int>) : bool

+  {

+    forall i :: 0 <= i < |s| ==> byte(s[i])

+  }

+

+  function f_exists(s:seq<int>) : bool

+  {

+    exists i :: 0 <= i < |s| && byte(s[i])

+  }

+

+  function g_forall(s:seq<int>) : bool

+    requires forall j :: 0 <= j < |s| ==> byte(s[j]);

+  {

+    |s| > 2

+  }

+

+  function h_forall(s:seq<int>) : bool

+  {

+    f_forall(s)

+  }

+

+  function h(s:seq<int>) : bool

+  {

+    g_forall(s) 

+  }

+

+  function i(s:seq<int>) : bool

+    requires forall k :: 0 <= k < |s| ==> 0 <= s[k] < 5;

+  {

+    true

+  }

+

+  function j(s:seq<int>) : bool

+  {

+    i(s)

+  }

+

+  function m(x:int) : bool

+  function n(x:int) : bool

+  

+  function f1(x:int) : bool

+	requires x > 3;

+	requires x < 16;

+

+  function variable_uniqueness_test(x:int) : bool

+  {

+    (forall y:int :: m(y))

+	&&

+	f1(x)

+  }

+}

+

+module CorrectReqOrdering {

+	function f1(x:int) : bool

+		requires x > 3;

+

+	function f2(b:bool) : bool

+		requires b;

+

+	// Should pass if done correctly.

+	// However, if Dafny incorrectly put the requires for f2 first,

+	// then the requires for f1 won't be satisfied

+	function {:autoReq} f3(z:int) : bool

+	{

+		f2(f1(z))

+	} 		

+

+}

+

+module ShortCircuiting {	

+	function f1(x:int) : bool

+		requires x > 3;

+

+	function f2(y:int) : bool

+		requires y < 10;

+

+	function {:autoReq} test1(x':int, y':int) : bool

+	{

+		f1(x') && f2(y')

+	}

+

+	function {:autoReq} test2(x':int, y':int) : bool

+	{

+		f1(x') ==> f2(y')

+	}

+

+	function {:autoReq} test3(x':int, y':int) : bool

+	{

+		f1(x') || f2(y')

+	}

+}

+

+module Lets {

+	function f1(x:int) : bool

+		requires x > 3;

+

+	function {:autoReq} test1(x':int) : bool

+	{

+		var y' := 3*x'; f1(y')

+	}

+}

+

+// Test nested module specification of :autoReq attribute

+module {:autoReq} M1 {

+    module M2 {

+        function f(x:int) : bool

+          requires x > 3;

+        {

+          x > 7

+        }

+

+        // Should succeed thanks to auto-generation based on f's requirements

+        function {:autoReq} h(y:int) : bool  

+        {

+          f(y)

+        }

+    }

+}

+

+/*  Not yet implemented

+module Matches {

+	datatype TheType = TheType_builder(x:int) | TheType_copier(t:TheType);

+

+	function f1(x:int):bool

+		requires x > 3;

+

+	function {:autoReq} basic_test(t:TheType) : bool

+	{

+		match t

+			case TheType_builder(x) => f1(x)

+			case TheType_copier(t) => true

+	}

+}

+*/

+

+

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index ae80dc89..3d4af611 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -29,7 +29,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy Definedness.dfy
             IteratorResolution.dfy Iterators.dfy

             RankPos.dfy RankNeg.dfy

             Computations.dfy ComputationsNeg.dfy

-            Include.dfy) do (

+            Include.dfy AutoReq.dfy) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f