Package: FunctionPostCondition

FunctionPostCondition

nameinstructionbranchcomplexitylinemethod
FunctionPostCondition(AExplicitFunctionDefinition, IPOContextStack, IPogAssistantFactory)
M: 24 C: 74
76%
M: 2 C: 6
75%
M: 2 C: 3
60%
M: 6 C: 15
71%
M: 0 C: 1
100%
FunctionPostCondition(AImplicitFunctionDefinition, IPOContextStack, IPogAssistantFactory)
M: 112 C: 0
0%
M: 10 C: 0
0%
M: 6 C: 0
0%
M: 23 C: 0
0%
M: 1 C: 0
0%
generateBody(AExplicitFunctionDefinition, List, PExp)
M: 0 C: 34
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 9
100%
M: 0 C: 1
100%
generatePredicate(AExplicitFunctionDefinition, AExplicitFunctionDefinition, List, PExp)
M: 0 C: 44
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 9
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:
29: import org.overture.ast.analysis.AnalysisException;
30: import org.overture.ast.definitions.AExplicitFunctionDefinition;
31: import org.overture.ast.definitions.AImplicitFunctionDefinition;
32: import org.overture.ast.expressions.AApplyExp;
33: import org.overture.ast.expressions.ANotYetSpecifiedExp;
34: import org.overture.ast.expressions.ASubclassResponsibilityExp;
35: import org.overture.ast.expressions.AVariableExp;
36: import org.overture.ast.expressions.PExp;
37: import org.overture.ast.factory.AstExpressionFactory;
38: import org.overture.ast.patterns.PPattern;
39: import org.overture.ast.types.ABooleanBasicType;
40: import org.overture.pog.pub.IPOContextStack;
41: import org.overture.pog.pub.IPogAssistantFactory;
42: import org.overture.pog.pub.POType;
43:
44: public class FunctionPostCondition extends ProofObligation
45: {
46:
47:         /**
48:          *
49:          */
50:         private static final long serialVersionUID = 1L;
51:
52:         public FunctionPostCondition(AExplicitFunctionDefinition func,
53:                         IPOContextStack ctxt, IPogAssistantFactory assistantFactory)
54:                         throws AnalysisException
55:         {
56:                 super(func, POType.FUNC_POST_CONDITION, ctxt, func.getLocation(), assistantFactory);
57:
58:                 List<PExp> params = new LinkedList<PExp>();
59:•                for (List<PPattern> pl : func.getParamPatternList())
60:                 {
61:•                        for (PPattern p : pl)
62:                         {
63:                                 params.add(patternToExp(p));
64:                         }
65:                 }
66:
67:                 PExp body = null;
68:                 // String body = null;
69:
70:•                if (func.getBody() instanceof ANotYetSpecifiedExp
71:•                                || func.getBody() instanceof ASubclassResponsibilityExp)
72:                 {
73:                         AApplyExp applyExp = new AApplyExp();
74:                         applyExp.setArgs(params);
75:                         AVariableExp varExp = getVarExp(func.getName().clone(), func.clone(), func.getType().clone());
76:                         applyExp.setRoot(varExp);
77:                         // We have to say "f(a)" because we have no expression yet
78:                         // I suppose this still still holds true with ast pos
79:                         body = applyExp;
80:                 } else
81:
82:                 {
83:                         body = func.getBody();
84:                 }
85:
86:                 PExp pred = generatePredicate(func.getPredef(), func.getPostdef().clone(), params, body);
87:                 stitch = pred;
88:                 valuetree.setPredicate(ctxt.getPredWithContext(pred));
89:         }
90:
91:         public FunctionPostCondition(AImplicitFunctionDefinition func,
92:                         IPOContextStack ctxt, IPogAssistantFactory assistantFactory)
93:                         throws AnalysisException
94:         {
95:                 super(func, POType.FUNC_POST_CONDITION, ctxt, func.getLocation(), assistantFactory);
96:
97:                 List<PExp> params = new LinkedList<PExp>();
98:
99:•                for (List<PPattern> pl : assistantFactory.createAImplicitFunctionDefinitionAssistant().getParamPatternList(func))
100:                 {
101:•                        for (PPattern p : pl)
102:                         {
103:                                 params.add(patternToExp(p));
104:                         }
105:                 }
106:
107:                 PExp body = null;
108:
109:                 // implicit body is apparently allowed
110:•                if (func.getBody() == null)
111:                 {
112:                         body = patternToExp(func.getResult().getPattern());
113:
114:•                } else if (func.getBody() instanceof ANotYetSpecifiedExp
115:•                                || func.getBody() instanceof ASubclassResponsibilityExp)
116:                 {
117:                         AApplyExp applyExp = new AApplyExp();
118:                         applyExp.setArgs(params);
119:                         AVariableExp varExp = getVarExp(func.getName().clone(), func.clone(), func.getType().clone());
120:                         applyExp.setRoot(varExp);
121:                         body = applyExp;
122:                 } else
123:                 {
124:                         body = func.getBody().clone();
125:                 }
126:
127:                 // valuetree.setContext(ctxt.getContextNodeList());
128:                 PExp pred = generatePredicate(func.getPredef(), func.getPostdef(), cloneListPExp(params), body);
129:                 stitch = pred;
130:                 valuetree.setPredicate(ctxt.getPredWithContext(pred));
131:
132:         }
133:
134:         private PExp generatePredicate(AExplicitFunctionDefinition predef,
135:                         AExplicitFunctionDefinition postdef, List<PExp> params, PExp body)
136:         {
137:
138:•                if (predef != null)
139:                 {
140:                         // pre(params) =>
141:                         AApplyExp applyExp = new AApplyExp();
142:                         applyExp.setType(new ABooleanBasicType());
143:                         applyExp.setArgs(cloneListPExp(params));
144:                         AVariableExp varExp = getVarExp(predef.getName().clone());
145:                         varExp.setType(predef.getType().clone());
146:                         applyExp.setRoot(varExp);
147:
148:                         return AstExpressionFactory.newAImpliesBooleanBinaryExp(applyExp, generateBody(postdef, params, body));
149:
150:                 }
151:                 return generateBody(postdef, params, body);
152:
153:         }
154:
155:         private PExp generateBody(AExplicitFunctionDefinition postdef,
156:                         List<PExp> params, PExp body)
157:         {
158:                 // post(params, body)
159:                 AApplyExp applyExp = new AApplyExp();
160:                 applyExp.setType(new ABooleanBasicType());
161:
162:                 AVariableExp varExp = getVarExp(postdef.getName());
163:                 varExp.setType(postdef.getType().clone());
164:                 applyExp.setRoot(varExp);
165:
166:                 List<PExp> args = params;
167:                 args.add(body.clone());
168:                 applyExp.setArgs(args);
169:
170:                 return applyExp;
171:         }
172:
173: }