54 (*The bad invariant FAILS in cmd1V*) |
54 (*The bad invariant FAILS in cmd1V*) |
55 Goalw [Mprg_def, bad_invariantU_def] "Invariant Mprg bad_invariantU"; |
55 Goalw [Mprg_def, bad_invariantU_def] "Invariant Mprg bad_invariantU"; |
56 by (rtac InvariantI 1); |
56 by (rtac InvariantI 1); |
57 by (Force_tac 1); |
57 by (Force_tac 1); |
58 by (constrains_tac cmd_defs 1); |
58 by (constrains_tac cmd_defs 1); |
|
59 by Auto_tac; |
59 by (safe_tac (claset() addSEs [le_SucE])); |
60 by (safe_tac (claset() addSEs [le_SucE])); |
60 by (Asm_full_simp_tac 1); |
61 by (Asm_full_simp_tac 1); |
61 (*Resulting state: n=1, p=false, m=4, u=false. |
62 (*Resulting state: n=1, p=false, m=4, u=false. |
62 Execution of cmd1V (the command of process v guarded by n=1) sets p:=true, |
63 Execution of cmd1V (the command of process v guarded by n=1) sets p:=true, |
63 violating the invariant!*) |
64 violating the invariant!*) |
71 by (constrains_tac cmd_defs 1); |
72 by (constrains_tac cmd_defs 1); |
72 qed "U_F0"; |
73 qed "U_F0"; |
73 |
74 |
74 Goal "LeadsTo Mprg {s. MM s=1} {s. PP s = VV s & MM s = 2}"; |
75 Goal "LeadsTo Mprg {s. MM s=1} {s. PP s = VV s & MM s = 2}"; |
75 by (ensures_tac cmd_defs "cmd1U" 1); |
76 by (ensures_tac cmd_defs "cmd1U" 1); |
|
77 by Auto_tac; |
76 qed "U_F1"; |
78 qed "U_F1"; |
77 |
79 |
78 Goal "LeadsTo Mprg {s. ~ PP s & MM s = 2} {s. MM s = 3}"; |
80 Goal "LeadsTo Mprg {s. ~ PP s & MM s = 2} {s. MM s = 3}"; |
79 by (cut_facts_tac [invariantU] 1); |
81 by (cut_facts_tac [invariantU] 1); |
80 by (rewtac Mprg_def); |
82 by (rewtac Mprg_def); |
81 by (ensures_tac cmd_defs "cmd2U" 1); |
83 by (ensures_tac cmd_defs "cmd2U" 1); |
|
84 by Auto_tac; |
82 qed "U_F2"; |
85 qed "U_F2"; |
83 |
86 |
84 Goal "LeadsTo Mprg {s. MM s = 3} {s. PP s}"; |
87 Goal "LeadsTo Mprg {s. MM s = 3} {s. PP s}"; |
85 by (res_inst_tac [("B", "{s. MM s = 4}")] LeadsTo_Trans 1); |
88 by (res_inst_tac [("B", "{s. MM s = 4}")] LeadsTo_Trans 1); |
86 by (ensures_tac cmd_defs "cmd4U" 2); |
89 by (ensures_tac cmd_defs "cmd4U" 2); |
87 by (ensures_tac cmd_defs "cmd3U" 1); |
90 by (ensures_tac cmd_defs "cmd3U" 1); |
|
91 by Auto_tac; |
88 qed "U_F3"; |
92 qed "U_F3"; |
89 |
93 |
90 Goal "LeadsTo Mprg {s. MM s = 2} {s. PP s}"; |
94 Goal "LeadsTo Mprg {s. MM s = 2} {s. PP s}"; |
91 by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] |
95 by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] |
92 MRS LeadsTo_Diff) 1); |
96 MRS LeadsTo_Diff) 1); |
120 by (constrains_tac cmd_defs 1); |
124 by (constrains_tac cmd_defs 1); |
121 qed "V_F0"; |
125 qed "V_F0"; |
122 |
126 |
123 Goal "LeadsTo Mprg {s. NN s=1} {s. PP s = (~ UU s) & NN s = 2}"; |
127 Goal "LeadsTo Mprg {s. NN s=1} {s. PP s = (~ UU s) & NN s = 2}"; |
124 by (ensures_tac cmd_defs "cmd1V" 1); |
128 by (ensures_tac cmd_defs "cmd1V" 1); |
|
129 by Auto_tac; |
125 qed "V_F1"; |
130 qed "V_F1"; |
126 |
131 |
127 Goal "LeadsTo Mprg {s. PP s & NN s = 2} {s. NN s = 3}"; |
132 Goal "LeadsTo Mprg {s. PP s & NN s = 2} {s. NN s = 3}"; |
128 by (cut_facts_tac [invariantV] 1); |
133 by (cut_facts_tac [invariantV] 1); |
129 by (ensures_tac cmd_defs "cmd2V" 1); |
134 by (ensures_tac cmd_defs "cmd2V" 1); |
|
135 by Auto_tac; |
130 qed "V_F2"; |
136 qed "V_F2"; |
131 |
137 |
132 Goal "LeadsTo Mprg {s. NN s = 3} {s. ~ PP s}"; |
138 Goal "LeadsTo Mprg {s. NN s = 3} {s. ~ PP s}"; |
133 by (res_inst_tac [("B", "{s. NN s = 4}")] LeadsTo_Trans 1); |
139 by (res_inst_tac [("B", "{s. NN s = 4}")] LeadsTo_Trans 1); |
134 by (ensures_tac cmd_defs "cmd4V" 2); |
140 by (ensures_tac cmd_defs "cmd4V" 2); |
135 by (ensures_tac cmd_defs "cmd3V" 1); |
141 by (ensures_tac cmd_defs "cmd3V" 1); |
|
142 by Auto_tac; |
136 qed "V_F3"; |
143 qed "V_F3"; |
137 |
144 |
138 Goal "LeadsTo Mprg {s. NN s = 2} {s. ~ PP s}"; |
145 Goal "LeadsTo Mprg {s. NN s = 2} {s. ~ PP s}"; |
139 by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] |
146 by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] |
140 MRS LeadsTo_Diff) 1); |
147 MRS LeadsTo_Diff) 1); |