Package: SatisfiabilityObligation

SatisfiabilityObligation

nameinstructionbranchcomplexitylinemethod
SatisfiabilityObligation(AClassInvariantDefinition, IPOContextStack, IPogAssistantFactory)
M: 0 C: 39
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 9
100%
M: 0 C: 1
100%
SatisfiabilityObligation(AImplicitFunctionDefinition, IPOContextStack, IPogAssistantFactory)
M: 5 C: 173
97%
M: 1 C: 9
90%
M: 1 C: 5
83%
M: 1 C: 32
97%
M: 0 C: 1
100%
SatisfiabilityObligation(AImplicitOperationDefinition, PDefinition, IPOContextStack, IPogAssistantFactory)
M: 0 C: 23
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 5
100%
M: 0 C: 1
100%
SatisfiabilityObligation(AStateDefinition, IPOContextStack, IPogAssistantFactory)
M: 0 C: 39
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 9
100%
M: 0 C: 1
100%
SatisfiabilityObligation(ATypeDefinition, IPOContextStack, IPogAssistantFactory)
M: 0 C: 65
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 15
100%
M: 0 C: 1
100%
buildPredicate(AImplicitOperationDefinition, PDefinition)
M: 5 C: 289
98%
M: 1 C: 19
95%
M: 1 C: 10
91%
M: 1 C: 58
98%
M: 0 C: 1
100%
getInvBinds(AStateDefinition)
M: 0 C: 34
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 5
100%
M: 0 C: 1
100%
stateInPost(List, List, PDefinition)
M: 0 C: 62
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 11
100%
M: 0 C: 1
100%
stateInPre(List, PDefinition)
M: 0 C: 32
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 7
100%
M: 0 C: 1
100%
stateInvBinds(AClassInvariantDefinition)
M: 0 C: 38
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 6
100%
M: 0 C: 1
100%
static {...}
M: 0 C: 29
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 4
100%
M: 0 C: 1
100%

Coverage

