Package: OpPostConditionContext

OpPostConditionContext

nameinstructionbranchcomplexitylinemethod
OpPostConditionContext(AExplicitFunctionDefinition, AApplyExp, SOperationDefinitionBase, IPogAssistantFactory, IPOContextStack)
M: 0 C: 37
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 8
100%
M: 0 C: 1
100%
OpPostConditionContext(AExplicitFunctionDefinition, ACallStm, SOperationDefinitionBase, IPogAssistantFactory, IPOContextStack)
M: 0 C: 37
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 8
100%
M: 0 C: 1
100%
buildInvExp(SOperationDefinitionBase, IPogAssistantFactory)
M: 13 C: 35
73%
M: 1 C: 5
83%
M: 1 C: 3
75%
M: 3 C: 9
75%
M: 0 C: 1
100%
getChangedVarsExp(AExplicitFunctionDefinition, SOperationDefinitionBase)
M: 4 C: 59
94%
M: 1 C: 9
90%
M: 1 C: 5
83%
M: 1 C: 13
93%
M: 0 C: 1
100%
getContext()
M: 2 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
getContextNode(PExp)
M: 5 C: 49
91%
M: 0 C: 6
100%
M: 0 C: 4
100%
M: 3 C: 10
77%
M: 0 C: 1
100%
getStateVars(SOperationDefinitionBase)
M: 4 C: 41
91%
M: 1 C: 7
88%
M: 1 C: 4
80%
M: 1 C: 10
91%
M: 0 C: 1
100%
introduceFreshVar(AInstanceVariableDefinition)
M: 0 C: 123
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 25
100%
M: 0 C: 1
100%
introduceFreshVars(LinkedList, List)
M: 16 C: 23
59%
M: 3 C: 3
50%
M: 2 C: 2
50%
M: 3 C: 5
63%
M: 0 C: 1
100%
refreshAllState(SOperationDefinitionBase, List)
M: 0 C: 22
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 5
100%
M: 0 C: 1
100%
rewritePost(PExp, List, IPogAssistantFactory)
M: 3 C: 29
91%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 2 C: 7
78%
M: 0 C: 1
100%
spellCondition(AExplicitFunctionDefinition, IPogAssistantFactory, List, PExp)
M: 2 C: 79
98%
M: 1 C: 7
88%
M: 1 C: 4
80%
M: 1 C: 15
94%
M: 0 C: 1
100%
toString()
M: 13 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%

Coverage

