diff options
| author |  stefanheule <unknown> | 2011-07-07 17:42:54 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2011-07-07 17:42:54 +0200 |
| commit | c1f5342aac7c1d95c5f3281726e2cfd00051001e (patch) | |
| tree | 12a3f0ac1ee69a6b8644b689ea0731174bfa5e09 /Chalice/tests/examples | |
| parent | 0e4936c6b468b371c502cc5c7e7a311d7ae43bd6 (diff) | |
Chalice: Allow _ as wildcard in the eval construct for parameters. Usage is demonstrated in a new test case.
Diffstat (limited to 'Chalice/tests/examples')
| -rw-r--r-- | Chalice/tests/examples/Solver.chalice | 44 | ||||
| -rw-r--r-- | Chalice/tests/examples/Solver.output.txt | 4 |
2 files changed, 48 insertions, 0 deletions
diff --git a/Chalice/tests/examples/Solver.chalice b/Chalice/tests/examples/Solver.chalice new file mode 100644 index 00000000..0de8a987 --- /dev/null +++ b/Chalice/tests/examples/Solver.chalice @@ -0,0 +1,44 @@ +class Client {
+
+ method main(p: Problem, s: Solver) returns (r: int)
+ requires acc(p.f) && s != null
+ ensures acc(p.f)
+ {
+ // start randomized computations
+ var tk1: token<Solver.solve>
+ var tk2: token<Solver.solve>
+ call tk1 := s.start(p)
+ call tk2 := s.start(p)
+
+ // get the results
+ var r1: int
+ join r1 := tk1
+ var r2: int
+ join r2:= tk2
+ r := r1 > r2 ? r1 : r2
+ }
+
+}
+class Solver {
+
+ method solve(p: Problem, d: Data) returns (r: int)
+ requires rd(p.f)
+ requires acc(d.*)
+ ensures rd(p.f)
+ { /* ... */ }
+
+ method start(p: Problem)
+ returns (tk: token<Solver.solve>)
+ requires rd(p.f)
+ ensures acc(p.f, rd-rd(tk))
+ ensures acc(tk.joinable) && tk.joinable;
+ ensures eval(tk.fork this.solve(p,_), true)
+ {
+ var d: Data := new Data
+ /* .. perform some set-up/initialization and prepare the data d for the solve method */
+ fork tk := solve(p, d)
+ }
+
+}
+class Problem { var f: int }
+class Data { var f: int; var g: int }
diff --git a/Chalice/tests/examples/Solver.output.txt b/Chalice/tests/examples/Solver.output.txt new file mode 100644 index 00000000..e88f63d9 --- /dev/null +++ b/Chalice/tests/examples/Solver.output.txt @@ -0,0 +1,4 @@ +Verification of Solver.chalice using parameters=""
+
+
+Boogie program verifier finished with 10 verified, 0 errors
|