equal
deleted
inserted
replaced
1 (* |
1 (* |
2 File: MemClerk.ML |
2 File: MemClerk.ML |
|
3 ID: $Id$ |
3 Author: Stephan Merz |
4 Author: Stephan Merz |
4 Copyright: 1997 University of Munich |
5 Copyright: 1997 University of Munich |
5 |
6 |
6 RPC-Memory example: Memory clerk specification (theorems and proofs) |
7 RPC-Memory example: Memory clerk specification (theorems and proofs) |
7 *) |
8 *) |
8 |
9 |
9 val MC_action_defs = |
10 val MC_action_defs = |
10 [MClkInit_def, MClkFwd_def, MClkRetry_def, MClkReply_def, MClkNext_def]; |
11 [MClkInit_def, MClkFwd_def, MClkRetry_def, MClkReply_def, MClkNext_def]; |
11 |
12 |
12 val MC_temp_defs = [MClkIPSpec_def, MClkISpec_def]; |
13 val MC_temp_defs = [MClkIPSpec_def, MClkISpec_def]; |
13 |
14 |
14 val mem_css = (claset(), simpset()); |
15 val mem_css = (claset(), simpset()); |
39 qed "MClkFwd_ch_enabled"; |
40 qed "MClkFwd_ch_enabled"; |
40 |
41 |
41 Goal "|- MClkReply send rcv cst p --> \ |
42 Goal "|- MClkReply send rcv cst p --> \ |
42 \ <MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p)"; |
43 \ <MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p)"; |
43 by (auto_tac (mem_css addsimps2 [angle_def,MClkReply_def] |
44 by (auto_tac (mem_css addsimps2 [angle_def,MClkReply_def] |
44 addEs2 [Return_changed])); |
45 addEs2 [Return_changed])); |
45 qed "MClkReply_change"; |
46 qed "MClkReply_change"; |
46 |
47 |
47 Goal "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==> \ |
48 Goal "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==> \ |
48 \ |- Calling send p & ~Calling rcv p & cst!p = #clkB \ |
49 \ |- Calling send p & ~Calling rcv p & cst!p = #clkB \ |
49 \ --> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"; |
50 \ --> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"; |