equal
deleted
inserted
replaced
1 (* |
1 (* |
2 File: RPC.ML |
2 File: RPC.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: RPC specification (theorems and proofs) |
7 RPC-Memory example: RPC specification (theorems and proofs) |
7 *) |
8 *) |
8 |
9 |
9 val RPC_action_defs = [RPCInit_def, RPCFwd_def, RPCReject_def, RPCFail_def, |
10 val RPC_action_defs = [RPCInit_def, RPCFwd_def, RPCReject_def, RPCFail_def, |
10 RPCReply_def, RPCNext_def]; |
11 RPCReply_def, RPCNext_def]; |
11 |
12 |
12 val RPC_temp_defs = [RPCIPSpec_def, RPCISpec_def]; |
13 val RPC_temp_defs = [RPCIPSpec_def, RPCISpec_def]; |
13 |
14 |
14 val mem_css = (claset(), simpset()); |
15 val mem_css = (claset(), simpset()); |
27 |
28 |
28 (* RPC failure actions are visible. *) |
29 (* RPC failure actions are visible. *) |
29 Goal "|- RPCFail send rcv rst p --> \ |
30 Goal "|- RPCFail send rcv rst p --> \ |
30 \ <RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p)"; |
31 \ <RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p)"; |
31 by (auto_tac (claset() addSDs [Return_changed], |
32 by (auto_tac (claset() addSDs [Return_changed], |
32 simpset() addsimps [angle_def,RPCNext_def,RPCFail_def])); |
33 simpset() addsimps [angle_def,RPCNext_def,RPCFail_def])); |
33 qed "RPCFail_vis"; |
34 qed "RPCFail_vis"; |
34 |
35 |
35 Goal "|- Enabled (RPCFail send rcv rst p) --> \ |
36 Goal "|- Enabled (RPCFail send rcv rst p) --> \ |
36 \ Enabled (<RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p))"; |
37 \ Enabled (<RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p))"; |
37 by (force_tac (mem_css addSEs2 [enabled_mono,RPCFail_vis]) 1); |
38 by (force_tac (mem_css addSEs2 [enabled_mono,RPCFail_vis]) 1); |