Rename Modallity#program() to Modality#programBlock()

Drodt · Drodt · commit fa641e804fcf · 2025-06-06T14:53:55.000+02:00
diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicExecutionTreeBuilder.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicExecutionTreeBuilder.java
@@ -284,7 +284,7 @@ protected void initMethodCallStack(final Node root, Services services) {
         // Check if modality contains method frames
         if (!modalityTerms.isEmpty()) {
             final Modality mod = (Modality) modalityTerm.op();
-            JavaBlock javaBlock = mod.program();
+            JavaBlock javaBlock = mod.programBlock();
             final ProgramElement program = javaBlock.program();
             final List<Node> initialStack = new LinkedList<>();
             new JavaASTVisitor(program, services) {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/OpCollectorJavaBlock.java b/key.core/src/main/java/de/uka/ilkd/key/logic/OpCollectorJavaBlock.java
@@ -18,8 +18,8 @@ public class OpCollectorJavaBlock extends OpCollector {
     @Override
     public void visit(org.key_project.logic.Term t) {
         super.visit(t);
-        if (t.op() instanceof Modality mod && !mod.program().isEmpty()) {
-            var collect = new JavaASTCollector(mod.program().program(), LocationVariable.class);
+        if (t.op() instanceof Modality mod && !mod.programBlock().isEmpty()) {
+            var collect = new JavaASTCollector(mod.programBlock().program(), LocationVariable.class);
             collect.start();
             for (ProgramElement programElement : collect.getNodes()) {
                 if (programElement instanceof LocationVariable locationVariable) {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java b/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java
@@ -202,7 +202,7 @@ public ImmutableArray<QuantifiableVariable> varsBoundHere(int n) {
     @Override
     public @NonNull JavaBlock javaBlock() {
         if (op instanceof Modality mod) {
-            return mod.program();
+            return mod.programBlock();
         } else {
             return JavaBlock.EMPTY_JAVABLOCK;
         }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java
@@ -151,7 +151,7 @@ private boolean unifyHelp(Term t0, Term t1, ImmutableList<QuantifiableVariable>
             if (mod0.kind() != mod1.kind()) {
                 return false;
             }
-            nat = handleJava(mod0.program(), mod1.program(), nat);
+            nat = handleJava(mod0.programBlock(), mod1.programBlock(), nat);
             if (nat == FAILED) {
                 return false;
             }
@@ -366,7 +366,7 @@ private int hashQuantifiableVariable(QuantifiableVariable qv,
      * @return the hash code
      */
     private int hashJavaBlock(Modality mod) {
-        final JavaBlock jb = mod.program();
+        final JavaBlock jb = mod.programBlock();
         if (!jb.isEmpty()) {
             final JavaProgramElement jpe = jb.program();
             return jpe != null ? jpe.hashCodeModProperty(RENAMING_SOURCE_ELEMENT_PROPERTY) : 0;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/TermLabelsProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/TermLabelsProperty.java
@@ -54,7 +54,7 @@ public <V> boolean equalsModThisProperty(Term term1, Term term2, V... v) {
         }
 
         if (term1.op() instanceof Modality mod1
-                && !(mod1.program().equals(((Modality) (term2.op())).program()))) {
+                && !(mod1.programBlock().equals(((Modality) (term2.op())).programBlock()))) {
             return false;
         }
 
@@ -88,7 +88,7 @@ public int hashCodeModThisProperty(Term term) {
                     this::hashCodeModThisProperty);
         hashcode = hashcode * 17 + term.boundVars().hashCode();
         hashcode =
-            hashcode * 17 + (term.op() instanceof Modality mod ? mod.program().hashCode() : 3);
+            hashcode * 17 + (term.op() instanceof Modality mod ? mod.programBlock().hashCode() : 3);
 
         return hashcode;
     }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Modality.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Modality.java
@@ -12,6 +12,7 @@
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.sort.ProgramSVSort;
 
+import org.jspecify.annotations.NonNull;
 import org.key_project.logic.Name;
 import org.key_project.logic.TermCreationException;
 import org.key_project.logic.sort.Sort;
@@ -59,7 +60,8 @@ private Modality(JavaBlock prg, JavaModalityKind kind) {
     }
 
     @Override
-    public JavaBlock program() {
+    @NonNull
+    public JavaBlock programBlock() {
         return javaBlock;
     }
 
diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java
@@ -1693,7 +1693,7 @@ public void printModalityTerm(String left, JavaBlock jb, String right, Term phi,
                         ta[i] = phi.sub(i);
                     }
                     final Modality m =
-                        Modality.getModality((Modality.JavaModalityKind) o, mod.program());
+                        Modality.getModality((Modality.JavaModalityKind) o, mod.programBlock());
                     final Term term = services.getTermFactory().createTerm(m, ta,
                         phi.boundVars(), null);
                     notationInfo.getNotation(m).print(term, this);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/TermProgramVariableCollector.java b/key.core/src/main/java/de/uka/ilkd/key/proof/TermProgramVariableCollector.java
@@ -36,9 +36,9 @@ public void visit(Term visited) {
             result.add(variable);
         }
 
-        if (visited.op() instanceof Modality mod && !mod.program().isEmpty()) {
+        if (visited.op() instanceof Modality mod && !mod.programBlock().isEmpty()) {
             ProgramVariableCollector pvc =
-                new ProgramVariableCollector(mod.program().program(), services);
+                new ProgramVariableCollector(mod.programBlock().program(), services);
             pvc.start();
             result.addAll(pvc.result());
         }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java
@@ -358,7 +358,7 @@ private void populateNamespaces(Term term, NamespaceSet namespaces,
                 rootGoal.addProgramVariable(pv);
             }
         } else if (term.op() instanceof Modality mod) {
-            final ProgramElement pe = mod.program().program();
+            final ProgramElement pe = mod.programBlock().program();
             final Services serv = rootGoal.proof().getServices();
             final ImmutableSet<LocationVariable> freeProgVars =
                 MiscTools.getLocalIns(pe, serv).union(MiscTools.getLocalOuts(pe, serv));
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java
@@ -295,7 +295,7 @@ private static ExecutionContext extractExecutionContext(final MethodFrame frame)
          */
         private JavaStatement getFirstStatementInPrefixWithAtLeastOneApplicableContract(
                 final Modality modality, final Goal goal) {
-            SourceElement element = modality.program().program().getFirstElement();
+            SourceElement element = modality.programBlock().program().getFirstElement();
             while ((element instanceof ProgramPrefix || element instanceof CatchAllStatement)
                     && !(element instanceof StatementBlock
                             && ((StatementBlock) element).isEmpty())) {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/EqualityModuloProofIrrelevancy.java b/key.core/src/main/java/de/uka/ilkd/key/rule/EqualityModuloProofIrrelevancy.java
@@ -58,8 +58,8 @@ public static boolean equalsModProofIrrelevancy(Operator _this, Operator that) {
             return equalsModProofIrrelevancy(_thisLoc, (LocationVariable) that);
         } else if (_this instanceof Modality _thisMod) {
             return _thisMod.kind().equals(((Modality) that).kind()) &&
-                    equalsModProofIrrelevancy(_thisMod.program(),
-                        ((Modality) that).program());
+                    equalsModProofIrrelevancy(_thisMod.programBlock(),
+                        ((Modality) that).programBlock());
         }
 
         // assume name and arity uniquely identifies operator
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/LightweightSyntacticalReplaceVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/rule/LightweightSyntacticalReplaceVisitor.java
@@ -146,7 +146,7 @@ private Operator instantiateModality(Modality op, JavaBlock jb) {
         if (op.kind() instanceof ModalOperatorSV) {
             kind = (Modality.JavaModalityKind) svInst.getInstantiation(op.kind());
         }
-        if (jb != op.program() || kind != op.kind()) {
+        if (jb != op.programBlock() || kind != op.kind()) {
             return Modality.getModality(kind, jb);
         }
         return op;
@@ -217,7 +217,7 @@ public void visit(final org.key_project.logic.Term p_visited) {
             boolean jblockChanged = false;
             JavaBlock jb = JavaBlock.EMPTY_JAVABLOCK;
             if (visited.op() instanceof final Modality mod) {
-                final JavaBlock originalBlock = mod.program();
+                final JavaBlock originalBlock = mod.programBlock();
                 jb = replacePrg(svInst, originalBlock);
                 if (jb != originalBlock) {
                     jblockChanged = true;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/SyntacticalReplaceVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/rule/SyntacticalReplaceVisitor.java
@@ -272,7 +272,7 @@ private Operator instantiateModality(Modality op, JavaBlock jb) {
         if (op.kind() instanceof ModalOperatorSV) {
             kind = (Modality.JavaModalityKind) svInst.getInstantiation(op.kind());
         }
-        if (jb != op.program() || kind != op.kind()) {
+        if (jb != op.programBlock() || kind != op.kind()) {
             return Modality.getModality(kind, jb);
         }
         return op;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletSchemaVariableCollector.java b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletSchemaVariableCollector.java
@@ -91,7 +91,7 @@ public void visit(@NonNull Term p_visited) {
             if (mod.kind() instanceof ModalOperatorSV msv) {
                 varList = varList.prepend(msv);
             }
-            varList = collectSVInProgram(mod.program(), varList);
+            varList = collectSVInProgram(mod.programBlock(), varList);
         } else if (op instanceof ElementaryUpdate) {
             varList = collectSVInElementaryUpdate((ElementaryUpdate) op, varList);
         }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/UseOperationContractRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/UseOperationContractRule.java
@@ -767,7 +767,7 @@ public boolean isApplicable(Goal goal, PosInOccurrence pio) {
         JavaBlock postJavaBlock = JavaBlock.createJavaBlock(postSB);
         Modality modality = Modality.getModality(inst.modality.kind(), postJavaBlock);
         final Term normalPost = tb.apply(anonUpdate,
-            tb.prog(modality.kind(), modality.program(), inst.progPost.sub(0),
+            tb.prog(modality.kind(), modality.programBlock(), inst.progPost.sub(0),
                 TermLabelManager.instantiateLabels(termLabelState, services,
                     ruleApp.posInOccurrence(), this, ruleApp, postGoal, "PostModality", null,
                     tb.tf().createTerm(modality,
@@ -789,7 +789,7 @@ public boolean isApplicable(Goal goal, PosInOccurrence pio) {
         final Modality instantiatedModality =
             Modality.getModality(inst.modality.kind(), excJavaBlock);
         final Term originalExcPost = tb.apply(anonUpdate, tb.prog(instantiatedModality.kind(),
-            instantiatedModality.program(), inst.progPost.sub(0),
+            instantiatedModality.programBlock(), inst.progPost.sub(0),
             TermLabelManager.instantiateLabels(termLabelState, services, ruleApp.posInOccurrence(),
                 this, ruleApp, excPostGoal, "ExceptionalPostModality", null,
                 tb.tf().createTerm(instantiatedModality,
diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/InfFlowProgVarRenamer.java b/key.core/src/main/java/de/uka/ilkd/key/util/InfFlowProgVarRenamer.java
@@ -204,7 +204,7 @@ private Term applyRenamingsToPrograms(Term term,
             return null;
         } else if (term.op() instanceof Modality mod) {
             final JavaBlock renamedJavaBlock =
-                renameJavaBlock(progVarReplaceMap, mod.program().program(), services);
+                renameJavaBlock(progVarReplaceMap, mod.programBlock().program(), services);
             final Term[] appliedSubs = applyProgramRenamingsToSubs(term, progVarReplaceMap);
 
             return tf().createTerm(Modality.getModality(mod.kind(), renamedJavaBlock), appliedSubs,
diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java b/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java
@@ -1431,7 +1431,7 @@ private static HashSet<LocationVariable> getProgramLocationsHashSet(
             org.key_project.logic.Term programCounterTerm,
             Services services) {
         final var mod = (Modality) programCounterTerm.op();
-        final JavaProgramElement program = mod.program().program();
+        final JavaProgramElement program = mod.programBlock().program();
         if (program instanceof StatementBlock && (((StatementBlock) program).isEmpty()
                 || (((StatementBlock) program).getInnerMostMethodFrame() != null
                         && ((StatementBlock) program).getInnerMostMethodFrame().getBody()
diff --git a/key.ncore/src/main/java/org/key_project/logic/op/Modality.java b/key.ncore/src/main/java/org/key_project/logic/op/Modality.java
@@ -31,7 +31,7 @@ public final <K extends Kind> K kind() {
     /// The program contained in this modality.
     ///
     /// @return the program.
-    public abstract Program program();
+    public abstract Program programBlock();
 
     @Override
     public int getChildCount() {
@@ -42,7 +42,7 @@ public int getChildCount() {
     public SyntaxElement getChild(int n) {
         return switch (n) {
         case 0 -> kind;
-        case 1 -> program();
+        case 1 -> programBlock();
         default -> throw new IndexOutOfBoundsException(
             "Modality " + name() + " has only two children");
         };

Original file line number	Diff line number	Diff line change
`@@ -202,7 +202,7 @@ public ImmutableArray<QuantifiableVariable> varsBoundHere(int n) {`
`202`	`202`	`@Override`
`203`	`203`	`public @NonNull JavaBlock javaBlock() {`
`204`	`204`	`if (op instanceof Modality mod) {`
`205`		`- return mod.program();`
	`205`	`+ return mod.programBlock();`
`206`	`206`	`} else {`
`207`	`207`	`return JavaBlock.EMPTY_JAVABLOCK;`
`208`	`208`	`}`
Original file line number	Diff line number	Diff line change
`@@ -54,7 +54,7 @@ public <V> boolean equalsModThisProperty(Term term1, Term term2, V... v) {`
`54`	`54`	`}`
`55`	`55`
`56`	`56`	`if (term1.op() instanceof Modality mod1`
`57`		`- && !(mod1.program().equals(((Modality) (term2.op())).program()))) {`
	`57`	`+ && !(mod1.programBlock().equals(((Modality) (term2.op())).programBlock()))) {`
`58`	`58`	`return false;`
`59`	`59`	`}`
`60`	`60`
`@@ -88,7 +88,7 @@ public int hashCodeModThisProperty(Term term) {`
`88`	`88`	`this::hashCodeModThisProperty);`
`89`	`89`	`hashcode = hashcode * 17 + term.boundVars().hashCode();`
`90`	`90`	`hashcode =`
`91`		`- hashcode * 17 + (term.op() instanceof Modality mod ? mod.program().hashCode() : 3);`
	`91`	`+ hashcode * 17 + (term.op() instanceof Modality mod ? mod.programBlock().hashCode() : 3);`
`92`	`92`
`93`	`93`	`return hashcode;`
`94`	`94`	`}`
Original file line number	Diff line number	Diff line change
`@@ -12,6 +12,7 @@`
`12`	`12`	`import de.uka.ilkd.key.logic.Term;`
`13`	`13`	`import de.uka.ilkd.key.logic.sort.ProgramSVSort;`
`14`	`14`
	`15`	`+import org.jspecify.annotations.NonNull;`
`15`	`16`	`import org.key_project.logic.Name;`
`16`	`17`	`import org.key_project.logic.TermCreationException;`
`17`	`18`	`import org.key_project.logic.sort.Sort;`
`@@ -59,7 +60,8 @@ private Modality(JavaBlock prg, JavaModalityKind kind) {`
`59`	`60`	`}`
`60`	`61`
`61`	`62`	`@Override`
`62`		`- public JavaBlock program() {`
	`63`	`+ @NonNull`
	`64`	`+ public JavaBlock programBlock() {`
`63`	`65`	`return javaBlock;`
`64`	`66`	`}`
`65`	`67`
Original file line number	Diff line number	Diff line change
`@@ -1693,7 +1693,7 @@ public void printModalityTerm(String left, JavaBlock jb, String right, Term phi,`
`1693`	`1693`	`ta[i] = phi.sub(i);`
`1694`	`1694`	`}`
`1695`	`1695`	`final Modality m =`
`1696`		`- Modality.getModality((Modality.JavaModalityKind) o, mod.program());`
	`1696`	`+ Modality.getModality((Modality.JavaModalityKind) o, mod.programBlock());`
`1697`	`1697`	`final Term term = services.getTermFactory().createTerm(m, ta,`
`1698`	`1698`	`phi.boundVars(), null);`
`1699`	`1699`	`notationInfo.getNotation(m).print(term, this);`
Original file line number	Diff line number	Diff line change
`@@ -36,9 +36,9 @@ public void visit(Term visited) {`
`36`	`36`	`result.add(variable);`
`37`	`37`	`}`
`38`	`38`
`39`		`- if (visited.op() instanceof Modality mod && !mod.program().isEmpty()) {`
	`39`	`+ if (visited.op() instanceof Modality mod && !mod.programBlock().isEmpty()) {`
`40`	`40`	`ProgramVariableCollector pvc =`
`41`		`- new ProgramVariableCollector(mod.program().program(), services);`
	`41`	`+ new ProgramVariableCollector(mod.programBlock().program(), services);`
`42`	`42`	`pvc.start();`
`43`	`43`	`result.addAll(pvc.result());`
`44`	`44`	`}`
Original file line number	Diff line number	Diff line change
`@@ -358,7 +358,7 @@ private void populateNamespaces(Term term, NamespaceSet namespaces,`
`358`	`358`	`rootGoal.addProgramVariable(pv);`
`359`	`359`	`}`
`360`	`360`	`} else if (term.op() instanceof Modality mod) {`
`361`		`- final ProgramElement pe = mod.program().program();`
	`361`	`+ final ProgramElement pe = mod.programBlock().program();`
`362`	`362`	`final Services serv = rootGoal.proof().getServices();`
`363`	`363`	`final ImmutableSet<LocationVariable> freeProgVars =`
`364`	`364`	`MiscTools.getLocalIns(pe, serv).union(MiscTools.getLocalOuts(pe, serv));`