diff options
| -rw-r--r-- | Chalice/refinements/DuplicatesVideo.chalice | 4 | ||||
| -rw-r--r-- | Chalice/src/Parser.scala | 2 | ||||
| -rw-r--r-- | Util/Emacs/chalice-mode.el | 1 |
3 files changed, 5 insertions, 2 deletions
diff --git a/Chalice/refinements/DuplicatesVideo.chalice b/Chalice/refinements/DuplicatesVideo.chalice index f4894faf..abb2a429 100644 --- a/Chalice/refinements/DuplicatesVideo.chalice +++ b/Chalice/refinements/DuplicatesVideo.chalice @@ -2,7 +2,7 @@ class Duplicates0 { method find(s:seq<int>) returns (b: bool)
requires forall i in s :: i in [0..100];
{
- spec b [b <==> (exists i in [0..|s|] :: s[i] in s[..i])];
+ spec b [b <==> exists i in [0..|s|] :: s[i] in s[..i] ];
}
}
@@ -13,7 +13,7 @@ class Duplicates1 refines Duplicates0 { b := false;
while (n < |s|)
invariant 0 <= n && n <= |s|;
- invariant b <==> (exists i in [0..n] :: s[i] in s[..i]);
+ invariant b <==> exists i in [0..n] :: s[i] in s[..i];
{
spec c:bool [c <==> s[n] in s[..n] ];
b := b || c;
diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala index 2d3f99fc..27b4945d 100644 --- a/Chalice/src/Parser.scala +++ b/Chalice/src/Parser.scala @@ -274,6 +274,8 @@ class Parser extends StandardTokenParsers { case Some(NewRhs(tid, _, _, _)) => Type(tid, Nil)
case Some(BoolLiteral(b)) => Type("bool", Nil)
case Some(x:BinaryExpr) if x.ResultType != null => new Type(x.ResultType);
+ case Some(x:Contains) => Type("bool", Nil)
+ case Some(x:Quantification) => Type("bool", Nil)
case _ => Type("int", Nil)
}
}, ghost, const)
diff --git a/Util/Emacs/chalice-mode.el b/Util/Emacs/chalice-mode.el index 34a95a87..0798753e 100644 --- a/Util/Emacs/chalice-mode.el +++ b/Util/Emacs/chalice-mode.el @@ -33,6 +33,7 @@ "class" "ghost" "var" "const" "external" "function" "method"
"predicate" "returns" "requires" "ensures" "lockchange"
"invariant" "channel" "condition" "where"
+ "refines" "replaces" "by" "transforms"
)) . font-lock-builtin-face)
`(,(chalice-regexp-opt '(
"above" "acc" "acquire" "and" "assert" "assigned" "assume"
|