Chalice: added "exists" quantifier; changed surface syntax for quantifier expressions

8 files changed, 68 insertions, 46 deletions

diff --git a/Chalice/examples/RockBand.chalice b/Chalice/examples/RockBand.chalice
index c7a2bba0..49b99a68 100644
--- a/Chalice/examples/RockBand.chalice
+++ b/Chalice/examples/RockBand.chalice
@@ -19,7 +19,7 @@ class RockBand module M {
     acc(gigs) && 0 <= gigs &&

     acc(gt) && gt != null && gt.Valid &&

     acc(gt.mu) &&  // to enable an eventual free

-    acc(doowops) && //forall{d: Vocalist in doowops; d != null && d.Valid} &&

+    acc(doowops) && //forall d: Vocalist in doowops :: d != null && d.Valid} &&

     acc(b3) && b3 != null && b3.Valid &&

     acc(b3.mu)  // to enable an eventual free

   }

diff --git a/Chalice/examples/iterator.chalice b/Chalice/examples/iterator.chalice
index 356e6d83..833a5a61 100644
--- a/Chalice/examples/iterator.chalice
+++ b/Chalice/examples/iterator.chalice
@@ -12,7 +12,7 @@ class List module Collections {
   method add(x: int) 

     requires valid;

     ensures valid && size(100) == old(size(100)+1) && get(size(100)-1, 100) == x;

-    ensures forall { i in [0:size(100)-1]; get(i, 100) == old(get(i, 100)) };

+    ensures forall i in [0:size(100)-1] :: get(i, 100) == old(get(i, 100));

   {

     unfold valid;

     contents := contents ++ [x];

@@ -21,7 +21,7 @@ class List module Collections {
 

   function get(index: int, f: int): int 

     requires 0<f && f<=100 && acc(valid, f) && (0<=index && index<size(f));

-    ensures forall { i in [1:f]; get(index, f) == get(index, i)};

+    ensures forall i in [1:f] :: get(index, f) == get(index, i);

   {

     unfolding acc(valid, f) in contents[index]

   }

@@ -29,7 +29,7 @@ class List module Collections {
   function size(f: int): int 

     requires 0<f && f<=100 && acc(valid, f);

     ensures 0<=result;

-    ensures forall { i in [1:f]; size(f) == size(i)};

+    ensures forall i in [1:f] :: size(f) == size(i);

   {

     unfolding acc(valid, f) in |contents|

   }

@@ -147,4 +147,4 @@ class Program module Main {
     assert list.valid;

     assert list.size(50)==2;

   }

-}
\ No newline at end of file
+}

diff --git a/Chalice/examples/iterator2.chalice b/Chalice/examples/iterator2.chalice
index 5b75c1ca..f5a86909 100644
--- a/Chalice/examples/iterator2.chalice
+++ b/Chalice/examples/iterator2.chalice
@@ -14,7 +14,7 @@ class List module Collections {
   method add(x: int) 

     requires valid;

     ensures valid && size() == old(size()+1) && get(size()-1) == x; // I don't know why this happens.

-    ensures forall { i in [0:size()-1]; get(i) == old(get(i)) };

+    ensures forall i in [0:size()-1] :: get(i) == old(get(i));

   {

     unfold valid;

     contents := contents ++ [x];

@@ -131,4 +131,4 @@ class Program module Main {
     assert list.valid;

     assert list.size()==2;

   }

-}
\ No newline at end of file
+}

diff --git a/Chalice/examples/producer-consumer.chalice b/Chalice/examples/producer-consumer.chalice
index 99756d65..11687e80 100644
--- a/Chalice/examples/producer-consumer.chalice
+++ b/Chalice/examples/producer-consumer.chalice
@@ -164,7 +164,7 @@ class List module Collections {
   method add(x: int) 

     requires valid;

     ensures valid && size() == old(size()+1) && get(size()-1) == x;

-    ensures forall { i in [0:size()-1]; get(i) == old(get(i)) };

+    ensures forall i in [0:size()-1] :: get(i) == old(get(i));

   {

     unfold valid;

     contents := contents ++ [x];

@@ -174,7 +174,7 @@ class List module Collections {
   method removeFirst() returns (rt: int) 

     requires valid && 0<size();

     ensures valid && size() == old(size()-1);

-    ensures forall { i  in [0:size()]; get(i) == old(get(i+1)) };

+    ensures forall i in [0:size()] :: get(i) == old(get(i+1));

   {

     unfold valid;

     rt := contents[0];

@@ -199,4 +199,4 @@ class List module Collections {
   predicate valid {

     acc(contents)

   }

-}
\ No newline at end of file
+}

diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index 61d7a0f3..9ca324d7 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -371,6 +371,9 @@ sealed abstract class Quantification(is: List[String], seq: Expression, e: Expre
 case class Forall(is: List[String], seq: Expression, e: Expression) extends Quantification(is, seq, e) {

   override def Quantor = "forall"

 }

+case class Exists(is: List[String], seq: Expression, e: Expression) extends Quantification(is, seq, e) {

+  override def Quantor = "exists"

+}

 

 // sequences

 

@@ -380,10 +383,10 @@ case class Range(min: Expression, max: Expression /* non-inclusive*/) extends Ex
 case class Append(s0: Expression, s1: Expression) extends SeqAccess(s0, s1) {

   override val OpName = "++"

 }

- sealed abstract case class SeqAccess(e0: Expression, e1: Expression) extends BinaryExpr(e0, e1)

+sealed abstract case class SeqAccess(e0: Expression, e1: Expression) extends BinaryExpr(e0, e1)

 case class Length(e: Expression) extends Expression

 case class At(s: Expression, n: Expression) extends SeqAccess(s, n) {

-  override val OpName = "@"

+  override val OpName = ""

 }

 case class Drop(s: Expression, n: Expression) extends SeqAccess(s, n) {

   override val OpName = ""

diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index 98ba0416..8a87d2f6 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -40,7 +40,7 @@ class Parser extends StandardTokenParsers {
                          "<==>", "==>", "&&", "||",

                          "==", "!=", "<", "<=", ">=", ">", "<<",

                          "+", "-", "*", "/", "%", "!", ".", "..",

-                         ";", ":", ":=", ",", "?", "|", "@", "[", "]", "++")

+                         ";", ":", ":=", ",", "?", "|", "[", "]", "++", "::")

 

   def programUnit = (classDecl | channelDecl)*

 

@@ -459,11 +459,18 @@ class Parser extends StandardTokenParsers {
     | ("nil" ~> "<") ~> (typeDecl <~ ">") ^^ EmptySeq

     | ("[" ~> expressionList <~ "]") ^^ { case es => ExplicitSeq(es) }

     )

-  def forall: Parser[Forall] =

-    (("forall" ~ "{") ~> repsep(ident, ",") <~ "in") into { is => (expression <~ ";") ~ (exprWithLocals(is) <~ "}") ^^ 

-      { case seq ~ e => val result = Forall(is, seq, e); currentLocalVariables = currentLocalVariables -- is; result } }

+  def forall: Parser[Quantification] =

+    (("forall" | "exists") ~ repsep(ident, ",") <~ "in") into {case quant ~ is => quantifierBody(quant, is)}

+

+  def quantifierBody(quant: String, is: List[String]) : Parser[Quantification] =

+    ((expression <~ "::") ~ (exprWithLocals(is))) ^^

+      { case seq ~ e =>

+        val result = quant match {case "forall" => Forall(is, seq, e); case "exists" => Exists(is, seq, e);};

+        currentLocalVariables = currentLocalVariables -- is;

+        result

+      }  

+

   def exprWithLocals(i: List[String]) : Parser[Expression] = {

-    val savedCurrentLocals = currentLocalVariables;

     currentLocalVariables = currentLocalVariables ++ i;

     val result = ((expression) ^^ { case e => e});

     result

diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala
index dea0f2d5..bcf51826 100644
--- a/Chalice/src/PrettyPrinter.scala
+++ b/Chalice/src/PrettyPrinter.scala
@@ -262,12 +262,12 @@ object PrintProgram {
     case e:Div => BinExpr(e, e.OpName, 0x60, false, true, contextBindingPower, fragileContext)

     case e:Mod => BinExpr(e, e.OpName, 0x60, false, true, contextBindingPower, fragileContext)

     case q:Quantification => 

-      print(q.Quantor + "{"); 

+      print("(" + q.Quantor + " "); 

       q.Is match {

         case Nil =>

         case i :: rest => print(i); rest foreach { v => print(", " + v) }

       }

-      print(" in "); Expr(q.Seq); print("; "); Expr(q.E); print("}");

+      print(" in "); Expr(q.Seq); print(" :: "); Expr(q.E); print(")");

     case EmptySeq(t) =>

       print("nil<"); print(t.FullName); print(">");

     case ExplicitSeq(es) =>

@@ -276,8 +276,8 @@ object PrintProgram {
       print("("); Expr(min); print(":"); Expr(max); print(")");

     case Length(e)=>

       print("|"); Expr(e); print("|");

-    case e:At =>

-      BinExpr(e, e.OpName, 0x45, true, true, contextBindingPower, fragileContext)

+    case At(s, n) =>

+      Expr(s); print("["); Expr(n); print("]");

     case e:Append =>

       BinExpr(e, e.OpName, 0x45, true, true, contextBindingPower, fragileContext)

     case Drop(s, n) =>

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index efee5b13..5039395b 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -1254,14 +1254,15 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
       case e: ArithmeticExpr =>

         isDefined(e.E0) ::: isDefined(e.E1)

       case q@Forall(i, Range(min, max), e) =>

-        // optimize for range

-        isDefinedForall(q.variables, min, max, e)

+        isDefinedQuantification(q.variables, min, max, e)

+      case q@Exists(i, Range(min, max), e) =>

+        isDefinedQuantification(q.variables, min, max, e)

       case q@Forall(i, seq, e) =>

-      var newVars = Nil : List[Variable];

-        for(i <- q.variables) {

-          newVars = newVars + new Variable(i.UniqueName, new Type(IntClass))

-        }

-        isDefinedForall(newVars, IntLiteral(0), Length(seq), SubstVars(e, q.variables, newVars map {newVar => At(seq, new VariableExpr(newVar)) }))

+        var newVars = q.variables map (v => new Variable(v.UniqueName, new Type(IntClass)))

+        isDefinedQuantification(newVars, IntLiteral(0), Length(seq), SubstVars(e, q.variables, newVars map {v => At(seq, new VariableExpr(v)) }))

+      case q@Exists(i, seq, e) =>

+        var newVars = q.variables map (v => new Variable(v.UniqueName, new Type(IntClass)))

+        isDefinedQuantification(newVars, IntLiteral(0), Length(seq), SubstVars(e, q.variables, newVars map {v => At(seq, new VariableExpr(v)) }))

       case EmptySeq(t) => Nil

       case ExplicitSeq(es) =>

         es flatMap { e => isDefined(e) }

@@ -1284,7 +1285,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
     }

   }

 

-  def isDefinedForall(is: List[Variable], min: Expression, max: Expression, e: Expression)(implicit assumption: Expr): List[Stmt] = {

+  def isDefinedQuantification(is: List[Variable], min: Expression, max: Expression, e: Expression)(implicit assumption: Expr): List[Stmt] = {

     var iTmps = Nil: List[Variable];

     var assumption2 = assumption;

     for(i <- is) { 

@@ -1296,9 +1297,9 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
     isDefined(min) ::: isDefined(max) :::

     // introduce a new local iTmp with an arbitrary value

     (iTmps map { iTmp =>

-      BLocal(Boogie.BVar(iTmp.UniqueName, Boogie.NamedType("int")))

+      BLocal(Boogie.BVar(iTmp.UniqueName, tint))

     }) :::

-    // prove that the body is well-defined for iTmp, provided iTmp lies betweeen min and max 

+    // prove that the body is well-defined for iTmp, provided iTmp lies between min and max

     isDefined(SubstVars(e, is, iTmps map { iTmp => new VariableExpr(iTmp)}))(assumption2)

   }

 

@@ -1395,15 +1396,10 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
       Tr(e0) / Tr(e1)

     case Mod(e0,e1) =>

       Tr(e0) % Tr(e1)

-    case q@Forall(is, Range(min, max), e) =>

-      // optimize translation for range expressions

-      translateForall(q.variables, min, max, e)

-    case q@Forall(is, seq, e) =>

-      var newVars = Nil : List[Variable];

-      for(i <- q.variables) {

-        newVars = newVars + new Variable(i.UniqueName, new Type(IntClass))

-      }

-      translateForall(newVars, IntLiteral(0), Length(seq), SubstVars(e, q.variables, newVars map {newVar => At(seq, new VariableExpr(newVar)) }))

+    case q: Forall =>

+      translateQuantification(q)

+    case q: Exists =>

+      translateQuantification(q)

     case EmptySeq(t) =>

       createEmptySeq

     case ExplicitSeq(es) =>

@@ -1430,12 +1426,28 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
       evalEtran.Tr(e)

   }

 

-  def translateForall(is: List[Variable], min: Expression, max: Expression, e: Expression): Expr = {

+  def translateQuantification(q: Quantification): Expr = {

+    // generate index variables

+    var (is, min, max, e) = q match {

+      case Forall(_, Range(min, max), e) => (q.variables, min, max, e);

+      case Exists(_, Range(min, max), e) => (q.variables, min, max, e);

+      case Forall(_, seq, eo) =>

+        var is = q.variables map (v => new Variable(v.UniqueName, new Type(IntClass)));

+        var e = SubstVars(eo, q.variables, is map {v => At(seq, new VariableExpr(v))});

+        (is, IntLiteral(0), Length(seq), e);

+      case Exists(_, seq, eo) =>

+        var is = q.variables map (v => new Variable(v.UniqueName, new Type(IntClass)));

+        var e = SubstVars(eo, q.variables, is map {v => At(seq, new VariableExpr(v))});

+        (is, IntLiteral(0), Length(seq), e);

+    }

     var assumption = true: Expr;

     for(i <- is) {

       assumption = assumption && (Tr(min) <= VarExpr(i.UniqueName) && VarExpr(i.UniqueName) < Tr(max));

     }

-    new Boogie.Forall(is map { i=> Variable2BVar(i)}, Nil, assumption ==> Tr(e))

+    q match {

+      case _: Forall => new Boogie.Forall(is map { i => Variable2BVar(i)}, Nil, assumption ==> Tr(e));

+      case _: Exists => new Boogie.Exists(is map { i => Variable2BVar(i)}, Nil, assumption && Tr(e));

+    }

   }

 

   def ShaveOffOld(e: Expression): (Expression, boolean) = e match {

@@ -1906,11 +1918,11 @@ object S_ExpressionTranslator {
   }

 }

 

+  // implicit

 

-  // implicit 

-  implicit def string2VarExpr(s: String) = VarExpr(s)

-  implicit def expression2Expr(e: Expression) = etran.Tr(e)

-  implicit def field2Expr(f: Field) = VarExpr(f.FullName)

+  implicit def string2VarExpr(s: String) = VarExpr(s);

+  implicit def expression2Expr(e: Expression) = etran.Tr(e);

+  implicit def field2Expr(f: Field) = VarExpr(f.FullName);

 

   // prelude