1: /*******************************************************************************
2: *
3: *        Copyright (C) 2008 Fujitsu Services Ltd.
4: *
5: *        Author: Nick Battle
6: *
7: *        This file is part of VDMJ.
8: *
9: *        VDMJ is free software: you can redistribute it and/or modify
10: *        it under the terms of the GNU General Public License as published by
11: *        the Free Software Foundation, either version 3 of the License, or
12: *        (at your option) any later version.
13: *
14: *        VDMJ is distributed in the hope that it will be useful,
15: *        but WITHOUT ANY WARRANTY; without even the implied warranty of
16: *        MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
17: *        GNU General Public License for more details.
18: *
19: *        You should have received a copy of the GNU General Public License
20: *        along with VDMJ. If not, see <http://www.gnu.org/licenses/>.
21: *
22: ******************************************************************************/
23:
24: package org.overture.pog.obligation;
25:
26: import java.util.LinkedList;
27: import java.util.List;
28: import java.util.Vector;
29:
30: import org.overture.ast.analysis.AnalysisException;
31: import org.overture.ast.definitions.AClassInvariantDefinition;
32: import org.overture.ast.definitions.AImplicitFunctionDefinition;
33: import org.overture.ast.definitions.AImplicitOperationDefinition;
34: import org.overture.ast.definitions.AInstanceVariableDefinition;
35: import org.overture.ast.definitions.AStateDefinition;
36: import org.overture.ast.definitions.ATypeDefinition;
37: import org.overture.ast.definitions.PDefinition;
38: import org.overture.ast.expressions.AApplyExp;
39: import org.overture.ast.expressions.AExistsExp;
40: import org.overture.ast.expressions.AImpliesBooleanBinaryExp;
41: import org.overture.ast.expressions.AVariableExp;
42: import org.overture.ast.expressions.PExp;
43: import org.overture.ast.factory.AstExpressionFactory;
44: import org.overture.ast.intf.lex.ILexNameToken;
45: import org.overture.ast.lex.LexNameToken;
46: import org.overture.ast.patterns.AIdentifierPattern;
47: import org.overture.ast.patterns.APatternListTypePair;
48: import org.overture.ast.patterns.ATypeMultipleBind;
49: import org.overture.ast.patterns.PMultipleBind;
50: import org.overture.ast.patterns.PPattern;
51: import org.overture.ast.types.ABooleanBasicType;
52: import org.overture.ast.types.AFieldField;
53: import org.overture.pog.pub.IPOContextStack;
54: import org.overture.pog.pub.IPogAssistantFactory;
55: import org.overture.pog.pub.POType;
56:
57: public class SatisfiabilityObligation extends ProofObligation
58: {
59:         private static final long serialVersionUID = -8922392508326253099L;
60:
61:         private static final ILexNameToken OLD_STATE_ARG = new LexNameToken("", "oldstate", null);
62:         private static final ILexNameToken OLD_SELF_ARG = new LexNameToken("", "oldself", null);
63:         private static final ILexNameToken NEW_STATE_ARG = new LexNameToken("", "newstate", null);
64:         private static final ILexNameToken NEW_SELF_ARG = new LexNameToken("", "newself", null);
65:
66:         public SatisfiabilityObligation(AImplicitFunctionDefinition func,
67:                         IPOContextStack ctxt, IPogAssistantFactory af)
68:                         throws AnalysisException
69:         {
70:                 super(func, POType.FUNC_SATISFIABILITY, ctxt, func.getLocation(), af);
71:
72:                 /**
73:                  * f: A * B -> R [pre ...] post ... [pre_f(a, b) =>] exists r:R & post_f(a, b, r)
74:                  */
75:
76:                 List<PExp> arglist = new Vector<PExp>();
77:
78:•                for (APatternListTypePair pltp : func.getParamPatterns())
79:                 {
80:•                        for (PPattern pattern : pltp.getPatterns())
81:                         {
82:                                 arglist.add(patternToExp(pattern));
83:                         }
84:                 }
85:
86:                 AApplyExp preApply = null;
87:
88:•                if (func.getPredef() != null)
89:                 {
90:                         preApply = getApplyExp(getVarExp(func.getPredef().getName().clone(), func.getPredef().clone()), arglist);
91:                         preApply.setType(new ABooleanBasicType());
92:                         preApply.getRoot().setType(func.getPredef().getType().clone());
93:                 }
94:
95:                 AExistsExp existsExp = new AExistsExp();
96:                 existsExp.setType(new ABooleanBasicType());
97:                 List<PExp> postArglist = new Vector<PExp>(arglist);
98:
99:•                if (func.getResult().getPattern() instanceof AIdentifierPattern)
100:                 {
101:                         AIdentifierPattern ip = (AIdentifierPattern) func.getResult().getPattern().clone();
102:                         postArglist.add(patternToExp(func.getResult().getPattern()));
103:                         existsExp.setBindList(getMultipleTypeBindList(func.getResult().getType().clone(), ip.getName()));
104:                 } else
105:                 {
106:                         throw new RuntimeException("Expecting identifier pattern in function result");
107:                 }
108:
109:                 AApplyExp postApply = getApplyExp(getVarExp(func.getPostdef().getName(), func.getPostdef()), postArglist);
110:                 postApply.setType(new ABooleanBasicType());
111:                 postApply.getRoot().setType(func.getPostdef().getType().clone());
112:                 existsExp.setPredicate(postApply);
113:
114:•                if (preApply != null)
115:                 {
116:                         AImpliesBooleanBinaryExp implies = AstExpressionFactory.newAImpliesBooleanBinaryExp(preApply, existsExp);
117:                         stitch = implies;
118:                         valuetree.setPredicate(ctxt.getPredWithContext(implies));
119:                 } else
120:                 {
121:                         stitch = existsExp;
122:                         valuetree.setPredicate(ctxt.getPredWithContext(existsExp));
123:                 }
124:
125:                 // valuetree.setContext(ctxt.getContextNodeList());
126:         }
127:
128:         public SatisfiabilityObligation(AImplicitOperationDefinition op,
129:                         PDefinition stateDefinition, IPOContextStack ctxt,
130:                         IPogAssistantFactory af) throws AnalysisException
131:         {
132:                 super(op, POType.OP_SATISFIABILITY, ctxt, op.getLocation(), af);
133:
134:                 /**
135:                  * op: A * B ==> R [pre ...] post ... [pre_op(a, b, state) =>] exists r:R, state:Sigma & post_op(a, b, r,
136:                  * state~, state) The state argument is either a Sigma(SL) or self(PP).
137:                  */
138:
139:                 PExp predExp = buildPredicate(op, stateDefinition);
140:
141:                 stitch = predExp;
142:                 valuetree.setPredicate(ctxt.getPredWithContext(predExp));
143:
144:         }
145:
146:         public SatisfiabilityObligation(ATypeDefinition node, IPOContextStack ctxt,
147:                         IPogAssistantFactory af) throws AnalysisException
148:         {
149:                 super(node, POType.TYPE_INV_SAT, ctxt, node.getLocation(), af);
150:
151:                 AExistsExp exists_exp = new AExistsExp();
152:                 exists_exp.setType(new ABooleanBasicType());
153:
154:                 ATypeMultipleBind tmb = new ATypeMultipleBind();
155:                 List<PPattern> pats = new LinkedList<PPattern>();
156:                 pats.add(node.getInvPattern().clone());
157:                 tmb.setPlist(pats);
158:                 tmb.setType(node.getInvType().clone());
159:                 List<PMultipleBind> binds = new LinkedList<PMultipleBind>();
160:                 binds.add(tmb);
161:
162:                 exists_exp.setBindList(binds);
163:                 exists_exp.setPredicate(node.getInvExpression().clone());
164:
165:                 stitch = exists_exp;
166:                 valuetree.setPredicate(ctxt.getPredWithContext(exists_exp));
167:         }
168:
169:         public SatisfiabilityObligation(AStateDefinition node,
170:                         IPOContextStack ctxt, IPogAssistantFactory af)
171:                         throws AnalysisException
172:         {
173:                 super(node, POType.STATE_INV_SAT, ctxt, node.getLocation(), af);
174:
175:                 AExistsExp exists_exp = new AExistsExp();
176:                 exists_exp.setType(new ABooleanBasicType());
177:                 List<PMultipleBind> binds = getInvBinds(node);
178:
179:                 exists_exp.setBindList(binds);
180:                 exists_exp.setPredicate(node.getInvExpression().clone());
181:
182:                 stitch = exists_exp;
183:                 valuetree.setPredicate(ctxt.getPredWithContext(exists_exp));
184:         }
185:
186:         private List<PMultipleBind> getInvBinds(AStateDefinition node)
187:         {
188:                 List<PMultipleBind> r = new Vector<PMultipleBind>();
189:
190:•                for (AFieldField f : node.getFields())
191:                 {
192:                         r.add(getMultipleTypeBind(f.getType().clone(), f.getTagname().clone()));
193:                 }
194:
195:                 return r;
196:         }
197:
198:         public SatisfiabilityObligation(AClassInvariantDefinition node,
199:                         IPOContextStack ctxt, IPogAssistantFactory af)
200:                         throws AnalysisException
201:         {
202:                 super(node, POType.STATE_INV_SAT, ctxt, node.getLocation(), af);
203:
204:                 AExistsExp exists_exp = new AExistsExp();
205:                 exists_exp.setType(new ABooleanBasicType());
206:                 List<PMultipleBind> binds = stateInvBinds(node);
207:
208:                 exists_exp.setBindList(binds);
209:                 exists_exp.setPredicate(node.getExpression().clone());
210:
211:                 stitch = exists_exp;
212:                 valuetree.setPredicate(ctxt.getPredWithContext(exists_exp));
213:         }
214:
215:         protected List<PMultipleBind> stateInvBinds(AClassInvariantDefinition node)
216:         {
217:                 List<PMultipleBind> binds = new LinkedList<PMultipleBind>();
218:
219:•                for (PDefinition p : node.getClassDefinition().getDefinitions())
220:                 {
221:•                        if (p instanceof AInstanceVariableDefinition)
222:                         {
223:                                 binds.add(getMultipleTypeBind(p.getType().clone(), p.getName().clone()));
224:                         }
225:                 }
226:
227:                 return binds;
228:         }
229:
230:         PExp buildPredicate(AImplicitOperationDefinition op,
231:                         PDefinition stateDefinition) throws AnalysisException
232:         {
233:                 List<PExp> arglist = new Vector<PExp>();
234:
235:•                for (APatternListTypePair pltp : op.getParameterPatterns())
236:                 {
237:•                        for (PPattern pattern : pltp.getPatterns())
238:                         {
239:                                 arglist.add(patternToExp(pattern.clone()));
240:                         }
241:                 }
242:
243:•                if (stateDefinition != null)
244:                 {
245:                         stateInPre(arglist, stateDefinition);
246:                 }
247:                 AApplyExp preApply = null;
248:
249:•                if (op.getPredef() != null)
250:                 {
251:                         preApply = getApplyExp(getVarExp(op.getPredef().getName().clone(), op.getPredef()), arglist);
252:                         preApply.getRoot().setType(op.getPredef().getType().clone());
253:                         preApply.setType(new ABooleanBasicType());
254:                 }
255:
256:                 PExp mainExp;
257:
258:                 // Operation Has a Result. Add it in the post condition.
259:•                if (op.getResult() != null)
260:                 {
261:
262:                         AExistsExp existsExp = new AExistsExp();
263:                         existsExp.setType(new ABooleanBasicType());
264:                         List<PExp> postArglist = new Vector<PExp>(arglist);
265:
266:•                        if (op.getResult().getPattern() instanceof AIdentifierPattern)
267:                         {
268:                                 AIdentifierPattern ip = (AIdentifierPattern) op.getResult().getPattern();
269:                                 postArglist.add(patternToExp(op.getResult().getPattern().clone()));
270:
271:•                                if (stateDefinition != null)
272:                                 {
273:
274:•                                        if (stateDefinition instanceof AStateDefinition)
275:                                         {
276:                                                 AVariableExp varExp = getVarExp(OLD_STATE_ARG,stateDefinition.clone());
277:                                                 varExp.setType(((AStateDefinition) stateDefinition).getRecordType().clone());
278:                                                 postArglist.add(varExp);
279:                                                 AVariableExp varExp2 = getVarExp(NEW_STATE_ARG,stateDefinition.clone());
280:                                                 varExp2.setType(((AStateDefinition) stateDefinition).getRecordType().clone());
281:                                                 postArglist.add(varExp2);
282:                                         } else
283:                                         {
284:                                                 AVariableExp varExp = getVarExp(OLD_SELF_ARG,stateDefinition.clone());
285:                                                 postArglist.add(varExp);
286:                                                 varExp.setType(stateDefinition.getType().clone());
287:                                                 AVariableExp varExp2 = getVarExp(NEW_SELF_ARG,stateDefinition.clone());
288:                                                 postArglist.add(varExp2);
289:                                                 varExp2.setType(stateDefinition.getType().clone());
290:                                         }
291:                                 }
292:
293:                                 existsExp.setBindList(getMultipleTypeBindList(op.getResult().getType().clone(), ip.getName().clone()));
294:                         } else
295:                         {
296:                                 throw new RuntimeException("Expecting single identifier pattern in operation result");
297:                         }
298:
299:                         AApplyExp postApply = getApplyExp(getVarExp(op.getPostdef().getName(),op.getPostdef().clone()), postArglist);
300:                         postApply.getRoot().setType(op.getPostdef().getType().clone());
301:                         postApply.setType(new ABooleanBasicType());
302:                         existsExp.setPredicate(postApply);
303:                         mainExp = existsExp;
304:                 }
305:
306:                 // No Result. Just add new state to post condition
307:                 else
308:                 {
309:
310:                         AExistsExp exists_exp = new AExistsExp();
311:                         exists_exp.setType(new ABooleanBasicType());
312:                         List<PExp> postArglist = new Vector<PExp>(arglist);
313:
314:                         List<PMultipleBind> exists_binds = new LinkedList<PMultipleBind>();
315:•                        if (stateDefinition != null)
316:                         {
317:                                 stateInPost(exists_binds, postArglist, stateDefinition);
318:                         }
319:                         exists_exp.setBindList(exists_binds);
320:                         AApplyExp postApply = getApplyExp(getVarExp(op.getPostdef().getName(),op.getPostdef().clone()), new Vector<PExp>(postArglist));
321:                         postApply.setType(new ABooleanBasicType());
322:                         postApply.getRoot().setType(op.getPostdef().getType().clone());
323:                         exists_exp.setPredicate(postApply);
324:                         mainExp = exists_exp;
325:                 }
326:
327:•                if (preApply != null)
328:                 {
329:                         return AstExpressionFactory.newAImpliesBooleanBinaryExp(preApply, mainExp);
330:                 } else
331:                 {
332:                         return mainExp;
333:                 }
334:         }
335:
336:         protected void stateInPre(List<PExp> args, PDefinition stateDefinition)
337:         {
338:
339:                 AVariableExp varExp;
340:•                if (stateDefinition instanceof AStateDefinition)
341:                 {
342:                         varExp = getVarExp(OLD_STATE_ARG,stateDefinition.clone());
343:                         varExp.setType(((AStateDefinition) stateDefinition).getRecordType().clone());
344:                 } else
345:                 {
346:                         varExp = getVarExp(OLD_SELF_ARG,stateDefinition.clone());
347:                         varExp.setType(stateDefinition.getType().clone());
348:                 }
349:                 args.add(varExp);
350:
351:         }
352:
353:         protected void stateInPost(List<PMultipleBind> exists_binds,
354:                         List<PExp> postArglist, PDefinition stateDefinition)
355:         {
356:
357:                 AVariableExp varExp;
358:                 // replace with super call
359:•                if (stateDefinition instanceof AStateDefinition)
360:                 {
361:                         varExp = getVarExp(NEW_STATE_ARG,stateDefinition.clone());
362:                         AStateDefinition aStateDefinition = (AStateDefinition) stateDefinition;
363:                         varExp.setType(aStateDefinition.getRecordType().clone());
364:                         exists_binds.addAll(getMultipleTypeBindList(aStateDefinition.getRecordType().clone(), NEW_STATE_ARG));
365:                 } else
366:                 {
367:                         varExp = getVarExp(NEW_SELF_ARG,stateDefinition.clone());
368:                         varExp.setType(stateDefinition.getType().clone());
369:                         exists_binds.addAll(getMultipleTypeBindList(stateDefinition.getType().clone(), NEW_SELF_ARG));
370:                 }
371:                 postArglist.add(varExp);
372:         }
373:
374: }