Package: ProofObligation

ProofObligation

nameinstructionbranchcomplexitylinemethod
ProofObligation(INode, POType, IPOContextStack, ILexLocation, IPogAssistantFactory)
M: 0 C: 41
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 11
100%
M: 0 C: 1
100%
cloneListMultipleBind(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%
cloneListPExp(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%
cloneListType(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%
compareTo(IProofObligation)
M: 6 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
getApplyExp(PExp, List)
M: 0 C: 33
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 8
100%
M: 0 C: 1
100%
getApplyExp(PExp, PExp[])
M: 0 C: 6
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
getApplyExp(PExp, PType, PExp[])
M: 0 C: 11
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
getDefPredString()
M: 11 C: 0
0%
M: 2 C: 0
0%
M: 2 C: 0
0%
M: 4 C: 0
0%
M: 1 C: 0
0%
getEqualsExp(PExp, PExp)
M: 0 C: 6
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
getFullPredString()
M: 2 C: 11
85%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 1 C: 3
75%
M: 0 C: 1
100%
getIntLiteral(long)
M: 0 C: 15
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 4
100%
M: 0 C: 1
100%
getIsaName()
M: 0 C: 43
100%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 0 C: 6
100%
M: 0 C: 1
100%
getKind()
M: 3 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
getKindString()
M: 0 C: 4
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
getLocale()
M: 3 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
getLocation()
M: 0 C: 3
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
getMultipleSetBind(PExp, ILexNameToken[])
M: 0 C: 45
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 9
100%
M: 0 C: 1
100%
getMultipleSetBindList(PExp, ILexNameToken[])
M: 0 C: 13
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
getMultipleTypeBind(PType, ILexNameToken[])
M: 0 C: 45
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 9
100%
M: 0 C: 1
100%
getMultipleTypeBindList(PType, ILexNameToken[])
M: 0 C: 13
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
getName()
M: 3 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
getNode()
M: 3 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
getNumber()
M: 0 C: 3
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
getStatus()
M: 3 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
getUnique(String)
M: 0 C: 5
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
getUniqueGenerator()
M: 0 C: 3
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
getUniqueName()
M: 11 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
getValueTree()
M: 0 C: 3
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
getVarExp(ILexNameToken)
M: 0 C: 14
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 4
100%
M: 0 C: 1
100%
getVarExp(ILexNameToken, PDefinition)
M: 0 C: 18
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 5
100%
M: 0 C: 1
100%
getVarExp(ILexNameToken, PDefinition, PType)
M: 0 C: 10
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
getVarExp(ILexNameToken, PType)
M: 0 C: 10
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
makeAnd(PExp, PExp)
M: 0 C: 30
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 8
100%
M: 0 C: 1
100%
makeOr(PExp, PExp)
M: 0 C: 30
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 8
100%
M: 0 C: 1
100%
makeRelContext(ATypeDefinition, AVariableExp[])
M: 0 C: 61
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 12
100%
M: 0 C: 1
100%
patternToExp(PPattern)
M: 0 C: 13
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
setLocale(String)
M: 4 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 2 C: 0
0%
M: 1 C: 0
0%
setNumber(int)
M: 0 C: 4
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
setStatus(POStatus)
M: 4 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 2 C: 0
0%
M: 1 C: 0
0%
toString()
M: 0 C: 23
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
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.io.Serializable;
27: import java.util.Arrays;
28: import java.util.LinkedList;
29: import java.util.List;
30: import java.util.Vector;
31:
32: import org.overture.ast.analysis.AnalysisException;
33: import org.overture.ast.definitions.ATypeDefinition;
34: import org.overture.ast.definitions.PDefinition;
35: import org.overture.ast.expressions.*;
36: import org.overture.ast.factory.AstExpressionFactory;
37: import org.overture.ast.factory.AstFactory;
38: import org.overture.ast.intf.lex.ILexIntegerToken;
39: import org.overture.ast.intf.lex.ILexLocation;
40: import org.overture.ast.intf.lex.ILexNameToken;
41: import org.overture.ast.lex.LexIntegerToken;
42: import org.overture.ast.lex.LexKeywordToken;
43: import org.overture.ast.lex.VDMToken;
44: import org.overture.ast.node.INode;
45: import org.overture.ast.patterns.AIdentifierPattern;
46: import org.overture.ast.patterns.ASetMultipleBind;
47: import org.overture.ast.patterns.ATypeMultipleBind;
48: import org.overture.ast.patterns.PMultipleBind;
49: import org.overture.ast.patterns.PPattern;
50: import org.overture.ast.types.ABooleanBasicType;
51: import org.overture.ast.types.PType;
52: import org.overture.pof.AVdmPoTree;
53: import org.overture.pog.pub.IPOContextStack;
54: import org.overture.pog.pub.IPogAssistantFactory;
55: import org.overture.pog.pub.IProofObligation;
56: import org.overture.pog.pub.POStatus;
57: import org.overture.pog.pub.POType;
58: import org.overture.pog.utility.UniqueNameGenerator;
59: import org.overture.pog.visitors.PatternToExpVisitor;
60:
61: /**
62: * New class for Proof Obligations with a an AST-based representation of PO expressions
63: *
64: * @author ldc
65: */
66:
67: abstract public class ProofObligation implements IProofObligation, Serializable
68: {
69:         private static final long serialVersionUID = 1L;
70:
71:         public final INode rootNode;
72:         public final String name;
73:         public String isaName;
74:
75:         public AVdmPoTree valuetree;
76:         public PExp stitch;
77:         public POStatus status;
78:
79:         public final POType kind;
80:         public int number;
81:         private final UniqueNameGenerator generator;
82:         private ILexLocation location;
83:         private String locale;
84:         private final IPogAssistantFactory af;
85:
86:         public ProofObligation(INode rootnode, POType kind,
87:                         IPOContextStack context, ILexLocation location,
88:                         IPogAssistantFactory af) throws AnalysisException
89:         {
90:                 this.locale = rootnode.apply(af.getLocaleExtractVisitor());
91:                 this.rootNode = rootnode;
92:                 this.location = location;
93:                 this.kind = kind;
94:                 this.af = af;
95:                 this.name = context.getName();
96:                 this.status = POStatus.UNPROVED;
97:                 this.valuetree = new AVdmPoTree();
98:                 this.generator = new UniqueNameGenerator(rootNode);
99:         }
100:
101:         @Override
102:         public String getLocale()
103:         {
104:                 return locale;
105:         }
106:
107:         public void setLocale(String locale)
108:         {
109:                 this.locale = locale;
110:         }
111:
112:         public UniqueNameGenerator getUniqueGenerator()
113:         {
114:                 return generator;
115:         }
116:
117:         public AVdmPoTree getValueTree()
118:         {
119:                 return valuetree;
120:         }
121:
122:         // this method should call a visitor on the potree that creates the "value"
123:         // string as it exists in the current version
124:         @Override
125:         public String getFullPredString()
126:         {
127:•                if (valuetree.getPredicate() == null)
128:                 {
129:                         return "";
130:                 }
131:                 String result = valuetree.getPredicate().toString();
132:                 return result;
133:         }
134:
135:         @Override
136:         public String getDefPredString()
137:         {
138:•                if (stitch == null)
139:                 {
140:                         return "";
141:                 }
142:                 String result = stitch.toString();
143:                 return result;
144:         }
145:
146:         @Override
147:         public void setStatus(POStatus status)
148:         {
149:                 this.status = status;
150:
151:         }
152:
153:         @Override
154:         public String toString()
155:         {
156:                 return name + ": " + kind + " obligation " + location + "\n"
157:                                 + getFullPredString();
158:         }
159:
160:         public String getIsaName()
161:         {
162:•                if (isaName == null)
163:                 {
164:                         isaName = "PO" + name;
165:                         isaName = isaName.replaceAll(", ", "_");
166:                         isaName = isaName.replaceAll("\\(.*\\)|\\$", "");
167:                         isaName = isaName + getNumber();
168:                 }
169:                 return isaName;
170:         }
171:
172:         @Override
173:         public String getUniqueName()
174:         {
175:                 return getName() + getNumber();
176:         }
177:
178:         @Override
179:         public INode getNode()
180:         {
181:                 return rootNode;
182:         }
183:
184:         // I'm not sure why the comparable is implemented...
185:         public int compareTo(IProofObligation other)
186:         {
187:                 return number - other.getNumber();
188:         }
189:
190:         @Override
191:         public POType getKind()
192:         {
193:                 return kind;
194:         }
195:
196:         @Override
197:         public String getName()
198:         {
199:                 return name;
200:         }
201:
202:         @Override
203:         public String getKindString()
204:         {
205:                 return kind.toString();
206:         }
207:
208:         @Override
209:         public POStatus getStatus()
210:         {
211:                 return status;
212:         }
213:
214:         @Override
215:         public void setNumber(int i)
216:         {
217:                 number = i;
218:
219:         }
220:
221:         @Override
222:         public int getNumber()
223:         {
224:                 return number;
225:         }
226:
227:         @Override
228:         public ILexLocation getLocation()
229:         {
230:                 return location;
231:         }
232:
233:         /**
234:          * Create the context (forall x,y,z...) for a Proof Obligation for
235:          * eq and ord relations.
236:          */
237:         protected AForAllExp makeRelContext(ATypeDefinition node, AVariableExp... exps){
238:
239:                 AForAllExp forall_exp = new AForAllExp();
240:                 forall_exp.setType(new ABooleanBasicType());
241:
242:                 ATypeMultipleBind tmb = new ATypeMultipleBind();
243:                 List<PPattern> pats = new LinkedList<>();
244:•                for (AVariableExp exp : exps)
245:                 {
246:                         pats.add(AstFactory.newAIdentifierPattern(exp.getName().clone()));
247:                 }
248:                 tmb.setPlist(pats);
249:                 tmb.setType(node.getType().clone());
250:                 List<PMultipleBind> binds = new LinkedList<>();
251:                 binds.add(tmb);
252:                 forall_exp.setBindList(binds);
253:                 return forall_exp;
254:         }
255:
256:         /**
257:          * Create a multiple type bind with a varargs list of pattern variables, like a,b,c:T. This is used by several
258:          * obligations.
259:          */
260:         protected PMultipleBind getMultipleTypeBind(PType patternType,
261:                         ILexNameToken... patternNames)
262:         {
263:                 ATypeMultipleBind typeBind = new ATypeMultipleBind();
264:                 List<PPattern> patternList = new Vector<PPattern>();
265:
266:•                for (ILexNameToken patternName : patternNames)
267:                 {
268:                         AIdentifierPattern pattern = new AIdentifierPattern();
269:                         pattern.setName(patternName.clone());
270:                         patternList.add(pattern);
271:                 }
272:
273:                 typeBind.setPlist(patternList);
274:                 typeBind.setType(patternType.clone());
275:
276:                 return typeBind;
277:         }
278:
279:         /**
280:          * Create a multiple set bind with a varargs list of pattern variables, like a,b,c in set S. This is used by several
281:          * obligations.
282:          */
283:         protected PMultipleBind getMultipleSetBind(PExp setExp,
284:                         ILexNameToken... patternNames)
285:         {
286:                 ASetMultipleBind setBind = new ASetMultipleBind();
287:                 List<PPattern> patternList = new Vector<PPattern>();
288:
289:•                for (ILexNameToken patternName : patternNames)
290:                 {
291:                         AIdentifierPattern pattern = new AIdentifierPattern();
292:                         pattern.setName(patternName.clone());
293:                         patternList.add(pattern);
294:                 }
295:
296:                 setBind.setPlist(patternList);
297:                 setBind.setSet(setExp.clone());
298:
299:                 return setBind;
300:         }
301:
302:         /**
303:          * As above, but create a List of PMultipleBind with one element, for convenience.
304:          */
305:         protected List<PMultipleBind> getMultipleTypeBindList(PType patternType,
306:                         ILexNameToken... patternNames)
307:         {
308:                 List<PMultipleBind> typeBindList = new Vector<PMultipleBind>();
309:                 typeBindList.add(getMultipleTypeBind(patternType, patternNames));
310:                 return typeBindList;
311:         }
312:
313:         /**
314:          * As above, but create a List of PMultipleBind with one element, for convenience.
315:          */
316:         protected List<PMultipleBind> getMultipleSetBindList(PExp setExp,
317:                         ILexNameToken... patternNames)
318:         {
319:                 List<PMultipleBind> setBindList = new Vector<PMultipleBind>();
320:                 setBindList.add(getMultipleSetBind(setExp, patternNames));
321:                 return setBindList;
322:         }
323:
324:         /**
325:          * Create a LexNameToken with a numbered variable name, based on the stem passed. (See getVar above).
326:          */
327:         protected ILexNameToken getUnique(String name)
328:         {
329:                 return generator.getUnique(name);
330:         }
331:
332:         /**
333:          * Generate an AEqualsBinaryExp
334:          */
335:         protected AEqualsBinaryExp getEqualsExp(PExp left, PExp right)
336:         {
337:                 return AstExpressionFactory.newAEqualsBinaryExp(left.clone(), right.clone());
338:         }
339:
340:         /**
341:          * Generate an AVariableExp
342:          */
343:         protected AVariableExp getVarExp(ILexNameToken name)
344:         {
345:                 AVariableExp var = new AVariableExp();
346:                 var.setName(name.clone());
347:                 var.setOriginal(name.getFullName());
348:                 return var;
349:         }
350:
351:         /**
352:          * Generate a Var Exp with associated type.
353:          */
354:         protected AVariableExp getVarExp(ILexNameToken name, PType type)
355:         {
356:                 AVariableExp var = getVarExp(name);
357:                 var.setType(type.clone());
358:                 return var;
359:         }
360:
361:         /**
362:          * Generate AVariableExp with corresponding definition
363:          */
364:         protected AVariableExp getVarExp(ILexNameToken name, PDefinition vardef)
365:         {
366:                 AVariableExp var = new AVariableExp();
367:                 var.setName(name.clone());
368:                 var.setOriginal(name.getFullName());
369:                 var.setVardef(vardef.clone());
370:                 return var;
371:         }
372:         /**
373:          * Generate Var Exp with everything!
374:          * @return
375:          */
376:         protected AVariableExp getVarExp(ILexNameToken name, PDefinition vardef, PType type){
377:                 AVariableExp var = getVarExp(name, vardef);
378:                 var.setType(type);
379:                 return var;
380:         }
381:
382:         protected AApplyExp getApplyExp(PExp root, PType type, PExp... arglist)
383:         {
384:                 AApplyExp exp = getApplyExp(root, arglist);
385:                 exp.setType(type.clone());
386:                 return exp;
387:         }
388:
389:         /**
390:          * Generate an AApplyExp with varargs arguments
391:          */
392:         protected AApplyExp getApplyExp(PExp root, PExp... arglist)
393:         {
394:                 return getApplyExp(root, Arrays.asList(arglist));
395:         }
396:
397:         /**
398:          * Generate an AApplyExp
399:          */
400:         protected AApplyExp getApplyExp(PExp root, List<PExp> arglist)
401:         {
402:                 AApplyExp apply = new AApplyExp();
403:                 apply.setRoot(root.clone());
404:                 List<PExp> args = new Vector<PExp>();
405:
406:•                for (PExp arg : arglist)
407:                 {
408:                         args.add(arg.clone());
409:                 }
410:
411:                 apply.setArgs(args);
412:                 return apply;
413:         }
414:
415:         /**
416:          * Generate an AIntLiteral from a long.
417:          */
418:         protected AIntLiteralExp getIntLiteral(long i)
419:         {
420:                 AIntLiteralExp number = new AIntLiteralExp();
421:                 ILexIntegerToken literal = new LexIntegerToken(i, null);
422:                 number.setValue(literal);
423:                 return number;
424:         }
425:
426:         /**
427:          * Chain an AND expression onto a root, or just return the new expression if the root is null. Called in a loop,
428:          * this left-associates an AND tree.
429:          */
430:         protected PExp makeAnd(PExp root, PExp e)
431:         {
432:•                if (root != null)
433:                 {
434:                         AAndBooleanBinaryExp a = new AAndBooleanBinaryExp();
435:                         a.setLeft(root.clone());
436:                         a.setOp(new LexKeywordToken(VDMToken.AND, null));
437:                         a.setType(new ABooleanBasicType());
438:                         a.setRight(e.clone());
439:                         return a;
440:                 } else
441:                 {
442:                         return e;
443:                 }
444:         }
445:
446:         /**
447:          * Chain an OR expression onto a root, or just return the new expression if the root is null. Called in a loop, this
448:          * left-associates an OR tree.
449:          */
450:         protected PExp makeOr(PExp root, PExp e)
451:         {
452:•                if (root != null)
453:                 {
454:                         AOrBooleanBinaryExp o = new AOrBooleanBinaryExp();
455:                         o.setLeft(root.clone());
456:                         o.setOp(new LexKeywordToken(VDMToken.OR, null));
457:                         o.setType(new ABooleanBasicType());
458:                         o.setRight(e.clone());
459:                         return o;
460:                 } else
461:                 {
462:                         return e;
463:                 }
464:         }
465:
466:         /**
467:          * Create an expression equivalent to a pattern.
468:          */
469:         protected PExp patternToExp(PPattern pattern) throws AnalysisException
470:         {
471:                 PatternToExpVisitor visitor = new PatternToExpVisitor(getUniqueGenerator(), af);
472:                 return pattern.apply(visitor);
473:         }
474:
475:         protected List<PMultipleBind> cloneListMultipleBind(
476:                         List<PMultipleBind> binds)
477:         {
478:                 List<PMultipleBind> r = new LinkedList<PMultipleBind>();
479:
480:•                for (PMultipleBind bind : binds)
481:                 {
482:                         r.add(bind.clone());
483:                 }
484:
485:                 return r;
486:         }
487:
488:         /**
489:          * Clone a list of PTypes (and return a typed list)
490:          *
491:          * @param types the
492:          * list to clone
493:          * @return a Typed list of PTypes
494:          */
495:         protected List<PType> cloneListType(List<PType> types)
496:         {
497:                 List<PType> r = new LinkedList<PType>();
498:•                for (PType type : types)
499:                 {
500:                         r.add(type.clone());
501:                 }
502:                 return r;
503:         }
504:
505:         /**
506:          * Clone a list of PExps (and return a typed list)
507:          *
508:          * @param args the
509:          * list to clone
510:          * @return a Typed list of PExps
511:          */
512:         protected List<PExp> cloneListPExp(List<PExp> args)
513:         {
514:                 List<PExp> clones = new LinkedList<PExp>();
515:•                for (PExp pexp : args)
516:                 {
517:                         clones.add(pexp.clone());
518:                 }
519:                 return clones;
520:         }
521:
522: }