1: package org.overture.pog.contexts;
2:
3: import java.util.Collection;
4: import java.util.LinkedList;
5: import java.util.List;
6:
7: import org.overture.ast.analysis.AnalysisException;
8: import org.overture.ast.definitions.AExplicitFunctionDefinition;
9: import org.overture.ast.definitions.AExplicitOperationDefinition;
10: import org.overture.ast.definitions.AImplicitOperationDefinition;
11: import org.overture.ast.definitions.AInstanceVariableDefinition;
12: import org.overture.ast.definitions.PDefinition;
13: import org.overture.ast.definitions.SOperationDefinitionBase;
14: import org.overture.ast.expressions.AApplyExp;
15: import org.overture.ast.expressions.ABooleanConstExp;
16: import org.overture.ast.expressions.AForAllExp;
17: import org.overture.ast.expressions.APostOpExp;
18: import org.overture.ast.expressions.AVariableExp;
19: import org.overture.ast.expressions.PExp;
20: import org.overture.ast.factory.AstExpressionFactory;
21: import org.overture.ast.intf.lex.ILexNameToken;
22: import org.overture.ast.lex.LexBooleanToken;
23: import org.overture.ast.lex.VDMToken;
24: import org.overture.ast.patterns.AIdentifierPattern;
25: import org.overture.ast.patterns.ATypeMultipleBind;
26: import org.overture.ast.patterns.PMultipleBind;
27: import org.overture.ast.patterns.PPattern;
28: import org.overture.ast.statements.ACallStm;
29: import org.overture.ast.statements.AExternalClause;
30: import org.overture.pog.pub.IPOContext;
31: import org.overture.pog.pub.IPOContextStack;
32: import org.overture.pog.pub.IPogAssistantFactory;
33: import org.overture.pog.utility.Substitution;
34: import org.overture.pog.visitors.IVariableSubVisitor;
35:
36: public class OpPostConditionContext extends StatefulContext implements
37:                 IPOContext
38: {
39:
40:         AForAllExp forall_exp;
41:         PExp pred;
42:         IVariableSubVisitor visitor;
43:
44:         public OpPostConditionContext(AExplicitFunctionDefinition postDef,
45:                         ACallStm stm, SOperationDefinitionBase calledOp,
46:                         IPogAssistantFactory af, IPOContextStack ctxt)
47:         {
48:                 super(ctxt);
49:                 this.gen = ctxt.getGenerator();
50:                 this.subs = new LinkedList<Substitution>();
51:                 this.forall_exp = getChangedVarsExp(postDef, calledOp);
52:                 PExp inv = buildInvExp(calledOp, af);
53:                 this.pred = spellCondition(postDef, af, stm.getArgs(), inv);
54:                 this.visitor = af.getVarSubVisitor();
55:
56:         }
57:
58:         private PExp buildInvExp(SOperationDefinitionBase calledOp,
59:                         IPogAssistantFactory af)
60:         {
61:                 List<PExp> invariants = new LinkedList<PExp>();
62:•                if (calledOp.getClassDefinition() != null)
63:                 {
64:                         try
65:                         {
66:                                 invariants = calledOp.getClassDefinition().apply(af.getInvExpGetVisitor());
67:•                                if (invariants.size() > 0)
68:                                 {
69:
70:                                         PExp inv = invariants.get(0).clone();
71:
72:•                                        for (int i = 1; i < invariants.size(); i++)
73:                                         {
74:                                                 inv = AstExpressionFactory.newAAndBooleanBinaryExp(inv, invariants.get(i).clone());
75:
76:                                         }
77:                                         return inv;
78:                                 } else
79:                                 {
80:                                         return null;
81:                                 }
82:                         } catch (AnalysisException e)
83:                         {
84:                                 e.printStackTrace();
85:                         }
86:                 }
87:                 return null;
88:         }
89:
90:         public OpPostConditionContext(AExplicitFunctionDefinition postDef,
91:                         AApplyExp exp, SOperationDefinitionBase calledOp,
92:                         IPogAssistantFactory af, IPOContextStack ctxt)
93:         {
94:                 super(ctxt);
95:                 this.visitor = af.getVarSubVisitor();
96:                 this.gen = ctxt.getGenerator();
97:                 this.subs = new LinkedList<Substitution>();
98:                 this.forall_exp = getChangedVarsExp(postDef, calledOp);
99:                 PExp inv = buildInvExp(calledOp, af);
100:                 this.pred = spellCondition(postDef, af, exp.getArgs(), inv);
101:         }
102:
103:         @Override
104:         public String toString()
105:         {
106:                 return forall_exp.toString() + pred.toString();
107:         }
108:
109:         private AForAllExp getChangedVarsExp(AExplicitFunctionDefinition postDef,
110:                         SOperationDefinitionBase calledOp)
111:         {
112:                 AForAllExp r = new AForAllExp();
113:                 List<PMultipleBind> binds = new LinkedList<PMultipleBind>();
114:
115:•                if (calledOp instanceof AExplicitOperationDefinition)
116:                 {
117:                         refreshAllState(calledOp, binds);
118:                 }
119:
120:•                if (calledOp instanceof AImplicitOperationDefinition)
121:                 {
122:                         AImplicitOperationDefinition implicitOp = (AImplicitOperationDefinition) calledOp;
123:•                        if (implicitOp.getExternals().size() > 0)
124:                         {
125:•                                for (AExternalClause external : implicitOp.getExternals())
126:                                 {
127:•                                        if (external.getMode().getType().equals(VDMToken.WRITE))
128:                                         {
129:                                                 binds.addAll(introduceFreshVars(external.getIdentifiers(), getStateVars(calledOp)));
130:                                         }
131:                                 }
132:
133:                         } else
134:                         {
135:                                 refreshAllState(calledOp, binds);
136:                         }
137:                 }
138:
139:                 r.setBindList(binds);
140:                 return r;
141:         }
142:
143:         private List<AInstanceVariableDefinition> getStateVars(
144:                         SOperationDefinitionBase calledOp)
145:         {
146:                 List<PDefinition> defs;
147:•                if (calledOp.getClassDefinition() != null)
148:                 {
149:                         defs = calledOp.getClassDefinition().getDefinitions();
150:                 } else
151:                 {
152:•                        if (calledOp.getState() != null)
153:                         {
154:                                 defs = calledOp.getState().getStateDefs();
155:                         } else
156:                         {
157:                                 return new LinkedList<AInstanceVariableDefinition>();
158:                         }
159:                 }
160:                 List<AInstanceVariableDefinition> r = new LinkedList<AInstanceVariableDefinition>();
161:•                for (PDefinition p : defs)
162:                 {
163:•                        if (p instanceof AInstanceVariableDefinition)
164:                         {
165:                                 r.add((AInstanceVariableDefinition) p);
166:                         }
167:                 }
168:                 return r;
169:         }
170:
171:         private void refreshAllState(SOperationDefinitionBase calledOp,
172:                         List<PMultipleBind> binds)
173:         {
174:                 List<AInstanceVariableDefinition> defs = getStateVars(calledOp);
175:
176:•                for (AInstanceVariableDefinition p : defs)
177:                 {
178:                         binds.add(introduceFreshVar(p));
179:                 }
180:         }
181:
182:         private Collection<? extends PMultipleBind> introduceFreshVars(
183:                         LinkedList<ILexNameToken> identifiers,
184:                         List<AInstanceVariableDefinition> defs)
185:         {
186:                 List<PMultipleBind> r = new LinkedList<PMultipleBind>();
187:•                for (ILexNameToken ilt : identifiers)
188:                 {
189:•                        for (AInstanceVariableDefinition d : defs)
190:                         {
191:•                                if (ilt.equals(d.getName()))
192:                                 {
193:                                         r.add(introduceFreshVar(d));
194:                                 }
195:                         }
196:
197:                 }
198:                 return r;
199:         }
200:
201:         private PMultipleBind introduceFreshVar(AInstanceVariableDefinition var)
202:         {
203:                 ATypeMultipleBind r = new ATypeMultipleBind();
204:
205:                 List<PPattern> pats = new LinkedList<PPattern>();
206:                 AIdentifierPattern idPat = new AIdentifierPattern();
207:
208:                 idPat.setName(gen.getUnique(var.getName().getName()));
209:                 pats.add(idPat);
210:
211:                 r.setPlist(pats);
212:                 r.setType(var.getType().clone());
213:
214:                 AVariableExp newVar = new AVariableExp();
215:                 newVar.setName(idPat.getName().clone());
216:                 newVar.setOriginal(idPat.getName().getFullName());
217:
218:                 Substitution sub = new Substitution(var.getName().clone(), newVar);
219:                 subs.add(sub);
220:
221:                 AVariableExp old_var = last_vars.get(var.getName());
222:•                if (old_var != null)
223:                 {
224:                         Substitution sub_old = new Substitution(var.getOldname().toString(), old_var);
225:                         subs.add(sub_old);
226:                 } else
227:                 {
228:                         AVariableExp var_exp = new AVariableExp();
229:                         var_exp.setName(var.getName().clone());
230:                         var_exp.setType(var.getType().clone());
231:                         var_exp.setOriginal(var.getName().getName());
232:                         Substitution sub_old = new Substitution(var.getOldname().toString(), var_exp);
233:                         subs.add(sub_old);
234:                 }
235:
236:                 last_vars.put(var.getName(), newVar);
237:
238:                 return r;
239:         }
240:
241:         @Override
242:         public String getContext()
243:         {
244:                 return null;
245:         }
246:
247:         @Override
248:         public PExp getContextNode(PExp stitch)
249:         {
250:                 try
251:                 {
252:•                        if (first)
253:                         {
254:                                 first = false;
255:                         }
256:                         PExp implies_exp = AstExpressionFactory.newAImpliesBooleanBinaryExp(pred.clone(), stitch.clone());
257:
258:•                        for (Substitution sub : subs)
259:                         {
260:                                 implies_exp = implies_exp.clone().apply(visitor, sub);
261:                         }
262:
263:•                        if (forall_exp.getBindList().size() > 0)
264:                         {
265:
266:                                 forall_exp.setPredicate(implies_exp);
267:                                 return forall_exp.clone();
268:                         } else
269:                         {
270:                                 return implies_exp.clone();
271:                         }
272:                 } catch (AnalysisException e)
273:                 {
274:                         //consider handling of exceptions inside final context construction
275:                         e.printStackTrace();
276:                 }
277:                 return null;
278:         }
279:
280:         private PExp spellCondition(AExplicitFunctionDefinition def,
281:                         IPogAssistantFactory af, List<PExp> args, PExp invariant)
282:         {
283:                 PExp post_exp;
284:•                if (def == null)
285:                 {
286:•                        if (invariant == null)
287:                         {
288:                                 // no postcondition: true
289:                                 ABooleanConstExp r = new ABooleanConstExp();
290:                                 r.setValue(new LexBooleanToken(true, null));
291:                                 return r;
292:                         } else
293:                         {
294:                                 return invariant;
295:                         }
296:                 } else
297:                 {
298:                         post_exp = def.getBody();
299:                 }
300:
301:•                if (invariant != null)
302:                 {
303:                         post_exp = AstExpressionFactory.newAAndBooleanBinaryExp(post_exp, invariant);
304:                 }
305:
306:                 List<Substitution> subs = new LinkedList<Substitution>();
307:
308:•                for (int i = 0; i < args.size(); i++)
309:                 {
310:                         PPattern orig = def.getParamPatternList().get(0).get(i);
311:                         ILexNameToken origName = af.createPPatternAssistant(def.getLocation().getModule()).getAllVariableNames(orig).get(0).clone();
312:                         PExp new_exp = args.get(0).clone();
313:                         subs.add(new Substitution(origName, new_exp));
314:                 }
315:                 return rewritePost(post_exp, subs, af);
316:         }
317:
318:         private PExp rewritePost(PExp post_exp, List<Substitution> subs,
319:                         IPogAssistantFactory af)
320:         {
321:•                if (post_exp instanceof APostOpExp)
322:                 {
323:                         // post-expression bodies are wrapped in a PostOpExp for some reason...
324:                         post_exp = ((APostOpExp) post_exp).getPostexpression();
325:                 }
326:
327:•                for (Substitution sub : subs)
328:                 {
329:                         try
330:                         {
331:                                 post_exp = post_exp.clone().apply(af.getVarSubVisitor(), sub);
332:                         } catch (AnalysisException e)
333:                         {
334:
335:                                 e.printStackTrace();
336:                         }
337:                 }
338:
339:                 return post_exp;
340:         }
341:
342: }