summaryrefslogtreecommitdiff
path: root/Chalice/tests/examples/Solver.chalice
diff options
context:
space:
mode:
Diffstat (limited to 'Chalice/tests/examples/Solver.chalice')
-rw-r--r--Chalice/tests/examples/Solver.chalice44
1 files changed, 0 insertions, 44 deletions
diff --git a/Chalice/tests/examples/Solver.chalice b/Chalice/tests/examples/Solver.chalice
deleted file mode 100644
index 0de8a987..00000000
--- a/Chalice/tests/examples/Solver.chalice
+++ /dev/null
@@ -1,44 +0,0 @@
-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 }