Package: MapInjectivityEnum

MapInjectivityEnum

nameinstructionbranchcomplexitylinemethod
MapInjectivityEnum(AMapEnumMapExp, IPOContextStack, IPogAssistantFactory)
M: 0 C: 275
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 45
100%
M: 0 C: 1
100%

Coverage

1: /*******************************************************************************
2: *
3: *
4: *        Copyright (C) 2008 Fujitsu Services Ltd.
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: import java.util.Vector;
28:
29: import org.overture.ast.analysis.AnalysisException;
30: import org.overture.ast.expressions.AApplyExp;
31: import org.overture.ast.expressions.AEqualsBinaryExp;
32: import org.overture.ast.expressions.AForAllExp;
33: import org.overture.ast.expressions.AImpliesBooleanBinaryExp;
34: import org.overture.ast.expressions.AMapDomainUnaryExp;
35: import org.overture.ast.expressions.AMapEnumMapExp;
36: import org.overture.ast.expressions.AMapletExp;
37: import org.overture.ast.expressions.ASetEnumSetExp;
38: import org.overture.ast.factory.AstExpressionFactory;
39: import org.overture.ast.intf.lex.ILexNameToken;
40: import org.overture.ast.patterns.PMultipleBind;
41: import org.overture.ast.types.ABooleanBasicType;
42: import org.overture.ast.types.ASetSetType;
43: import org.overture.ast.types.SSetType;
44: import org.overture.pog.pub.IPOContextStack;
45: import org.overture.pog.pub.IPogAssistantFactory;
46: import org.overture.pog.pub.POType;
47:
48: public class MapInjectivityEnum extends ProofObligation
49: {
50:         private static final long serialVersionUID = 2042036674338877124L;
51:
52:         public MapInjectivityEnum(AMapEnumMapExp mapEnumExp, IPOContextStack ctxt,
53:                         IPogAssistantFactory af) throws AnalysisException
54:         {
55:                 super(mapEnumExp, POType.MAP_INJ_ENUM, ctxt, mapEnumExp.getLocation(), af);
56:
57:                 /**
58:                  * This obligation applies to a map enumeration. Given a map enum of the form { <maplet>, <maplet>, ... }, the
59:                  * obligation becomes: forall m1, m2 in set { {<maplet>}, {<maplet>}, ... } & -- set of maps forall d1 in set
60:                  * dom m1, d2 in set dom m2 & (d1 = d2) => (m1(d1) = m2(d2)) The obligation means that there are no
61:                  * contradictory maplets, where the same domain key maps to different range values.
62:                  */
63:
64:                 ILexNameToken m1 = getUnique("m");
65:                 ILexNameToken m2 = getUnique("m");
66:
67:                 ASetEnumSetExp setOfMaplets = new ASetEnumSetExp();
68:                 SSetType somType = new ASetSetType();
69:                 somType.setSetof(mapEnumExp.getType().clone());
70:                 setOfMaplets.setType(somType);
71:
72:                 List<AMapEnumMapExp> singleMaplets = new Vector<AMapEnumMapExp>();
73:
74:•                for (AMapletExp maplet : mapEnumExp.getMembers())
75:                 {
76:                         AMapEnumMapExp mapOfOne = new AMapEnumMapExp();
77:                         List<AMapletExp> members = new Vector<AMapletExp>();
78:                         members.add(maplet.clone());
79:                         mapOfOne.setMembers(members);
80:                         mapOfOne.setType(maplet.getType().clone());
81:
82:                         singleMaplets.add(mapOfOne);
83:                 }
84:
85:                 setOfMaplets.setMembers(singleMaplets);
86:                 List<PMultipleBind> m1m2binding = getMultipleSetBindList(setOfMaplets, m1, m2);
87:
88:                 AForAllExp domForallExp = new AForAllExp();
89:                 domForallExp.setType(new ABooleanBasicType());
90:                 ILexNameToken d1 = getUnique("d");
91:                 ILexNameToken d2 = getUnique("d");
92:
93:                 AMapDomainUnaryExp domM1 = new AMapDomainUnaryExp();
94:                 domM1.setExp(getVarExp(m1, mapEnumExp.getType()));
95:                 SSetType domType = new ASetSetType();
96:                 domType.setSetof(af.createPTypeAssistant().getMap(mapEnumExp.getType().clone(), mapEnumExp.getLocation().getModule()));
97:                 domM1.setType(domType.clone());
98:                 AMapDomainUnaryExp domM2 = new AMapDomainUnaryExp();
99:                 domM2.setExp(getVarExp(m2, mapEnumExp.getType()));
100:                 domM2.setType(domType.clone());
101:
102:                 AApplyExp applyExp = getApplyExp(getVarExp(m2, mapEnumExp.getType()), af.createPTypeAssistant().getMap(mapEnumExp.getType(), mapEnumExp.getLocation().getModule()).getTo(), getVarExp(d2, domType));
103:                 AApplyExp applyExp2 = getApplyExp(getVarExp(m1, mapEnumExp.getType()),af.createPTypeAssistant().getMap(mapEnumExp.getType(), mapEnumExp.getLocation().getModule()).getTo(), getVarExp(d1, domType));
104:                 AEqualsBinaryExp equalsExp = getEqualsExp(applyExp2, applyExp);
105:                 AImpliesBooleanBinaryExp implies = AstExpressionFactory.newAImpliesBooleanBinaryExp(getEqualsExp(getVarExp(d1, domType), getVarExp(d2, domType)), equalsExp);
106:
107:                 List<PMultipleBind> domBinding = getMultipleSetBindList(domM1, d1);
108:                 domBinding.addAll(getMultipleSetBindList(domM2, d2));
109:
110:                 domForallExp.setBindList(domBinding);
111:                 domForallExp.setPredicate(implies);
112:
113:                 AForAllExp forallExp = new AForAllExp();
114:                 forallExp.setType(new ABooleanBasicType());
115:                 forallExp.setBindList(m1m2binding);
116:                 forallExp.setPredicate(domForallExp);
117:
118:                 stitch = forallExp;
119:                 valuetree.setPredicate(ctxt.getPredWithContext(forallExp));
120:         }
121: }