Package: MapInfo

MapInfo

nameinstructionbranchcomplexitylinemethod
MapInfo(boolean, AbstractTypeInfo, AbstractTypeInfo, boolean)
M: 0 C: 13
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 5
100%
M: 0 C: 1
100%
consCollectionCheck(String)
M: 0 C: 11
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
consElementCheck(String, String, String, NameGen, String)
M: 0 C: 49
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 9
100%
M: 0 C: 1
100%

Coverage

1: package org.overture.codegen.vdm2jml.predgen.info;
2:
3: import org.overture.codegen.vdm2jml.JmlGenerator;
4: import org.overture.codegen.vdm2jml.runtime.V2J;
5: import org.overture.codegen.vdm2jml.util.NameGen;
6:
7: public class MapInfo extends AbstractCollectionInfo
8: {
9:         public static final String IS_MAP_METHOD = "isMap";
10:         public static final String IS_INJECTIVE_MAP_METHOD = "isInjMap";
11:         public static final String GET_DOM_METHOD = "getDom";
12:         public static final String GET_RNG_METHOD = "getRng";
13:
14:         private AbstractTypeInfo domType;
15:         private AbstractTypeInfo rngType;
16:         private boolean injective;
17:
18:         public MapInfo(boolean optional, AbstractTypeInfo domType,
19:                         AbstractTypeInfo rngType, boolean injective)
20:         {
21:                 super(optional);
22:                 this.domType = domType;
23:                 this.rngType = rngType;
24:                 this.injective = injective;
25:         }
26:
27:         @Override
28:         public String consElementCheck(String enclosingClass,
29:                         String javaRootPackage, String arg, NameGen nameGen, String iteVar)
30:         {
31:                 String domArg = consSubjectCheckExtraArg(V2J.class.getSimpleName(), GET_DOM_METHOD, arg, iteVar);
32:                 String rngArg = consSubjectCheckExtraArg(V2J.class.getSimpleName(), GET_RNG_METHOD, arg, iteVar);
33:
34:                 String domCheck = domType.consCheckExp(enclosingClass, javaRootPackage, domArg, nameGen);
35:                 String rngCheck = rngType.consCheckExp(enclosingClass, javaRootPackage, rngArg, nameGen);
36:
37:                 StringBuilder sb = new StringBuilder();
38:                 sb.append(domCheck);
39:                 sb.append(JmlGenerator.JML_AND);
40:                 sb.append(rngCheck);
41:
42:                 return sb.toString();
43:         }
44:
45:         @Override
46:         public String consCollectionCheck(String arg)
47:         {
48:                 // e.g. (V2J.isMap(m) && (\forall int i; 0 <= i && i < VDM2JML.size(m); Utils.is_nat(VDM2JML.getDom(i,m)) &&
49:                 // Utils.is_nat(VDM2JML.getRng(i,m))));
50:•                return consSubjectCheck(V2J.class.getSimpleName(), injective
51:                                 ? IS_INJECTIVE_MAP_METHOD : IS_MAP_METHOD, arg);
52:         }
53: }