Package: AbstractCollectionInfo

AbstractCollectionInfo

nameinstructionbranchcomplexitylinemethod
AbstractCollectionInfo(boolean)
M: 0 C: 4
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
consCheckExp(String, String, String, NameGen)
M: 0 C: 99
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 17
100%
M: 0 C: 1
100%
getLeafTypesRecursively()
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%

Coverage

1: package org.overture.codegen.vdm2jml.predgen.info;
2:
3: import java.util.LinkedList;
4: import java.util.List;
5:
6: import org.overture.codegen.vdm2jml.JmlGenerator;
7: import org.overture.codegen.vdm2jml.runtime.V2J;
8: import org.overture.codegen.vdm2jml.util.NameGen;
9:
10: public abstract class AbstractCollectionInfo extends AbstractTypeInfo
11: {
12:         public static final String ITE_VAR_NAME_PREFIX = "i";
13:         public static final String SIZE__METHOD = "size";
14:
15:         public AbstractCollectionInfo(boolean optional)
16:         {
17:                 super(optional);
18:         }
19:
20:         @Override
21:         public List<LeafTypeInfo> getLeafTypesRecursively()
22:         {
23:                 return new LinkedList<>();
24:         }
25:
26:         abstract public String consElementCheck(String enclosingClass,
27:                         String javaRootPackage, String arg, NameGen nameGen, String iteVar);
28:
29:         abstract public String consCollectionCheck(String arg);
30:
31:         @Override
32:         public String consCheckExp(String enclosingClass, String javaRootPackage,
33:                         String arg, NameGen nameGen)
34:         {
35:                 String isColCheck = consCollectionCheck(arg);
36:                 String sizeCall = consSubjectCheck(V2J.class.getSimpleName(), SIZE__METHOD, arg);
37:                 String iteVar = nameGen.getName(ITE_VAR_NAME_PREFIX);
38:                 String elementCheck = consElementCheck(enclosingClass, javaRootPackage, arg, nameGen, iteVar);
39:
40:                 StringBuilder sb = new StringBuilder();
41:                 sb.append(isColCheck);
42:                 sb.append(JmlGenerator.JML_AND);
43:                 sb.append('(');
44:                 sb.append(String.format("\\forall int %1$s; 0 <= %1$s && %1$s < ", iteVar));
45:                 sb.append(sizeCall);
46:                 sb.append("; ");
47:                 sb.append(elementCheck);
48:                 sb.append(')');
49:
50:                 String seqCheckExp = "(" + sb.toString() + ")";
51:
52:•                if (isOptional())
53:                 {
54:                         return "(" + consIsNullCheck(arg) + JmlGenerator.JML_OR
55:                                         + seqCheckExp + ")";
56:                 } else
57:                 {
58:                         return seqCheckExp;
59:                 }
60:         }
61: }