|
5 | 5 |
|
6 | 6 | import java.util.LinkedHashMap; |
7 | 7 | import java.util.Map; |
| 8 | +import java.util.Objects; |
8 | 9 | import java.util.function.UnaryOperator; |
9 | 10 |
|
10 | 11 | import de.uka.ilkd.key.java.Services; |
@@ -88,22 +89,28 @@ public ClassInvariantImpl(String name, String displayName, KeYJavaType kjt, |
88 | 89 | * @param displayName the displayed name of the invariant |
89 | 90 | * @param kjt the KeYJavaType to which the invariant belongs |
90 | 91 | * @param visibility the visibility of the invariant (null for default visibility) |
| 92 | + * TODO weigl: what is the "default visibility"? |
91 | 93 | * @param inv the invariant formula itself |
92 | 94 | * @param selfVar the variable used for the receiver object |
93 | 95 | * @param free whether this contract is free. |
94 | 96 | */ |
95 | 97 | public ClassInvariantImpl(String name, String displayName, KeYJavaType kjt, |
96 | 98 | ModifierKind visibility, JTerm inv, LocationVariable selfVar, |
97 | 99 | boolean free) { |
98 | | - assert name != null && !name.isEmpty(); |
99 | | - assert displayName != null && !displayName.isEmpty(); |
100 | | - assert kjt != null; |
101 | | - assert inv != null; |
102 | | - this.name = name; |
103 | | - this.displayName = displayName; |
104 | | - this.kjt = kjt; |
105 | | - this.visibility = visibility; |
106 | | - this.originalInv = inv; |
| 100 | + |
| 101 | + this.name = Objects.requireNonNull(name); |
| 102 | + if (name.isBlank()) { |
| 103 | + throw new IllegalArgumentException("name must not be blank"); |
| 104 | + } |
| 105 | + |
| 106 | + this.displayName = Objects.requireNonNull(displayName); |
| 107 | + if (displayName.isEmpty()) { |
| 108 | + throw new IllegalArgumentException("displayName must not be empty"); |
| 109 | + } |
| 110 | + |
| 111 | + this.kjt = Objects.requireNonNull(kjt); |
| 112 | + this.visibility = Objects.requireNonNullElse(visibility, ModifierKind.PUBLIC); |
| 113 | + this.originalInv = Objects.requireNonNull(inv); |
107 | 114 | this.originalSelfVar = selfVar; |
108 | 115 | final OpCollector oc = new OpCollector(); |
109 | 116 | originalInv.execPostOrder(oc); |
|
0 commit comments