Boogie:

* Added support for polymorphism in lambda expressions
* Little clean-up here and there
* Added 'then' keyword to emacs and latex modes

Dafny:
* Added support for fine-grained framing, using the back-tick syntax from Region Logic
* Internally, changed checking of reads clauses to use a local variable $_Frame, analogous to the $_Frame variable used in checking modifies clauses

1 files changed, 2 insertions, 0 deletions

diff --git a/Source/AIFramework/CommonFunctionSymbols.ssc b/Source/AIFramework/CommonFunctionSymbols.ssc
index f014e963..e05e8dac 100644
--- a/Source/AIFramework/CommonFunctionSymbols.ssc
+++ b/Source/AIFramework/CommonFunctionSymbols.ssc
@@ -614,6 +614,7 @@ namespace Microsoft.AbstractInterpretationFramework
         private static readonly FunctionSymbol! _implies = new FunctionSymbol("==>", binproptype);

         private static readonly FunctionSymbol! _exists = new FunctionSymbol("Exists", quantifiertype);

         private static readonly FunctionSymbol! _forall = new FunctionSymbol("Forall", quantifiertype);

+        private static readonly FunctionSymbol! _lambda = new FunctionSymbol("Lambda", quantifiertype);

 

 

         [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! False { get { return _false; } }

@@ -624,6 +625,7 @@ namespace Microsoft.AbstractInterpretationFramework
         [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Implies { get { return _implies; } }

         [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Exists { get { return _exists; } }

         [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Forall { get { return _forall; } }

+        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Lambda { get { return _lambda; } }

 

 

         /// <summary>