1 | | % (c) 2020-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, |
2 | | % Heinrich Heine Universitaet Duesseldorf |
3 | | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html |
4 | | |
5 | | :- module(well_def_analyser, [analyse_wd_for_machine/3, analyse_wd_for_machine/4, |
6 | | compute_wd/4, compute_all_wd_pos/4, |
7 | | analyse_wd_for_expr/3, analyse_wd_for_expr/4, |
8 | | annotate_wd/2, transform_wd/4, |
9 | | tcltk_get_machine_wd_pos/4, |
10 | | get_hyps_for_top_level_operations/2, |
11 | | prove_sequent/1, |
12 | | prove_sequent/3, |
13 | | prove_sequent/4, |
14 | | analyse_invariants_for_machine/5, |
15 | | find_inconsistent_axiom/3, tcltk_check_for_inconsistent_axiom/1, |
16 | | toplevel_wd_pos/3 |
17 | | ]). |
18 | | |
19 | | :- use_module(probsrc(module_information),[module_info/2]). |
20 | | :- module_info(group,well_def_prover). |
21 | | :- module_info(description,'This module computes WD conditions in AST.'). |
22 | | |
23 | | :- use_module(probsrc(error_manager)). |
24 | | :- use_module(probsrc(debug)). |
25 | | :- use_module(probsrc(bsyntaxtree)). |
26 | | :- use_module(probsrc(b_ast_cleanup), [has_top_level_wd_condition/1]). |
27 | | :- use_module(probsrc(external_functions),[external_fun_has_wd_condition/1]). |
28 | | :- use_module(probsrc(specfile),[z_or_tla_minor_mode/0, eventb_mode/0]). |
29 | | |
30 | | :- use_module(library(ordsets)). |
31 | | :- use_module(library(avl)). |
32 | | :- use_module(wdsrc(well_def_hyps)). |
33 | | |
34 | | |
35 | | prove_sequent(Goal) :- |
36 | | prove_sequent(proving,Goal,[]). |
37 | | prove_sequent(Context,Goal,Hyps) :- |
38 | | prove_sequent(Context,Goal,Hyps,[push_more_hyps]). % push all hypotheses; usually not useful for WD proofs but useful if proof goals have other form than for WD POs |
39 | | prove_sequent(Context,Goal,Hyps,Opts) :- |
40 | | (Context=animation -> Val=true |
41 | | ; Context=proving -> Val=false |
42 | | ; add_internal_error('Unknown context:',Context), |
43 | | Val=false), |
44 | | temporary_set_preference(wd_analysis_for_animation,Val,Chng), |
45 | | call_cleanup(prove_sequent_cur_context(Goal,Hyps,Opts), |
46 | | reset_temporary_preference(wd_analysis_for_animation,Chng)). |
47 | | |
48 | | |
49 | | % utility for disprover |
50 | | prove_sequent_cur_context(_,Hyps,_) :- |
51 | ? | member(Falsity,Hyps), is_falsity(Falsity),!. % TO DO: upon pushing hyps |
52 | | prove_sequent_cur_context(Goal,Hypotheses,Opts) :- |
53 | | empty_hyps(E), |
54 | | list_to_ord_set([discharge_po|Opts],Options), |
55 | | push_hyps(E,Hypotheses,Options,Hyps), |
56 | | prove_sequent_goal(Goal,Hyps,Options). |
57 | | |
58 | | % process complex sequent goals which arise in Rodin; not generated by our POG |
59 | | prove_sequent_goal(b(Formula,pred,I),Hyps,Options) :- !, |
60 | | process_sequent_aux(Formula,I,Hyps,Options). |
61 | | prove_sequent_goal(Goal,Hyps,Options) :- |
62 | | add_internal_error('Goal not wrapped: ',prove_sequent_goal(Goal,Hyps,Options)),fail. |
63 | | |
64 | ? | process_sequent_aux(negation(b(Pred,pred,_)),I,Hyps,Options) :- cnf_negate(Pred,NegPred),!, |
65 | | (debug_mode(off) -> true |
66 | | ; print('Pushing negation in sequent goal: '), translate:print_bexpr(b(NegPred,pred,[])),nl), |
67 | | % example :prove x=3 => not( x=3 => x=2) |
68 | | process_sequent_aux(NegPred,I,Hyps,Options). |
69 | | process_sequent_aux(implication(A,B),_,Hyps,Options) :- !, |
70 | | (debug_mode(off) -> true ; print('Peeling implication in sequent goal: '), translate:print_bexpr(A),nl), |
71 | | push_hyp(Hyps,A,Options,Hyps2), |
72 | | (prove_sequent_goal(B,Hyps2,Options) -> true |
73 | | ; negate_hyp(A,NegA), prove_sequent_goal(NegA,Hyps,Options) |
74 | | ). |
75 | | process_sequent_aux(equivalence(A,B),I,Hyps,Options) :- !, |
76 | | process_sequent_aux(implication(A,B),I,Hyps,Options), |
77 | | process_sequent_aux(implication(B,A),I,Hyps,Options). |
78 | | process_sequent_aux(conjunct(A,B),_I,Hyps,Options) :- !, |
79 | | prove_sequent_goal(A,Hyps,Options), |
80 | | prove_sequent_goal(B,Hyps,Options). |
81 | | process_sequent_aux(disjunct(A,B),_I,Hyps,Options) :- !, |
82 | | (negate_hyp(B,NegB), |
83 | | push_hyp(Hyps,NegB,Options,Hyps2), % not(B) => A we have A or B ; |
84 | | % is a combination of OR_R proof rule and proof by case B, not(B) |
85 | | prove_sequent_goal(A,Hyps2,Options) |
86 | | -> true |
87 | | ; negate_hyp(A,NegA), |
88 | | push_hyp(Hyps,NegA,Options,Hyps2), % not(A) => B we have A or B |
89 | | prove_sequent_goal(B,Hyps2,Options)). |
90 | | process_sequent_aux(forall(Ids,A,B),_,Hyps,Options) :- !, |
91 | | (debug_mode(off) -> true ; print('Peeling forall in sequent goal: '), translate:print_bexpr(A),nl), |
92 | | add_new_hyp_variables(Hyps,Ids,Hyps1), |
93 | | push_hyp(Hyps1,A,Options,Hyps2), |
94 | | prove_sequent_goal(B,Hyps2,Options). |
95 | | process_sequent_aux(Goal,I,Hyps,Options) :- |
96 | | get_normalized_and_renamed_predicate(b(Goal,pred,I),Hyps,_RenTarget,NT), |
97 | | % print('PROVING: '),translate:print_bexpr(_RenTarget),nl, |
98 | | (get_current_po_label(POLabel,Options) -> true ; POLabel = ''), |
99 | | prove_proof_obligation(POLabel,Goal,NT,Hyps,ProofTree), |
100 | | debug_format(19,'WD PROVER SUCCESSFUL: ~w~n',[ProofTree]). |
101 | | |
102 | | :- use_module(probsrc(bsyntaxtree),[create_negation/2]). |
103 | | cnf_negate(implication(A,B),conjunct(A,NotB)) :- create_negation(B,NotB). |
104 | | cnf_negate(equivalence(A,B),conjunct(b(implication(A,NotB),pred,[]), |
105 | | b(implication(NotA,B),pred,[]))) :- |
106 | | % not( A <=> B ) <----> A=> not(B) & not(A) => B |
107 | | create_negation(A,NotA), |
108 | | create_negation(B,NotB). |
109 | | cnf_negate(disjunct(A,B),conjunct(NotA,NotB)) :- create_negation(A,NotA), create_negation(B,NotB). |
110 | | cnf_negate(conjunct(A,B),disjunct(NotA,NotB)) :- create_negation(A,NotA), create_negation(B,NotB). |
111 | | cnf_negate(NegA,A) :- negate_op(NegA,A). % deals with negation(A) -> A, truth->falsity, ... |
112 | | %cnf_negate(exists(Ids,Q),forall(Ids,LHS,RHS)) :- ... TODO |
113 | | |
114 | | compute_all_wd_pos(TExpr,OriginalHyps,Options,POs) :- |
115 | | findall(PO, compute_wd(TExpr,OriginalHyps,Options,PO), POs). |
116 | | |
117 | | |
118 | | % analyze and print WD POs for a given typed expression or predicate or subst: |
119 | | analyse_wd_for_expr(TExpr,_,_) :- |
120 | | analyse_wd_for_expr(TExpr,_,_,silent). |
121 | | |
122 | | % MsgLevel = silent, message, warning, error |
123 | | analyse_wd_for_expr(TExpr,_,_,MsgLevel) :- |
124 | | reset_stats, |
125 | | formatsilent('WD Proof Obligations:~n',[]), |
126 | | %empty_hyps(OriginalHyps), |
127 | | push_properties_invariant_hyps([],OriginalHyps), |
128 | | list_to_ord_set([create_full_po,create_not_discharged_msg(MsgLevel),discharge_po,ignore_wd_infos |
129 | | %,minimize_full_po |
130 | | %,prove_with_z3 % comment in to double-check with Z3 |
131 | | ],Options), |
132 | ? | compute_wd(TExpr,OriginalHyps,Options,PO), |
133 | | (silent_mode(on) -> true ; translate:nested_print_bexpr(PO),nl), |
134 | | fail. |
135 | | analyse_wd_for_expr(TExpr,ResStr,AllDischarged,MsgLevel) :- |
136 | | formatsilent('----~n',[]), |
137 | | print_stats, |
138 | | get_discharged_result(ResStr,_,_,AllDischarged), |
139 | | empty_hyps(OriginalHyps), |
140 | | transform_wd(TExpr,OriginalHyps,[discharge_po],NewTExpr), |
141 | | (silent_mode(on) -> true |
142 | | ; MsgLevel = silent -> true |
143 | | ; format('Annotated formula:~n',[]), |
144 | | nested_print_wd_bexpr(NewTExpr) |
145 | | ). |
146 | | |
147 | | nested_print_wd_bexpr(NewTExpr) :- |
148 | | temporary_set_preference(pp_wd_infos,true,Chng), |
149 | | translate:nested_print_bexpr(NewTExpr),nl, |
150 | | reset_temporary_preference(pp_wd_infos,Chng). |
151 | | |
152 | | :- use_module(probsrc(translate),[translate_bexpression_with_limit/3]). |
153 | | |
154 | | tcltk_get_machine_wd_pos(only_goal,list([Header|POs]),ResStr,AllDischarged) :- !, |
155 | | reset_stats, |
156 | | Header = list(['PO Label','Discharged','Proof Obligation Goal', 'Source']), |
157 | | list_to_ord_set([discharge_po,ignore_wd_infos,reorder_conjuncts],Options), |
158 | | findall(list([POLabel,Discharged,POStr,Source]), |
159 | | (get_machine_wd_po(Options,PO,PO_Name), |
160 | | get_texpr_info(PO,Infos), |
161 | | (member(discharged(D,POLabel),Infos) |
162 | | -> (D=true -> Discharged='yes' ; Discharged='no') |
163 | | ; Discharged='UNKNOWN',POLabel=PO_Name), |
164 | | translate:translate_bexpression_with_limit(PO,100,POStr), |
165 | | get_tk_table_position_info(Infos,Source) |
166 | | ), POs), |
167 | | get_discharged_result(ResStr,_,_,AllDischarged). |
168 | | tcltk_get_machine_wd_pos(goal_and_hyps,list([Header|POs]),ResStr,AllDischarged) :- |
169 | | reset_stats, |
170 | | get_preference(translation_limit_for_table_commands,Limit), |
171 | | Header = list(['PO Label','Discharged','PO Goal', '(Necessary) Hypotheses', 'Source']), |
172 | | % in case a PO is proven we only show the hyps necessary for the proof |
173 | | list_to_ord_set([discharge_po,ignore_wd_infos,reorder_conjuncts, create_full_po,minimize_full_po],Options), |
174 | | findall(list([POLabel,Discharged,GoalStr,HypsStr,Source]), |
175 | | (get_machine_wd_po(Options,PO,PO_Name), |
176 | | get_texpr_info(PO,Infos), |
177 | | (member(discharged(D,POLabel),Infos) |
178 | | -> (D=true -> Discharged='yes' ; Discharged='no') |
179 | | ; Discharged='UNKNOWN',POLabel=PO_Name), |
180 | | decompose_po(PO,Hyps,Goal), |
181 | | translate_bexpression_with_limit(Hyps,Limit,HypsStr), |
182 | | translate_bexpression_with_limit(Goal,Limit,GoalStr), |
183 | | get_tk_table_position_info(Infos,Source) |
184 | | ), POs), |
185 | | get_discharged_result(ResStr,_,_,AllDischarged). |
186 | | |
187 | | decompose_po(b(implication(Hyps,Goal),pred,_),Hyps,Goal) :- !. |
188 | | decompose_po(Goal,b(truth,pred,[]),Goal). |
189 | | |
190 | | % analyse all WD POs for the loaded B machine |
191 | | analyse_wd_for_machine(NrDischarged,NrTot,Discharged) :- |
192 | | Options = [create_not_discharged_msg(warning),discharge_po,ignore_wd_infos,reorder_conjuncts], |
193 | | analyse_wd_for_machine(NrDischarged,NrTot,Discharged,Options). |
194 | | analyse_wd_for_machine_with_double_check(NrDischarged,NrTot,Discharged) :- |
195 | | Options = [create_not_discharged_msg(warning),discharge_po,ignore_wd_infos,reorder_conjuncts, |
196 | | create_full_po, prove_with_z3], |
197 | | analyse_wd_for_machine(NrDischarged,NrTot,Discharged,Options). |
198 | | |
199 | | analyse_wd_for_machine(NrDischarged,NrTot,Discharged,UnsortedOptions) :- reset_stats, |
200 | | list_to_ord_set(UnsortedOptions,Options), |
201 | | %list_to_ord_set([discharge_po,reorder_conjuncts],Options), |
202 | | statistics(walltime,[Start,_]), |
203 | ? | ( get_machine_wd_po(Options,_PO,_), |
204 | | fail |
205 | | ; |
206 | | statistics(walltime,[Stop,_]), Delta is Stop-Start, |
207 | | formatsilent('Analysis walltime: ~w ms~n',[Delta]), |
208 | | print_stats, |
209 | | get_discharged_result(_ResStr,NrDischarged,NrTot,Discharged) |
210 | | ). |
211 | | |
212 | | :- use_module(probsrc(bmachine), [b_get_properties_from_machine/1, b_get_machine_all_constants/1, |
213 | | b_get_machine_variables/1, b_get_invariant_from_machine/1, |
214 | | b_get_static_assertions_from_machine/1, b_get_dynamic_assertions_from_machine/1, |
215 | | b_get_machine_operation/6, b_get_initialisation_from_machine/2]). |
216 | | |
217 | | transl_hyp(Axiom,Str) :- |
218 | | translate:translate_bexpression_with_limit(Axiom,500,Str). |
219 | | |
220 | | % if successful: returns a message explaining that an axiom is in contradiction with some other properties |
221 | | tcltk_check_for_inconsistent_axiom(list(['The following predicate from PROPERTIES/axioms:',AxiomStr, |
222 | | 'is in contradiction with these predicates:' | TPS])) :- |
223 | | find_inconsistent_axiom([],Axiom,NecHyps), |
224 | | %get_specification_description(properties,PS), |
225 | | translate:translate_bexpression_with_limit(Axiom,500,AxiomStr), |
226 | | maplist(transl_hyp,NecHyps,TPS). |
227 | | |
228 | | % try to find inconsistency in properties/axioms: |
229 | | find_inconsistent_axiom(LOpt,Axiom,NecHyps) :- |
230 | | reset_stats, |
231 | | get_fresh_hyps_for_constants(OriginalHyps), |
232 | | b_get_properties_from_machine(Properties), |
233 | | list_to_ord_set([push_more_hyps|LOpt],Options), |
234 | | push_hyp(OriginalHyps,Properties,Options,Hyps1), |
235 | | member_in_conjunction(Axiom,Properties), |
236 | | (debug_mode(on) -> print(' checking for contradiction with ==> '),translate:print_bexpr(Axiom),nl ; true), |
237 | | NegAxiom = b(negation(Axiom),pred,[]), |
238 | | prove_sequent_goal(NegAxiom,Hyps1,Options), |
239 | | print('INCONSISTENCY FOUND, negation of axiom can be proven: '), |
240 | | translate:print_bexpr(Axiom),nl, |
241 | | % ord_member(minimize_full_po,Options), |
242 | | print('Finding NECESSARY Hypotheses:'),nl, |
243 | | minimize_necessary_hyps(Hyps1,NegAxiom,Options,NecHyps), |
244 | | (debug_mode(on) -> translate:nested_print_bexpr(NecHyps),nl ; true). |
245 | | %TODO: optionally take prob-ignore into account (predicate_has_ignore_pragma/1 and get_preference(use_ignore_pragmas,true)) |
246 | | |
247 | | minimize_necessary_hyps(hyp_rec(AvlNH,_),Goal,Options,NecHyps) :- |
248 | | avl_range(AvlNH,Hyps), |
249 | | minimize_hyps(Hyps,Goal,Options,NecHyps). |
250 | | |
251 | | |
252 | | get_fresh_hyps_for_constants(OriginalHyps) :- |
253 | | empty_hyps(E), |
254 | | b_get_machine_all_constants(Csts), |
255 | | add_new_hyp_variables(E,Csts,OriginalHyps). |
256 | | |
257 | | % get POs for loaded B machine |
258 | | get_machine_wd_po(LOpt,PO,PO_Name) :- |
259 | | reset_stats, |
260 | | list_to_ord_set(LOpt,Options), |
261 | | b_get_properties_from_machine(Properties), |
262 | | % TO DO: move Conjuncts without WD condition to front in first pass |
263 | | get_fresh_hyps_for_constants(OriginalHyps), |
264 | | ( PO_Name = 'AXM', |
265 | | debug_format(19,'Checking WD of PROPERTIES~n',[]), |
266 | | ord_add_element(Options,po_label(PO_Name),Opt2), |
267 | ? | compute_wd_with_reordering(Properties,OriginalHyps,Opt2,PO) |
268 | | |
269 | | %debug:time(well_def_analyser:transform_wd(Properties,OriginalHyps,Opt2,NewProperties)),nl,fail) |
270 | | |
271 | | ; % TO DO: for transform: only use assertions if assertion checking is on!? |
272 | | |
273 | | push_hyp(OriginalHyps,Properties,Options,Hyps1), |
274 | | b_get_static_assertions_from_machine(StaticAssertions), |
275 | | |
276 | | ( PO_Name = 'THM-AXM', |
277 | | ord_add_element(Options,po_label(PO_Name),Opt2), |
278 | | conjunct_predicates(StaticAssertions,SAssPred), |
279 | ? | compute_wd(SAssPred,Hyps1,Opt2,PO) |
280 | | ; |
281 | | push_hyps(Hyps1,StaticAssertions,Options,Hyps2), |
282 | | %portray_hyps(Hyps2),nl, |
283 | | b_get_machine_variables(Vars), |
284 | | add_new_hyp_variables(Hyps2,Vars,Hyps3), |
285 | | b_get_invariant_from_machine(Invariant), |
286 | | ( PO_Name = 'INV', |
287 | | debug_format(19,'Checking WD of INVARIANT~n',[]), |
288 | | ord_add_element(Options,po_label(PO_Name),Opt2), |
289 | ? | compute_wd_with_reordering(Invariant,Hyps3,Opt2,PO) |
290 | | ; |
291 | | push_hyp(Hyps3,Invariant,Options,Hyps4), |
292 | | b_get_dynamic_assertions_from_machine(DynAssertions), |
293 | | ( PO_Name = 'THM-INV', |
294 | | debug_format(19,'Checking WD of ASSERTIONS~n',[]), |
295 | | ord_add_element(Options,po_label(PO_Name),Opt2), |
296 | | conjunct_predicates(DynAssertions,AssPred), |
297 | ? | compute_wd(AssPred,Hyps4,Opt2,PO) |
298 | | % TO DO: use assertions for operations |
299 | | ; push_hyps(Hyps4,DynAssertions,Options,Hyps5), |
300 | | ( |
301 | | b_get_initialisation_from_machine(Body,_OType), |
302 | | PO_Name = 'INIT', |
303 | | debug_format(19,'Checking WD of INITIALISATION~n',[]), |
304 | | ord_add_element(Options,po_label(PO_Name),Opt2), |
305 | ? | compute_wd(Body,Hyps5,Opt2,PO) |
306 | ? | ; b_get_machine_operation(OpName,OpResults,OpFormalParameters,Body,_OType,_TopLevel), |
307 | | PO_Name = OpName, |
308 | | debug_format(19,'Checking WD of OPERATION ~w~n',[OpName]), |
309 | | ord_add_element(Options,po_label(PO_Name),Opt2), |
310 | | add_new_hyp_variables(Hyps5,OpFormalParameters,Hyps6), |
311 | | add_new_hyp_variables(Hyps6,OpResults,Hyps7), |
312 | ? | compute_wd(Body,Hyps7,Opt2,PO) |
313 | | ) |
314 | | ) |
315 | | ) |
316 | | ) |
317 | | ), |
318 | | inc_counter(PO_Name). |
319 | | |
320 | | |
321 | | % -------------------- |
322 | | |
323 | | :- use_module(probsrc(tools_strings),[ajoin/2,ajoin_with_sep/3]). |
324 | | % get label of current PO from Options |
325 | | get_current_po_label(POLabel,Options) :- |
326 | | findall(Label,get_label(Label,Options),Labels), |
327 | | Labels \= [], |
328 | | ajoin_with_sep(Labels,'/',POLabel). |
329 | ? | get_label(Label,Options) :- member(po_label(L),Options), |
330 | | (L = [_|_] -> member(Label,L) ; Label=L). |
331 | | |
332 | | % -------------------- |
333 | | |
334 | | :- use_module(well_def_prover,[prove_po/3]). |
335 | | :- use_module(probsrc(tools_lists),[ord_member_nonvar_chk/2]). |
336 | | |
337 | | create_po(H,Target,Infos,Options,PO) :- create_po(H,Target,Infos,Options,PO,_). |
338 | | |
339 | | create_po(H,Target,Infos,Options,PO,D) :- (var(H) ; H \= hyp_rec(_,_) ; var(Options)),!, |
340 | | add_internal_error('Illegal hypotheses or options: ', create_po(H,Target,Infos,Options,PO,D)),fail. |
341 | | create_po(Hyps,Target,Infos,Options,PO,Discharged) :- |
342 | | get_normalized_and_renamed_predicate(Target,Hyps,RenTarget,NT), |
343 | | (get_current_po_label(POLabel,Options) -> true ; POLabel = ''), |
344 | | (ord_member(print_goal,Options) -> translate:print_bexpr(RenTarget),nl ; true), |
345 | | (ord_member(discharge_po,Options) |
346 | | -> (%nl,add_message(well_def_analyser,'Proving ',Target,Infos), |
347 | | prove_proof_obligation(POLabel,Target,NT,Hyps,ProofTree) |
348 | | -> debug_format(19,'PO ~w discharged: ~w~n',[POLabel,ProofTree]), %debug:nl_time, |
349 | | inc_counter(discharged_po), |
350 | | Discharged=true |
351 | | ; inc_counter(not_discharged_po), |
352 | | Discharged=false, |
353 | | (ord_member_nonvar_chk(create_not_discharged_msg(MsgType),Options) |
354 | ? | -> (prove_po(negation(NT),Hyps,_NegProofTree) |
355 | | -> NegProfStatus = ' (goal provably false)' |
356 | | % Negation can be proven; i.e., PO cannot be proven unless there is a contradiction in Hyps |
357 | | ; NegProfStatus = '' |
358 | | ), |
359 | | (POLabel = '' -> ajoin(['WD-PO not discharged', NegProfStatus, ': '],Msg) |
360 | | ; ajoin(['WD-PO [',POLabel,'] not discharged', NegProfStatus, ': '],Msg) |
361 | | ), |
362 | | ( MsgType=message -> add_message(well_def_analyser,Msg,Target,Infos) |
363 | | ; MsgType=warning -> add_warning(well_def_analyser,Msg,Target,Infos) |
364 | | ; MsgType=silent -> formatsilent('~w~w~n',[Msg,Target]) |
365 | | ; add_error(well_def_analyser,Msg,Target,Infos) |
366 | | ), |
367 | | debug_format(19,' Normalized Proof Target: ~w~n',[NT]) |
368 | | %,(debug_level_active_for(5) -> portray_hyps(Hyps) ; true) % hyps can be shown with create_full_po |
369 | | ; true |
370 | | ) |
371 | | ) |
372 | | ; Discharged=false % no discharging of POs |
373 | | ), |
374 | | extract_pos_infos(Infos,PosInfos), |
375 | | (ord_member(create_full_po,Options) |
376 | | -> Hyps = hyp_rec(AvlNH,_), |
377 | | avl_range(AvlNH,Hyp), |
378 | | (Discharged=true, ord_member(minimize_full_po,Options) |
379 | | -> minimize_hyps(Hyp,RenTarget,Options,NecHyps) % only show minimum core of hyps necessary for proving |
380 | | ; NecHyps=Hyp |
381 | | ), |
382 | | %length(NecHyps,Len), print(hyps(Len)),nl, |
383 | | conjunct_predicates(NecHyps,HypC), |
384 | | safe_create_texpr(implication(HypC,RenTarget),pred,[discharged(Discharged,POLabel)|PosInfos],PO), |
385 | | %nl,translate:print_bexpr(PO),nl, prove_po_with_atelierb(POLabel,[ml],PO,_), |
386 | | % terms:term_hash(PO,Hash), print(Hash),nl, |
387 | | %(ord_member(check_ast,Options) -> bsyntaxtree:check_ast(PO) ; true), |
388 | | (ord_member(prove_with_z3,Options) |
389 | | -> prove_po_with_smt(POLabel,z3,PO,Res),double_check(Discharged,z3,Res) ; true), |
390 | | (ord_member(prove_with_ml,Options) -> prove_po_with_atelierb(POLabel,[ml],PO,_) ; true), |
391 | | (ord_member(prove_with_pp,Options) -> prove_po_with_atelierb(POLabel,[pp],PO,_) ; true) |
392 | | ; RenTarget = b(POE,POT,POI), |
393 | | append([discharged(Discharged,POLabel)|PosInfos],POI,POInfos), |
394 | | PO = b(POE,POT,POInfos) |
395 | | ). |
396 | | |
397 | | double_check(true,Solver,solution(S)) :- !, |
398 | | add_error(Solver,'Double check of discharged PO failed, counter-example: ',S). |
399 | | double_check(_,_,_). |
400 | | |
401 | | % compute unsat core of hypotheses |
402 | | minimize_hyps(Hyps,Goal,Options,NecHyps) :- minimize_hyps_aux(Hyps,Goal,Options,NecHyps,NecHyps),nl. |
403 | | |
404 | | % TO DO: maybe do binary search / divide and conquer |
405 | | % we could also examine which hypotheses were retrieved during the proof |
406 | | % (but not easy; what if access inside a Prolog negation) |
407 | | minimize_hyps_aux([],_,_,_,[]). |
408 | | minimize_hyps_aux([H|T],Goal,Opts,NecessaryHyps,Tail) :- |
409 | | (ord_member(push_more_hyps,Opts) -> ProofOpts = [push_more_hyps] ; ProofOpts=[]), |
410 | | \+ (Tail=T,prove_sequent_cur_context(Goal,NecessaryHyps,ProofOpts)), % we need H to prove Goal |
411 | | !, |
412 | | write('+'), |
413 | | Tail = [H|TT], |
414 | | minimize_hyps_aux(T,Goal,Opts,NecessaryHyps,TT). |
415 | | minimize_hyps_aux([_|T],Goal,Opts,NecessaryHyps,Tail) :- |
416 | | write('-'), |
417 | | minimize_hyps_aux(T,Goal,Opts,NecessaryHyps,Tail). |
418 | | |
419 | | :- use_module(probsrc(runtime_profiler),[register_profiler_runtime/4]). |
420 | | :- use_module(extrasrc(atelierb_provers_interface),[prove_sequent_with_provers/3]). |
421 | | prove_po_with_atelierb(POLabel,Provers,PO,ProofRes) :- runtime_profiler:print_runtime_profile, |
422 | | format('Proving PO ~w with ~w~n',[POLabel,Provers]), |
423 | | statistics(walltime,[T1,_]), |
424 | | catch( |
425 | | prove_sequent_with_provers(Provers,PO,ProofRes), % we cannot use time_out as PP/ML/KRT are a separate process |
426 | | user_interrupt_signal, |
427 | | ProofRes = user_interrupt_signal), |
428 | | statistics(walltime,[T2,_]), WT is T2-T1, |
429 | | !, |
430 | | register_profiler_runtime(atelierb(ProofRes),POLabel,WT,WT), |
431 | | format('Result of ~w on PO = ~w (walltime ~w ms)~n',[Provers,ProofRes,WT]), |
432 | | (ProofRes=user_interrupt_signal |
433 | | -> write(' Continue? [y/n] => '), flush_output, read(Cont), |
434 | | (Cont='y' -> true ; Cont='yes' -> true ; throw(user_interrupt_signal)) |
435 | | ; true). |
436 | | |
437 | | :- use_module(probsrc(bsyntaxtree),[create_negation/2]). |
438 | | :- use_module(smt_solvers_interface(smt_solvers_interface),[smt_solve_predicate/4]). |
439 | | prove_po_with_smt(POLabel,Solver,PO,ProofRes) :- runtime_profiler:print_runtime_profile, |
440 | | format('Proving PO ~w with ~w~n',[POLabel,Solver]), |
441 | | %translate:print_bexpr(PO),nl, |
442 | | statistics(walltime,[T1,_]), |
443 | | create_negation(PO,NegPO), |
444 | | smt_solve_predicate(Solver,NegPO,_State,ProofRes),!, |
445 | | statistics(walltime,[T2,_]), WT is T2-T1, |
446 | | register_profiler_runtime(smt(Solver,ProofRes),POLabel,WT,WT), |
447 | | format('Result of ~w on PO = ~w (walltime ~w ms)~n',[Solver,ProofRes,WT]). |
448 | | |
449 | | % a wrapper to prove_po which also checks for obvious POs using type info: |
450 | | prove_proof_obligation(POLabel,Target,_NT,Hyps,ProofTree) :- |
451 | | obvious_po(Target,Hyps),!, |
452 | | debug_format(19,'Obvious PO (due to typing info): ~w~n',[POLabel]), |
453 | | register_profiler_runtime(wd_prob_prover(obvious_po),POLabel,0,0), |
454 | | ProofTree = obvious_po. |
455 | | prove_proof_obligation(POLabel,_Target,NT,Hyps,ProofTree) :- |
456 | | statistics(runtime,[RT1,_]), |
457 | | statistics(walltime,[T1,_]), |
458 | ? | (prove_po(NT,Hyps,ProofTree) -> Res=discharged |
459 | | ; Res=unknown,ProofTree='' % ,format('~n *********** WD PO UNKNOWN ~w~n~n',[POLabel]) |
460 | | ), |
461 | | statistics(runtime,[RT2,_]), RT is RT2-RT1, |
462 | | statistics(walltime,[T2,_]), WT is T2-T1, |
463 | | register_profiler_runtime(wd_prob_prover(Res),POLabel,RT,WT), |
464 | | (WT>10 -> format('Proof of \'~w\' took ~w ms, result=~w (~w)~n',[POLabel,WT,Res,ProofTree]) |
465 | | %, translate:print_bexpr(_Target),nl, assertz(well_def_prover:dt),(prove_po(NT,Hyps,_) -> true ; true), trace |
466 | | ; true), |
467 | | Res=discharged. |
468 | | |
469 | | %:- use_module(well_def_hyps,[is_finite_type_for_wd/2]). |
470 | | obvious_po(b(finite(Set),pred,_),Hyps) :- |
471 | | get_texpr_type(Set,Type), % check this proof rule here, as prove_po has no longer types in the AST |
472 | | is_finite_type_for_wd(Type,Hyps). |
473 | | |
474 | | % ------------------------------ |
475 | | |
476 | | :- dynamic counter/2. |
477 | | reset_stats :- retractall(counter(_,_)), |
478 | | assertz(counter(discharged_po,0)), |
479 | | assertz(counter(not_discharged_po,0)). |
480 | | |
481 | | inc_counter(C) :- (retract(counter(C,Nr)) -> N1 is Nr+1 ; N1 = 1), |
482 | | assertz(counter(C,N1)). |
483 | | |
484 | | print_stats :- silent_mode(on),!. |
485 | | print_stats :- findall(C/N,counter(C,N),L), format('WD Stats: ~w~n',[L]). |
486 | | |
487 | | %tcltk_get_stats(list([list(['Category','Nr'])|Stats])) :- |
488 | | % findall(list([C,N]),counter(C,N),Stats). |
489 | | |
490 | | get_discharged_result(ResStr,D,Tot,AllDischarged) :- counter(not_discharged_po,ND), |
491 | | counter(discharged_po,D), Tot is ND+D, |
492 | | ajoin([D,'/',Tot,' DISCHARGED'],ResStr), |
493 | | (ND=0 -> AllDischarged='TRUE' ; AllDischarged='FALSE'). |
494 | | |
495 | | % ------------------------------ |
496 | | |
497 | | annotate_wd(TExpr,AnnotatedTExpr) :- |
498 | | reset_stats, |
499 | | %empty_hyps(EH), |
500 | | push_properties_invariant_hyps([],EH), |
501 | | Options = [discharge_po], |
502 | | transform_wd(TExpr,EH,Options,AnnotatedTExpr), |
503 | | print_bexpr_with_wd_info(AnnotatedTExpr). |
504 | | |
505 | | |
506 | | :- use_module(probsrc(preferences),[temporary_set_preference/3, reset_temporary_preference/2, get_preference/2]). |
507 | | print_bexpr_with_wd_info(TExpr) :- |
508 | | temporary_set_preference(pp_wd_infos,true,Chng), |
509 | | call_cleanup(translate:nested_print_bexpr(TExpr),reset_temporary_preference(pp_wd_infos,Chng)), |
510 | | nl. |
511 | | |
512 | | % transform an AST by adding annotations about discharged POs |
513 | | transform_wd(b(Expr,Type,Info),Hypotheses,Options,b(NewExpr,Type,NewInfo)) :- |
514 | | memberchk(contains_wd_condition,Info), |
515 | | !, |
516 | | syntaxtransformation(Expr,Subs,TNames,NSubs,NewExpr), |
517 | | add_new_hyp_variables(Hypotheses,TNames,Hyps2), |
518 | | (wd_transparent(Expr) |
519 | | -> l_transform_wd(Subs,Hyps2,Options,NSubs), adapt_info(Info,NSubs,NewInfo) |
520 | | ; wd_like_conjunction(Expr,Ids,A,B) |
521 | | -> l_transform_conj_wd([A,B],Hyps2,Options,[TA,TB]), |
522 | | check_top_level_wd(conj,Expr,Type,Info,Hyps2,Options, [TA,TB], NewInfo), |
523 | | wd_like_conjunction(NewExpr,Ids,TA,TB) |
524 | | ; transform_special_expr(Expr,Type,Info,Hyps2,Options,NewExpr,NewInfo) -> true |
525 | | ; l_transform_wd(Subs,Hyps2,Options,NSubs) |
526 | | -> |
527 | | check_top_level_wd(other,Expr,Type,Info,Hyps2,Options, NSubs, NewInfo) |
528 | | ). |
529 | | transform_wd(TExpr,_,_,TExpr). % copy entire expression if no contains_wd_condition info |
530 | | |
531 | | check_top_level_wd(conj,Expr,Type,Info,Hyps,Options, _NSubs, NewInfo) :- |
532 | | Discharged=false, |
533 | | create_top_level_wd_po_conj_like(Expr,Type,Info,Hyps,Options,_PO,Discharged),!, % PO not proven; keep Info as is |
534 | | %write(-), flush_output, %print(not_discharged(PO)),nl, |
535 | | NewInfo=Info. |
536 | | check_top_level_wd(other,Expr,Type,Info,Hyps,Options, _NSubs, NewInfo) :- |
537 | | Discharged=false, |
538 | ? | create_top_level_wd_po(Expr,Type,Info,Hyps,Options,_PO,Discharged), |
539 | | !, % PO not proven; keep Info as is |
540 | | %write(-), flush_output, print(not_discharged(_PO)),nl, |
541 | | NewInfo=Info. |
542 | | check_top_level_wd(_,_Expr,_Type,Info,_Hyps,_Options, NSubs, NewInfo) :- % no top-level PO or PO proven |
543 | | adapt_info(Info,NSubs,NewInfo). |
544 | | |
545 | | %:- use_module(library(lists),[delete/3]). |
546 | | % adapt WD Info depending on result of analysis |
547 | ? | adapt_info(Info,Subs,NewInfo) :- subs_contain_wd_condition(Subs),!,NewInfo=Info. |
548 | | adapt_info(Info,_,[discharged_wd_po|NewInfo]) :- |
549 | | NewInfo=Info, memberchk(contains_wd_condition,Info). |
550 | | %delete(Info,contains_wd_condition,NewInfo). |
551 | | |
552 | | subs_contain_wd_condition(Subs) :- |
553 | ? | member(b(_,_,Infos),Subs), |
554 | | (memberchk(contains_wd_condition,Infos) -> nonmember(discharged_wd_po,Infos)). |
555 | | |
556 | | % transform independent sub-arguments |
557 | | l_transform_wd([],_Hyps,_Options,[]). |
558 | | l_transform_wd([Sub|T],Hyps,Options,[NSub|NT]) :- |
559 | | transform_wd(Sub,Hyps,Options,NSub), |
560 | | l_transform_wd(T,Hyps,Options,NT). |
561 | | |
562 | | % transform conjunction like sub-arguments, with left-to-right adding of hypotheses |
563 | | l_transform_conj_wd([],_Hyps,_Options,[]). |
564 | | l_transform_conj_wd([Sub|T],Hyps,Options,[NSub|NT]) :- |
565 | | transform_wd(Sub,Hyps,Options,NSub), |
566 | | push_hyp(Hyps,Sub,Options,Hyps2), |
567 | | l_transform_conj_wd(T,Hyps2,Options,NT). |
568 | | |
569 | | % transform special cases where sub-arguments are not independent nor conjunction-like |
570 | | % TO DO: assign |
571 | | transform_special_expr(disjunct(A,B),_,Info,Hyps,Options,disjunct(TA,TB),NewInfo) :- |
572 | | transform_wd(A,Hyps,Options,TA), |
573 | | negate_hyp(A,NA), |
574 | | push_hyp(Hyps,NA,Options,Hyps2), |
575 | | transform_wd(B,Hyps2,Options,TB), |
576 | | adapt_info(Info,[TA,TB],NewInfo). |
577 | | transform_special_expr(if_then_else(A,B,C),_,Info,Hyps,Options,if_then_else(TA,TB,TC),NewInfo) :- |
578 | | transform_wd(A,Hyps,Options,TA), |
579 | | push_hyp(Hyps,A,Options,Hyps2), |
580 | | transform_wd(B,Hyps2,Options,TB), |
581 | | negate_hyp(A,NA), |
582 | | push_hyp(Hyps,NA,Options,Hyps3), |
583 | | transform_wd(C,Hyps3,Options,TC), |
584 | | adapt_info(Info,[TA,TB,TC],NewInfo). |
585 | | transform_special_expr(recursive_let(ID,B),_,Info,Hyps,Options,recursive_let(ID,TB),NewInfo) :- NewInfo=Info, |
586 | | transform_wd(B,Hyps,Options,TB). |
587 | | transform_special_expr(general_sum(Ids,P,E),_Type,Info,Hyps,Options,general_sum(Ids,TP,TE),NewInfo) :- |
588 | | NewInfo=Info, % Note: we do not try to discharge finite PO; TODO: add |
589 | | transform_wd(P,Hyps,Options,TP), |
590 | | push_hyp(Hyps,P,Options,Hyps2), |
591 | | transform_wd(E,Hyps2,Options,TE). |
592 | | transform_special_expr(general_product(Ids,P,E),_Type,Info,Hyps,Options,general_product(Ids,TP,TE),NewInfo) :- |
593 | | NewInfo=Info, % Note: we do not try to discharge finite PO |
594 | | transform_wd(P,Hyps,Options,TP), |
595 | | push_hyp(Hyps,P,Options,Hyps2), |
596 | | transform_wd(E,Hyps2,Options,TE). |
597 | | transform_special_expr(if(List),_,Info,Hyps,Options,if(TList),NewInfo) :- |
598 | | list_transform_if_elsif_wd(List,Hyps,Options,TList), |
599 | | adapt_info(Info,TList,NewInfo). |
600 | | |
601 | | list_transform_if_elsif_wd([],_,_,[]). |
602 | | list_transform_if_elsif_wd([b(if_elsif(A,Body),Type,I) | T], Hyps,Options,Res) :- |
603 | | is_truth(A),!, |
604 | | Res=[b(if_elsif(A,TBody),Type,I) | T], |
605 | | transform_wd(Body,Hyps,Options,TBody). |
606 | | list_transform_if_elsif_wd([b(if_elsif(A,Body),Type,I) | T], Hyps,Options, |
607 | | [b(if_elsif(TA,TBody),Type,I) | TT]) :- |
608 | | transform_wd(A,Hyps,Options,TA), |
609 | | push_hyp(Hyps,A,Options,Hyps2), |
610 | | transform_wd(Body,Hyps2,Options,TBody), |
611 | | negate_hyp(A,NA), |
612 | | push_hyp(Hyps,NA,Options,Hyps3), |
613 | | list_transform_if_elsif_wd(T,Hyps3,Options,TT). |
614 | | |
615 | | % ------------------------------ |
616 | | |
617 | | :- use_module(probsrc(bsyntaxtree),[conjunction_to_list/2]). |
618 | | :- use_module(probsrc(tools),[split_list/4]). |
619 | | |
620 | | % process those conjuncts with no WD condition first; this means we have more hypotheses for proving and is safe for ProB |
621 | | % Option 'skip_finite_po' can be used to not generate finite(.) POs. |
622 | | % These POs are, e.g., irrelevant for constraint solving in ProB since the solver would exceed the timeout if finite(.) cannot be proven. |
623 | | compute_wd_with_reordering(TExpr,Hypotheses,Options,PO) :- \+ ord_member(reorder_conjuncts,Options),!, |
624 | | compute_wd(TExpr,Hypotheses,Options,PO). |
625 | | compute_wd_with_reordering(TExpr,Hypotheses,Options,PO) :- |
626 | | conjunction_to_list(TExpr,Conjuncts), |
627 | | split_list(is_well_defined_conjunct,Conjuncts,Conj1,Conj2), |
628 | | Conj2 \= [], % otherwise no WD condition anyway |
629 | | (ord_member(ignore_wd_infos,Options) |
630 | | -> append(Conj1,Conj2,Conj12), |
631 | ? | list_compute_wd(Conj12,Options,Hypotheses,PO) |
632 | | ; push_hyps(Hypotheses,Conj1,Options,Hyps2), % push the Hypotheses without WD checking |
633 | | list_compute_wd(Conj2,Options,Hyps2,PO) |
634 | | ). |
635 | | |
636 | | %is_well_defined_conjunct(TE) :- print('Checking conjunct: '), translate:print_bexpr(TE),nl,fail. |
637 | | is_well_defined_conjunct(b(_,_,Infos)) :- nonmember(contains_wd_condition,Infos),!. |
638 | | %is_well_defined_conjunct(TE) :- print('Not well defined: '), translate:print_bexpr(TE),nl,fail. |
639 | | |
640 | | compute_wd(TExpr,Hypotheses,Options,PO) :- |
641 | | syntaxtraversion(TExpr,Expr,Type,Infos,Subs,TNames), |
642 | | (ord_member(ignore_wd_infos,Options) -> true ; memberchk(contains_wd_condition,Infos) -> true), |
643 | | %(print(Expr),nl ; print(backtrack(Expr)),nl,fail), |
644 | ? | (get_info_labels(Infos,Label) -> ord_add_element(Options,po_label(Label),Opt2) ; Opt2=Options), |
645 | ? | compute_wd_aux(Expr,Type,Infos,Subs,TNames,Hypotheses,Opt2,PO), |
646 | | true. %check_if_po_expected(PO,TExpr,Infos). |
647 | | |
648 | | check_if_po_expected(PO,TExpr,Infos) :- |
649 | | ( memberchk(contains_wd_condition,Infos) -> true |
650 | | ; get_texpr_info(PO,POInfo), POInfo=[discharged(true,_)|_] -> true |
651 | | % Note: Sigma currently gets no contains_wd_condition, but has finiteness WD constraint |
652 | | ; add_error(well_def_analyser,'Unexpected WD-PO for expression marked to have no WD condition:',PO,TExpr) |
653 | | ). |
654 | | |
655 | | :- use_module(library(lists),[maplist/3]). |
656 | | % treat assignment substitution |
657 | | % see b_assign_values_or_functions in b_interpreter |
658 | | compute_wd_assign(Hyps,Options,PO,LHS,RHS) :- LHS=b(function(F,X),_,_), |
659 | | !, |
660 | | % special case for f(X) := RHS |
661 | | ( compute_wd(F,Hyps,Options,PO) % ? |
662 | | ; compute_wd(X,Hyps,Options,PO) |
663 | ? | ; compute_wd(RHS,Hyps,Options,PO) ). |
664 | | compute_wd_assign(Hyps,Options,PO,_,RHS) :- % LHS must be an identifier |
665 | ? | compute_wd(RHS,Hyps,Options,PO). |
666 | | |
667 | | compute_wd_aux(assign(LHSList,RHSList),_,_,_,[],Hypotheses,Options,PO) :- |
668 | | !, |
669 | ? | maplist(compute_wd_assign(Hypotheses,Options,PO),LHSList,RHSList). |
670 | | compute_wd_aux(Expr,_,_,Subs,TNames,Hypotheses,Options,PO) :- |
671 | | wd_transparent(Expr),!, |
672 | | % cut: only look at WD condition of all sub-arguments |
673 | | add_new_hyp_variables(Hypotheses,TNames,Hyps2), |
674 | ? | member(Sub,Subs), |
675 | ? | compute_wd(Sub,Hyps2,Options,PO). |
676 | | % Now the rules which do not look at all sub-arguments with original Hypotheses: |
677 | | compute_wd_aux(conjunct(A,B),_,_,_,_,Hypotheses,Options,PO) :- !, |
678 | | flatten_conjunct(A,B,List), % avoid re-pushing hyps if A is nested conjunct |
679 | ? | compute_wd_conjuncts(List,Hypotheses,Options,PO). |
680 | | compute_wd_aux(sequence(List),subst,_,_,_,Hypotheses,Options,PO) :- % sequential composition |
681 | | !, |
682 | ? | sequence_compute_wd(List,Options,Hypotheses,PO). |
683 | | compute_wd_aux(while(COND,STMT,INV,VARIANT),_,Infos,_,_,Hypotheses,Options,PO) :- !, |
684 | | (member(modifies(VarsModified),Infos) -> debug_println(9,computed_wd_while(VarsModified)) |
685 | | ; add_error(well_def_analyser,'While does not contain modifies info:',Infos,Infos), |
686 | | VarsModified=[] |
687 | | ), |
688 | | copy_hyp_variables(Hypotheses,VarsModified,Hyps2), % we can no longer make any assumption about the modified vars |
689 | | % this corresponds to a universal quantification |
690 | | ( compute_wd(INV,Hyps2,Options,PO) % Invariant must hold before and after WHILE loop |
691 | | ; |
692 | | push_hyp(Hyps2,INV,Options,Hyps3), % add INV to the hypotheses now for the other parts of the WHILE |
693 | | ( |
694 | | compute_wd(COND,Hyps3,Options,PO) |
695 | | ; |
696 | | compute_wd(VARIANT,Hyps3,Options,PO) % NAT proof rule for While must also hold if P is false according to Atelier-B handbook (otherwise we could have pushed COND onto the stack) |
697 | | ; |
698 | | push_hyp(Hyps3,COND,Options,Hyps4), |
699 | | compute_wd(STMT,Hyps4,Options,PO) % Statement is only executed if COND is true; INV is checked |
700 | | ) |
701 | | ). |
702 | | compute_wd_aux(Expr,Type,Infos,Subs,TNames,Hypotheses,Options,PO) :- |
703 | | wd_like_conjunction(Expr,_,A,B),!, |
704 | | add_new_hyp_variables(Hypotheses,TNames,Hyps2), |
705 | | ( create_top_level_wd_po_conj_like(Expr,Type,Infos,Hyps2,Options,PO,_Discharged) % e.g., for assertion_expression |
706 | | ; |
707 | ? | compute_wd_aux(conjunct(A,B),Type,Infos,Subs,TNames,Hyps2,Options,PO) |
708 | | ). |
709 | | compute_wd_aux(if_then_else(A,B,C),_,_,_,_,Hypotheses,Options,PO) :- !, |
710 | ? | (compute_wd(A,Hypotheses,Options,PO) |
711 | | ; |
712 | | push_hyp(Hypotheses,A,Options,NewHyp), |
713 | | compute_wd(B,NewHyp,Options,PO) |
714 | | ; |
715 | | negate_hyp(A,NA), |
716 | | push_hyp(Hypotheses,NA,Options,NewHyp), |
717 | ? | compute_wd(C,NewHyp,Options,PO)). |
718 | | compute_wd_aux(if(List),_,_,_,_,Hypotheses,Options,PO) :- !, |
719 | ? | list_compute_if_elsif_wd(List,Hypotheses,Options,PO). |
720 | | compute_wd_aux(disjunct(A,B),_,_,_,_,Hypotheses,Options,PO) :- !, |
721 | ? | (compute_wd(A,Hypotheses,Options,PO) |
722 | | ; |
723 | | negate_hyp(A,NA), |
724 | | push_hyp(Hypotheses,NA,Options,NewHyp), |
725 | ? | compute_wd(B,NewHyp,Options,PO)). |
726 | | compute_wd_aux(general_sum(Ids,P,E),Type,Infos,_,_,Hypotheses,Options,PO) :- !, % SIGMA, real or integer |
727 | | ( % first the sub arguments |
728 | | add_new_hyp_variables(Hypotheses,Ids,Hyps2), |
729 | | ( compute_wd(P,Hyps2,Options,PO) |
730 | | ; |
731 | | push_hyp(Hyps2,P,Options,NewHyp), |
732 | ? | compute_wd(E,NewHyp,Options,PO) |
733 | | ) |
734 | | ; % now the PO of general_sum itself |
735 | | create_top_level_wd_po(general_sum(Ids,P,E),Type,Infos,Hypotheses,Options,PO,_Discharged) |
736 | | ). |
737 | | compute_wd_aux(general_product(Ids,P,E),Type,Infos,Subs,TNames,Hypotheses,Options,PO) :- !, % PI |
738 | ? | compute_wd_aux(general_sum(Ids,P,E),Type,Infos,Subs,TNames,Hypotheses,Options,PO). |
739 | | compute_wd_aux(rlevent(_Name,_Sect,_Status,_Params,Guard,Theorems,Actions,VWit,PWit,_Unmod,_AbstractEvents), |
740 | | _,_Infos,_Subs,TNames,Hypotheses,Options,PO) :- !, |
741 | | add_new_hyp_variables(Hypotheses,TNames,Hyps2), |
742 | | % TO DO: treat nested lists VWit,... |
743 | | Act = b(parallel(Actions),subst,[]), |
744 | | append([[Guard],Theorems,VWit,PWit,[Act]],List), |
745 | ? | list_compute_wd(List,Options,Hyps2,PO). |
746 | | compute_wd_aux(recursive_let(_ID,Body),_,_,_,_,Hypotheses,Options,PO) :- !, |
747 | | % the ID does not have to be added to hypothesis stack ! |
748 | ? | compute_wd(Body,Hypotheses,Options,PO). |
749 | | % ---------------- |
750 | | % Now the rules where we also look at the sub-arguments with original Hypotheses: |
751 | | compute_wd_aux(_,_,_,Subs,TNames,Hypotheses,Options,PO) :- |
752 | | add_new_hyp_variables(Hypotheses,TNames,Hyp2), |
753 | | % look at WD condition of all sub-arguments independently |
754 | ? | member(Sub,Subs), |
755 | ? | compute_wd(Sub,Hyp2,Options,PO). |
756 | | % Now the specific rules: |
757 | | compute_wd_aux(Expr,Type,Infos,_,_,Hypotheses,Options,PO) :- |
758 | ? | create_top_level_wd_po(Expr,Type,Infos,Hypotheses,Options,PO,_Discharged). |
759 | | |
760 | | % treat a list of conjuncts (after flattening) |
761 | | %compute_wd_conjuncts([],_,_,_) :- fail. |
762 | | compute_wd_conjuncts([A|T],Hypotheses,Options,PO) :- |
763 | ? | (compute_wd(A,Hypotheses,Options,PO) |
764 | | ; |
765 | | T \= [], |
766 | | push_hyp(Hypotheses,A,Options,NewHyp), |
767 | ? | compute_wd_conjuncts(T,NewHyp,Options,PO)). |
768 | | |
769 | | % flatten conjuncts to avoid re-pushing the same hypotheses |
770 | | flatten_conjunct(ConjA,ConjB,List) :- |
771 | | flatten_conjunct_dl(ConjA,List,[ConjB]). % Tail not flattened; not necessary for performance |
772 | | flatten_conjunct_dl(b(conjunct(A,B),_,_)) --> !, flatten_conjunct_dl(A), flatten_conjunct_dl(B). |
773 | | flatten_conjunct_dl(X) --> [X]. |
774 | | |
775 | | |
776 | | % create top-level WD conditions for conjunction-like operators; not for sub-arguments |
777 | | create_top_level_wd_po_conj_like(assertion_expression(A,_Msg,_),_,Infos,Hypotheses,Options,PO,Discharged) :- !, |
778 | | Target = A, |
779 | | ord_add_element(Options,po_label('ASSERT'),Options2), |
780 | | create_po(Hypotheses,Target,Infos,Options2,PO,Discharged). |
781 | | |
782 | | % create top-level WD conditions; not for sub-arguments |
783 | | create_top_level_wd_po(function(A,B),_,Infos,Hypotheses,Options,PO,Discharged) :- !, |
784 | | (get_texpr_type(B,TB), |
785 | | safe_create_texpr(domain(A),set(TB),[],DomA), |
786 | | safe_create_texpr(member(B,DomA),pred,[],Target), |
787 | | create_po(Hypotheses,Target,Infos,Options,PO,Discharged) |
788 | | %, tools_printing:print_term_summary(created_function_po(Target,PO)) |
789 | | ; |
790 | | create_partial_fun_target(A,Target), |
791 | | create_po(Hypotheses,Target,Infos,Options,PO,Discharged) |
792 | | ). |
793 | | create_top_level_wd_po(div(_,B),integer,Infos,Hypotheses,Options,PO,Discharged) :- !, |
794 | | create_texpr(integer(0),integer,[],Zero), |
795 | | safe_create_texpr(not_equal(B,Zero),pred,[],Target), |
796 | | create_po(Hypotheses,Target,Infos,Options,PO,Discharged). |
797 | | create_top_level_wd_po(div_real(_,B),real,Infos,Hypotheses,Options,PO,Discharged) :- !, |
798 | | create_texpr(real('0.0'),real,[],Zero), |
799 | | safe_create_texpr(not_equal(B,Zero),pred,[],Target), |
800 | | create_po(Hypotheses,Target,Infos,Options,PO,Discharged). |
801 | | create_top_level_wd_po(floored_div(_,B),integer,Infos,Hypotheses,Options,PO,Discharged) :- !, |
802 | | create_texpr(integer(0),integer,[],Zero), |
803 | | safe_create_texpr(not_equal(B,Zero),pred,[],Target), |
804 | | create_po(Hypotheses,Target,Infos,Options,PO,Discharged). |
805 | | create_top_level_wd_po(modulo(A,B),integer,Infos,Hypotheses,Options,PO,Discharged) :- !, |
806 | | create_texpr(integer(0),integer,[],Zero), |
807 | | ( safe_create_texpr(greater(B,Zero),pred,[],Target), % does TLA require this to be positive?? |
808 | | create_po(Hypotheses,Target,Infos,Options,PO,Discharged) |
809 | | ; \+ z_or_tla_minor_mode, |
810 | | safe_create_texpr(greater_equal(A,Zero),pred,[],Target), % in B A must be positive |
811 | | create_po(Hypotheses,Target,Infos,Options,PO,Discharged) |
812 | | ). |
813 | | create_top_level_wd_po(power_of(A,B),integer,Infos,Hypotheses,Options,PO,Discharged) :- !, |
814 | | create_texpr(integer(0),integer,[],Zero), |
815 | | ( AB=B, % B >= 0 must hold in B and Event-B |
816 | | safe_create_texpr(greater_equal(AB,Zero),pred,[],Target), |
817 | | create_po(Hypotheses,Target,Infos,Options,PO,Discharged) |
818 | | ; eventb_mode, % TO DO: what happens in Z and TLA+? |
819 | | AB=A, % A >= 0 must hold in Event-B |
820 | | safe_create_texpr(greater_equal(AB,Zero),pred,[],Target), |
821 | | create_po(Hypotheses,Target,Infos,Options,PO,Discharged) |
822 | | ). |
823 | | create_top_level_wd_po(power_of_real(A,B),real,Infos,Hypotheses,Options,PO,Discharged) :- !, |
824 | | % power_of_real has a WD condition, real ** integer has not |
825 | | create_texpr(real('0.0'),real,[],Zero), |
826 | | ( % A < 0 => real(floor(B))=B |
827 | | safe_create_texpr(less_real(A,Zero),pred,[],LHS), |
828 | | safe_create_texpr(convert_int_floor(B),integer,[],FloorB), |
829 | | safe_create_texpr(convert_real(FloorB),real,[],BB), |
830 | | safe_create_texpr(equal(B,BB),pred,[],RHS), |
831 | | safe_create_texpr(implication(LHS,RHS),pred,[],Target), |
832 | | create_po(Hypotheses,Target,Infos,Options,PO,Discharged) |
833 | | ; % A = 0 => B >= 0 |
834 | | safe_create_texpr(equal(A,Zero),pred,[],LHS), |
835 | | safe_create_texpr(less_equal_real(Zero,B),pred,[],RHS), |
836 | | safe_create_texpr(implication(LHS,RHS),pred,[],Target), |
837 | | create_po(Hypotheses,Target,Infos,Options,PO,Discharged) |
838 | | ). |
839 | | create_top_level_wd_po(iteration(_Rel,Index),_,Infos,Hypotheses,Options,PO,Discharged) :- !, |
840 | | create_texpr(integer(0),integer,[],Zero), |
841 | | safe_create_texpr(greater_equal(Index,Zero),pred,[],Target), |
842 | | create_po(Hypotheses,Target,Infos,Options,PO,Discharged). |
843 | | create_top_level_wd_po(card(S),integer,Infos,Hypotheses,Options,PO,Discharged) :- |
844 | | !, |
845 | | \+ skip_finite_pos(Options), |
846 | | safe_create_texpr(finite(S),pred,[contains_wd_condition],Target), |
847 | | create_po(Hypotheses,Target,Infos,Options,PO,Discharged). |
848 | | create_top_level_wd_po(max(S),integer,Infos,Hypotheses,Options,PO,Discharged) :- !, |
849 | | get_texpr_type(S,TS), |
850 | | safe_create_texpr(not_equal(S,b(empty_set,TS,[])),pred,[],Target1), |
851 | | ( skip_finite_pos(Options) |
852 | | -> Target = Target1 |
853 | | ; safe_create_texpr(finite(S),pred,[contains_wd_condition],Target2), |
854 | | conjunct_predicates([Target1,Target2],Target) % this is a sufficient condition, not a necessary one |
855 | | ), |
856 | | % create a single PO, because of use in check_top_level_wd |
857 | | create_po(Hypotheses,Target,Infos,Options,PO,Discharged). |
858 | | create_top_level_wd_po(min(S),integer,Infos,Hypotheses,Options,PO,Discharged) :- !, |
859 | | get_texpr_type(S,TS), |
860 | | safe_create_texpr(not_equal(S,b(empty_set,TS,[])),pred,[],Target1), |
861 | | ( skip_finite_pos(Options) |
862 | | -> Target = Target1 |
863 | | ; safe_create_texpr(finite(S),pred,[contains_wd_condition],Target2), |
864 | | conjunct_predicates([Target1,Target2],Target) % this is a sufficient condition, not a necessary one |
865 | | ), |
866 | | create_po(Hypotheses,Target,Infos,Options,PO,Discharged). |
867 | | create_top_level_wd_po(max_real(S),real,Infos,Hypotheses,Options,PO,Discharged) :- !, |
868 | | create_top_level_wd_po(max(S),integer,Infos,Hypotheses,Options,PO,Discharged). % create same PO as for integer max |
869 | | create_top_level_wd_po(min_real(S),real,Infos,Hypotheses,Options,PO,Discharged) :- !, |
870 | | create_top_level_wd_po(min(S),integer,Infos,Hypotheses,Options,PO,Discharged). % ditto |
871 | | create_top_level_wd_po(general_intersection(A),TA,Infos,Hypotheses,Options,PO,Discharged) :- !, % inter |
872 | | safe_create_texpr(not_equal(A,b(empty_set,set(TA),[])),pred,[],Target), |
873 | | create_po(Hypotheses,Target,Infos,Options,PO,Discharged). |
874 | | % Sequence operators: |
875 | | create_top_level_wd_po(size(S),integer,Infos,Hypotheses,Options,PO,Discharged) :- !, |
876 | | % we do not have to create a finite PO: sequences are by construction finite |
877 | | create_sequence_target(S,Target), |
878 | | create_po(Hypotheses,Target,Infos,Options,PO,Discharged). |
879 | | create_top_level_wd_po(insert_tail(S,_),_,Infos,Hypotheses,Options,PO,Discharged) :- !, |
880 | | create_sequence_target(S,Target), create_po(Hypotheses,Target,Infos,Options,PO,Discharged). |
881 | | create_top_level_wd_po(insert_front(_,S),_,Infos,Hypotheses,Options,PO,Discharged) :- !, |
882 | | % page 174 of Abrial's book just requires that S is a partial function NATURAL1 +-> TYPE |
883 | | create_sequence_target(S,Target), create_po(Hypotheses,Target,Infos,Options,PO,Discharged). |
884 | | create_top_level_wd_po(rev(S),_,Infos,Hypotheses,Options,PO,Discharged) :- !, |
885 | | create_sequence_target(S,Target), create_po(Hypotheses,Target,Infos,Options,PO,Discharged). |
886 | | create_top_level_wd_po(concat(S1,S2),_,Infos,Hypotheses,Options,PO,Discharged) :- !, |
887 | | (create_sequence_target(S1,Target) ; create_sequence_target(S2,Target)), |
888 | | create_po(Hypotheses,Target,Infos,Options,PO,Discharged). |
889 | | create_top_level_wd_po(general_concat(S),_,Infos,Hypotheses,Options,PO,Discharged) :- !, |
890 | | create_seq_seq_target(S,Target), create_po(Hypotheses,Target,Infos,Options,PO,Discharged). |
891 | | create_top_level_wd_po(first(S),_,Infos,Hypotheses,Options,PO,Discharged) :- !, |
892 | | create_sequence1_target(S,Target), create_po(Hypotheses,Target,Infos,Options,PO,Discharged). |
893 | | create_top_level_wd_po(last(S),_,Infos,Hypotheses,Options,PO,Discharged) :- !, |
894 | | create_sequence1_target(S,Target), create_po(Hypotheses,Target,Infos,Options,PO,Discharged). |
895 | | create_top_level_wd_po(front(S),_,Infos,Hypotheses,Options,PO,Discharged) :- !, |
896 | | create_sequence1_target(S,Target), create_po(Hypotheses,Target,Infos,Options,PO,Discharged). |
897 | | create_top_level_wd_po(tail(S),_,Infos,Hypotheses,Options,PO,Discharged) :- !, |
898 | | create_sequence1_target(S,Target), create_po(Hypotheses,Target,Infos,Options,PO,Discharged). |
899 | | create_top_level_wd_po(restrict_front(S,N),_,Infos,Hypotheses,Options,PO,Discharged) :- !, |
900 | | ( create_sequence_target(S,Target) ; create_seq_interval_target(S,N,Target) ), |
901 | | create_po(Hypotheses,Target,Infos,Options,PO,Discharged). |
902 | | create_top_level_wd_po(restrict_tail(S,N),_,Infos,Hypotheses,Options,PO,Discharged) :- !, |
903 | | ( create_sequence_target(S,Target) ; create_seq_interval_target(S,N,Target) ), |
904 | | create_po(Hypotheses,Target,Infos,Options,PO,Discharged). |
905 | | create_top_level_wd_po(mu(S),_,Infos,Hypotheses,Options,PO,Discharged) :- !, % Z MU Operator |
906 | | get_texpr_type(S,TS), |
907 | | safe_create_texpr(not_equal(S,b(empty_set,TS,[])),pred,[],Target1), |
908 | | create_texpr(integer(1),integer,[],One), |
909 | | safe_create_texpr(card(S),integer,[contains_wd_condition],CardS), |
910 | | safe_create_texpr(less_equal(CardS,One),pred,[],Target2), |
911 | | ( skip_finite_pos(Options) |
912 | | -> conjunct_predicates([Target1,Target2],Target) |
913 | | ; safe_create_texpr(finite(S),pred,[contains_wd_condition],Target3), |
914 | | conjunct_predicates([Target1,Target3,Target2],Target) |
915 | | ), |
916 | | create_po(Hypotheses,Target,Infos,Options,PO,Discharged). |
917 | | % External Functions: |
918 | | create_top_level_wd_po(external_function_call('MU',[S]),T,Infos,Hypotheses,Options,PO,Discharged) :- !, |
919 | | create_top_level_wd_po(mu(S),T,Infos,Hypotheses,Options,PO,Discharged). |
920 | | create_top_level_wd_po(external_function_call('CHOOSE',[A]),_,Infos,Hypotheses,Options,PO,Discharged) :- !, |
921 | | get_texpr_type(A,TA), |
922 | | safe_create_texpr(not_equal(A,b(empty_set,set(TA),[])),pred,[],Target), |
923 | | create_po(Hypotheses,Target,Infos,Options,PO,Discharged). |
924 | | create_top_level_wd_po(external_function_call('SQUASH',[A]),_,Infos,Hypotheses,Options,PO,Discharged) :- !, |
925 | | create_partial_fun_target(A,Target), |
926 | | create_po(Hypotheses,Target,Infos,Options,PO,Discharged). |
927 | | create_top_level_wd_po(external_function_call(C,_),_,Infos,Hypotheses,Options,PO,Discharged) :- !, |
928 | | % external_fun_has_wd_condition is true |
929 | | get_preference(wd_ignore_external_funs,false), |
930 | | create_po(Hypotheses,b(unknown_truth_value(C),pred,[]),Infos,Options,PO,Discharged). |
931 | | create_top_level_wd_po(external_subst_call(C,_),_,Infos,Hypotheses,Options,PO,Discharged) :- !, % ditto |
932 | | get_preference(wd_ignore_external_funs,false), |
933 | | create_po(Hypotheses,b(unknown_truth_value(C),pred,[]),Infos,Options,PO,Discharged). |
934 | | create_top_level_wd_po(external_pred_call(C,_),_,Infos,Hypotheses,Options,PO,Discharged) :- !, % ditto |
935 | | get_preference(wd_ignore_external_funs,false), |
936 | | create_po(Hypotheses,b(unknown_truth_value(C),pred,[]),Infos,Options,PO,Discharged). |
937 | | create_top_level_wd_po(general_product(Ids,P,E),Type,Infos,Hypotheses,Options,PO,Discharged) :- !, |
938 | | create_top_level_wd_po(general_sum(Ids,P,E),Type,Infos,Hypotheses,Options,PO,Discharged). |
939 | | create_top_level_wd_po(general_sum(Ids,P,_E),_,Infos,Hypotheses,Options,PO,Discharged) :- !, |
940 | | \+ skip_finite_pos(Options), |
941 | | create_comprehension_set(Ids,P,[],TS), |
942 | | safe_create_texpr(finite(TS),pred,[contains_wd_condition],Target), |
943 | | create_po(Hypotheses,Target,Infos,Options,PO,Discharged). |
944 | | % Unsupported: |
945 | | create_top_level_wd_po(Expr,T,I,Hypotheses,Options,PO,Discharged) :- |
946 | | functor(Expr,F,N), |
947 | | ajoin(['Unsupported expression ',F,'/',N,': '],Msg), |
948 | | (ord_member_nonvar_chk(create_not_discharged_msg(MsgType),Options) |
949 | | -> (MsgType=silent -> true ; add_message(well_def_analyser,Msg,Expr,I)) % we create warning below |
950 | | ; known_to_be_unsupported(F,N) |
951 | | -> add_warning(well_def_analyser,Msg,Expr,I) |
952 | | ; wd_transparent(Expr) |
953 | | -> add_error(well_def_analyser,Msg,'transparent operator has no top-level WD condition',I) |
954 | | ; (wd_like_conjunction(Expr,_,_,_) ; Expr=disjunct(_,_)) |
955 | | -> add_error(well_def_analyser,Msg,'operator has no top-level WD condition',I) |
956 | | ; add_internal_error(Msg,create_top_level_wd_po(Expr,T,I,_,Options,PO,Discharged)) |
957 | | ), |
958 | | inc_counter(unsupported), |
959 | | create_po(Hypotheses,b(unknown_truth_value(F),pred,[wd(Expr)]),I,Options,PO,Discharged). |
960 | | |
961 | | skip_finite_pos(Options) :- |
962 | | (get_preference(wd_skip_finite_pos,true) -> true |
963 | | ; ord_member(skip_finite_po, Options)). |
964 | | |
965 | | known_to_be_unsupported(freetype_destructor,3). % has WD condition, see check_freetype_case in b_interpreter |
966 | | known_to_be_unsupported(lazy_let_expr,3). |
967 | | known_to_be_unsupported(lazy_let_pred,3). |
968 | | known_to_be_unsupported(lazy_let_subst,3). |
969 | | known_to_be_unsupported(quantified_intersection,3). |
970 | | |
971 | | create_partial_fun_target(A,Target) :- |
972 | | % see create_function_check in bvisual2 |
973 | | get_texpr_type(A,TA), is_set_type(TA,couple(TDom,TRan)), |
974 | | create_type_set(TDom,TDT), % we could also use create_maximal_type_set/2 |
975 | | create_type_set(TRan,TRT), |
976 | | safe_create_texpr(partial_function(TDT,TRT),set(TA),[],PF), |
977 | | safe_create_texpr(member(A,PF),pred,[],Target). |
978 | | |
979 | | :- use_module(probsrc(bsyntaxtree),[is_set_type/2]). |
980 | | % get texpr for set of all sequences: |
981 | | create_seq_type_expr(Seq,Sequences) :- |
982 | | get_texpr_type(Seq,ST), |
983 | | is_set_type(ST,couple(_,TRan)), |
984 | | create_type_set(TRan,TRT), |
985 | | safe_create_texpr(seq(TRT),set(ST),[],Sequences). |
986 | | create_seq1_type_expr(Seq,Sequences) :- |
987 | | get_texpr_type(Seq,ST), |
988 | | is_set_type(ST,couple(_,TRan)), |
989 | | create_type_set(TRan,TRT), |
990 | | safe_create_texpr(seq1(TRT),set(ST),[],Sequences). |
991 | | create_seq_seq_type_expr(SeqSeq,SequencesOfSequences) :- |
992 | | get_texpr_type(SeqSeq,SST), |
993 | | is_set_type(SST,couple(_,SeqT)), % SeqT = type of the inner sequences |
994 | | is_set_type(SeqT,couple(_,TRan)), % TRan is type elements in the inner sequence |
995 | | create_type_set(TRan,TRT1), |
996 | | safe_create_texpr(seq(TRT1),set(SeqT),[],Sequences), |
997 | | safe_create_texpr(seq(Sequences),set(SST),[],SequencesOfSequences). |
998 | | |
999 | | create_type_set(boolean,Res) :- !, Res=b(bool_set,set(boolean),[]). % custom rule not necessary |
1000 | | create_type_set(integer,Res) :- !, Res=b(integer_set('INTEGER'),set(integer),[]). |
1001 | | create_type_set(string,Res) :- !, Res=b(string_set,set(string),[]). |
1002 | | create_type_set(Type,Res) :- create_texpr(typeset,set(Type),[],Res). |
1003 | | |
1004 | | create_sequence_target(S,Target) :- |
1005 | | create_seq_type_expr(S,Sequences), |
1006 | | extract_pos_infos(S,PosInfos), |
1007 | | safe_create_texpr(member(S,Sequences),pred,PosInfos,Target). |
1008 | | create_sequence1_target(S,Target) :- |
1009 | | create_seq1_type_expr(S,Sequences), |
1010 | | extract_pos_infos(S,PosInfos), |
1011 | | safe_create_texpr(member(S,Sequences),pred,PosInfos,Target). |
1012 | | create_seq_seq_target(S,Target) :- |
1013 | | create_seq_seq_type_expr(S,SeqSeq), |
1014 | | extract_pos_infos(S,PosInfos), |
1015 | | safe_create_texpr(member(S,SeqSeq),pred,PosInfos,Target). |
1016 | | |
1017 | | create_seq_interval_target(S,N,Target) :- |
1018 | | create_texpr(integer(0),integer,[],Zero), |
1019 | | safe_create_texpr(size(S),integer,[contains_wd_condition],MaxIdx), |
1020 | | safe_create_texpr(interval(Zero,MaxIdx),set(integer),[],ValidIdxs), |
1021 | | safe_create_texpr(member(N,ValidIdxs),pred,[],Target). |
1022 | | |
1023 | | % compute WD of a conjunction/sequence of formulas |
1024 | | list_compute_wd([A|_],Options,Hyps,PO) :- |
1025 | ? | compute_wd(A,Hyps,Options,PO). |
1026 | | list_compute_wd([A|T],Options,Hyps,PO) :- T \= [], |
1027 | | push_hyp(Hyps,A,Options,Hyps2), |
1028 | ? | list_compute_wd(T,Options,Hyps2,PO). |
1029 | | |
1030 | | % compute WD of a list of independent formulas |
1031 | | %list_indep_compute_wd([A|T],Options,Hyps,PO) :- |
1032 | | % (compute_wd(A,Hyps,Options,PO) |
1033 | | % ; |
1034 | | % list_indep_compute_wd(T,Options,Hyps,PO)). |
1035 | | |
1036 | | % compute WD of a list of IF-THEN-ELSE cases: |
1037 | | list_compute_if_elsif_wd([b(if_elsif(A,Body),_,_) | T], Hyps,Options,PO) :- |
1038 | | ( is_truth(A) -> compute_wd(Body,Hyps,Options,PO) |
1039 | ? | ; ( compute_wd(A,Hyps,Options,PO) |
1040 | | ; |
1041 | | push_hyp(Hyps,A,Options,NewHyp), |
1042 | ? | compute_wd(Body,NewHyp,Options,PO) |
1043 | | ; |
1044 | | T \= [], |
1045 | | negate_hyp(A,NA), |
1046 | | push_hyp(Hyps,NA,Options,NewHyp), |
1047 | | list_compute_if_elsif_wd(T, NewHyp,Options,PO) |
1048 | | ) |
1049 | | ). |
1050 | | |
1051 | | % compute WD of a conjunction/sequence of formulas |
1052 | | sequence_compute_wd([A|_],Options,Hyps,PO) :- |
1053 | ? | compute_wd(A,Hyps,Options,PO). |
1054 | | sequence_compute_wd([A|T],Options,Hyps,PO) :- T \= [], |
1055 | | update_hyp_for_sequence_lhs(Hyps,A,Options,Hyps2), |
1056 | ? | sequence_compute_wd(T,Options,Hyps2,PO). |
1057 | | |
1058 | | :- use_module(probsrc(b_read_write_info), [get_accessed_vars/4]). |
1059 | | % update the hypotheses depending on effect of LHS of a sequential composition: |
1060 | | update_hyp_for_sequence_lhs(Hyps,b(LHS,subst,_),Options,Hyps2) :- |
1061 | | process_seq_lhs_aux(LHS,Hyps,Options,Hyps2), |
1062 | | !. |
1063 | | update_hyp_for_sequence_lhs(Hyps,TStmt,_Options,Hyps2) :- |
1064 | | add_modified_vars_to_hyp(Hyps,TStmt,Hyps2). |
1065 | | %add_message(well_def_analyser,'Uncovered substitution in sequential composition: ',TStmt,TStmt). |
1066 | | |
1067 | | % add all modified vars as new hyp vars: new hypotheses and goals will thus refer to new version (like priming variables) |
1068 | | add_modified_vars_to_hyp(Hyps,TLHS,Hyps2) :- |
1069 | | (get_accessed_vars(TLHS,[],ModifiedVars,_Read) -> true |
1070 | | ; add_error(well_def_analyser,'Could not obtain modified vars:',TLHS,TLHS), ModifiedVars=[] |
1071 | | ), |
1072 | | maplist(construct_typed_var(Hyps),ModifiedVars,TModVars), |
1073 | | add_new_hyp_variables(Hyps,TModVars,Hyps2). |
1074 | | |
1075 | | construct_typed_var(Hyps,ID,b(identifier(ID),Type,[])) :- |
1076 | | (get_hyp_var_type(ID,Hyps,Type) -> true |
1077 | | ; add_internal_error('Unknown identifier in hyps:',ID), Type=any). |
1078 | | |
1079 | | rename_expr(Hyps,Expr,RenExpr) :- get_renamed_expression(Expr,Hyps,RenExpr). |
1080 | | :- use_module(probsrc(bsyntaxtree),[get_texpr_id/2]). |
1081 | | construct_equal(TID,RenExpr, b(equal(TID,RenExpr),pred,[])) :- get_texpr_id(TID,_),!. |
1082 | | construct_equal(_,_,b(truth,pred,[])). % TO DO: deal with more complex assignments f(i) := E -> f' = f <+ {i|->E} |
1083 | | |
1084 | | process_seq_lhs_aux(assign_single_id(TID,Expr),Hyps,Options,Hyps2) :- !, |
1085 | | get_renamed_expression(Expr,Hyps,RenExpr), % rename in old context; e.g., if we have x:=x+1 |
1086 | | add_new_hyp_variables(Hyps,[TID],Hyps1), |
1087 | | get_renamed_expression(TID,Hyps1,RenTID), |
1088 | | Eq = b(equal(RenTID,RenExpr),pred,[]), % print('Add: '), translate:print_bexpr(Eq),nl, |
1089 | | push_hyps_wo_renaming(Hyps1,[Eq],Options,Hyps2). %, portray_hyps(Hyps2). |
1090 | | process_seq_lhs_aux(assign(FTIDs,Exprs),Hyps,Options,Hyps2) :- !, |
1091 | | maplist(rename_expr(Hyps),Exprs,RenExprs),% rename in old context; e.g., if we have x:=x+1 |
1092 | | maplist(get_assigned_ids,FTIDs,TIDs), |
1093 | | add_new_hyp_variables(Hyps,TIDs,Hyps1), |
1094 | | maplist(rename_expr(Hyps1),TIDs,RenTIDs), |
1095 | | maplist(well_def_analyser:construct_equal,RenTIDs,RenExprs,Equalities), |
1096 | | push_hyps_wo_renaming(Hyps1,Equalities,Options,Hyps2). |
1097 | | |
1098 | | % get assigned ids for things like f(x) := E or r'f := E |
1099 | | get_assigned_ids(b(Expr,_,_),TID) :- get_assigned_id(Expr,F), !,get_assigned_ids(F,TID). |
1100 | | get_assigned_ids(TID,TID). |
1101 | | |
1102 | | get_assigned_id(function(F,_),F). |
1103 | | get_assigned_id(record_field(R,_),R). |
1104 | | |
1105 | | % wd_like_conjunction(Construct,NewTypedVars,Conjunct1,Conjunct2) |
1106 | | wd_like_conjunction(conjunct(A,B),[],A,B). |
1107 | | wd_like_conjunction(implication(A,B),[],A,B). |
1108 | | wd_like_conjunction(precondition(A,B),[],A,B). |
1109 | | wd_like_conjunction(assertion(A,B),[],A,B). |
1110 | | wd_like_conjunction(select_when(A,B),[],A,B). |
1111 | | wd_like_conjunction(assertion_expression(A,_Msg,B),[],A,B). % Note: this has associated WD condition |
1112 | | wd_like_conjunction(any(Ids,A,B),Ids,A,B). |
1113 | | wd_like_conjunction(forall(Ids,A,B),Ids,A,B). |
1114 | | wd_like_conjunction(quantified_union(Ids,A,B),Ids,A,B). % rewritten |
1115 | | wd_like_conjunction(let_predicate(Ids,E,P),Ids,A,P) :- construct_let_eq_pred(Ids,E,A). |
1116 | | wd_like_conjunction(let_expression(Ids,E,P),Ids,A,P) :- construct_let_eq_pred(Ids,E,A). |
1117 | | wd_like_conjunction(let(Ids,E,P),Ids,A,P) :- A=E. % this is already a predicate |
1118 | | |
1119 | | |
1120 | | :- use_module(library(lists),[maplist/4,append/2]). |
1121 | | construct_let_eq_pred(Ids,E,Pred) :- |
1122 | | (ground(Pred) |
1123 | | -> conjunction_to_list(Pred,Ps), % enable predicate to be used both ways |
1124 | | maplist(deconstruct_eq,Ids,E,Ps) |
1125 | | ; maplist(construct_eq,Ids,E,Ps), |
1126 | | conjunct_predicates(Ps,Pred) |
1127 | | ),!. |
1128 | | construct_let_eq_pred(Ids,E,Pred) :- add_internal_error('Call failed: ',construct_let_eq_pred(Ids,E,Pred)),fail. |
1129 | | |
1130 | | construct_eq(TID,E,EqPred) :- safe_create_texpr(equal(TID,E),pred,EqPred). |
1131 | | deconstruct_eq(TID,E,b(equal(TID,E),pred,_)). |
1132 | | |
1133 | | % The constructs which have no WD condition of their own; they just require checking the arguments: |
1134 | | wd_transparent(truth). |
1135 | | wd_transparent(falsity). |
1136 | | wd_transparent(negation(_)). |
1137 | | wd_transparent(equivalence(_,_)). |
1138 | | wd_transparent(equal(_,_)). |
1139 | | wd_transparent(not_equal(_,_)). |
1140 | | wd_transparent(member(_,_)). |
1141 | | wd_transparent(not_member(_,_)). |
1142 | | wd_transparent(subset(_,_)). |
1143 | | wd_transparent(subset_strict(_,_)). |
1144 | | wd_transparent(not_subset(_,_)). |
1145 | | wd_transparent(not_subset_strict(_,_)). |
1146 | | wd_transparent(less_equal(_,_)). |
1147 | | wd_transparent(less(_,_)). |
1148 | | wd_transparent(less_equal_real(_,_)). |
1149 | | wd_transparent(less_real(_,_)). |
1150 | | wd_transparent(greater_equal(_,_)). |
1151 | | wd_transparent(greater(_,_)). |
1152 | | wd_transparent(finite(_)). |
1153 | | wd_transparent(partition(_,_)). |
1154 | | wd_transparent(value(_)). |
1155 | | wd_transparent(boolean_true). |
1156 | | wd_transparent(boolean_false). |
1157 | | wd_transparent(max_int). |
1158 | | wd_transparent(min_int). |
1159 | | wd_transparent(empty_set). |
1160 | | wd_transparent(bool_set). |
1161 | | wd_transparent(float_set). |
1162 | | wd_transparent(real_set). |
1163 | | wd_transparent(string_set). |
1164 | | wd_transparent(convert_bool(_)). |
1165 | | wd_transparent(convert_int_ceiling(_)). |
1166 | | wd_transparent(convert_int_floor(_)). |
1167 | | wd_transparent(convert_real(_)). |
1168 | | wd_transparent(add(_,_)). |
1169 | | wd_transparent(add_real(_,_)). |
1170 | | wd_transparent(minus(_,_)). |
1171 | | wd_transparent(minus_real(_,_)). |
1172 | | wd_transparent(minus_or_set_subtract(_,_)). |
1173 | | wd_transparent(unary_minus(_)). |
1174 | | wd_transparent(unary_minus_real(_)). |
1175 | | wd_transparent(multiplication(_,_)). |
1176 | | wd_transparent(multiplication_real(_,_)). |
1177 | | wd_transparent(mult_or_cart(_,_)). |
1178 | | wd_transparent(cartesian_product(_,_)). |
1179 | | wd_transparent(successor). |
1180 | | wd_transparent(predecessor). |
1181 | | wd_transparent(couple(_,_)). |
1182 | | wd_transparent(pow_subset(_)). |
1183 | | wd_transparent(pow1_subset(_)). |
1184 | | wd_transparent(fin_subset(_)). |
1185 | | wd_transparent(fin1_subset(_)). |
1186 | | wd_transparent(general_union(_)). |
1187 | | wd_transparent(interval(_,_)). |
1188 | | wd_transparent(union(_,_)). |
1189 | | wd_transparent(intersection(_,_)). |
1190 | | wd_transparent(set_subtraction(_,_)). |
1191 | | wd_transparent(relations(_,_)). |
1192 | | wd_transparent(identity(_)). |
1193 | | wd_transparent(event_b_identity). |
1194 | | wd_transparent(reverse(_)). |
1195 | | wd_transparent(first_projection(_,_)). |
1196 | | wd_transparent(first_of_pair(_)). |
1197 | | wd_transparent(event_b_first_projection(_)). |
1198 | | wd_transparent(event_b_first_projection_v2). |
1199 | | wd_transparent(second_projection(_,_)). |
1200 | | wd_transparent(event_b_second_projection(_)). |
1201 | | wd_transparent(event_b_second_projection_v2). |
1202 | | wd_transparent(second_of_pair(_)). |
1203 | | wd_transparent(composition(_,_)). |
1204 | | wd_transparent(ring(_,_)). |
1205 | | wd_transparent(direct_product(_,_)). |
1206 | | wd_transparent(parallel_product(_,_)). |
1207 | | wd_transparent(trans_function(_)). |
1208 | | wd_transparent(trans_relation(_)). |
1209 | | %wd_transparent(iteration(_,_)). % has a WD condition on index of iteration |
1210 | | wd_transparent(reflexive_closure(_)). |
1211 | | wd_transparent(closure(_)). |
1212 | | wd_transparent(domain(_)). |
1213 | | wd_transparent(range(_)). |
1214 | | wd_transparent(image(_,_)). |
1215 | | wd_transparent(domain_restriction(_,_)). |
1216 | | wd_transparent(domain_subtraction(_,_)). |
1217 | | wd_transparent(range_restriction(_,_)). |
1218 | | wd_transparent(range_subtraction(_,_)). |
1219 | | wd_transparent(overwrite(_,_)). |
1220 | | wd_transparent(partial_function(_,_)). |
1221 | | wd_transparent(total_function(_,_)). |
1222 | | wd_transparent(partial_injection(_,_)). |
1223 | | wd_transparent(total_injection(_,_)). |
1224 | | wd_transparent(partial_surjection(_,_)). |
1225 | | wd_transparent(total_surjection(_,_)). |
1226 | | wd_transparent(total_bijection(_,_)). |
1227 | | wd_transparent(partial_bijection(_,_)). |
1228 | | wd_transparent(total_relation(_,_)). |
1229 | | wd_transparent(surjection_relation(_,_)). |
1230 | | wd_transparent(total_surjection_relation(_,_)). |
1231 | | wd_transparent(seq(_)). |
1232 | | wd_transparent(seq1(_)). |
1233 | | wd_transparent(iseq(_)). |
1234 | | wd_transparent(iseq1(_)). |
1235 | | wd_transparent(perm(_)). |
1236 | | wd_transparent(empty_sequence). |
1237 | | wd_transparent(identifier(_)). |
1238 | | wd_transparent(lazy_lookup_expr(_)). |
1239 | | wd_transparent(lazy_lookup_pred(_)). |
1240 | | wd_transparent(integer(_)). |
1241 | | wd_transparent(integer_set(_)). |
1242 | | wd_transparent(real(_)). |
1243 | | wd_transparent(string(_)). |
1244 | | wd_transparent(set_extension(_)). |
1245 | | wd_transparent(sequence_extension(_)). |
1246 | | wd_transparent(struct(_)). |
1247 | | wd_transparent(rec(_)). |
1248 | | wd_transparent(record_field(_,_)). |
1249 | | wd_transparent(typeset). |
1250 | | |
1251 | | wd_transparent(external_function_call(F,_)) :- \+ external_fun_has_wd_condition(F). |
1252 | | wd_transparent(external_pred_call(F,_)) :- \+ external_fun_has_wd_condition(F). |
1253 | | wd_transparent(external_subst_call(F,_)) :- \+ external_fun_has_wd_condition(F). |
1254 | | |
1255 | | wd_transparent(operation_call_in_expr(_,_)). % the operations will be checked for WD independently |
1256 | | % PRE conditions are not part of WD checking |
1257 | | |
1258 | | wd_transparent(freetype_set(_)). |
1259 | | wd_transparent(freetype_constructor(_,_,_)). |
1260 | | wd_transparent(freetype_case(_,_,_)). % predicate to check if we match a given case |
1261 | | |
1262 | | % substitutions: |
1263 | | wd_transparent(skip). |
1264 | | wd_transparent(block(_)). |
1265 | | wd_transparent(parallel(_)). |
1266 | | wd_transparent(choice(_)). |
1267 | | wd_transparent(assign(_,_)). % TO DO: f(X) := E ==> f := f <+ {X|->E}, etc,... |
1268 | | wd_transparent(assign_single_id(_,_)). |
1269 | | wd_transparent(select(_)). |
1270 | | wd_transparent(select(_,_)). % TOD: Else only reached if all cases do not apply |
1271 | | wd_transparent(becomes_element_of(_,_)). % in classical B we do not have to check set not empty? |
1272 | | wd_transparent(becomes_such(_,_)). % in classical B we do not have to check satisfiability |
1273 | | wd_transparent(operation_call(_,_,_)). % I.e., we do not see checking PRE condition checking as part of WD checking |
1274 | | wd_transparent(var(_,_)). |
1275 | | |
1276 | | wd_transparent(witness(_,_)). |
1277 | | |
1278 | | % transparent with new quantified variables |
1279 | | wd_transparent(comprehension_set(_,_)). |
1280 | | wd_transparent(exists(_,_)). % WD must be proven universally for all subexpression |
1281 | | |
1282 | | |
1283 | | /* |
1284 | | Not yet covered: |
1285 | | |
1286 | | syntaxelement(kodkod(PId,Ids), Ids,[],[Ids],PId, pred). |
1287 | | |
1288 | | syntaxelement(operation_call_in_expr(Id,As), [Id|As], [], [As], [], expr). |
1289 | | |
1290 | | % rewritten: |
1291 | | syntaxelement(event_b_comprehension_set(Ids,E,P),[E,P|Ids], Ids,[Ids], [], expr/only_typecheck). |
1292 | | syntaxelement(lambda(Ids,P,E), [P,E|Ids],Ids,[Ids], [], expr). |
1293 | | |
1294 | | syntaxelement(quantified_intersection(Ids,P,E), [P,E|Ids],Ids,[Ids], [], expr). |
1295 | | |
1296 | | |
1297 | | TREE operations |
1298 | | |
1299 | | syntaxelement(let_expression_global(Ids,As,Expr), Exprs, Ids, [Ids,As], [], expr) :- % version used by b_compiler |
1300 | | append([Ids,As,[Expr]],Exprs). |
1301 | | syntaxelement(lazy_let_expr(TID,A,Expr), Exprs, [TID], [[TID],[A]], [], expr) :- |
1302 | | append([[TID],[A],[Expr]],Exprs). |
1303 | | syntaxelement(lazy_let_pred(TID,A,Expr), Exprs, [TID], [[TID],[A]], [], pred) :- |
1304 | | append([[TID],[A],[Expr]],Exprs). |
1305 | | syntaxelement(lazy_let_subst(TID,A,Expr), Exprs, [TID], [[TID],[A]], [], subst) :- |
1306 | | append([[TID],[A],[Expr]],Exprs). |
1307 | | |
1308 | | syntaxelement(compaction(A), [A], [], [], [], expr). |
1309 | | syntaxelement(mu(A), [A], [], [], [], expr). |
1310 | | syntaxelement(bag_items(A), [A], [], [], [], expr). |
1311 | | |
1312 | | syntaxelement(freetype_set(Id), [], [], [], Id, expr). |
1313 | | syntaxelement(freetype_case(Type,Case,Expr), [Expr], [], [], [Type,Case], pred). |
1314 | | syntaxelement(freetype_constructor(Type,Case,Expr), [Expr], [], [], [Type,Case], expr). |
1315 | | syntaxelement(freetype_destructor(Type,Case,Expr), [Expr], [], [], [Type,Case], expr). |
1316 | | |
1317 | | rlevent(Name,Section,_Status,_Params,Guard,_Theorems,_Actions,_VWitnesses,_PWitnesses,_Unmod,_AbstractEvents), |
1318 | | |
1319 | | |
1320 | | |
1321 | | seval /Users/leuschel/git_root/private_examples/ClearSy/2020/03_Mar/wd_timeout/invalidRef_welldef.mch |
1322 | | :wd |
1323 | | Analysis walltime: 183 ms |
1324 | | |
1325 | | Stats: [AXM/1084,THM/104,unsupported/7,not_discharged_po/545,discharged_po/704,caval__rule__1__compute/61] |
1326 | | Stats: [unsupported/2,AXM/1085,THM/104,not_discharged_po/542,discharged_po/708,caval__rule__1__compute/61] |
1327 | | |
1328 | | Analysis walltime: 31 ms |
1329 | | Stats: [AXM/1085,THM/104,not_discharged_po/542,discharged_po/708,caval__rule__1__compute/61] |
1330 | | when reordering and not ignoring infos: |
1331 | | Analysis walltime: 17 ms |
1332 | | Stats: [AXM/1085,THM/104,not_discharged_po/540,discharged_po/710,caval__rule__1__compute/61] |
1333 | | |
1334 | | Tests: |
1335 | | |
1336 | | :wd a>0 & x>0 & x:1..10 & f:1..10-->INTEGER & f(x)=2 & x>1 |
1337 | | :wd %x.(x:2..4 | %x.(x:4..8|10/x)(2*x)) = x |
1338 | | |
1339 | | :wd x:NATURAL1 & y>=x & x mod y = x/y |
1340 | | -> same PO generated twice |
1341 | | |
1342 | | :wd f6 = %x.(x>10 & x<20|100) & res=f6(11) |
1343 | | :wd i5 = %x.(x>10|100+x) & i5(100) = 200 |
1344 | | seval /Users/leuschel/git_root/prob_examples/examples/B/ASTD/wetransfer-545a33/Case_Study_Handmade/TRAIN_CONTROL_M6.mch |
1345 | | |
1346 | | :wd n:NATURAL & a:1..n --> 1..10 & a /= {} & a(1)=1 |
1347 | | |
1348 | | -> support for $0 missing |
1349 | | -> support for ; and while (adding condition and invariant to loop body hyps) for transform |
1350 | | -> support for operation all in expression |
1351 | | -> Parallel in classical B: we could propagate guards from first to second subst; CarlaTravelAgency; but Atelier-B considers this to be not well-defined; each parallel construct should be WD on its own; we should make no assumption about order |
1352 | | -> CASE statement: treat cases specially |
1353 | | |
1354 | | % Processing file 2/3: /Users/leuschel/git_root/private_examples/ClearSy/2020/01_Jan/logxml_system_error/rule.mch |
1355 | | Proof of AXM took 169 ms, result=discharged ... |
1356 | | */ |
1357 | | |
1358 | | % --------------------------------- |
1359 | | % Annotating operations so that we can discharge WD conditions statically |
1360 | | |
1361 | | % this can be called once for all operations: it gets the hypotheses that are available for (all) operations |
1362 | | get_hyps_for_top_level_operations(Options,Hyps) :- |
1363 | | push_properties_invariant_hyps(Options,Hyps). |
1364 | | |
1365 | | :- public transform_machine_operation/7. |
1366 | | |
1367 | | % should call get_hyps_for_top_level_operations |
1368 | | % Note: should be run after global types are pre-compiled; otherwise we do not detect global constants |
1369 | | % TODO: pre-compile global sets before computing operations? |
1370 | | transform_machine_operation(OpName,OpResults,OpFormalParameters,Body,Hyps,Options,NewBody) :- |
1371 | | PO_Name = OpName, |
1372 | | format('Checking WD of OPERATION ~w~n',[OpName]), |
1373 | | ord_add_element(Options,po_label(PO_Name),Opt1), |
1374 | | add_new_hyp_variables(Hyps,OpFormalParameters,Hyps6), |
1375 | | add_new_hyp_variables(Hyps6,OpResults,Hyps7), |
1376 | | ord_add_element(Opt1,discharge_po,Opt2), |
1377 | | ord_add_element(Opt2,reorder_conjuncts,Opt3), |
1378 | | transform_wd(Body,Hyps7,Opt3,NewBody), |
1379 | | print_wd_subst(NewBody). |
1380 | | |
1381 | | print_wd_subst(NewTExpr) :- |
1382 | | temporary_set_preference(pp_wd_infos,true,Chng), |
1383 | | translate:print_subst(NewTExpr),nl, |
1384 | | reset_temporary_preference(pp_wd_infos,Chng). |
1385 | | |
1386 | | push_properties_invariant_hyps(Options,Hyps4) :- |
1387 | | b_get_properties_from_machine(Properties), |
1388 | | empty_hyps(E), |
1389 | | b_get_machine_all_constants(Csts), |
1390 | | add_new_hyp_variables(E,Csts,OriginalHyps), |
1391 | | push_hyp(OriginalHyps,Properties,Options,Hyps1), |
1392 | | b_get_static_assertions_from_machine(StaticAssertions), |
1393 | | push_hyps(Hyps1,StaticAssertions,Options,Hyps2), |
1394 | | b_get_machine_variables(Vars), |
1395 | | add_new_hyp_variables(Hyps2,Vars,Hyps3), |
1396 | | b_get_invariant_from_machine(Invariant), |
1397 | | push_hyp(Hyps3,Invariant,Options,Hyps4). |
1398 | | |
1399 | | % --------------------------------- |
1400 | | |
1401 | | :- use_module(probsrc(bsyntaxtree), [def_get_texpr_ids/2]). |
1402 | | :- use_module(probsrc(btypechecker),[prime_identifiers/2]). |
1403 | | :- use_module(extrasrc(before_after_predicates),[prime_bexpr_for_ids/4, |
1404 | | before_after_predicate_for_operation_no_equalities/5]). |
1405 | | % try and prove invariant preservation using BA predicate |
1406 | | prove_invariant_preservation(OpName,TargetInv,Proven,Options) :- |
1407 | | push_properties_invariant_hyps(Options,Hyps), |
1408 | | b_get_invariant_from_machine(Invariant), |
1409 | | conjunction_to_list(Invariant,Invs), |
1410 | | before_after_predicate_for_operation_no_equalities(OpName,Paras,Results,BAPred,TChangedIds), |
1411 | | add_new_hyp_variables(Hyps,Paras,Hyps1), |
1412 | | add_new_hyp_variables(Hyps1,Results,Hyps2), |
1413 | | prime_identifiers(TChangedIds,NewPrimedIds), |
1414 | | add_new_hyp_variables(Hyps2,NewPrimedIds,Hyps3), |
1415 | | push_hyp(Hyps3,BAPred,Options,Hyps4), |
1416 | | formatsilent('~nProving invariant preservation for operation ~w~n',[OpName]), |
1417 | | (silent_mode(on) -> true ; translate:print_bexpr(BAPred),nl), |
1418 | | member(TargetInv,Invs), |
1419 | | def_get_texpr_ids(TChangedIds,ChangedIds), |
1420 | | prime_bexpr_for_ids(TargetInv,ChangedIds,PrimedTargetInv,ChangesPerformed), |
1421 | | (ChangesPerformed=false |
1422 | | -> Proven=unchanged % Invariant unaffected by event |
1423 | | ; prove_sequent_goal(PrimedTargetInv,Hyps4,Options) |
1424 | | -> Proven=proven |
1425 | | ; Proven=unproven), |
1426 | | (silent_mode(on) -> true |
1427 | | ; format(' ~w => ',[Proven]), translate:print_bexpr(PrimedTargetInv),nl). |
1428 | | |
1429 | | % well_def_analyser:prove_invariant_preservation(OpName,Target,Proven),fail. |
1430 | | |
1431 | | :- use_module(probsrc(tools_lists),[count_occurences/2]). |
1432 | | |
1433 | | analyse_invariants_for_machine(UnchangedNr,ProvenNr,UnProvenNr,TotPOsNr,Options) :- |
1434 | | findall(Proven,prove_invariant_preservation(_Op,_,Proven,Options),Ls), |
1435 | | count_occurences(Ls,Res), |
1436 | | (member(proven-ProvenNr,Res) -> true ; ProvenNr=0), |
1437 | | (member(unchanged-UnchangedNr,Res) -> true ; UnchangedNr=0), |
1438 | | (member(unproven-UnProvenNr,Res) -> true ; UnProvenNr=0), |
1439 | | TotPOsNr is UnchangedNr + ProvenNr + UnProvenNr. |
1440 | | |
1441 | | % TODO: look at weakest_precondition/3: no need to prime? |
1442 | | |
1443 | | % --------------------------------- |
1444 | | |
1445 | | |
1446 | | %% toplevel_wd_pos(Predicate, Hypotheses, ProofObligations). |
1447 | | % |
1448 | | % Returns a list of proof obligations for the given Ast, but only those relevant |
1449 | | % for the root node. |
1450 | | toplevel_wd_pos(b(Node, _, _), _, []) :- |
1451 | | wd_transparent(Node), !. |
1452 | | toplevel_wd_pos(b(Node, Type, Info), Hyps, WDPOs) :- |
1453 | | wd_like_conjunction(Node, _, _, _), !, |
1454 | | findall(PO, create_top_level_wd_po_conj_like(Node, Type, Info, Hyps, [discharge_po], PO, _), WDPOs). |
1455 | | toplevel_wd_pos(b(Node, Type, Info), Hyps, WDPOs) :- |
1456 | ? | has_top_level_wd_condition(Node), !, |
1457 | | findall(PO, create_top_level_wd_po(Node, Type, Info, Hyps, [discharge_po], PO, _), WDPOs). |
1458 | | toplevel_wd_pos(_, _, []). |
1459 | | |