Chalice: Introduced '[[ S ]]' as a shorthand syntax for 'lock (this) { S }'. Think of the new brackets as atomicity brackets (see PetersonsAlgorithm.chalice)

Chalice:  Added Peterson's algorithm to test suite (safety properties only)
VS 2010 integration: Updated Chalice and Dafny modes, added keyword highlighting for a new Boogie mode

5 files changed, 15 insertions, 10 deletions

diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Configuration.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Configuration.cs
index 8615eee7..2eb57f11 100644
--- a/Util/VS2010/Chalice/ChaliceLanguageService/Configuration.cs
+++ b/Util/VS2010/Chalice/ChaliceLanguageService/Configuration.cs
@@ -7,9 +7,8 @@ namespace Demo
 {

     public static partial class Configuration

     {

-        public const string Name = "My C";

-//        public const string FormatList = "My C File (*.myc)\n*.myc";

-        public const string FormatList = "My C File (*.chalice)\n*.chalice";

+        public const string Name = "Chalice";

+        public const string FormatList = "Chalice File (*.chalice)\n*.chalice";

 

         static Configuration()

         {

diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs
index 56f53c28..7a856d36 100644
--- a/Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs
+++ b/Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs
@@ -5,7 +5,7 @@ using Irony.Parsing;
 

 namespace Demo

 {

-    [Language("My C", "1.0", "My C Programming Language")]

+    [Language("Chalice", "1.0", "Chalice Programming Language")]

     public class Grammar : Irony.Parsing.Grammar

     {

       public Grammar() {

@@ -74,10 +74,12 @@ namespace Demo
         NonTerminal NewStmt = new NonTerminal("NewStmt");

         NonTerminal NewArrStmt = new NonTerminal("NewArrStmt");

         NonTerminal QualifiedName = new NonTerminal("QualifiedName");

+        NonTerminal AccessQualName = new NonTerminal("AccessQualName");

         NonTerminal GenericsPostfix = new NonTerminal("GenericsPostfix");

         NonTerminal ArrayExpression = new NonTerminal("ArrayExpression");

         NonTerminal FunctionExpression = new NonTerminal("FunctionExpression");

         NonTerminal selectExpr = new NonTerminal("selectExpr");

+        NonTerminal accessExpr = new NonTerminal("accessExpr");

         #endregion

 

         #region 2.3 Statement

@@ -125,6 +127,7 @@ namespace Demo
 

         #region 3.1 Expressions

         selectExpr.Rule = (ToTerm("this") + ".").Q() + QualifiedName;

+        accessExpr.Rule = (ToTerm("this") + ".").Q() + AccessQualName;

         evalstate.Rule =

           ident + ToTerm(".") +

           (ToTerm("acquire")

@@ -159,7 +162,7 @@ namespace Demo
                     | LMb + declaration.Star() + RMb

                     | LParen + expression + RParen

                     | ToTerm("unfolding") + expression + "in" + expression

-                    | ToTerm("acc") + "(" + selectExpr  + (("," + expression) | Empty) + ")"

+                    | ToTerm("acc") + "(" + accessExpr  + (("," + expression) | Empty) + ")"

                     | ToTerm("old") + "(" + expression + ")"

                     | ToTerm("eval") + "(" + evalstate + "," + expression + ")"

                     | ToTerm("credit") + "(" + expression + "," + expression + ")"

@@ -167,7 +170,7 @@ namespace Demo
                     | expression + PreferShiftHere() + "?" + expression + ":" + expression

                     | ToTerm("rd") +

                       (ToTerm("holds") + "(" + expression + ")"

-                      | "(" + selectExpr + rdPermArg.Q() + ")"

+                      | "(" + accessExpr + rdPermArg.Q() + ")"

                       )

 

                     ;

@@ -196,6 +199,7 @@ namespace Demo
         FunctionExpression.Rule = QualifiedName + LParen + expressionList.Q() + RParen;

 

         QualifiedName.Rule = ident | QualifiedName + dot + ident;

+        AccessQualName.Rule = ident | "*" | QualifiedName + dot + (ident | "*");

 

 

         GenericsPostfix.Rule = less + QualifiedName + greater;

@@ -256,6 +260,8 @@ namespace Demo
                         | "assert" + expression + Semi

                         | "assume" + expression + Semi

                         | "unshare" + expression + Semi

+                        | "lock" + Condition + Statement

+                        | "[[" + Statements + "]]"

                         | "acquire" + expression + Semi

                         | "release" + expression + Semi

                         | "downgrade" + expression + Semi

diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/IronyLanguageServicePackage.cs b/Util/VS2010/Chalice/ChaliceLanguageService/IronyLanguageServicePackage.cs
index 5c475d35..8b9cb825 100644
--- a/Util/VS2010/Chalice/ChaliceLanguageService/IronyLanguageServicePackage.cs
+++ b/Util/VS2010/Chalice/ChaliceLanguageService/IronyLanguageServicePackage.cs
@@ -53,7 +53,7 @@ namespace Demo
     // package needs to have a valid load key (it can be requested at 

     // http://msdn.microsoft.com/vstudio/extend/). This attributes tells the shell that this 

     // package has a load key embedded in its resources.

-    [ProvideLoadKey("Standard", "1.0", "My C", "Demo", 104)]

+    [ProvideLoadKey("Standard", "1.0", "Chalice", "Demo", 104)]

     [Guid(GuidList.guidIronyLanguageServicePkgString)]

     public sealed class MyCLanguageService : IronyPackage

     {

diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/VSPackage.resx b/Util/VS2010/Chalice/ChaliceLanguageService/VSPackage.resx
index c4e76be7..4c4adabd 100644
--- a/Util/VS2010/Chalice/ChaliceLanguageService/VSPackage.resx
+++ b/Util/VS2010/Chalice/ChaliceLanguageService/VSPackage.resx
@@ -121,9 +121,9 @@
     <value>Paste PLK Here</value>

   </data>

   <data name="110" xml:space="preserve">

-    <value>My C</value>

+    <value>Chalice</value>

   </data>

   <data name="112" xml:space="preserve">

-    <value>My C Programming Language</value>

+    <value>Chalice Programming Language</value>

   </data>

 </root>
\ No newline at end of file
diff --git a/Util/VS2010/Chalice/StartChalice.bat b/Util/VS2010/Chalice/StartChalice.bat
index 8e066298..d91322ba 100644
--- a/Util/VS2010/Chalice/StartChalice.bat
+++ b/Util/VS2010/Chalice/StartChalice.bat
@@ -3,7 +3,7 @@ echo ---------- Starting ------------ < nul >> c:\tmp\coo.out
 time < nul >> c:\tmp\coo.out

 echo. < nul >> c:\tmp\coo.out

 

-call "c:\Program Files\Scala\bin\scala" -cp c:\boogie\Chalice\bin Chalice -nologo -vs -noDeadlockChecks %* 2>> c:\tmp\coo.out

+call "c:\Program Files\Scala\bin\scala" -cp c:\boogie\Chalice\bin Chalice -nologo -vs %* 2>> c:\tmp\coo.out

 

 time < nul >> c:\tmp\coo.out

 echo. < nul >> c:\tmp\coo.out