diff options
| author |  kyessenov <unknown> | 2010-08-22 08:22:30 +0000 |
|---|---|---|
| committer | kyessenov <unknown> | 2010-08-22 08:22:30 +0000 |
| commit | f21eae9384b0bf2c53085b6663550b539c0987e0 (patch) | |
| tree | 14025e269860ac6047789a21b6f2f07cf06159dd | |
| parent | 1b845564918d06c7aca9f35421ccd1dccee3df01 (diff) | |
Chalice: refining lists doesn't quite work yet...
| -rw-r--r-- | Chalice/refinements/List.chalice | 47 | ||||
| -rw-r--r-- | Chalice/src/Translator.scala | 2 |
2 files changed, 49 insertions, 0 deletions
diff --git a/Chalice/refinements/List.chalice b/Chalice/refinements/List.chalice new file mode 100644 index 00000000..b13f6ee3 --- /dev/null +++ b/Chalice/refinements/List.chalice @@ -0,0 +1,47 @@ +class List0 {
+ var rep: seq<int>;
+
+ method init()
+ requires acc(rep);
+ ensures acc(rep);
+ {
+ rep := [0];
+ }
+
+ method get(i) returns (v)
+ requires acc(rep);
+ requires 0 <= i && i < |rep|;
+ ensures acc(rep);
+ {
+ v := rep[i];
+ }
+}
+
+class List1 refines List0 {
+ var sub: seq<List1>;
+ var data: int;
+
+ replaces rep by acc(sub) && acc(data) && acc(sub[*].sub) && acc(sub[*].data) &&
+ /** valid */ |sub| >= 0 &&
+ (forall i in [0..|sub|] :: sub[i] != null && sub[i].sub == sub[i+1..]) &&
+ /** coupling */ |sub| + 1 == |rep| &&
+ (forall i in [0..|sub|] :: sub[i].data == rep[i+1]) &&
+ data == rep[0]
+
+ refines init()
+ {
+ data := 0;
+ sub := nil<List1>;
+ }
+
+ refines get(i) returns (v)
+ {
+ if (i == 0) {
+ v := data;
+ } else {
+ var next:List1 := sub[0];
+ call v := next.get(i-1);
+ //v := sub[i-1].data;
+ }
+ }
+}
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala index ef27e635..5b9e442f 100644 --- a/Chalice/src/Translator.scala +++ b/Chalice/src/Translator.scala @@ -2250,6 +2250,7 @@ object TranslationHelper { def FractionOf(expr: Expression, fraction: Expression) : Expression = {
val result = expr match {
case Access(e, Full) => Access(e, Frac(fraction))
+ case AccessSeq(e, f, Full) => AccessSeq(e, f, Frac(fraction))
case And(lhs, rhs) => And(FractionOf(lhs, fraction), FractionOf(rhs, fraction))
case Implies(lhs, rhs) => Implies(lhs, FractionOf(rhs, fraction))
case _ if ! expr.isInstanceOf[PermissionExpr] => expr
@@ -2262,6 +2263,7 @@ object TranslationHelper { def canTakeFractionOf(expr: Expression): Boolean = {
expr match {
case Access(e, Full) => true
+ case AccessSeq(e, f, Full) => true
case And(lhs, rhs) => canTakeFractionOf(lhs) && canTakeFractionOf(rhs)
case Implies(lhs, rhs) => canTakeFractionOf(rhs)
case _ if ! expr.isInstanceOf[PermissionExpr] => true
|