Package: POForAllContext

POForAllContext

nameinstructionbranchcomplexitylinemethod
POForAllContext(AExistsExp)
M: 0 C: 7
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
POForAllContext(AForAllExp)
M: 0 C: 7
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
POForAllContext(ALambdaExp)
M: 0 C: 41
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 9
100%
M: 0 C: 1
100%
POForAllContext(ALetBeStExp, IPogAssistantFactory)
M: 0 C: 12
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
POForAllContext(AMapCompMapExp)
M: 0 C: 7
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
POForAllContext(ASeqCompSeqExp, IPogAssistantFactory)
M: 0 C: 9
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
POForAllContext(ASetCompSetExp)
M: 0 C: 7
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
POForAllContext(ITypeCheckerAssistantFactory, AExists1Exp)
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%
POForAllContext(ITypeCheckerAssistantFactory, AIotaExp)
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%
POForAllContext(PBind, PExp)
M: 33 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 8 C: 0
0%
M: 1 C: 0
0%
cloneBinds(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%
getContext()
M: 39 C: 0
0%
M: 2 C: 0
0%
M: 2 C: 0
0%
M: 10 C: 0
0%
M: 1 C: 0
0%
getContextNode(PExp)
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%
getMultipleBindList(PBind)
M: 8 C: 27
77%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 1 C: 6
86%
M: 0 C: 1
100%
getSuperContext(PExp)
M: 0 C: 20
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 5
100%
M: 0 C: 1
100%
isScopeBoundary()
M: 0 C: 2
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
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.ArrayList;
27: import java.util.LinkedList;
28: import java.util.List;
29: import java.util.Vector;
30:
31: import org.overture.ast.expressions.AElementsUnaryExp;
32: import org.overture.ast.expressions.AExists1Exp;
33: import org.overture.ast.expressions.AExistsExp;
34: import org.overture.ast.expressions.AForAllExp;
35: import org.overture.ast.expressions.AIotaExp;
36: import org.overture.ast.expressions.ALambdaExp;
37: import org.overture.ast.expressions.ALetBeStExp;
38: import org.overture.ast.expressions.AMapCompMapExp;
39: import org.overture.ast.expressions.ASeqCompSeqExp;
40: import org.overture.ast.expressions.ASetCompSetExp;
41: import org.overture.ast.expressions.PExp;
42: import org.overture.ast.factory.AstFactory;
43: import org.overture.ast.patterns.ASeqBind;
44: import org.overture.ast.patterns.ASetBind;
45: import org.overture.ast.patterns.ASetMultipleBind;
46: import org.overture.ast.patterns.ATypeBind;
47: import org.overture.ast.patterns.ATypeMultipleBind;
48: import org.overture.ast.patterns.PBind;
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.pog.pub.IPogAssistantFactory;
53: import org.overture.typechecker.assistant.ITypeCheckerAssistantFactory;
54:
55: public class POForAllContext extends POContext
56: {
57:         public final List<PMultipleBind> bindings;
58:
59:         public POForAllContext(AMapCompMapExp exp)
60:         {
61:                 this.bindings = exp.getBindings();
62:         }
63:
64:         public POForAllContext(ASetCompSetExp exp)
65:         {
66:                 this.bindings = exp.getBindings();
67:         }
68:
69:         public POForAllContext(ASeqCompSeqExp exp,
70:                         IPogAssistantFactory assistantFactory)
71:         {
72:                 this.bindings = getMultipleBindList(exp.getBind());
73:         }
74:
75:         public POForAllContext(AForAllExp exp)
76:         {
77:                 this.bindings = exp.getBindList();
78:         }
79:
80:         public POForAllContext(AExistsExp exp)
81:         {
82:                 this.bindings = exp.getBindList();
83:         }
84:
85:         public POForAllContext(ITypeCheckerAssistantFactory af, AExists1Exp exp)
86:         {
87:                 this.bindings = af.createPBindAssistant().getMultipleBindList(exp.getBind());
88:         }
89:
90:         public POForAllContext(ITypeCheckerAssistantFactory af, AIotaExp exp)
91:         {
92:                 this.bindings = af.createPBindAssistant().getMultipleBindList(exp.getBind());
93:         }
94:
95:         public POForAllContext(ALambdaExp exp)
96:         {
97:                 this.bindings = new Vector<PMultipleBind>();
98:
99:•                for (ATypeBind tb : exp.getBindList())
100:                 {
101:                         List<PPattern> pl = new ArrayList<PPattern>();
102:                         pl.add(tb.getPattern().clone());
103:                         ATypeMultipleBind mtb = AstFactory.newATypeMultipleBind(pl, tb.getType().clone());
104:                         bindings.add(mtb);
105:                 }
106:         }
107:
108:         public POForAllContext(ALetBeStExp exp,
109:                         IPogAssistantFactory assistantFactory)
110:         {
111:                 this.bindings = cloneBinds(assistantFactory.createPMultipleBindAssistant().getMultipleBindList(exp.getBind()));
112:         }
113:
114:         public POForAllContext(PBind bind, PExp exp)
115:         {
116:                 // Create new binding for "bind.pattern in set elems exp"
117:                 bindings = new Vector<PMultipleBind>();
118:                 List<PPattern> pl = new ArrayList<PPattern>();
119:                 pl.add(bind.getPattern().clone());
120:                 
121:                 AElementsUnaryExp elems = AstFactory.newAElementsUnaryExp(exp.getLocation(), exp.clone());
122:                 ASetMultipleBind msb = AstFactory.newASetMultipleBind(pl, elems);
123:                 bindings.add(msb);
124:         }
125:
126:         private List<PMultipleBind> cloneBinds(List<PMultipleBind> multipleBindList)
127:         {
128:                 List<PMultipleBind> r = new LinkedList<PMultipleBind>();
129:•                for (PMultipleBind pmb : multipleBindList)
130:                 {
131:                         r.add(pmb.clone());
132:                 }
133:                 return r;
134:         }
135:
136:         @Override
137:         public PExp getContextNode(PExp stitch)
138:         {
139:                 return getSuperContext(stitch);
140:         }
141:
142:         protected AForAllExp getSuperContext(PExp stitch)
143:         {
144:                 AForAllExp forAllExp = new AForAllExp();
145:                 forAllExp.setType(new ABooleanBasicType());
146:                 forAllExp.setBindList(cloneBinds(bindings));
147:                 forAllExp.setPredicate(stitch);
148:                 return forAllExp;
149:         }
150:
151:         @Override
152:         public boolean isScopeBoundary()
153:         {
154:                 return true;
155:         }
156:
157:         @Override
158:         public String getContext()
159:         {
160:                 StringBuilder sb = new StringBuilder();
161:
162:                 sb.append("forall ");
163:                 String prefix = "";
164:
165:•                for (PMultipleBind mb : bindings)
166:                 {
167:                         sb.append(prefix);
168:                         sb.append(mb);
169:                         prefix = ", ";
170:                 }
171:
172:                 sb.append(" &");
173:
174:                 return sb.toString();
175:         }
176:         
177:         public List<PMultipleBind> getMultipleBindList(PBind bind)
178:         {
179:                 List<PPattern> plist = new ArrayList<PPattern>();
180:                 plist.add(bind.getPattern());
181:                 List<PMultipleBind> mblist = new Vector<PMultipleBind>();
182:                 
183:•                if (bind instanceof ASetBind)
184:                 {
185:                         mblist.add(AstFactory.newASetMultipleBind(plist, ((ASetBind)bind).getSet()));
186:                 }
187:                 else
188:                 {
189:                         mblist.add(AstFactory.newASetMultipleBind(plist, ((ASeqBind)bind).getSeq()));
190:                 }
191:
192:                 return mblist;
193:         }
194: }