summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Chalice/refinements/Answer3
-rw-r--r--Chalice/refinements/Calculator.chalice69
-rw-r--r--Chalice/refinements/Counter.chalice92
-rw-r--r--Chalice/refinements/test.sh3
-rw-r--r--Chalice/src/Ast.scala2
-rw-r--r--Chalice/src/Parser.scala10
-rw-r--r--Chalice/src/PrettyPrinter.scala2
-rw-r--r--Chalice/src/Resolver.scala11
8 files changed, 110 insertions, 82 deletions
diff --git a/Chalice/refinements/Answer b/Chalice/refinements/Answer
index 6db2a988..a6654fc2 100644
--- a/Chalice/refinements/Answer
+++ b/Chalice/refinements/Answer
@@ -35,3 +35,6 @@ Processing TestCoupling.chalice
66.5: Location might not be writable
Boogie program verifier finished with 17 verified, 3 errors
+Processing Calculator.chalice
+
+Boogie program verifier finished with 15 verified, 0 errors
diff --git a/Chalice/refinements/Calculator.chalice b/Chalice/refinements/Calculator.chalice
new file mode 100644
index 00000000..57c4c87d
--- /dev/null
+++ b/Chalice/refinements/Calculator.chalice
@@ -0,0 +1,69 @@
+/*
+ Carrol Morgan's calculator
+ 7/2/2010 Kuat Dafny version
+ 8/22/2010 translated into Chalice
+*/
+
+class Calc0 {
+ var vals: seq<int>;
+
+ method reset()
+ requires acc(vals);
+ ensures acc(vals);
+ {
+ vals := [];
+ }
+
+ method add(x: int)
+ requires acc(vals);
+ ensures acc(vals);
+ {
+ vals := [x] ++ vals;
+ }
+
+ method mean() returns (m: int)
+ requires acc(vals) && |vals| > 0;
+ ensures acc(vals);
+ {
+ m := total(vals)/|vals|;
+ }
+
+ unlimited function total(s: seq<int>): int
+ {
+ |s| == 0 ? 0 : s[0] + total(s[1..])
+ }
+}
+
+
+
+class Calc1 refines Calc0 {
+ var sum: int;
+ var num: int;
+ replaces vals by acc(sum) && acc(num) && sum == total(vals) && num == |vals|;
+
+ refines reset()
+ {
+ sum := 0;
+ num := 0;
+ }
+
+ refines add(x: int)
+ {
+ sum := sum + x;
+ num := num + 1;
+ }
+
+ refines mean() returns (m: int)
+ {
+ m := sum/num;
+ }
+}
+
+
+
+
+
+
+
+
+
diff --git a/Chalice/refinements/Counter.chalice b/Chalice/refinements/Counter.chalice
index c9576a13..e0c0c7df 100644
--- a/Chalice/refinements/Counter.chalice
+++ b/Chalice/refinements/Counter.chalice
@@ -21,24 +21,6 @@ class Counter0 {
{
x := x - 1;
}
-
- /** Interesting issues */
-
- /* We can expose representation here */
- method magic1() returns (c: Cell)
- requires acc(x)
- ensures acc(c.n) && x == old(x);
- {
- var c [acc(c.n)];
- }
-
- /* This should prevent us from exposing representation */
- method magic2() returns (c: Cell)
- requires acc(x);
- ensures acc(x) && x == old(x) && acc(c.n);
- {
- var c [acc(c.n)];
- }
}
class Counter1 refines Counter0 {
@@ -46,80 +28,50 @@ class Counter1 refines Counter0 {
var z: int;
replaces x by acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0;
- transforms init()
+ refines init()
{
- replaces * by {this.y := 0; this.z := 0;}
+ this.y := 0;
+ this.z := 0;
}
- transforms inc()
+ refines inc()
{
- replaces * by {this.y := this.y + 1;}
+ this.y := this.y + 1;
}
- transforms dec()
+ refines dec()
{
- replaces * by {this.z := this.z + 1;}
+ this.z := this.z + 1;
}
-
- /** This violates abstraction of x -- we must hold all permissions to x to update it */
- method magic3()
- requires acc(y);
- {
- y := y + 1;
- }
-
- /** This does also -- but it also prohibits us from reading part of the state across refinement */
- method magic4() returns (i)
- requires acc(y);
- {
- i := y;
- }
}
class Cell {var n: int}
-/*
+
+/** TODO:
+Two-step data refinement doesn't work for the following reason:
+the spec of Counter1 uses the abstract field x which disappears at the concrete method body level.
+I'm not sure what a good solution to this problem...
+*/
+
class Counter2 refines Counter1 {
var a: Cell;
var b: Cell;
replaces y, z by acc(a) && acc(b) && acc(a.n) && acc(b.n) && y == a.n && z == b.n;
- transforms init()
- {
- replaces * by {
- this.a := new Cell {n := 0};
- this.b := new Cell {n := 0};
- }
- }
-
- transforms inc()
- {
- replaces * by {this.a.n := this.a.n + 1;}
- }
-
- transforms dec()
- {
- replaces * by {this.b.n := this.b.n + 1;}
- }
-
- transforms magic1() returns (c: Cell)
- {
- replaces * by {c := this.a;}
- }
-
- transforms magic2() returns (c: Cell)
- {
- replaces * by {c := this.a;}
+ refines init()
+ {
+ this.a := new Cell {n := 0};
+ this.b := new Cell {n := 0};
}
- transforms magic3()
+ refines inc()
{
- replaces * by {this.a.n := this.a.n + 1;}
+ this.a.n := this.a.n + 1;
}
- transforms magic4() returns (i)
+ refines dec()
{
- replaces * by {i := this.a.n;}
+ this.b.n := this.b.n + 1;
}
}
-*/
diff --git a/Chalice/refinements/test.sh b/Chalice/refinements/test.sh
index 24dbd6e5..80b42258 100644
--- a/Chalice/refinements/test.sh
+++ b/Chalice/refinements/test.sh
@@ -14,6 +14,7 @@ TESTS="
LoopFiniteDiff.chalice
Pick.chalice
TestCoupling.chalice
+ Calculator.chalice
"
# Switch to test directory
@@ -31,7 +32,7 @@ START=`date +%s`
for f in ${TESTS}
do
echo "Processing $f" | tee -a Output
- scala -cp ../bin chalice.Chalice -nologo $f >> Output 2>&1
+ scala -cp ../bin chalice.Chalice -nologo -noTermination $f >> Output 2>&1
done
END=`date +%s`
echo "Time: $(( $END - $START )) seconds"
diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index 92c339ea..7beba704 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -164,7 +164,7 @@ case class Function(id: String, ins: List[Variable], out: Type, spec: List[Speci
result.f = this;
result
}
- val isUnlimited = false
+ var isUnlimited = false
var isRecursive = false
var SCC: List[Function] = Nil
}
diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index d12ca00f..f086487d 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -30,7 +30,7 @@ class Parser extends StandardTokenParsers {
"predicate", "function", "free", "send", "receive",
"ite", "fold", "unfold", "unfolding", "in", "forall", "exists",
"seq", "nil", "result", "eval", "token",
- "wait", "signal",
+ "wait", "signal", "unlimited",
"refines", "transforms", "replaces", "by"
)
// todo: can we remove "nil"?
@@ -88,8 +88,12 @@ class Parser extends StandardTokenParsers {
def predicateDecl: Parser[Predicate] =
("predicate" ~> ident) ~ ("{" ~> expression <~ "}") ^^ { case id ~ definition => Predicate(id, definition) }
def functionDecl =
- ("function" ~> ident) ~ formalParameters(true) ~ (":" ~> typeDecl) ~ (methodSpec*) ~ opt("{" ~> expression <~ "}") ^^ {
- case id ~ ins ~ out ~ specs ~ body => Function(id, ins, out, specs, body)
+ ("unlimited" ?) ~ ("function" ~> ident) ~ formalParameters(true) ~ (":" ~> typeDecl) ~ (methodSpec*) ~ opt("{" ~> expression <~ "}") ^^ {
+ case u ~ id ~ ins ~ out ~ specs ~ body => {
+ val f = Function(id, ins, out, specs, body);
+ if (u.isDefined) f.isUnlimited = true;
+ f
+ }
}
def conditionDecl =
"condition" ~> ident ~ ("where" ~> expression ?) <~ Semi ^^ {
diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala
index b2f30c5c..236e74cc 100644
--- a/Chalice/src/PrettyPrinter.scala
+++ b/Chalice/src/PrettyPrinter.scala
@@ -283,7 +283,7 @@ object PrintProgram {
case Old(e) =>
print("old("); Expr(e); print(")")
case IfThenElse(con, then, els) =>
- print("ite("); Expr(con); print(", "); Expr(then); print(", "); Expr(els); print(")");
+ print("("); Expr(con); print(" ? "); Expr(then); print(" : "); Expr(els); print(")");
case Not(e) => print("!"); Expr(e, 0x80, false)
case FunctionApplication(obj, id, ins) =>
Expr(obj); print("."); print(id); print("("); ExprList(ins); print(")");
diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index d4adbec3..2729a0d5 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -216,12 +216,11 @@ object Resolver {
// resolve function calls
calls addNode f;
e visit {
- case app : FunctionApplication =>
- assert(app.f != null);
- calls addNode app.f;
- calls.addEdge(f, app.f);
- if (app.f == f) f.isRecursive = true; // self-recursion
- case _ =>
+ case app : FunctionApplication if app.f != null /* may not be resolved */ =>
+ calls addNode app.f;
+ calls.addEdge(f, app.f);
+ if (app.f == f) f.isRecursive = true; // self-recursion
+ case _ =>
}
case None =>
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-16 01:12:12 +0000