Dafny: Changed the semantics of the assign-such-that statement "x :| P;" to check the existence of a value. The previous "assume only" version is available by supplying the keyword "assume" in front of "P".

1 files changed, 29 insertions, 3 deletions

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 95110629..f8b78692 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -1703,14 +1703,22 @@ namespace Microsoft.Dafny {
 

   public class AssignSuchThatStmt : ConcreteUpdateStatement

   {

-    public readonly AssumeStmt Assume;

-    public AssignSuchThatStmt(IToken tok, List<Expression> lhss, Expression expr)

+    public readonly Expression Expr;

+    public readonly IToken AssumeToken;

+    /// <summary>

+    /// "assumeToken" is allowed to be "null", in which case the verifier will check that a RHS value exists.

+    /// If "assumeToken" is non-null, then it should denote the "assume" keyword used in the statement.

+    /// </summary>

+    public AssignSuchThatStmt(IToken tok, List<Expression> lhss, Expression expr, IToken assumeToken)

       : base(tok, lhss) {

       Contract.Requires(tok != null);

       Contract.Requires(cce.NonNullElements(lhss));

       Contract.Requires(lhss.Count != 0);

       Contract.Requires(expr != null);

-      Assume = new AssumeStmt(tok, expr);

+      Expr = expr;

+      if (assumeToken != null) {

+        AssumeToken = assumeToken;

+      }

     }

   }

 

@@ -1771,6 +1779,24 @@ namespace Microsoft.Dafny {
         }

       }

     }

+

+    /// <summary>

+    /// This method assumes "lhs" has been successfully resolved.

+    /// </summary>

+    public static bool LhsIsToGhost(Expression lhs) {

+      Contract.Requires(lhs != null);

+      lhs = lhs.Resolved;

+      if (lhs is IdentifierExpr) {

+        var x = (IdentifierExpr)lhs;

+        return x.Var.IsGhost;

+      } else if (lhs is FieldSelectExpr) {

+        var x = (FieldSelectExpr)lhs;

+        return x.Field.IsGhost;

+      } else {

+        // LHS denotes an array element, which is always non-ghost

+        return false;

+      }

+    }

   }

 

   public class VarDecl : Statement, IVariable {