Package: OperationPostConditionObligation

OperationPostConditionObligation

nameinstructionbranchcomplexitylinemethod
OperationPostConditionObligation(AExplicitOperationDefinition, IPOContextStack, IPogAssistantFactory)
M: 0 C: 27
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 5
100%
M: 0 C: 1
100%
OperationPostConditionObligation(AImplicitOperationDefinition, IPOContextStack, IPogAssistantFactory)
M: 28 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 4 C: 0
0%
M: 1 C: 0
0%
buildErrsExp(List)
M: 36 C: 0
0%
M: 2 C: 0
0%
M: 2 C: 0
0%
M: 6 C: 0
0%
M: 1 C: 0
0%
buildExp(PExp, PExp, List)
M: 24 C: 4
14%
M: 3 C: 1
25%
M: 2 C: 1
33%
M: 5 C: 2
29%
M: 0 C: 1
100%
handleErrorCase(AErrorCase)
M: 14 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 4 C: 0
0%
M: 1 C: 0
0%
handlePrePost(PExp, PExp, List)
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%

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.List;
27:
28: import org.overture.ast.analysis.AnalysisException;
29: import org.overture.ast.definitions.AExplicitOperationDefinition;
30: import org.overture.ast.definitions.AImplicitOperationDefinition;
31: import org.overture.ast.expressions.AAndBooleanBinaryExp;
32: import org.overture.ast.expressions.AOrBooleanBinaryExp;
33: import org.overture.ast.expressions.PExp;
34: import org.overture.ast.factory.AstExpressionFactory;
35: import org.overture.ast.statements.AErrorCase;
36: import org.overture.pog.pub.IPOContextStack;
37: import org.overture.pog.pub.IPogAssistantFactory;
38: import org.overture.pog.pub.POType;
39:
40: public class OperationPostConditionObligation extends ProofObligation
41: {
42:         /**
43:          *
44:          */
45:         private static final long serialVersionUID = 7717481924562707647L;
46:
47:         public OperationPostConditionObligation(AExplicitOperationDefinition op,
48:                         IPOContextStack ctxt, IPogAssistantFactory af)
49:                         throws AnalysisException
50:         {
51:                 super(op, POType.OP_POST_CONDITION, ctxt, op.getLocation(), af);
52:                 PExp pred = buildExp(op.getPrecondition(), op.getPostcondition().clone(), null);
53:
54:                 stitch = pred;
55:                 valuetree.setPredicate(ctxt.getPredWithContext(pred));
56:         }
57:
58:         public OperationPostConditionObligation(AImplicitOperationDefinition op,
59:                         IPOContextStack ctxt, IPogAssistantFactory af)
60:                         throws AnalysisException
61:         {
62:                 super(op, POType.OP_POST_CONDITION, ctxt, op.getLocation(), af);
63:
64:                 stitch = buildExp(op.getPrecondition(), op.getPostcondition().clone(), op.clone().getErrors());
65:                 valuetree.setPredicate(ctxt.getPredWithContext(stitch));
66:         }
67:
68:         private PExp handlePrePost(PExp preexp, PExp postexp, List<AErrorCase> errs)
69:         {
70:•                if (preexp != null)
71:                 {
72:                         // (preexp and postexp)
73:                         AAndBooleanBinaryExp andExp = AstExpressionFactory.newAAndBooleanBinaryExp(preexp.clone(), postexp);
74:
75:                         return andExp;
76:                 } else
77:                 {
78:                         return postexp;
79:                 }
80:         }
81:
82:         private PExp buildExp(PExp preexp, PExp postexp, List<AErrorCase> errs)
83:         {
84:•                if (errs == null || errs.isEmpty())
85:                 {
86:                         return postexp;
87:                 } else
88:                 {// handled prepost or errors
89:                         AOrBooleanBinaryExp orExp = new AOrBooleanBinaryExp();
90:                         orExp.setLeft(handlePrePost(preexp.clone(), postexp, errs));
91:                         PExp errorsExp = buildErrsExp(errs);
92:                         orExp.setRight(errorsExp);
93:
94:                         return orExp;
95:                 }
96:         }
97:
98:         private PExp handleErrorCase(AErrorCase err)
99:         {
100:                 // (errlet and errright)
101:                 AAndBooleanBinaryExp andExp = new AAndBooleanBinaryExp();
102:                 andExp.setLeft(err.getLeft());
103:                 andExp.setRight(err.getRight());
104:                 return andExp;
105:         }
106:
107:         private PExp buildErrsExp(List<AErrorCase> errs)
108:         {
109:•                if (errs.size() == 1)
110:                 { // termination case
111:                         return handleErrorCase(errs.get(0));
112:                 } else
113:                 { // recurse on error list
114:                         AOrBooleanBinaryExp orExp = new AOrBooleanBinaryExp();
115:                         orExp.setLeft(handleErrorCase(errs.get(0)));
116:                         orExp.setRight(buildErrsExp(errs.subList(1, errs.size() - 1)));
117:                         return orExp;
118:                 }
119:         }
120:
121: }