1		% (c) 2009-2022 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(weakest_preconditions, [weakest_precondition/3,set_reference_machine/1,delete_reference_machine/0]).
6
7		:- use_module(probsrc(module_information),[module_info/2]).
8		:- module_info(group,cbc).
9		:- module_info(description,'This module provides weakest precondition calculation for B and Event-B operations.').
10
11		:- use_module(library(lists)).
12		:- use_module(library(sets), [subset/2]).
13
14		:- use_module(probsrc(bsyntaxtree), [get_texpr_expr/2,
15		get_texpr_id/2, get_texpr_ids/2,
16		get_texpr_type/2,
17		create_texpr/4, safe_create_texpr/3,
18		create_forall/3,
19		create_negation/2,
20		conjunct_predicates/2,
21		replace_id_by_expr/4,
22		replace_ids_by_exprs/4,
23		find_typed_identifier_uses/2,
24		remove_all_infos/2]).
25		:- use_module(probsrc(b_read_write_info), [get_accessed_vars/4]).
26		:- use_module(probsrc(btypechecker), [prime_identifiers/2,prime_identifier/2, is_primed_id/1]).
27		:- use_module(probsrc(error_manager), [add_error_fail/3]).
28		:- use_module(probsrc(tools), [assert_once/1]).
29		:- use_module(probsrc(bmachine), [b_get_machine_operation/4]).
30		:- use_module(probsrc(bmachine_structure), [get_section/3]).
31
32		:- use_module(probsrc(translate),[translate_substitution/2,print_subst/1]).
33		:- use_module(probsrc(debug),[debug_mode/1]).
34
35		% dynamic predicate may contain a machine in which operations are looked up
36		% this is nessasary for the wp of operation calls, if the operation does not
37		% belong to the currently loaded machine
38		% (but for example to a refinement/abstraction)
39		:- volatile machine/1.
40		:- dynamic machine/1.
41
42		set_reference_machine(M) :-
43		delete_reference_machine,
44		assert_once(machine(M)).
45		delete_reference_machine :-
46		retractall(machine(_)).
47
48		% lookup operations in the reference machine if it exists
49		% otherwise, lookup in loaded machine
50		lookup_operation(Name,Results,Parameters,Body) :-
51		ground(Name), % only for lookup of operations
52		get_texpr_id(Name,op(OperationName)),
53		(machine(M)
54		-> get_section(operation_bodies,M,Ops),
55		get_texpr_expr(Op,operation(TId,Results,Parameters,Body)),
56		get_texpr_id(TId,op(Name)),
57		member(Op,Ops)
58		; b_get_machine_operation(OperationName,Results,Parameters,Body)).
59
60		%! weakest_precondition(+Action, +Pred,-WP)
61		weakest_precondition(Action,Pred,WP) :-
62		get_texpr_expr(Action,Expr),
63		weakest_precondition2(Expr,Pred,WP).
64
65		% any statement. see schneider p. 126
66		weakest_precondition2(any(Parameters,PreCond,Body),Pred,WP) :- !,
67		weakest_precondition(Body,Pred,InnerWP),
68		safe_create_texpr(implication(PreCond,InnerWP),pred,UnquantifiedWP),
69		create_forall(Parameters,UnquantifiedWP,WP).
70		weakest_precondition2(assign(TIds,Exprs),Pred,WP) :- !,
71		function_assignment_to_overwrite(TIds,Exprs,TIds2,Exprs2),
72		get_texpr_ids(TIds2,StrippedIDs),
73		replace_ids_by_exprs(Pred,StrippedIDs,Exprs2,WP).
74		weakest_precondition2(assign_single_id(TId,Expr),Pred,WP) :- !,
75		function_assignment_to_overwrite([TId],[Expr],[TId2],[Expr2]),
76		get_texpr_id(TId2,Id),
77		replace_id_by_expr(Pred,Id,Expr2,WP).
78		% nondeterministic choice. see schneider p. 126
79		weakest_precondition2(becomes_element_of(IDs,Set),Pred,WP) :- !,
80		create_members(Set,IDs,MemberOf),
81		safe_create_texpr(implication(MemberOf,Pred),pred,InnerWP),
82		create_forall(IDs,InnerWP,WP).
83		% nondet choice of action. see schneider p. 129
84		weakest_precondition2(choice(Choices),Pred,WP) :- !,
85		choice_wps(Choices,Pred,WPs),
86		conjunct_predicates(WPs,WP).
87		weakest_precondition2(if(IfList),Pred,WP) :- !,
88		if_wp(IfList,Pred,WP).
89		% let statement: local variable with value. see schneider p. 125
90		weakest_precondition2(let(Parameters,Defs,Body),Pred,WP) :- !,
91		weakest_precondition(Body,Pred,InnerWP),
92		safe_create_texpr(implication(Defs,InnerWP),pred,UnquantifiedWP),
93		create_forall(Parameters,UnquantifiedWP,WP).
94		weakest_precondition2(operation_call(Operation,ResultsCall,ParametersCall),Pred,WP) :- !,
95		lookup_operation(Operation,ResultsOperation,ParametersOperation,Body),
96		% replace parameter/results identifiers
97		append([ResultsOperation,ParametersOperation],IDs), append([ResultsCall,ParametersCall],Replacements),
98		get_texpr_ids(IDs,StrippedIDs),
99		replace_ids_by_exprs(Body,StrippedIDs,Replacements,NewBody),
100		weakest_precondition(NewBody,Pred,WP).
101		weakest_precondition2(parallel(Actions),Pred,WP) :- !,
102		merge_parallels(Actions,Action),
103		weakest_precondition(Action,Pred,WP).
104		weakest_precondition2(precondition(Condition,Action),Pred,WP) :- !,
105		weakest_precondition(Action,Pred,InnerWP),
106		conjunct_predicates([Condition,InnerWP],WP).
107		% weakest precondition for event-b events
108		weakest_precondition2(rlevent(_Name,_Section,_Stat,Parameters,Guard,_Thm,Act,_VWit,_PWit,_Unmod,_AbsEvents),Pred,WP) :- !,
109		(is_list(Act)
110		-> create_texpr(parallel(Act),subst,[],NewAct)
111		; NewAct=Act
112		),
113		weakest_precondition2(any(Parameters,Guard,NewAct),Pred,WP).
114		% there are two kinds of selects: just whens and whens/else
115		% the else case just collects all guards and negates them
116		% see schneider p. 132
117		weakest_precondition2(select(Whens),Pred,WP) :- !,
118		select_whens_wps(Whens,Pred,WPs),
119		conjunct_predicates(WPs,WP).
120		weakest_precondition2(select(Whens,Else),Pred,WP) :- !,
121		select_whens_wps(Whens,Pred,WPs),
122		conjunct_predicates(WPs,WhensWP),
123		% collect all guards and negate them
124		% => precondition for else-case
125		findall(PC,(member(SW,Whens),get_texpr_expr(SW,select_when(PC,_))), AllPreconds),
126		maplist(create_negation,AllPreconds,NegAllPreconds),
127		conjunct_predicates(NegAllPreconds,ElsePrecond),
128		% imply [T_n]S
129		weakest_precondition(Else,Pred,InnerWP),
130		safe_create_texpr(implication(ElsePrecond,InnerWP),pred,ElseWP),
131		conjunct_predicates([WhensWP,ElseWP],WP).
132		weakest_precondition2(sequence(Actions),Pred,WP) :- !,
133		sequence_wp(Actions,Pred,WP).
134		weakest_precondition2(skip,Pred,WP) :- !,WP=Pred.
135		weakest_precondition2(var(IDs,Subst),Pred,WP) :- !,
136		weakest_precondition(Subst,Pred,InnerWP),
137		create_forall(IDs,InnerWP,WP).
138		weakest_precondition2(while(P,S,I,V),R,WP) :- !,
139		% [while P DO S INVARIANT I VARIANT V END] R
140		% see abrial, b-book, p. 395:
141		% there are five predicates. their conjunction is equal to the weakest precondition
142		% first, create the list of all variables modified by the Stmt (used in forall)
143		find_typed_identifier_uses(S,AllIdentifiersInStmt),
144		get_accessed_vars(S,[],ModifiedVarsInStmt,_Reads),
145		% the identifiers in ModifiedVarsInStmt are not typed. fetch the types from the list of all identifiers
146		% TypedModifiedVarsInStmt = X
147		get_texpr_ids(TypedModifiedVarsInStmt,ModifiedVarsInStmt),
148		subset(TypedModifiedVarsInStmt,AllIdentifiersInStmt),
149
150		ForAlls = TypedModifiedVarsInStmt,
151
152		% first obligation: the invariant
153		WP1 = I,
154
155		% second obligation: forall x in X: (I & P => [S]I)
156		conjunct_predicates([I,P],LHS2),
157		weakest_precondition(S,I,RHS2),
158		safe_create_texpr(implication(LHS2,RHS2),pred,Inner2),
159		create_forall(ForAlls,Inner2,WP2),
160
161		% third obligation: forall x in X: (I => v in N)
162		safe_create_texpr(member(V,b(integer_set('NATURAL'),set(integer),[])),pred,RHS3),
163		safe_create_texpr(implication(I,RHS3),pred,Inner3),
164		create_forall(ForAlls,Inner3,WP3),
165
166		% fourth obligation: forall x in X: I & P => [gamma:=V][S](V<gamma)
167		create_texpr(identifier('gamma\''),integer,[],Gamma),
168		create_texpr(assign_single_id(Gamma,V),subst,[],AssignVariantToGamma),
169		safe_create_texpr(less(V,Gamma),pred,VLessGamma),
170		weakest_precondition(S,VLessGamma,RHS4T),
171		weakest_precondition(AssignVariantToGamma,RHS4T,RHS4),
172		LHS4 = LHS2,
173		safe_create_texpr(implication(LHS4,RHS4),pred,Inner4),
174		create_forall(ForAlls,Inner4,WP4),
175
176		% fifth obligation: forall x in X: (I & not P) => R
177		create_negation(P,NotP), conjunct_predicates([I,NotP],LHS5),
178		safe_create_texpr(implication(LHS5,R),pred,Inner5),
179		create_forall(ForAlls,Inner5,WP5),
180
181		% conjunct them all together
182		conjunct_predicates([WP1,WP2,WP3,WP4,WP5],WP).
183		weakest_precondition2(Action,Pred,_WeakestPrecondition) :- !,
184		get_texpr_expr(Action,ActionExpr),
185		add_error_fail(weakest_precondition,'weakest-precondition implementation missing: ',[ActionExpr,Pred]).
186
187		choice_wps([],_Pred,[]).
188		choice_wps([Choice|Choices],Pred,[ChoiceWP|WPs]) :-
189		weakest_precondition(Choice,Pred,ChoiceWP),
190		choice_wps(Choices,Pred,WPs).
191
192		% see schneider p. 38
193		% [if E then S else T end] P = (E => [S]P) & (not E => [T]P)
194		if_wp([IF|IFs],Pred,WP) :-
195		get_texpr_expr(IF,if_elsif(Test,Body)),
196		% if-part
197		weakest_precondition(Body,Pred,InnerWP),
198		safe_create_texpr(implication(Test,InnerWP),pred,IfWP),
199		% if there are further else/elseif parts, create pos
200		(if_wp(IFs,Pred,SubWP)
201		-> create_negation(Test,NegTest),
202		safe_create_texpr(implication(NegTest,SubWP),pred,ElseWP),
203		conjunct_predicates([IfWP,ElseWP],WP)
204		; WP = IfWP).
205
206		merge_parallels(ParallelAssigns,Result) :-
207		create_texpr(truth,pred,[],True),
208		create_texpr(parallel([]),subst,[],Body),
209		EmptyAny = any([],True,Body),
210		EmptyAssign = assign([],[]),
211		merge_parallels1(ParallelAssigns,EmptyAssign,EmptyAny,Assigns,Anys,Rest),
212		(Rest == [] ->
213		merge_assigns_and_anys(Assigns,Anys,Res),
214		create_texpr(Res,subst,[],Result),
215		(debug_mode(on) -> print_subst(Result),nl; true)
216		;
217		add_error_fail(merge_parallels, 'merging of parallel executions failed (implementation missing?):', Rest)
218		).
219
220		merge_parallels1([],Assigns,Anys,Assigns,Anys,[]).
221		merge_parallels1([Subst|Substs],assign(IDs2,Exprs2),any(Par2,PreCond2,Body2),ResAssigns,ResAnys,Rest) :-
222		get_texpr_expr(Subst,Expr),
223		merge_parallels_normalize(Expr,ExprN),
224		(ExprN = assign(IDs1,Exprs1) ->
225		append(IDs2,IDs1,IDs3),
226		append(Exprs2,Exprs1,Exprs3),
227		NewAssign = assign(IDs3,Exprs3),
228		NewAny = any(Par2,PreCond2,Body2),
229		Rest = Rest1
230		; ExprN = any(Par1,PreCond1,Body1) ->
231		append(Par2,Par1,Par3),
232		conjunct_predicates([PreCond2,PreCond1],PreCond3),
233		get_texpr_expr(Body2,parallel(AnySubsts2)),
234		create_texpr(parallel([Body1|AnySubsts2]),subst,[],Body3),
235		NewAny = any(Par3,PreCond3,Body3),
236		NewAssign = assign(IDs2,Exprs2),
237		Rest = Rest1
238		; ExprN = skip ->
239		NewAssign = assign(IDs2,Exprs2),
240		NewAny = any(Par2,PreCond2,Body2),
241		Rest = Rest1
242		;
243		NewAssign = assign(IDs2,Exprs2),
244		NewAny = any(Par2,PreCond2,Body2),
245		Rest = [Subst|Rest1]
246		), !, % do not backtrack once the a substitution is merged to the assignment or any generator
247		merge_parallels1(Substs,NewAssign,NewAny,ResAssigns,ResAnys,Rest1).
248
249		merge_assigns_and_anys(Assign,Any,Result) :-
250		(empty_any_statement(Any),empty_assign_statement(Assign) ->
251		add_error_fail(merge_assigns_and_anys,'merging of parallel executions failed (empty assignment and any statements): ', (Assign,Any))
252		; empty_any_statement(Any) ->
253		Result = Assign
254		; empty_assign_statement(Assign) ->
255		Result = Any
256		;
257		Any = any(Par,PreCond,Body),
258		get_texpr_expr(Body,parallel(Actions)),
259		create_texpr(Assign,subst,[],BAssign),
260		create_texpr(parallel([BAssign|Actions]),subst,[],NewBody),
261		Result = any(Par,PreCond,NewBody)
262		).
263
264		empty_any_statement(any([],_Precond,b(parallel([]),subst,_))).
265
266		empty_assign_statement(assign([],[])).
267
268		% The old implementation for merging parallel assignments
269
270		%% merge_parallels([X],X) :- !.
271		%% merge_parallels([A1,A2|As],X) :-
272		%% merge_parallels2(A1,A2,AMerged), !,
273		%% merge_parallels([AMerged|As],X).
274		%% merge_parallels([A1,A2|As],X) :-
275		%% merge_parallels2(A2,A1,AMerged), !,
276		%% merge_parallels([AMerged|As],X).
277		%% merge_parallels([A1,A2|_As],_X) :-
278		%% get_texpr_expr(A1,A1E), get_texpr_expr(A2,A2E),
279		%% add_error_fail(merge_parallels,'merging of parallel executions failed (implementation missing?): ',(A1E,A2E)).
280
281		%% merge_parallels2(A1,A2,AMerged) :-
282		%% get_texpr_expr(A1,A1Expr), get_texpr_expr(A2,A2Expr),
283		%% merge_parallels_normalize(A1Expr,A1ExprN),
284		%% merge_parallels_normalize(A2Expr,A2ExprN),
285		%% merge_parallels3(A1ExprN,A2ExprN,AMergedExpr),
286		%% create_texpr(AMergedExpr,subst,[],AMerged).
287
288		%% merge_parallels3(assign(IDs1,Exprs1),assign(IDs2,Exprs2),assign(IDs3,Exprs3)) :-
289		%% append(IDs1,IDs2,IDs3), append(Exprs1,Exprs2,Exprs3).
290		%% merge_parallels3(any(Parameters,PreCond,Body),SomeSubstitution,any(Parameters,PreCond,NewBody)) :-
291		%% create_texpr(SomeSubstitution,subst,[],SomeSubstitutionTExpr),
292		%% create_texpr(parallel([Body,SomeSubstitutionTExpr]),subst,[],NewBody).
293		% in case we have more than two substitutions in a parallel block (see for example B/Ivo/WeakestPreconditon/Tickets/MergeParallels.mch WP: [Evt1](G(Evt2)))
294
295		merge_parallels_normalize(assign_single_id(ID,Expr),assign([ID],[Expr])) :- !.
296		merge_parallels_normalize(becomes_element_of(IDs,Set), any(Parameters,PreCond,Body)) :- !,
297		prime_identifiers(IDs,Parameters), create_members(Set,Parameters,PreCond),
298		create_texpr(assign(IDs,Parameters),subst,[],Body).
299		merge_parallels_normalize(becomes_such(Vars,Condition),any(PrimedIDs,Condition,Body)) :- !,
300		find_typed_identifier_uses(Condition,UsedIDs),
301		get_primed_ids(UsedIDs,PrimedIDs), % TO DO: check if we can reuse find_read_vars_for_becomes_such in b_read_write_info.pl
302		get_non_represented_vars(Vars,PrimedIDs,NonRepresented),
303		(NonRepresented\=[] ->
304		get_texpr_ids(NonRepresented,VarsIDs),
305		create_texpr(becomes_such(Vars,Condition),subst,[],TExpr),
306		translate_substitution(TExpr,Subst),
307		add_error_fail(merge_parallels_normalize,'Normalising becomes_such(...) costruct failed because the following variables were not reprsented by prime variables: ', (VarsIDs,Subst))
308		;
309		create_texpr(assign(Vars,PrimedIDs),subst,[],Body)
310		).
311		% Functional overrides in Event-B will be translated to assignments using the override operator (<+)
312		merge_parallels_normalize(X,X).
313
314		get_non_represented_vars([],_PrimedVars,[]).
315		get_non_represented_vars([Var|Vars],PrimedVars,NonRepresented) :-
316		prime_identifier(Var,VarPrimed),
317		remove_all_infos(VarPrimed,VarPrimedNoInfos),
318		(member(VarPrimedNoInfos,PrimedVars) ->
319		NonRepresented = NonRepresented1
320		;
321		NonRepresented = [Var|NonRepresented1]
322		),
323		get_non_represented_vars(Vars,PrimedVars,NonRepresented1).
324
325		get_primed_ids([],[]).
326		get_primed_ids([ID|IDs],[ID|Rest]) :-
327		get_texpr_id(ID,I),
328		is_primed_id(I),!,
329		get_primed_ids(IDs,Rest).
330		get_primed_ids([_ID|IDs],Rest) :-
331		get_primed_ids(IDs,Rest).
332
333		sequence_wp(Actions,Pred,WP) :-
334		reverse(Actions,ReversedActions),
335		sequence_wp2(ReversedActions,Pred,WP).
336		sequence_wp2([],Pred,Pred).
337		sequence_wp2([Action|Actions],PredIn,PredOut) :-
338		weakest_precondition(Action,PredIn,PredT),
339		sequence_wp2(Actions,PredT,PredOut).
340
341		select_whens_wps([],_Pred,[]).
342		select_whens_wps([When|Whens],Pred,[WP|WPs]) :-
343		get_texpr_expr(When,select_when(PreCond, Body)),
344		weakest_precondition(Body,Pred,InnerWP),
345		safe_create_texpr(implication(PreCond,InnerWP),pred,WP),
346		select_whens_wps(Whens,Pred,WPs).
347
348		create_members(Set,IDs,MemberOf) :-
349		maplist(create_member(Set),IDs,Preds),
350		conjunct_predicates(Preds,MemberOf).
351		create_member(Set,ID,Res) :-
352		safe_create_texpr(member(ID,Set),pred,Res).
353
354		%create_renaming(I1,I2,rename(I1,I2)).
355
356		function_assignment_to_overwrite([],[],[],[]).
357		function_assignment_to_overwrite([b(identifier(ID),Type,Infos)|IdOrFuns],[Expr|Exprs],[b(identifier(ID),Type,Infos)|IdOuts],[Expr|ExprOuts]) :-
358		function_assignment_to_overwrite(IdOrFuns,Exprs,IdOuts,ExprOuts).
359		function_assignment_to_overwrite([b(function(Function,Argument),_Type,_Infos)|IdOrFuns],[Expr|Exprs],[Function|IdOuts],[ExprOut|ExprOuts]) :-
360		get_texpr_type(Argument,ArgumentType), get_texpr_type(Expr,ExprType),
361		get_texpr_type(Function,FunctionType),
362		CoupleType = couple(ArgumentType,ExprType),
363		safe_create_texpr(couple(Argument,Expr),CoupleType,OverwriteCouple),
364		safe_create_texpr(set_extension([OverwriteCouple]),set(CoupleType),CoupleInSet),
365		safe_create_texpr(overwrite(Function,CoupleInSet),FunctionType,ExprOut),
366		function_assignment_to_overwrite(IdOrFuns,Exprs,IdOuts,ExprOuts).