Package: POOperationDefinitionContext

POOperationDefinitionContext

nameinstructionbranchcomplexitylinemethod
POOperationDefinitionContext(AExplicitOperationDefinition, boolean, PDefinition)
M: 0 C: 31
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 9
100%
M: 0 C: 1
100%
POOperationDefinitionContext(AImplicitOperationDefinition, boolean, PDefinition, IPogAssistantFactory)
M: 0 C: 31
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 9
100%
M: 0 C: 1
100%
POOperationDefinitionContext(ILexNameToken, AOperationType, LinkedList, boolean, PExp, PDefinition, PDefinition)
M: 24 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 9 C: 0
0%
M: 1 C: 0
0%
addParameterBinds(LinkedList)
M: 0 C: 44
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 10
100%
M: 0 C: 1
100%
addStateBinds(LinkedList)
M: 0 C: 58
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 16
100%
M: 0 C: 1
100%
anyBinds()
M: 0 C: 9
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
appendStatePatterns(StringBuilder)
M: 38 C: 0
0%
M: 4 C: 0
0%
M: 3 C: 0
0%
M: 11 C: 0
0%
M: 1 C: 0
0%
cloneList(LinkedList)
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%
getContext()
M: 87 C: 0
0%
M: 12 C: 0
0%
M: 7 C: 0
0%
M: 21 C: 0
0%
M: 1 C: 0
0%
getContextNode(PExp)
M: 0 C: 53
100%
M: 2 C: 8
80%
M: 2 C: 4
67%
M: 0 C: 14
100%
M: 0 C: 1
100%
makeBinds()
M: 0 C: 12
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 4
100%
M: 0 C: 1
100%
static {...}
M: 0 C: 15
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.contexts;
25:
26: import java.util.Iterator;
27: import java.util.LinkedList;
28: import java.util.List;
29:
30: import org.overture.ast.definitions.AExplicitOperationDefinition;
31: import org.overture.ast.definitions.AImplicitOperationDefinition;
32: import org.overture.ast.definitions.AStateDefinition;
33: import org.overture.ast.definitions.PDefinition;
34: import org.overture.ast.definitions.SClassDefinition;
35: import org.overture.ast.expressions.AForAllExp;
36: import org.overture.ast.expressions.AImpliesBooleanBinaryExp;
37: import org.overture.ast.expressions.PExp;
38: import org.overture.ast.factory.AstExpressionFactory;
39: import org.overture.ast.intf.lex.ILexNameToken;
40: import org.overture.ast.lex.LexNameToken;
41: import org.overture.ast.patterns.AIdentifierPattern;
42: import org.overture.ast.patterns.AIgnorePattern;
43: import org.overture.ast.patterns.ATypeMultipleBind;
44: import org.overture.ast.patterns.PMultipleBind;
45: import org.overture.ast.patterns.PPattern;
46: import org.overture.ast.types.ABooleanBasicType;
47: import org.overture.ast.types.AOperationType;
48: import org.overture.ast.types.PType;
49: import org.overture.pog.pub.IPogAssistantFactory;
50:
51: public class POOperationDefinitionContext extends POContext
52: {
53:         public final ILexNameToken name;
54:         public final AOperationType deftype;
55:         public final List<PPattern> paramPatternList;
56:         public final boolean addPrecond;
57:         public final PExp precondition;
58:         public final PDefinition stateDefinition;
59:         final PDefinition opDef;
60:
61:         protected POOperationDefinitionContext(ILexNameToken name,
62:                         AOperationType deftype, LinkedList<PPattern> paramPatternList,
63:                         boolean addPrecond, PExp precondition, PDefinition stateDefinition,
64:                         PDefinition opDef)
65:         {
66:                 super();
67:                 this.name = name;
68:                 this.deftype = deftype;
69:                 this.paramPatternList = paramPatternList;
70:                 this.addPrecond = addPrecond;
71:                 this.precondition = precondition;
72:                 this.stateDefinition = stateDefinition;
73:                 this.opDef = opDef;
74:         }
75:
76:         public POOperationDefinitionContext(
77:                         AExplicitOperationDefinition definition, boolean precond,
78:                         PDefinition stateDefinition)
79:         {
80:                 this.name = definition.getName();
81:                 this.deftype = (AOperationType) definition.getType();
82:                 this.addPrecond = precond;
83:                 this.paramPatternList = cloneList(definition.getParameterPatterns());
84:                 this.precondition = definition.getPrecondition();
85:                 this.stateDefinition = stateDefinition;
86:                 this.opDef = definition;
87:
88:         }
89:
90:         private List<PPattern> cloneList(LinkedList<PPattern> parameterPatterns)
91:         {
92:                 List<PPattern> r = new LinkedList<PPattern>();
93:
94:•                for (PPattern p : parameterPatterns)
95:                 {
96:                         r.add(p.clone());
97:                 }
98:                 return r;
99:         }
100:
101:         public POOperationDefinitionContext(
102:                         AImplicitOperationDefinition definition, boolean precond,
103:                         PDefinition stateDefinition, IPogAssistantFactory assistantFactory)
104:         {
105:                 this.name = definition.getName();
106:                 this.deftype = (AOperationType) definition.getType();
107:                 this.addPrecond = precond;
108:                 this.paramPatternList = assistantFactory.createAImplicitOperationDefinitionAssistant().getParamPatternList(definition);
109:                 this.precondition = definition.getPrecondition();
110:                 this.stateDefinition = stateDefinition;
111:                 this.opDef = definition;
112:         }
113:
114:         protected boolean anyBinds()
115:         {
116:•                return !deftype.getParameters().isEmpty();
117:         }
118:
119:         @Override
120:         public PExp getContextNode(PExp stitch)
121:         {
122:•                if (anyBinds())
123:                 {
124:                         AForAllExp forAllExp = new AForAllExp();
125:                         forAllExp.setType(new ABooleanBasicType());
126:                         forAllExp.setBindList(makeBinds());
127:
128:•                        if (addPrecond && precondition != null)
129:                         {
130:                                 AImpliesBooleanBinaryExp impliesExp = AstExpressionFactory.newAImpliesBooleanBinaryExp(precondition.clone(), stitch);
131:                                 forAllExp.setPredicate(impliesExp);
132:                         } else
133:                         {
134:                                 forAllExp.setPredicate(stitch);
135:                         }
136:
137:                         return forAllExp;
138:
139:                 } else
140:                 {
141:•                        if (addPrecond && precondition != null)
142:                         {
143:                                 AImpliesBooleanBinaryExp impliesExp = AstExpressionFactory.newAImpliesBooleanBinaryExp(precondition.clone(), stitch);
144:                                 return impliesExp;
145:                         }
146:                 }
147:                 return stitch;
148:
149:         }
150:
151:         private static final ILexNameToken OLD_STATE_ARG = new LexNameToken("", "oldstate", null);
152:         private static final ILexNameToken OLD_SELF_ARG = new LexNameToken("", "oldself", null);
153:
154:         private void addParameterBinds(LinkedList<PMultipleBind> r)
155:         {
156:                 Iterator<PType> types = deftype.getParameters().iterator();
157:•                for (PPattern p : paramPatternList)
158:                 {
159:                         ATypeMultipleBind tmBind = new ATypeMultipleBind();
160:                         List<PPattern> pats = new LinkedList<PPattern>();
161:
162:                         pats.add(p.clone());
163:                         tmBind.setType(types.next().clone());
164:                         tmBind.setPlist(pats);
165:                         r.add(tmBind);
166:                 }
167:         }
168:
169:         protected void addStateBinds(LinkedList<PMultipleBind> r)
170:         {
171:•                if (stateDefinition != null)
172:                 {
173:                         ATypeMultipleBind tmBind2 = new ATypeMultipleBind();
174:                         AIdentifierPattern pattern = new AIdentifierPattern();
175:
176:•                        if (stateDefinition instanceof AStateDefinition)
177:                         {
178:                                 AStateDefinition def = (AStateDefinition) stateDefinition;
179:
180:                                 tmBind2.setType(def.getRecordType().clone());
181:                                 pattern.setName(OLD_STATE_ARG.clone());
182:                         } else
183:                         {
184:                                 SClassDefinition def = (SClassDefinition) stateDefinition;
185:                                 tmBind2.setType(def.getClasstype().clone());
186:                                 pattern.setName(OLD_SELF_ARG.clone());
187:                         }
188:
189:                         List<PPattern> plist = new LinkedList<PPattern>();
190:                         plist.add(pattern);
191:                         tmBind2.setPlist(plist);
192:                         r.add(tmBind2);
193:                 }
194:         }
195:
196:         private List<? extends PMultipleBind> makeBinds()
197:         {
198:                 LinkedList<PMultipleBind> r = new LinkedList<PMultipleBind>();
199:
200:                 addParameterBinds(r);
201:
202:                 addStateBinds(r);
203:
204:                 return r;
205:
206:         }
207:
208:         @Override
209:         public String getContext()
210:         {
211:                 StringBuilder sb = new StringBuilder();
212:
213:•                if (!deftype.getParameters().isEmpty())
214:                 {
215:                         sb.append("forall ");
216:                         String sep = "";
217:                         Iterator<PType> types = deftype.getParameters().iterator();
218:
219:•                        for (PPattern p : paramPatternList)
220:                         {
221:•                                if (!(p instanceof AIgnorePattern))
222:                                 {
223:                                         sb.append(sep);
224:                                         sb.append(p.toString());
225:                                         sb.append(":");
226:                                         sb.append(types.next());
227:                                         sep = ", ";
228:                                 }
229:                         }
230:
231:•                        if (stateDefinition != null)
232:                         {
233:                                 appendStatePatterns(sb);
234:                         }
235:
236:                         sb.append(" &");
237:
238:•                        if (addPrecond && precondition != null)
239:                         {
240:                                 sb.append(" ");
241:                                 sb.append(precondition);
242:                                 sb.append(" =>");
243:                         }
244:                 }
245:
246:                 return sb.toString();
247:         }
248:
249:         private void appendStatePatterns(StringBuilder sb)
250:         {
251:•                if (stateDefinition == null)
252:                 {
253:                         return;
254:•                } else if (stateDefinition instanceof AStateDefinition)
255:                 {
256:                         AStateDefinition def = (AStateDefinition) stateDefinition;
257:                         sb.append(", oldstate:");
258:                         sb.append(def.getName().getName());
259:                 } else
260:                 {
261:                         SClassDefinition def = (SClassDefinition) stateDefinition;
262:                         sb.append(", oldself:");
263:                         sb.append(def.getName().getName());
264:                 }
265:         }
266:
267: }