diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java index ae8e2bf013c..a6a66be472a 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java @@ -3,6 +3,10 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.symbolic_execution.rule; +import java.util.LinkedHashSet; +import java.util.List; +import java.util.Set; + import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.op.*; @@ -11,15 +15,13 @@ import de.uka.ilkd.key.rule.*; import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil; import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil; -import org.jspecify.annotations.NonNull; + import org.key_project.logic.Name; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.Pair; -import java.util.LinkedHashSet; -import java.util.List; -import java.util.Set; +import org.jspecify.annotations.NonNull; /** *

@@ -180,8 +182,9 @@ public ImmutableList apply(Goal goal, Services services, RuleApp ruleApp) Set resultTerms = new LinkedHashSet<>(); for (ResultsAndCondition conditionsAndResult : conditionsAndResultsMap) { Term conditionTerm = tb.and(conditionsAndResult.conditions()); - Term resultEqualityTerm = varFirst ? tb.equals(conditionsAndResult.result(), otherTerm) - : tb.equals(otherTerm, conditionsAndResult.result()); + Term resultEqualityTerm = + varFirst ? tb.equals(conditionsAndResult.result(), otherTerm) + : tb.equals(otherTerm, conditionsAndResult.result()); Term resultTerm = pio.isInAntec() ? tb.imp(conditionTerm, resultEqualityTerm) : tb.and(conditionTerm, resultEqualityTerm); resultTerms.add(resultTerm); diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/QuerySideProofRule.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/QuerySideProofRule.java index a88b20100c3..7e45277119d 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/QuerySideProofRule.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/QuerySideProofRule.java @@ -237,8 +237,9 @@ public ImmutableList apply(Goal goal, Services services, RuleApp ruleApp) if (pio.isTopLevel() || queryConditionTerm != null) { for (ResultsAndCondition conditionsAndResult : conditionsAndResultsMap) { Term conditionTerm = tb.and(conditionsAndResult.conditions()); - Term newEqualityTerm = varFirst ? tb.equals(varTerm, conditionsAndResult.result()) - : tb.equals(conditionsAndResult.result(), varTerm); + Term newEqualityTerm = + varFirst ? tb.equals(varTerm, conditionsAndResult.result()) + : tb.equals(conditionsAndResult.result(), varTerm); Term resultTerm = pio.isInAntec() ? tb.imp(conditionTerm, newEqualityTerm) : tb.and(conditionTerm, newEqualityTerm); if (queryConditionTerm != null) { diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionSideProofUtil.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionSideProofUtil.java index f26b338c655..3a4fb926956 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionSideProofUtil.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionSideProofUtil.java @@ -3,6 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.symbolic_execution.util; +import java.util.*; + import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.abstraction.KeYJavaType; import de.uka.ilkd.key.ldt.HeapLDT; @@ -33,6 +35,7 @@ import de.uka.ilkd.key.symbolic_execution.rule.AbstractSideProofRule.ResultsAndCondition; import de.uka.ilkd.key.util.ProofStarter; import de.uka.ilkd.key.util.SideProofUtil; + import org.key_project.logic.Name; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; @@ -40,8 +43,6 @@ import org.key_project.util.collection.Pair; import org.key_project.util.java.CollectionUtil; -import java.util.*; - /** * Provides utility methods for side proofs. * @@ -64,7 +65,7 @@ private SymbolicExecutionSideProofUtil() { * @return The general initial {@link Sequent}. */ public static Sequent computeGeneralSequentToProve(Sequent goalSequent, - SequentFormula currentSF) { + SequentFormula currentSF) { Sequent sequentToProve = Sequent.EMPTY_SEQUENT; for (SequentFormula sf : goalSequent.antecedent()) { if (sf != currentSF) { @@ -105,12 +106,12 @@ public static Sequent computeGeneralSequentToProve(Sequent goalSequent, * @throws ProofInputException Occurred Exception. */ public static List> computeResults(Services services, Proof proof, - ProofEnvironment sideProofEnvironment, Sequent sequentToProve, TermLabel label, - String description, String methodTreatment, String loopTreatment, String queryTreatment, - String splittingOption, boolean addNamesToServices) throws ProofInputException { + ProofEnvironment sideProofEnvironment, Sequent sequentToProve, TermLabel label, + String description, String methodTreatment, String loopTreatment, String queryTreatment, + String splittingOption, boolean addNamesToServices) throws ProofInputException { // Execute side proof ApplyStrategyInfo info = startSideProof(proof, sideProofEnvironment, sequentToProve, - methodTreatment, loopTreatment, queryTreatment, splittingOption); + methodTreatment, loopTreatment, queryTreatment, splittingOption); try { // Extract results and conditions from side proof List> conditionsAndResultsMap = new LinkedList<>(); @@ -176,11 +177,11 @@ public static List computeResultsAndConditions( throws ProofInputException { // Execute side proof ApplyStrategyInfo info = startSideProof(proof, sideProofEnvironment, sequentToProve, - methodTreatment, loopTreatment, queryTreatment, splittingOption); + methodTreatment, loopTreatment, queryTreatment, splittingOption); try { // Extract relevant things Set relevantThingsInSequentToProve = - extractRelevantThings(info.getProof().getServices(), sequentToProve); + extractRelevantThings(info.getProof().getServices(), sequentToProve); // Extract results and conditions from side proof List conditionsAndResultsMap = new LinkedList<>(); for (Goal resultGoal : info.getProof().openGoals()) { @@ -195,18 +196,18 @@ public static List computeResultsAndConditions( if (newPredicateIsSequentFormula) { if (Operator.opEquals(sf.formula().op(), operator)) { throw new IllegalStateException( - "Result predicate found in antecedent."); + "Result predicate found in antecedent."); } else { Term constructedResult = - constructResultIfContained(services, sf, operator); + constructResultIfContained(services, sf, operator); if (constructedResult != null) { throw new IllegalStateException( - "Result predicate found in antecedent."); + "Result predicate found in antecedent."); } } } if (!isIrrelevantCondition(services, sequentToProve, - relevantThingsInSequentToProve, sf)) { + relevantThingsInSequentToProve, sf)) { if (resultConditions.add(sf.formula()) && addNamesToServices) { addNewNamesToNamespace(services, sf.formula()); } @@ -217,7 +218,7 @@ public static List computeResultsAndConditions( if (Operator.opEquals(sf.formula().op(), operator)) { if (result != null) { throw new IllegalStateException( - "Result predicate found multiple times in succedent."); + "Result predicate found multiple times in succedent."); } result = sf.formula().sub(0); } @@ -226,14 +227,14 @@ public static List computeResultsAndConditions( if (constructedResult != null) { if (result != null) { throw new IllegalStateException( - "Result predicate found multiple times in succedent."); + "Result predicate found multiple times in succedent."); } result = constructedResult; } } if (result == null) { if (!isIrrelevantCondition(services, sequentToProve, - relevantThingsInSequentToProve, sf)) { + relevantThingsInSequentToProve, sf)) { if (resultConditions.add(services.getTermBuilder().not(sf.formula())) && addNamesToServices) { addNewNamesToNamespace(services, sf.formula()); @@ -244,7 +245,8 @@ public static List computeResultsAndConditions( if (result == null) { result = services.getTermBuilder().ff(); } - conditionsAndResultsMap.add(new ResultsAndCondition(result, resultConditions, resultGoal.node())); + conditionsAndResultsMap + .add(new ResultsAndCondition(result, resultConditions, resultGoal.node())); } return conditionsAndResultsMap; } finally { @@ -253,12 +255,12 @@ public static List computeResultsAndConditions( } private static Term constructResultIfContained(Services services, SequentFormula sf, - Operator operator) { + Operator operator) { return constructResultIfContained(services, sf.formula(), operator); } private static Term constructResultIfContained(Services services, Term term, - Operator operator) { + Operator operator) { if (Operator.opEquals(term.op(), operator)) { return term.sub(0); } else { @@ -278,8 +280,8 @@ private static Term constructResultIfContained(Services services, Term term, } } result = services.getTermFactory().createTerm(term.op(), - new ImmutableArray<>(newSubs), term.boundVars(), - term.getLabels()); + new ImmutableArray<>(newSubs), term.boundVars(), + term.getLabels()); } return result; } @@ -287,7 +289,7 @@ private static Term constructResultIfContained(Services services, Term term, private static boolean isOperatorASequentFormula(Sequent sequent, final Operator operator) { return CollectionUtil.search(sequent, - element -> Operator.opEquals(element.formula().op(), operator)) != null; + element -> Operator.opEquals(element.formula().op(), operator)) != null; } /** @@ -377,7 +379,7 @@ public boolean isContainsModalityOrQuery() { * @return The found relevant things. */ public static Set extractRelevantThings(final Services services, - Sequent sequentToProve) { + Sequent sequentToProve) { final Set result = new HashSet<>(); for (SequentFormula sf : sequentToProve) { sf.formula().execPreOrder((DefaultVisitor) visited -> { @@ -429,7 +431,7 @@ private static boolean isRelevantThing(Services services, Term term) { * {@link SequentFormula} is not a relevant condition. */ public static boolean isIrrelevantCondition(Services services, Sequent initialSequent, - Set relevantThingsInSequentToProve, SequentFormula sf) { + Set relevantThingsInSequentToProve, SequentFormula sf) { return initialSequent.antecedent().contains(sf) || initialSequent.succedent().contains(sf) || containsModalityOrQuery(sf) // isInOrOfAntecedent(initialSequent, sf) || || containsIrrelevantThings(services, sf, relevantThingsInSequentToProve); @@ -473,9 +475,9 @@ public static boolean isIrrelevantCondition(Services services, Sequent initialSe * {@link SequentFormula} contains no irrelevant things. */ public static boolean containsIrrelevantThings(Services services, SequentFormula sf, - Set relevantThings) { + Set relevantThings) { ContainsIrrelevantThingsVisitor visitor = - new ContainsIrrelevantThingsVisitor(services, relevantThings); + new ContainsIrrelevantThingsVisitor(services, relevantThings); sf.formula().execPostOrder(visitor); return visitor.isContainsIrrelevantThings(); } @@ -550,11 +552,11 @@ public boolean isContainsIrrelevantThings() { * @throws ProofInputException Occurred Exception */ public static ApplyStrategyInfo startSideProof(Proof proof, - ProofEnvironment sideProofEnvironment, Sequent sequentToProve) + ProofEnvironment sideProofEnvironment, Sequent sequentToProve) throws ProofInputException { return startSideProof(proof, sideProofEnvironment, sequentToProve, - StrategyProperties.METHOD_NONE, StrategyProperties.LOOP_NONE, - StrategyProperties.QUERY_OFF, StrategyProperties.SPLITTING_OFF); + StrategyProperties.METHOD_NONE, StrategyProperties.LOOP_NONE, + StrategyProperties.QUERY_OFF, StrategyProperties.SPLITTING_OFF); } /** @@ -567,12 +569,12 @@ public static ApplyStrategyInfo startSideProof(Proof proof, * @throws ProofInputException Occurred Exception */ public static ApplyStrategyInfo startSideProof(Proof proof, - ProofEnvironment sideProofEnvironment, Sequent sequentToProve, String methodTreatment, - String loopTreatment, String queryTreatment, String splittingOption) + ProofEnvironment sideProofEnvironment, Sequent sequentToProve, String methodTreatment, + String loopTreatment, String queryTreatment, String splittingOption) throws ProofInputException { ProofStarter starter = createSideProof(sideProofEnvironment, sequentToProve, null); return startSideProof(proof, starter, methodTreatment, loopTreatment, queryTreatment, - splittingOption); + splittingOption); } /** @@ -586,7 +588,7 @@ public static ApplyStrategyInfo startSideProof(Proof proof, * @throws ProofInputException Occurred Exception. */ public static ProofStarter createSideProof(ProofEnvironment sideProofEnvironment, - Sequent sequentToProve, String proofName) throws ProofInputException { + Sequent sequentToProve, String proofName) throws ProofInputException { return SideProofUtil.createSideProof(sideProofEnvironment, sequentToProve, proofName); } @@ -599,8 +601,8 @@ public static ProofStarter createSideProof(ProofEnvironment sideProofEnvironment * @return The site proof result. */ public static ApplyStrategyInfo startSideProof(Proof proof, ProofStarter starter, - String methodTreatment, String loopTreatment, String queryTreatment, - String splittingOption) { + String methodTreatment, String loopTreatment, String queryTreatment, + String splittingOption) { assert starter != null; starter.setMaxRuleApplications(10000); StrategyProperties sp = proof != null && !proof.isDisposed() @@ -613,7 +615,7 @@ public static ApplyStrategyInfo startSideProof(Proof proof, ProofStarter starter sp.setProperty(StrategyProperties.QUERY_OPTIONS_KEY, queryTreatment); sp.setProperty(StrategyProperties.SPLITTING_OPTIONS_KEY, splittingOption); sp.setProperty(StrategyProperties.QUANTIFIERS_OPTIONS_KEY, - StrategyProperties.QUANTIFIERS_NON_SPLITTING); + StrategyProperties.QUANTIFIERS_NON_SPLITTING); starter.setStrategyProperties(sp); // Execute proof in the current thread return starter.start(); @@ -660,8 +662,8 @@ public static Term extractOperatorTerm(ApplyStrategyInfo info, Operator operator assert info != null; if (info.getProof().openGoals().size() != 1) { throw new ProofInputException( - "Assumption that return value extraction has one goal does not hold because " - + info.getProof().openGoals().size() + " goals are available."); + "Assumption that return value extraction has one goal does not hold because " + + info.getProof().openGoals().size() + " goals are available."); } // Get node of open goal return extractOperatorTerm(info.getProof().openGoals().head(), operator); @@ -715,11 +717,11 @@ public static Term extractOperatorTerm(Node node, final Operator operator) { * {@link Proof} but with its own {@link OneStepSimplifier} instance. */ public static ProofEnvironment cloneProofEnvironmentWithOwnOneStepSimplifier(final Proof source, - final boolean useSimplifyTermProfile) { + final boolean useSimplifyTermProfile) { assert source != null; assert !source.isDisposed(); return cloneProofEnvironmentWithOwnOneStepSimplifier(source.getInitConfig(), - useSimplifyTermProfile); + useSimplifyTermProfile); } /** @@ -745,13 +747,13 @@ protected ImmutableList computeTermLabelConfiguration() Profile sourceProfile = sourceInitConfig.getProfile(); if (sourceProfile instanceof SymbolicExecutionJavaProfile) { ImmutableList result = - super.computeTermLabelConfiguration(); + super.computeTermLabelConfiguration(); // Make sure that the term labels of symbolic execution are also supported // by the new environment. result = result.prepend(SymbolicExecutionJavaProfile .getSymbolicExecutionTermLabelConfigurations( - SymbolicExecutionJavaProfile - .isTruthValueEvaluationEnabled(sourceInitConfig))); + SymbolicExecutionJavaProfile + .isTruthValueEvaluationEnabled(sourceInitConfig))); return result; } else { return super.computeTermLabelConfiguration(); @@ -765,13 +767,13 @@ protected ImmutableList computeTermLabelConfiguration() Profile sourceProfile = sourceInitConfig.getProfile(); if (sourceProfile instanceof SymbolicExecutionJavaProfile) { ImmutableList result = - super.computeTermLabelConfiguration(); + super.computeTermLabelConfiguration(); // Make sure that the term labels of symbolic execution are also supported // by the new environment. result = result.prepend(SymbolicExecutionJavaProfile .getSymbolicExecutionTermLabelConfigurations( - SymbolicExecutionJavaProfile - .isTruthValueEvaluationEnabled(sourceInitConfig))); + SymbolicExecutionJavaProfile + .isTruthValueEvaluationEnabled(sourceInitConfig))); return result; } else { return super.computeTermLabelConfiguration(); @@ -781,7 +783,7 @@ protected ImmutableList computeTermLabelConfiguration() } // Create new InitConfig final InitConfig initConfig = - new InitConfig(sourceInitConfig.getServices().copy(profile, false)); + new InitConfig(sourceInitConfig.getServices().copy(profile, false)); // Set modified taclet options in which runtime exceptions are banned. Choice runtimeExceptionTreatment = new Choice("ban", "runtimeExceptions"); ImmutableSet choices = SideProofUtil @@ -793,14 +795,14 @@ protected ImmutableList computeTermLabelConfiguration() : null; initConfig.setSettings(clonedSettings); initConfig.setTaclet2Builder( - (HashMap>) sourceInitConfig.getTaclet2Builder() - .clone()); + (HashMap>) sourceInitConfig.getTaclet2Builder() + .clone()); initConfig.setTaclets(sourceInitConfig.getTaclets()); // Create new ProofEnvironment and initialize it with values from initial one. ProofEnvironment env = new ProofEnvironment(initConfig); for (Taclet taclet : initConfig.activatedTaclets()) { initConfig.getJustifInfo().addJustification(taclet, - sourceJustiInfo.getJustification(taclet)); + sourceJustiInfo.getJustification(taclet)); } for (BuiltInRule rule : initConfig.builtInRules()) { RuleJustification origJusti = sourceJustiInfo.getJustification(rule); diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java b/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java index 23a70913479..bc34b6eaf8a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java @@ -77,7 +77,7 @@ public KeYEnvironment(U ui, InitConfig initConfig) { * @param initConfig The loaded project. */ public KeYEnvironment(U ui, InitConfig initConfig, Proof loadedProof, - @Nullable ProofScriptEntry proofScript, ReplayResult replayResult) { + @Nullable ProofScriptEntry proofScript, ReplayResult replayResult) { this.ui = ui; this.initConfig = initConfig; this.loadedProof = loadedProof; diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java index ed7bc2fa1f5..0ab8731d275 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java @@ -89,7 +89,7 @@ public static class File extends KeyAst { if (ctx.problem() != null && ctx.problem().proofScript() != null) { KeYParser.ProofScriptContext pctx = ctx.problem().proofScript(); Location location = new Location(url, - Position.newOneBased(pctx.ps.getLine(), pctx.ps.getCharPositionInLine())); + Position.newOneBased(pctx.ps.getLine(), pctx.ps.getCharPositionInLine())); String text = pctx.ps.getText(); return new ProofScriptEntry(StringUtil.trim(text, '"'), location); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java index 0f5cae49926..eb6ef17abb2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java @@ -21,13 +21,13 @@ import de.uka.ilkd.key.speclang.SLEnvInput; import de.uka.ilkd.key.util.ProgressMonitor; -import org.jspecify.annotations.Nullable; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableSet; import org.antlr.v4.runtime.CharStream; import org.antlr.v4.runtime.Token; import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java index a637f5fa1e9..e230cfe65d3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java @@ -3,6 +3,20 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.proof.io; +import java.io.ByteArrayInputStream; +import java.io.File; +import java.io.FileNotFoundException; +import java.io.IOException; +import java.lang.reflect.InvocationTargetException; +import java.lang.reflect.Method; +import java.nio.charset.StandardCharsets; +import java.nio.file.*; +import java.util.*; +import java.util.function.Consumer; +import java.util.stream.Collectors; +import java.util.stream.Stream; +import java.util.zip.ZipFile; + import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.nparser.KeYLexer; import de.uka.ilkd.key.nparser.ProofScriptEntry; @@ -22,28 +36,16 @@ import de.uka.ilkd.key.strategy.Strategy; import de.uka.ilkd.key.strategy.StrategyProperties; import de.uka.ilkd.key.util.ExceptionHandlerException; -import org.antlr.runtime.MismatchedTokenException; -import org.jspecify.annotations.Nullable; + import org.key_project.util.collection.Pair; import org.key_project.util.java.IOUtil; import org.key_project.util.reflection.ClassLoaderUtil; + +import org.antlr.runtime.MismatchedTokenException; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import java.io.ByteArrayInputStream; -import java.io.File; -import java.io.FileNotFoundException; -import java.io.IOException; -import java.lang.reflect.InvocationTargetException; -import java.lang.reflect.Method; -import java.nio.charset.StandardCharsets; -import java.nio.file.*; -import java.util.*; -import java.util.function.Consumer; -import java.util.stream.Collectors; -import java.util.stream.Stream; -import java.util.zip.ZipFile; - /** *

* This class provides the basic functionality to load something in KeY. The loading process is done @@ -196,7 +198,7 @@ public boolean hasErrors() { // format: (expected, found) mismatchErrors = new HashMap<>(); mismatchErrors.put(new Pair<>(KeYLexer.SEMI, KeYLexer.COMMA), - "there may be only one declaration per line"); + "there may be only one declaration per line"); missedErrors = new HashMap<>(); missedErrors.put(KeYLexer.RPAREN, "closing parenthesis"); @@ -222,19 +224,19 @@ public boolean hasErrors() { * the loaded {@link InitConfig}. */ public AbstractProblemLoader(File file, List classPath, File bootClassPath, - List includes, Profile profileOfNewProofs, boolean forceNewProfileOfNewProofs, - ProblemLoaderControl control, - boolean askUiToSelectAProofObligationIfNotDefinedByLoadedFile, - Properties poPropertiesToForce) { + List includes, Profile profileOfNewProofs, boolean forceNewProfileOfNewProofs, + ProblemLoaderControl control, + boolean askUiToSelectAProofObligationIfNotDefinedByLoadedFile, + Properties poPropertiesToForce) { this.file = file; this.classPath = classPath; this.bootClassPath = bootClassPath; this.control = control; this.profileOfNewProofs = - profileOfNewProofs != null ? profileOfNewProofs : AbstractProfile.getDefaultProfile(); + profileOfNewProofs != null ? profileOfNewProofs : AbstractProfile.getDefaultProfile(); this.forceNewProfileOfNewProofs = forceNewProfileOfNewProofs; this.askUiToSelectAProofObligationIfNotDefinedByLoadedFile = - askUiToSelectAProofObligationIfNotDefinedByLoadedFile; + askUiToSelectAProofObligationIfNotDefinedByLoadedFile; this.poPropertiesToForce = poPropertiesToForce; this.includes = includes; } @@ -308,14 +310,14 @@ protected void loadEnvironment() throws ProofInputException, IOException { LOGGER.info("Loading environment from " + file); envInput = createEnvInput(fileRepo); LOGGER.debug( - "Environment load took " + PerfScope.formatTime(System.nanoTime() - timeBeforeEnv)); + "Environment load took " + PerfScope.formatTime(System.nanoTime() - timeBeforeEnv)); problemInitializer = createProblemInitializer(fileRepo); var beforeInitConfig = System.nanoTime(); LOGGER.info("Creating init config"); initConfig = createInitConfig(); initConfig.setFileRepo(fileRepo); LOGGER.debug( - "Init config took " + PerfScope.formatTime(System.nanoTime() - beforeInitConfig)); + "Init config took " + PerfScope.formatTime(System.nanoTime() - beforeInitConfig)); if (!problemInitializer.getWarnings().isEmpty() && !ignoreWarnings) { control.reportWarnings(problemInitializer.getWarnings()); } @@ -343,7 +345,7 @@ protected void selectAndLoadProof(ProblemLoaderControl control, InitConfig initC * @see AbstractProblemLoader#load() */ protected void loadSelectedProof(LoadedPOContainer poContainer, ProofAggregate proofList, - Consumer callbackProofLoaded) + Consumer callbackProofLoaded) throws ProofInputException, ProblemLoaderException { // try to replay first proof proof = proofList.getProof(poContainer.getProofNum()); @@ -381,23 +383,23 @@ protected ProblemLoaderException recoverParserErrorMessage(Exception e) { if (c0 instanceof org.antlr.runtime.MismatchedTokenException) { if (c0 instanceof org.antlr.runtime.MissingTokenException) { final org.antlr.runtime.MissingTokenException mte = - (org.antlr.runtime.MissingTokenException) c0; + (org.antlr.runtime.MissingTokenException) c0; // TODO: other commonly missed tokens final String readable = missedErrors.get(mte.expecting); final String token = readable == null ? "token id " + mte.expecting : readable; final String msg = "Syntax error: missing " + token - + (occurrence == null ? "" : " at " + occurrence.getText()) + " statement (" - + mte.input.getSourceName() + ":" + mte.line + ")"; + + (occurrence == null ? "" : " at " + occurrence.getText()) + " statement (" + + mte.input.getSourceName() + ":" + mte.line + ")"; return new ProblemLoaderException(this, msg, mte); // TODO other ANTLR exceptions } else { final org.antlr.runtime.MismatchedTokenException mte = - (MismatchedTokenException) c0; + (MismatchedTokenException) c0; final String genericMsg = "expected " + mte.expecting + ", but found " + mte.c; final String readable = - mismatchErrors.get(new Pair<>(mte.expecting, mte.c)); + mismatchErrors.get(new Pair<>(mte.expecting, mte.c)); final String msg = "Syntax error: " + (readable == null ? genericMsg : readable) - + " (" + mte.input.getSourceName() + ":" + mte.line + ")"; + + " (" + mte.input.getSourceName() + ":" + mte.line + ")"; return new ProblemLoaderException(this, msg, mte); } } @@ -446,7 +448,7 @@ protected EnvInput createEnvInput(FileRepo fileRepo) throws IOException { ret = new SLEnvInput(".", classPath, bootClassPath, profileOfNewProofs, includes); } else { ret = new SLEnvInput(file.getParentFile().getAbsolutePath(), classPath, - bootClassPath, profileOfNewProofs, includes); + bootClassPath, profileOfNewProofs, includes); } ret.setJavaFile(file.getAbsolutePath()); ret.setIgnoreOtherJavaFiles(loadSingleJavaFile); @@ -506,26 +508,26 @@ protected EnvInput createEnvInput(FileRepo fileRepo) throws IOException { Path unzippedProof = tmpDir.resolve(proofFilename.toPath()); return new KeYUserProblemFile(unzippedProof.toString(), unzippedProof.toFile(), - fileRepo, control, profileOfNewProofs, false); + fileRepo, control, profileOfNewProofs, false); } else if (filename.endsWith(".key") || filename.endsWith(".proof") || filename.endsWith(".proof.gz")) { // KeY problem specification or saved proof return new KeYUserProblemFile(filename, file, fileRepo, control, profileOfNewProofs, - filename.endsWith(".proof.gz")); + filename.endsWith(".proof.gz")); } else if (file.isDirectory()) { // directory containing java sources, probably enriched // by specifications return new SLEnvInput(file.getPath(), classPath, bootClassPath, profileOfNewProofs, - includes); + includes); } else { if (filename.lastIndexOf('.') != -1) { throw new IllegalArgumentException("Unsupported file extension '" - + filename.substring(filename.lastIndexOf('.')) + "' of read-in file " - + filename + ". Allowed extensions are: .key, .proof, .java or " - + "complete directories."); + + filename.substring(filename.lastIndexOf('.')) + "' of read-in file " + + filename + ". Allowed extensions are: .key, .proof, .java or " + + "complete directories."); } else { throw new FileNotFoundException( - "File or directory\n\t " + filename + "\n not found."); + "File or directory\n\t " + filename + "\n not found."); } } } @@ -602,7 +604,7 @@ protected LoadedPOContainer createProofObligationContainer() throws IOException // Load proof obligation settings final Properties properties = new Properties(); properties.load( - new ByteArrayInputStream(proofObligation.getBytes(StandardCharsets.UTF_8))); + new ByteArrayInputStream(proofObligation.getBytes(StandardCharsets.UTF_8))); properties.setProperty(IPersistablePO.PROPERTY_FILENAME, file.getAbsolutePath()); if (poPropertiesToForce != null) { properties.putAll(poPropertiesToForce); @@ -610,7 +612,7 @@ protected LoadedPOContainer createProofObligationContainer() throws IOException String poClass = properties.getProperty(IPersistablePO.PROPERTY_CLASS); if (poClass == null || poClass.isEmpty()) { throw new IOException("Proof obligation class property \"" - + IPersistablePO.PROPERTY_CLASS + "\" is not defiend or empty."); + + IPersistablePO.PROPERTY_CLASS + "\" is not defiend or empty."); } try { // Try to instantiate proof obligation by calling static method: public static @@ -618,13 +620,13 @@ protected LoadedPOContainer createProofObligationContainer() throws IOException // IOException Class poClassInstance = ClassLoaderUtil.getClassforName(poClass); Method loadMethod = - poClassInstance.getMethod("loadFrom", InitConfig.class, Properties.class); + poClassInstance.getMethod("loadFrom", InitConfig.class, Properties.class); return (LoadedPOContainer) loadMethod.invoke(null, initConfig, properties); } catch (NoSuchMethodException | IllegalAccessException | IllegalArgumentException - | ClassNotFoundException e) { + | ClassNotFoundException e) { throw new IOException( - "Can't call static factory method \"loadFrom\" on class \"" + poClass + "\".", - e); + "Can't call static factory method \"loadFrom\" on class \"" + poClass + "\".", + e); } catch (InvocationTargetException e) { // Try to unwrap the inner exception as good as possible if (e.getCause() instanceof IOException) { @@ -652,7 +654,7 @@ protected LoadedPOContainer createProofObligationContainer() throws IOException protected ProofAggregate createProof(LoadedPOContainer poContainer) throws ProofInputException { ProofAggregate proofList = - problemInitializer.startProver(initConfig, poContainer.getProofOblInput()); + problemInitializer.startProver(initConfig, poContainer.getProofOblInput()); for (Proof p : proofList.getProofs()) { // register proof @@ -707,7 +709,7 @@ private ReplayResult replayProof(Proof proof) { assert envInput instanceof KeYUserProblemFile; IntermediatePresentationProofFileParser parser = - new IntermediatePresentationProofFileParser(proof); + new IntermediatePresentationProofFileParser(proof); problemInitializer.tryReadProof(parser, (KeYUserProblemFile) envInput); parserResult = parser.getResult(); @@ -718,14 +720,14 @@ private ReplayResult replayProof(Proof proof) { // able to load proofs that used it even if the user has currently // turned OSS off. StrategyProperties newProps = - proof.getSettings().getStrategySettings().getActiveStrategyProperties(); + proof.getSettings().getStrategySettings().getActiveStrategyProperties(); newProps.setProperty(StrategyProperties.OSS_OPTIONS_KEY, StrategyProperties.OSS_ON); Strategy.updateStrategySettings(proof, newProps); OneStepSimplifier.refreshOSS(proof); replayer = new IntermediateProofReplayer(this, proof, parserResult); replayResult = - replayer.replay(problemInitializer.getListener(), problemInitializer.getProgMon()); + replayer.replay(problemInitializer.getListener(), problemInitializer.getProgMon()); lastTouchedNode = replayResult.getLastSelectedGoal() != null ? replayResult.getLastSelectedGoal().node() @@ -746,13 +748,13 @@ private ReplayResult replayProof(Proof proof) { } status += (status.isEmpty() ? "Proof replayed successfully." : "\n\n") + (replayResult != null ? replayResult.getStatus() - : "Error while loading proof."); + : "Error while loading proof."); if (replayResult != null) { errors.addAll(replayResult.getErrors()); } StrategyProperties newProps = - proof.getSettings().getStrategySettings().getActiveStrategyProperties(); + proof.getSettings().getStrategySettings().getActiveStrategyProperties(); newProps.setProperty(StrategyProperties.OSS_OPTIONS_KEY, ossStatus); Strategy.updateStrategySettings(proof, newProps); OneStepSimplifier.refreshOSS(proof); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java index 70d6ea8dbdd..766d5b2a6c2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java @@ -111,7 +111,7 @@ public class IntermediateProofReplayer { private final LinkedList> queue = new LinkedList<>(); - public record PartnerNode(Node first, PosInOccurrence second, NodeIntermediate third){} + public record PartnerNode(Node first, PosInOccurrence second, NodeIntermediate third) {} /** Maps join node IDs to previously seen join partners */ private final HashMap> joinPartnerNodes = new HashMap<>(); @@ -265,7 +265,7 @@ public Result replay(ProblemInitializer.ProblemInitializerListener listener, if (appInterm instanceof MergeAppIntermediate joinAppInterm) { HashSet partnerNodesInfo = - joinPartnerNodes.get(((MergeAppIntermediate) appInterm).getId()); + joinPartnerNodes.get(((MergeAppIntermediate) appInterm).getId()); if (partnerNodesInfo == null || partnerNodesInfo.size() < joinAppInterm.getNrPartners()) { @@ -804,12 +804,12 @@ private MergeRuleBuiltInRuleApp instantiateJoinApp(final MergeAppIntermediate jo ImmutableList joinPartners = ImmutableSLList.nil(); for (PartnerNode partnerNodeInfo : partnerNodesInfo) { - var ownSEState = + var ownSEState = sequentToSETriple(currNode, joinApp.posInOccurrence(), services); var partnerSEState = sequentToSETriple(partnerNodeInfo.first, partnerNodeInfo.second, services); - assert ownSEState.third().equals(partnerSEState.third()) + assert ownSEState.programCounter().equals(partnerSEState.programCounter()) : "Cannot merge incompatible program counters"; joinPartners = joinPartners.append( diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java index 8748007d5de..868ec0a682b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java @@ -3,6 +3,11 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.proof.mgt; +import java.net.URI; +import java.util.*; +import java.util.Map.Entry; +import java.util.function.UnaryOperator; + import de.uka.ilkd.key.java.JavaInfo; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.Statement; @@ -29,18 +34,15 @@ import de.uka.ilkd.key.speclang.jml.translation.ProgramVariableCollection; import de.uka.ilkd.key.speclang.translation.SLTranslationException; import de.uka.ilkd.key.util.MiscTools; -import org.jspecify.annotations.Nullable; + import org.key_project.logic.Name; import org.key_project.logic.sort.Sort; import org.key_project.util.collection.*; + +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import java.net.URI; -import java.util.*; -import java.util.Map.Entry; -import java.util.function.UnaryOperator; - /** * Central storage for all specification elements, such as contracts, class axioms, and loop * invariants. Provides methods for adding such elements to the repository, and for retrieving them @@ -61,29 +63,39 @@ public final class SpecificationRepository { private final ContractFactory cf; private final Map, ImmutableSet> contracts = - new LinkedHashMap<>(); + new LinkedHashMap<>(); private final Map, ImmutableSet> operationContracts = - new LinkedHashMap<>(); + new LinkedHashMap<>(); private final Map, ImmutableSet> wdChecks = - new LinkedHashMap<>(); + new LinkedHashMap<>(); private final Map contractsByName = new LinkedHashMap<>(); - private final Map> contractTargets = new LinkedHashMap<>(); + private final Map> contractTargets = + new LinkedHashMap<>(); private final Map> invs = new LinkedHashMap<>(); private final Map> axioms = new LinkedHashMap<>(); - private final Map> initiallyClauses = new LinkedHashMap<>(); + private final Map> initiallyClauses = + new LinkedHashMap<>(); private final Map> proofs = new LinkedHashMap<>(); - private final Map, LoopSpecification> loopInvs = new LinkedHashMap<>(); - private final Map> blockContracts = new LinkedHashMap<>(); - private final Map> loopContracts = new LinkedHashMap<>(); + private final Map, LoopSpecification> loopInvs = + new LinkedHashMap<>(); + private final Map> blockContracts = + new LinkedHashMap<>(); + private final Map> loopContracts = + new LinkedHashMap<>(); /** * A map which relates each loop statement its starting line number and set of loop contracts. */ - private final Map, ImmutableSet> loopContractsOnLoops = new LinkedHashMap<>(); - private final Map> mergeContracts = new LinkedHashMap<>(); - private final Map unlimitedToLimited = new LinkedHashMap<>(); - private final Map limitedToUnlimited = new LinkedHashMap<>(); - private final Map> unlimitedToLimitTaclets = new LinkedHashMap<>(); + private final Map, ImmutableSet> loopContractsOnLoops = + new LinkedHashMap<>(); + private final Map> mergeContracts = + new LinkedHashMap<>(); + private final Map unlimitedToLimited = + new LinkedHashMap<>(); + private final Map limitedToUnlimited = + new LinkedHashMap<>(); + private final Map> unlimitedToLimitTaclets = + new LinkedHashMap<>(); /** *

@@ -98,13 +110,13 @@ public final class SpecificationRepository { *

*/ private final Map> allClassAxiomsCache = - new LinkedHashMap<>(); + new LinkedHashMap<>(); private final Services services; private final TermBuilder tb; private final Map contractCounters = - new de.uka.ilkd.key.util.LinkedHashMap<>(); + new de.uka.ilkd.key.util.LinkedHashMap<>(); public SpecificationRepository(Services services) { this.services = services; @@ -131,7 +143,7 @@ private static String getUniqueNameForObserver(IObserverFunction obs) { } private static Taclet getLimitedToUnlimitedTaclet(IObserverFunction limited, - IObserverFunction unlimited, TermServices services) { + IObserverFunction unlimited, TermServices services) { final TermBuilder tb = services.getTermBuilder(); assert limited.arity() == unlimited.arity(); @@ -139,7 +151,7 @@ private static Taclet getLimitedToUnlimitedTaclet(IObserverFunction limited, final Term[] subs = new Term[limited.arity()]; for (int i = 0; i < subs.length; i++) { final SchemaVariable argSV = SchemaVariableFactory.createTermSV(new Name("t" + i), - limited.argSort(i), false, false); + limited.argSort(i), false, false); subs[i] = tb.var(argSV); } final Term limitedTerm = tb.func(limited, subs); @@ -149,14 +161,14 @@ private static Taclet getLimitedToUnlimitedTaclet(IObserverFunction limited, final RewriteTacletBuilder tacletBuilder = new RewriteTacletBuilder<>(); tacletBuilder.setFind(limitedTerm); tacletBuilder.addTacletGoalTemplate(new RewriteTacletGoalTemplate(Sequent.EMPTY_SEQUENT, - ImmutableSLList.nil(), unlimitedTerm)); + ImmutableSLList.nil(), unlimitedTerm)); tacletBuilder.setName( - MiscTools.toValidTacletName("unlimit " + getUniqueNameForObserver(unlimited))); + MiscTools.toValidTacletName("unlimit " + getUniqueNameForObserver(unlimited))); return tacletBuilder.getTaclet(); } private static Taclet getUnlimitedToLimitedTaclet(IObserverFunction limited, - IObserverFunction unlimited, TermServices services) { + IObserverFunction unlimited, TermServices services) { assert limited.arity() == unlimited.arity(); final TermBuilder tb = services.getTermBuilder(); @@ -164,7 +176,7 @@ private static Taclet getUnlimitedToLimitedTaclet(IObserverFunction limited, final Term[] subs = new Term[limited.arity()]; for (int i = 0; i < subs.length; i++) { final SchemaVariable argSV = SchemaVariableFactory.createTermSV(new Name("t" + i), - limited.argSort(i), false, false); + limited.argSort(i), false, false); subs[i] = tb.var(argSV); } final Term limitedTerm = tb.func(limited, subs); @@ -175,12 +187,12 @@ private static Taclet getUnlimitedToLimitedTaclet(IObserverFunction limited, tacletBuilder.setFind(tb.func(unlimited, subs)); final SequentFormula cf = new SequentFormula(tb.equals(limitedTerm, unlimitedTerm)); final Sequent addedSeq = - Sequent.createAnteSequent(Semisequent.EMPTY_SEMISEQUENT.insertFirst(cf).semisequent()); + Sequent.createAnteSequent(Semisequent.EMPTY_SEMISEQUENT.insertFirst(cf).semisequent()); tacletBuilder.addTacletGoalTemplate(new RewriteTacletGoalTemplate(addedSeq, - ImmutableSLList.nil(), tb.func(unlimited, subs))); + ImmutableSLList.nil(), tb.func(unlimited, subs))); tacletBuilder.setApplicationRestriction(RewriteTaclet.IN_SEQUENT_STATE); tacletBuilder.setName( - MiscTools.toValidTacletName("limit " + getUniqueNameForObserver(unlimited))); + MiscTools.toValidTacletName("limit " + getUniqueNameForObserver(unlimited))); tacletBuilder.addRuleSet(new RuleSet(new Name("limitObserver"))); return tacletBuilder.getTaclet(); @@ -211,9 +223,8 @@ private IObserverFunction getCanonicalFormForKJT(IObserverFunction obs, KeYJavaT final String name = pm.getMethodDeclaration().getName(); final int numParams = pm.getParameterDeclarationCount(); final ImmutableList candidatePMs = - services.getJavaInfo().getAllProgramMethods(kjt); - outer: - for (IProgramMethod candidatePM : candidatePMs) { + services.getJavaInfo().getAllProgramMethods(kjt); + outer: for (IProgramMethod candidatePM : candidatePMs) { if (candidatePM.getMethodDeclaration().getName().equals(name) && candidatePM.getParameterDeclarationCount() == numParams) { for (int i = 0; i < numParams; i++) { @@ -240,7 +251,7 @@ private IObserverFunction getCanonicalFormForKJT(IObserverFunction obs, KeYJavaT } private ImmutableSet> getOverridingMethods(KeYJavaType kjt, - IProgramMethod pm) { + IProgramMethod pm) { ImmutableList> result = ImmutableSLList.nil(); // static methods and constructors are not overriden @@ -260,7 +271,7 @@ private ImmutableSet> getOverridingMethods( } public ImmutableSet> getOverridingTargets(KeYJavaType kjt, - IObserverFunction target) { + IObserverFunction target) { if (target instanceof IProgramMethod) { return getOverridingMethods(kjt, (IProgramMethod) target); } else { @@ -351,19 +362,19 @@ assert getCanonicalFormForKJT(contract.getTarget(), contract.getKJT()) private void registerContract(Contract contract) { final Pair target = - new Pair<>(contract.getKJT(), contract.getTarget()); + new Pair<>(contract.getKJT(), contract.getTarget()); registerContract(contract, target); } private void registerContract(Contract contract, - final ImmutableSet> targets) { + final ImmutableSet> targets) { for (Pair impl : targets) { registerContract(contract, impl); } } private void registerContract(Contract contract, - Pair targetPair) { + Pair targetPair) { LOGGER.trace("Contract registered {}", contract); if (!WellDefinednessCheck.isOn() && contract instanceof WellDefinednessCheck) { return; @@ -376,30 +387,30 @@ private void registerContract(Contract contract, : "Tried to add a contract with a non-unique name: " + name; assert !name.contains(CONTRACT_COMBINATION_MARKER) : "Tried to add a contract with a name containing the" + " reserved character " - + CONTRACT_COMBINATION_MARKER + ": " + name; + + CONTRACT_COMBINATION_MARKER + ": " + name; assert contract.id() != Contract.INVALID_ID : "Tried to add a contract with an invalid id!"; contracts.put(targetPair, getContracts(targetKJT, targetMethod).add(contract)); if (contract instanceof FunctionalOperationContract) { operationContracts.put(new Pair<>(targetKJT, (IProgramMethod) targetMethod), - getOperationContracts(targetKJT, (IProgramMethod) targetMethod) - .add((FunctionalOperationContract) contract)); + getOperationContracts(targetKJT, (IProgramMethod) targetMethod) + .add((FunctionalOperationContract) contract)); // Create new well-definedness check final MethodWellDefinedness mwd = - new MethodWellDefinedness((FunctionalOperationContract) contract, services); + new MethodWellDefinedness((FunctionalOperationContract) contract, services); registerContract(mwd); } else if (contract instanceof DependencyContract && contract.getOrigVars().atPres.isEmpty() && targetMethod.getContainerType() - .equals(services.getJavaInfo().getJavaLangObject())) { + .equals(services.getJavaInfo().getJavaLangObject())) { // Create or extend a well-definedness check for a class invariant final Term deps = - contract.getAccessible(services.getTypeConverter().getHeapLDT().getHeap()); + contract.getAccessible(services.getTypeConverter().getHeapLDT().getHeap()); final Term mby = contract.getMby(); final String invName = "JML model class invariant in " + targetKJT.getName(); final ClassInvariant inv = new ClassInvariantImpl(invName, invName, targetKJT, - contract.getVisibility(), tb.tt(), contract.getOrigVars().self); + contract.getVisibility(), tb.tt(), contract.getOrigVars().self); ClassWellDefinedness cwd = - new ClassWellDefinedness(inv, targetMethod, deps, mby, services); + new ClassWellDefinedness(inv, targetMethod, deps, mby, services); final ImmutableSet cwds = getWdClassChecks(targetKJT); if (!cwds.isEmpty()) { assert cwds.size() == 1; @@ -413,9 +424,9 @@ private void registerContract(Contract contract, && contract.getOrigVars().atPres.isEmpty()) { // Create or extend a well-definedness check for a model field MethodWellDefinedness mwd = - new MethodWellDefinedness((DependencyContract) contract, services); + new MethodWellDefinedness((DependencyContract) contract, services); final ImmutableSet mwds = - getWdMethodChecks(targetKJT, targetMethod); + getWdMethodChecks(targetKJT, targetMethod); if (!mwds.isEmpty()) { assert mwds.size() == 1; final MethodWellDefinedness oldMwd = mwds.iterator().next(); @@ -441,12 +452,12 @@ private void unregisterContract(Contract contract) { contracts.put(tp, contracts.get(tp).remove(contract)); if (contract instanceof FunctionalOperationContract) { final Pair tp2 = - new Pair<>(tp.first, (IProgramMethod) tp.second); + new Pair<>(tp.first, (IProgramMethod) tp.second); operationContracts.put(tp2, - operationContracts.get(tp2).remove((FunctionalOperationContract) contract)); + operationContracts.get(tp2).remove((FunctionalOperationContract) contract)); if (!getWdChecks(contract.getKJT(), contract.getTarget()).isEmpty()) { ImmutableSet wdcs = - getWdChecks(contract.getKJT(), contract.getTarget()); + getWdChecks(contract.getKJT(), contract.getTarget()); for (WellDefinednessCheck wdc : wdcs) { if (wdc instanceof MethodWellDefinedness && ((MethodWellDefinedness) wdc).getMethodContract().equals(contract)) { @@ -478,7 +489,7 @@ private void createContractsFromInitiallyClause(InitiallyClause inv, KeYJavaType if (!JMLInfoExtractor.isHelper(pm)) { final ImmutableSet oldContracts = getContracts(kjt, pm); ImmutableSet oldFuncContracts = - DefaultImmutableSet.nil(); + DefaultImmutableSet.nil(); for (Contract old : oldContracts) { if (old instanceof FunctionalOperationContract) { oldFuncContracts = oldFuncContracts.add((FunctionalOperationContract) old); @@ -530,7 +541,7 @@ private static ImmutableSet removeWdChecks(ImmutableSet cont */ private void registerWdCheck(WellDefinednessCheck check) { ImmutableSet checks = - getWdChecks(check.getKJT(), check.getTarget()).add(check); + getWdChecks(check.getKJT(), check.getTarget()).add(check); wdChecks.put(new Pair<>(check.getKJT(), check.getTarget()), checks); } @@ -542,7 +553,7 @@ private void registerWdCheck(WellDefinednessCheck check) { */ private void unregisterWdCheck(WellDefinednessCheck check) { wdChecks.put(new Pair<>(check.getKJT(), check.getTarget()), - getWdChecks(check.getKJT(), check.getTarget()).remove(check)); + getWdChecks(check.getKJT(), check.getTarget()).remove(check)); } /** @@ -563,7 +574,7 @@ private ImmutableSet getWdChecks(KeYJavaType kjt) { * Returns all registered (atomic) well-definedness checks for the passed target and kjt. */ private ImmutableSet getWdChecks(KeYJavaType kjt, - IObserverFunction target) { + IObserverFunction target) { assert kjt != null; assert target != null; target = getCanonicalFormForKJT(target, kjt); @@ -603,7 +614,7 @@ private ImmutableSet getWdMethodChecks(KeYJavaType kjt) { * Returns all registered (atomic) well-definedness method checks for the passed target and kjt. */ private ImmutableSet getWdMethodChecks(KeYJavaType kjt, - IObserverFunction target) { + IObserverFunction target) { assert kjt != null; assert target != null; ImmutableSet result = DefaultImmutableSet.nil(); @@ -638,7 +649,7 @@ private ImmutableSet getWdClassChecks(KeYJavaType kjt) { */ @SuppressWarnings("unchecked") private void mapValueSets(Map> map, - UnaryOperator op, Services services) { + UnaryOperator op, Services services) { for (Entry> entry : map.entrySet()) { final K key = entry.getKey(); final ImmutableSet oldSet = entry.getValue(); @@ -669,7 +680,7 @@ private void mapValueSets(Map void mapValues(Map map, - UnaryOperator op, Services services) { + UnaryOperator op, Services services) { for (Entry entry : map.entrySet()) { final K key = entry.getKey(); final V oldContract = entry.getValue(); @@ -725,10 +736,10 @@ public ImmutableSet getAllContracts() { */ public ImmutableSet getContracts(KeYJavaType kjt, IObserverFunction target) { target = - getCanonicalFormForKJT(Objects.requireNonNull(target), Objects.requireNonNull(kjt)); + getCanonicalFormForKJT(Objects.requireNonNull(target), Objects.requireNonNull(kjt)); final Pair pair = new Pair<>(kjt, target); final ImmutableSet result = - WellDefinednessCheck.isOn() ? contracts.get(pair) : removeWdChecks(contracts.get(pair)); + WellDefinednessCheck.isOn() ? contracts.get(pair) : removeWdChecks(contracts.get(pair)); return result == null ? DefaultImmutableSet.nil() : result; } @@ -736,7 +747,7 @@ public ImmutableSet getContracts(KeYJavaType kjt, IObserverFunction ta * Returns all registered (atomic) operation contracts for the passed operation. */ public ImmutableSet getOperationContracts(KeYJavaType kjt, - IProgramMethod pm) { + IProgramMethod pm) { pm = (IProgramMethod) getCanonicalFormForKJT(pm, kjt); final Pair pair = new Pair<>(kjt, pm); final ImmutableSet result = operationContracts.get(pair); @@ -748,14 +759,14 @@ public ImmutableSet getOperationContracts(KeYJavaTy * the passed modality. */ public ImmutableSet getOperationContracts(KeYJavaType kjt, - IProgramMethod pm, Modality.JavaModalityKind modalityKind) { + IProgramMethod pm, Modality.JavaModalityKind modalityKind) { ImmutableSet result = getOperationContracts(kjt, pm); final boolean transactionModality = - modalityKind.transaction(); + modalityKind.transaction(); final Modality.JavaModalityKind matchModality = transactionModality ? ((modalityKind == Modality.JavaModalityKind.DIA_TRANSACTION) - ? Modality.JavaModalityKind.DIA - : Modality.JavaModalityKind.BOX) + ? Modality.JavaModalityKind.DIA + : Modality.JavaModalityKind.BOX) : modalityKind; for (FunctionalOperationContract contract : result) { if (!contract.getModalityKind().equals(matchModality) @@ -782,7 +793,7 @@ public Contract getContractByName(String name) { ImmutableSet baseContracts = DefaultImmutableSet.nil(); for (String baseName : baseNames) { FunctionalOperationContract baseContract = - (FunctionalOperationContract) contractsByName.get(baseName); + (FunctionalOperationContract) contractsByName.get(baseName); if (baseContract == null) { return null; } @@ -799,7 +810,7 @@ public Contract getContractByName(String name) { public ImmutableSet getInheritedContracts(Contract contract) { ImmutableSet result = DefaultImmutableSet.nil().add(contract); final ImmutableSet> subs = - getOverridingTargets(contract.getKJT(), contract.getTarget()); + getOverridingTargets(contract.getKJT(), contract.getTarget()); for (Pair sub : subs) { for (Contract subContract : getContracts(sub.first, sub.second)) { if (subContract.id() == contract.id()) { @@ -839,13 +850,13 @@ public void addContract(Contract contract) { // register and inherit final ImmutableSet> impls = - getOverridingTargets(contract.getKJT(), contract.getTarget()) - .add(new Pair<>(contract.getKJT(), contract.getTarget())); + getOverridingTargets(contract.getKJT(), contract.getTarget()) + .add(new Pair<>(contract.getKJT(), contract.getTarget())); registerContract(contract, impls); if (!contractTargets.get(contract.getKJT()).contains(contract.getTarget())) { throw new IllegalStateException( - "target " + contract.getTarget() + " missing for contract " + contract); + "target " + contract.getTarget() + " missing for contract " + contract); } } @@ -878,7 +889,7 @@ public FunctionalOperationContract combineOperationContracts( // sort contracts alphabetically (for determinism) FunctionalOperationContract[] contractsArray = - toCombine.toArray(new FunctionalOperationContract[toCombine.size()]); + toCombine.toArray(new FunctionalOperationContract[toCombine.size()]); Arrays.sort(contractsArray, Comparator.comparing(SpecificationElement::getName)); return cf.union(contractsArray); @@ -925,7 +936,7 @@ public void addClassInvariant(ClassInvariant inv) { ClassWellDefinedness cwd = cwds.iterator().next(); unregisterContract(cwd); cwd = cwd.combine(new ClassWellDefinedness(inv, cwd.getTarget(), null, null, services), - services); + services); registerContract(cwd); } @@ -941,13 +952,13 @@ public void addClassInvariant(ClassInvariant inv) { for (KeYJavaType sub : subs) { ClassInvariant subInv = inv.setKJT(sub); final IObserverFunction subTarget = - subInv.isStatic() ? services.getJavaInfo().getStaticInv(sub) - : services.getJavaInfo().getInv(); + subInv.isStatic() ? services.getJavaInfo().getStaticInv(sub) + : services.getJavaInfo().getInv(); invs.put(sub, getClassInvariants(sub).add(subInv)); final ImmutableSet subCwds = getWdClassChecks(sub); if (subCwds.isEmpty()) { registerContract( - new ClassWellDefinedness(subInv, subTarget, null, null, services)); + new ClassWellDefinedness(subInv, subTarget, null, null, services)); } else { for (ClassWellDefinedness cwd : subCwds) { unregisterContract(cwd); @@ -980,7 +991,7 @@ public void createContractsFromInitiallyClauses() throws SLTranslationException createContractsFromInitiallyClause(inv, kjt); if (VisibilityModifier.allowsInheritance(inv.getVisibility())) { final ImmutableList subs = - services.getJavaInfo().getAllSubtypes(kjt); + services.getJavaInfo().getAllSubtypes(kjt); for (KeYJavaType sub : subs) { createContractsFromInitiallyClause(inv, sub); } @@ -1062,7 +1073,7 @@ public ImmutableSet getClassAxioms(KeYJavaType selfKjt) { staticInvDef = tb.and(staticInvDef, inv.getInv(null, services)); } else { freeStaticInvDef = - tb.and(freeStaticInvDef, inv.getInv(selfVar, services)); + tb.and(freeStaticInvDef, inv.getInv(selfVar, services)); } } } @@ -1070,9 +1081,9 @@ public ImmutableSet getClassAxioms(KeYJavaType selfKjt) { invDef = tb.tf().createTerm(Equality.EQV, tb.inv(tb.var(selfVar)), invDef); staticInvDef = tb.tf().createTerm(Equality.EQV, tb.staticInv(kjt), staticInvDef); freeInvDef = tb.tf().createTerm(Equality.EQV, - tb.invFree(tb.var(selfVar)), freeInvDef); + tb.invFree(tb.var(selfVar)), freeInvDef); freeStaticInvDef = tb.tf().createTerm(Equality.EQV, - tb.staticInvFree(kjt), freeStaticInvDef); + tb.staticInvFree(kjt), freeStaticInvDef); final IObserverFunction invSymbol = services.getJavaInfo().getInv(); final IObserverFunction staticInvSymbol = services.getJavaInfo().getStaticInv(kjt); @@ -1081,24 +1092,24 @@ public ImmutableSet getClassAxioms(KeYJavaType selfKjt) { .getStaticInvFree(kjt); final ClassAxiom invRepresentsAxiom = - new RepresentsAxiom("Class invariant axiom for " + kjt.getFullName(), invSymbol, - kjt, new Private(), null, invDef, selfVar, ImmutableSLList.nil(), null); + new RepresentsAxiom("Class invariant axiom for " + kjt.getFullName(), invSymbol, + kjt, new Private(), null, invDef, selfVar, ImmutableSLList.nil(), null); result = result.add(invRepresentsAxiom); final ClassAxiom staticInvRepresentsAxiom = new RepresentsAxiom( - "Static class invariant axiom for " + kjt.getFullName(), staticInvSymbol, kjt, - new Private(), null, staticInvDef, null, ImmutableSLList.nil(), null); + "Static class invariant axiom for " + kjt.getFullName(), staticInvSymbol, kjt, + new Private(), null, staticInvDef, null, ImmutableSLList.nil(), null); result = result.add(staticInvRepresentsAxiom); final ClassAxiom invFreeRepresentsAxiom = new RepresentsAxiom( - "Free class invariant axiom for " + kjt.getFullName(), freeInvSymbol, kjt, - new Private(), null, freeInvDef, selfVar, ImmutableSLList.nil(), null); + "Free class invariant axiom for " + kjt.getFullName(), freeInvSymbol, kjt, + new Private(), null, freeInvDef, selfVar, ImmutableSLList.nil(), null); result = result.add(invFreeRepresentsAxiom); final ClassAxiom staticFreeInvRepresentsAxiom = new RepresentsAxiom( - "Free static class invariant axiom for " + kjt.getFullName(), - freeStaticInvSymbol, kjt, new Private(), null, freeStaticInvDef, null, - ImmutableSLList.nil(), null); + "Free static class invariant axiom for " + kjt.getFullName(), + freeStaticInvSymbol, kjt, new Private(), null, freeStaticInvDef, null, + ImmutableSLList.nil(), null); result = result.add(staticFreeInvRepresentsAxiom); } @@ -1114,7 +1125,7 @@ freeStaticInvSymbol, kjt, new Private(), null, freeStaticInvDef, null, } final ClassAxiom queryAxiom = new QueryAxiom("Query axiom for " + pm.getName() - + "_" + sb + " in " + selfKjt.getFullName(), pm, selfKjt); + + "_" + sb + " in " + selfKjt.getFullName(), pm, selfKjt); result = result.add(queryAxiom); } } @@ -1143,7 +1154,7 @@ private ImmutableSet getModelMethodAxioms() { List heaps = HeapContext.getModHeaps(services, false); for (LocationVariable heap : heaps) { atPreVars.put(heap, - tb.atPreVar(heap.name().toString(), heap.sort(), false)); + tb.atPreVar(heap.name().toString(), heap.sort(), false)); } ProgramVariable resultVar = tb.resultVar(pm, false); @@ -1152,10 +1163,10 @@ private ImmutableSet getModelMethodAxioms() { // We need to construct an inheritance chain of contracts // starting at the bottom ImmutableList lookupContracts = - ImmutableSLList.nil(); + ImmutableSLList.nil(); ImmutableSet cs = getOperationContracts(kjt, pm); ImmutableList superTypes = - services.getJavaInfo().getAllSupertypes(kjt); + services.getJavaInfo().getAllSupertypes(kjt); for (KeYJavaType superType : superTypes) { for (FunctionalOperationContract fop : cs) { if (fop.getSpecifiedIn().equals(superType)) { @@ -1165,9 +1176,9 @@ private ImmutableSet getModelMethodAxioms() { } for (FunctionalOperationContract fop : lookupContracts) { Term representsFromContract = fop.getRepresentsAxiom(heaps.get(0), selfVar, - paramVars, tb.resultVar(pm, false), atPreVars, services); + paramVars, tb.resultVar(pm, false), atPreVars, services); Term preContract = - fop.getPre(heaps, selfVar, paramVars, atPreVars, services); + fop.getPre(heaps, selfVar, paramVars, atPreVars, services); if (preContract == null) { preContract = tb.tt(); } @@ -1179,11 +1190,11 @@ private ImmutableSet getModelMethodAxioms() { // (pm.isProtected() ? new Protected() : // (pm.isPublic() ? new Public() : null)); final ClassAxiom modelMethodRepresentsAxiom = - new RepresentsAxiom( - "Definition axiom for " + pm.getName() + " in " - + kjt.getFullName(), - pm, kjt, new Private(), preContract, representsFromContract, - selfVar, paramVars, atPreVars); + new RepresentsAxiom( + "Definition axiom for " + pm.getName() + " in " + + kjt.getFullName(), + pm, kjt, new Private(), preContract, representsFromContract, + selfVar, paramVars, atPreVars); result = result.add(modelMethodRepresentsAxiom); break; } @@ -1193,24 +1204,24 @@ pm, kjt, new Private(), preContract, representsFromContract, continue; } Term preFromContract = - fop.getPre(heaps, selfVar, paramVars, atPreVars, services); + fop.getPre(heaps, selfVar, paramVars, atPreVars, services); Term freePreFromContract = - fop.getFreePre(heaps, selfVar, paramVars, atPreVars, services); + fop.getFreePre(heaps, selfVar, paramVars, atPreVars, services); Term postFromContract = fop.getPost(heaps, selfVar, paramVars, resultVar, - null, atPreVars, services); + null, atPreVars, services); Term freePostFromContract = fop.getFreePost(heaps, selfVar, paramVars, - resultVar, null, atPreVars, services); + resultVar, null, atPreVars, services); if (preFromContract != null && ((postFromContract != null && postFromContract != tb.tt()) - || (freePostFromContract != null - && freePostFromContract != tb.tt()))) { + || (freePostFromContract != null + && freePostFromContract != tb.tt()))) { Term mbyFromContract = - fop.hasMby() ? fop.getMby(selfVar, paramVars, services) : null; + fop.hasMby() ? fop.getMby(selfVar, paramVars, services) : null; final ClassAxiom modelMethodContractAxiom = new ContractAxiom( - "Contract axiom for " + pm.getName() + " in " + kjt.getName(), pm, - kjt, new Private(), preFromContract, freePreFromContract, - postFromContract, freePostFromContract, mbyFromContract, atPreVars, - selfVar, resultVar, paramVars); + "Contract axiom for " + pm.getName() + " in " + kjt.getName(), pm, + kjt, new Private(), preFromContract, freePreFromContract, + postFromContract, freePostFromContract, mbyFromContract, atPreVars, + selfVar, resultVar, paramVars); result = result.add(modelMethodContractAxiom); } } @@ -1311,7 +1322,7 @@ public ImmutableSet getProofs(Contract atomicContract) { */ public ImmutableSet getProofs(KeYJavaType kjt, IObserverFunction target) { final ImmutableSet> targets = - getOverridingTargets(kjt, target).add(new Pair<>(kjt, target)); + getOverridingTargets(kjt, target).add(new Pair<>(kjt, target)); ImmutableSet result = DefaultImmutableSet.nil(); for (Map.Entry> entry : proofs.entrySet()) { final ProofOblInput po = entry.getKey(); @@ -1319,7 +1330,7 @@ public ImmutableSet getProofs(KeYJavaType kjt, IObserverFunction target) if (po instanceof ContractPO) { final Contract contract = ((ContractPO) po).getContract(); final Pair pair = - new Pair<>(contract.getKJT(), contract.getTarget()); + new Pair<>(contract.getKJT(), contract.getTarget()); if (targets.contains(pair)) { result = result.union(sop); } @@ -1478,7 +1489,8 @@ public void addLoopInvariant(final LoopSpecification inv) { * @return all block contracts for the specified block. */ public ImmutableSet getBlockContracts(StatementBlock block) { - var b = new BlockContractKey(block, block.getParentClass(), block.getStartPosition().line()); + var b = + new BlockContractKey(block, block.getParentClass(), block.getStartPosition().line()); final ImmutableSet contracts = blockContracts.get(b); if (contracts == null) { return DefaultImmutableSet.nil(); @@ -1535,7 +1547,7 @@ public ImmutableSet getMergeContracts(MergePointStatement mps) { * @param modalityKind the given modality. */ public ImmutableSet getBlockContracts(final StatementBlock block, - final Modality.JavaModalityKind modalityKind) { + final Modality.JavaModalityKind modalityKind) { ImmutableSet result = getBlockContracts(block); final Modality.JavaModalityKind matchModality = getMatchModalityKind(modalityKind); for (BlockContract contract : result) { @@ -1548,7 +1560,7 @@ public ImmutableSet getBlockContracts(final StatementBlock block, } public ImmutableSet getLoopContracts(final StatementBlock block, - final Modality.JavaModalityKind modalityKind) { + final Modality.JavaModalityKind modalityKind) { ImmutableSet result = getLoopContracts(block); final Modality.JavaModalityKind matchModality = getMatchModalityKind(modalityKind); for (LoopContract contract : result) { @@ -1568,7 +1580,7 @@ public ImmutableSet getLoopContracts(final StatementBlock block, * @return the set of resulting loop statements. */ public ImmutableSet getLoopContracts(final LoopStatement loop, - final Modality.JavaModalityKind modalityKind) { + final Modality.JavaModalityKind modalityKind) { ImmutableSet result = getLoopContracts(loop); final Modality.JavaModalityKind matchModality = getMatchModalityKind(modalityKind); for (LoopContract contract : result) { @@ -1598,7 +1610,8 @@ public void addBlockContract(final BlockContract contract) { */ public void addBlockContract(final BlockContract contract, boolean addFunctionalContract) { final StatementBlock block = contract.getBlock(); - var b =new BlockContractKey(block, block.getParentClass(), block.getStartPosition().line()); + var b = + new BlockContractKey(block, block.getParentClass(), block.getStartPosition().line()); blockContracts.put(b, getBlockContracts(block).add(contract)); if (addFunctionalContract) { @@ -1619,7 +1632,8 @@ public void addBlockContract(final BlockContract contract, boolean addFunctional */ public void removeBlockContract(final BlockContract contract) { final StatementBlock block = contract.getBlock(); - var b = new BlockContractKey(block, block.getParentClass(), block.getStartPosition().line()); + var b = + new BlockContractKey(block, block.getParentClass(), block.getStartPosition().line()); blockContracts.compute(b, (k, set) -> set.remove(contract)); } @@ -1643,12 +1657,13 @@ public void addLoopContract(final LoopContract contract) { public void addLoopContract(final LoopContract contract, boolean addFunctionalContract) { if (contract.isOnBlock()) { final StatementBlock block = contract.getBlock(); - var b = new LoopContractKey(block, block.getParentClass(), block.getStartPosition().line()); + var b = + new LoopContractKey(block, block.getParentClass(), block.getStartPosition().line()); loopContracts.put(b, getLoopContracts(block).add(contract)); } else { final LoopStatement loop = contract.getLoop(); final Pair b = - new Pair<>(loop, loop.getStartPosition().line()); + new Pair<>(loop, loop.getStartPosition().line()); loopContractsOnLoops.put(b, getLoopContracts(loop).add(contract)); } @@ -1675,13 +1690,14 @@ public void addLoopContract(final LoopContract contract, boolean addFunctionalCo public void removeLoopContract(final LoopContract contract) { if (contract.isOnBlock()) { final StatementBlock block = contract.getBlock(); - var b =new LoopContractKey(block, block.getParentClass(), block.getStartPosition().line()); + var b = + new LoopContractKey(block, block.getParentClass(), block.getStartPosition().line()); loopContracts.compute(b, (k, set) -> set.remove(contract)); } else { final LoopStatement loop = contract.getLoop(); final Pair b = - new Pair<>(loop, loop.getStartPosition().line()); + new Pair<>(loop, loop.getStartPosition().line()); loopContractsOnLoops.compute(b, (k, set) -> set.remove(contract)); } @@ -1747,11 +1763,11 @@ public Pair> limitObs(IObserverFunction if (limited == null) { final String baseName = - ((ProgramElementName) obs.name()).getProgramName() + LIMIT_SUFFIX; + ((ProgramElementName) obs.name()).getProgramName() + LIMIT_SUFFIX; final Sort heapSort = services.getTypeConverter().getHeapLDT().targetSort(); limited = new ObserverFunction(baseName, obs.sort(), obs.getType(), heapSort, - obs.getContainerType(), obs.isStatic(), obs.getParamTypes(), - obs.getHeapCount(services), obs.getStateCount()); + obs.getContainerType(), obs.isStatic(), obs.getParamTypes(), + obs.getHeapCount(services), obs.getStateCount()); unlimitedToLimited.put(obs, limited); limitedToUnlimited.put(limited, obs); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java index c82f3103c63..47dd43357d4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java @@ -565,8 +565,8 @@ private Term useCaseFormula(TermLabelState termLabelState, Services services, Ru } private Guard prepareGuard(final Instantiation inst, - final KeYJavaType booleanKJT, LoopInvariantBuiltInRuleApp loopRuleApp, - final TermServices services) { + final KeYJavaType booleanKJT, LoopInvariantBuiltInRuleApp loopRuleApp, + final TermServices services) { final TermBuilder tb = services.getTermBuilder(); final ProgramElementName guardVarName = new ProgramElementName(tb.newName("b")); final LocationVariable guardVar = new LocationVariable(guardVarName, booleanKJT); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeRule.java index db812dda262..f1e47d81eab 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeRule.java @@ -165,7 +165,8 @@ public final ImmutableList apply(Goal goal, final Services services, RuleA // The merge loop SymbolicExecutionState mergedState = - new SymbolicExecutionState(thisSEState.first(), thisSEState.second(), newGoal.node()); + new SymbolicExecutionState(thisSEState.symbolicState(), thisSEState.pathCondition(), + newGoal.node()); LinkedHashSet newNames = new LinkedHashSet<>(); LinkedHashSet sideConditionsToProve = new LinkedHashSet<>(); HashMap mergePartnerNodesToStates = new HashMap<>(); @@ -183,7 +184,7 @@ public final ImmutableList apply(Goal goal, final Services services, RuleA mergePartnerNodesToStates.put(state.getCorrespondingNode(), state); MergeStateEntry mergeResult = - mergeStates(mergeRule, mergedState, state, thisSEState.third(), + mergeStates(mergeRule, mergedState, state, thisSEState.programCounter(), mergeRuleApp.getDistinguishingFormula(), services); newNames.addAll(mergeResult.second); sideConditionsToProve.addAll(mergeResult.third); @@ -206,7 +207,7 @@ public final ImmutableList apply(Goal goal, final Services services, RuleA for (MergePartner mergePartner : mergePartners) { closeMergePartnerGoal(newGoal.node(), mergePartner.getGoal(), mergePartner.getPio(), mergedState, mergePartnerNodesToStates.get(mergePartner.getGoal().node()), - thisSEState.third(), newNames); + thisSEState.programCounter(), newNames); } // Delete previous sequents @@ -239,7 +240,7 @@ public final ImmutableList apply(Goal goal, final Services services, RuleA } // Add new succedent (symbolic state & program counter) - final Term succedentFormula = tb.apply(mergedState.first, thisSEState.third()); + final Term succedentFormula = tb.apply(mergedState.first, thisSEState.programCounter()); final SequentFormula newSuccedent = new SequentFormula(succedentFormula); newGoal.addFormula(newSuccedent, new PosInOccurrence(newSuccedent, PosInTerm.getTopLevel(), false)); @@ -294,14 +295,14 @@ public final ImmutableList apply(Goal goal, final Services services, RuleA *

* Override this method for special merge procedures. * - * @param mergeRule The merge procedure to use for the merge. - * @param state1 First state to merge. - * @param state2 Second state to merge. - * @param programCounter The formula \<{ ... }\> phi consisting of the common program - * counter and the post condition. + * @param mergeRule The merge procedure to use for the merge. + * @param state1 First state to merge. + * @param state2 Second state to merge. + * @param programCounter The formula \<{ ... }\> phi consisting of the common program + * counter and the post condition. * @param distinguishingFormula The user-specified distinguishing formula. May be null (for - * automatic generation). - * @param services The services object. + * automatic generation). + * @param services The services object. * @return A new merged SE state (U*,C*) which is a weakening of the original states. */ @SuppressWarnings("unused") @@ -675,7 +676,8 @@ public static ImmutableList findPotentialMergePartners(Goal goal, final ImmutableList allGoals = services.getProof().openGoals(); - final SymbolicExecutionStateWithProgCnt ownSEState = sequentToSETriple(goal.node(), pio, services); + final SymbolicExecutionStateWithProgCnt ownSEState = + sequentToSETriple(goal.node(), pio, services); // Find potential partners -- for which isApplicable is true and // they have the same program counter (and post condition). @@ -694,7 +696,7 @@ public static ImmutableList findPotentialMergePartners(Goal goal, final SymbolicExecutionStateWithProgCnt partnerSEState = sequentToSETriple(g.node(), gPio, services); - if (ownSEState.third().equals(partnerSEState.third())) { + if (ownSEState.programCounter().equals(partnerSEState.programCounter())) { potentialPartners = potentialPartners.prepend(new MergePartner(g, gPio)); @@ -714,5 +716,5 @@ public interface MergeRuleProgressListener { } public record MergeStateEntry(SymbolicExecutionState first, LinkedHashSet second, - LinkedHashSet third) {} + LinkedHashSet third) {} } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/merge/procedures/MergeByIfThenElse.java b/key.core/src/main/java/de/uka/ilkd/key/rule/merge/procedures/MergeByIfThenElse.java index 538e1dd3865..2591e2e9b72 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/merge/procedures/MergeByIfThenElse.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/merge/procedures/MergeByIfThenElse.java @@ -135,16 +135,16 @@ public static Term createIfThenElseTerm(final SymbolicExecutionState state1, * the discriminating condition, the second and third elements are the respective parts for the * if and else branch. * - * @param v Variable to return the update for. - * @param state1 First state to evaluate. - * @param state2 Second state to evaluate. + * @param v Variable to return the update for. + * @param state1 First state to evaluate. + * @param state2 Second state to evaluate. * @param services The services object. * @return Input to construct an elementary update like - * { v := \if (first) \then (second) \else (third) }, where first, second - * and third are the respective components of the returned triple. The fourth component - * indicates whether the path condition of the first (fourth component = false) or the - * second (fourth component = true) state was used as a basis for the condition (first - * component). + * { v := \if (first) \then (second) \else (third) }, where first, second + * and third are the respective components of the returned triple. The fourth component + * indicates whether the path condition of the first (fourth component = false) or the + * second (fourth component = true) state was used as a basis for the condition (first + * component). */ static DistanceFormRightSide createDistFormAndRightSidesForITEUpd( LocationVariable v, SymbolicExecutionState state1, SymbolicExecutionState state2, @@ -177,17 +177,17 @@ static DistanceFormRightSide createDistFormAndRightSidesForITEUpd( * the triple is the discriminating condition, the second and third elements are the respective * parts for the if and else branch. * - * @param state1 First state to evaluate. - * @param state2 Second state to evaluate. - * @param ifTerm The if term. + * @param state1 First state to evaluate. + * @param state2 Second state to evaluate. + * @param ifTerm The if term. * @param elseTerm The else term. * @param services The services object. * @return Input to construct an elementary update like - * { v := \if (first) \then (second) \else (third) }, where first, second - * and third are the respective components of the returned triple. The fourth component - * indicates whether the path condition of the first (fourth component = false) or the - * second (fourth component = true) state was used as a basis for the condition (first - * component). + * { v := \if (first) \then (second) \else (third) }, where first, second + * and third are the respective components of the returned triple. The fourth component + * indicates whether the path condition of the first (fourth component = false) or the + * second (fourth component = true) state was used as a basis for the condition (first + * component). */ static DistanceFormRightSide createDistFormAndRightSidesForITEUpd( SymbolicExecutionState state1, SymbolicExecutionState state2, Term ifTerm, diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/ContractFactory.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/ContractFactory.java index 17d64a0d76a..f779a413d70 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/ContractFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/ContractFactory.java @@ -193,7 +193,7 @@ public DependencyContract dep(KeYJavaType containerType, IObserverFunction pm, } public DependencyContract dep(KeYJavaType kjt, LocationVariable targetHeap, - TranslatedDependencyContract dep, ProgramVariable selfVar) { + TranslatedDependencyContract dep, ProgramVariable selfVar) { final ImmutableList paramVars = tb.paramVars(dep.first(), false); assert (selfVar == null) == dep.first().isStatic(); Map pres = new LinkedHashMap<>(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLSpecCase.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLSpecCase.java index 8371394e48a..25af75155b7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLSpecCase.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLSpecCase.java @@ -194,7 +194,9 @@ public void addRequires(LabeledParserRuleContext label) { addClause(REQUIRES, label); } - public record Abbreviation(LabeledParserRuleContext first, LabeledParserRuleContext second, LabeledParserRuleContext thrid){} + public record Abbreviation(LabeledParserRuleContext typeName, + LabeledParserRuleContext abbrevName, + LabeledParserRuleContext abbreviatedTerm) {} public Abbreviation[] getAbbreviations() { /* weigl: prepare for future use of generated abbreviations from JML specifications */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java index 9cf9d03a442..de423f25f59 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java @@ -546,12 +546,11 @@ private LabeledParserRuleContext getAssignableFreeNothing() { */ private ImmutableList registerAbbreviationVariables(TextualJMLSpecCase textualSpecCase, Context context, ProgramVariableCollection progVars, ContractClauses clauses) { - for (Triple abbrv : textualSpecCase - .getAbbreviations()) { + for (TextualJMLSpecCase.Abbreviation abbrv : textualSpecCase.getAbbreviations()) { final KeYJavaType abbrKJT = - services.getJavaInfo().getKeYJavaType(abbrv.first.first.getText()); + services.getJavaInfo().getKeYJavaType(abbrv.typeName().first.getText()); final ProgramElementName abbrVarName = - new ProgramElementName(abbrv.second.first.getText()); + new ProgramElementName(abbrv.abbrevName().first.getText()); final LocationVariable abbrVar = new LocationVariable(abbrVarName, abbrKJT, true, true); assert abbrVar.isGhost() : "specification parameter not ghost"; services.getNamespaces().programVariables().addSafely(abbrVar); @@ -560,7 +559,7 @@ private ImmutableList registerAbbreviationVariables(TextualJMLSpecCase tex // parameter Term rhs = new JmlIO(services).context(context).parameters(progVars.paramVars) .atPres(progVars.atPres).atBefore(progVars.atBefores) - .translateTerm(abbrv.third); + .translateTerm(abbrv.abbreviatedTerm()); clauses.abbreviations = clauses.abbreviations.append(tb.elementary(tb.var(abbrVar), rhs)); } @@ -1159,9 +1158,8 @@ public Contract createJMLDependencyContract(KeYJavaType kjt, LocationVariable ta var context = Context.inClass(kjt, false, tb); // translateToTerm expression - Triple dep = - new JmlIO(services).context(context).translateDependencyContract(originalDep); - return cf.dep(kjt, targetHeap, dep, dep.first.isStatic() ? null : context.selfVar()); + var dep = new JmlIO(services).context(context).translateDependencyContract(originalDep); + return cf.dep(kjt, targetHeap, dep, dep.first().isStatic() ? null : context.selfVar()); } public Contract createJMLDependencyContract(KeYJavaType kjt, TextualJMLDepends textualDep) { @@ -1433,8 +1431,7 @@ public void translateJmlAssertCondition(final JmlAssert jmlAssert, final IProgra } public @Nullable String checkSetStatementAssignee(Term assignee) { - if (assignee.op() instanceof LocationVariable) { - var variable = (LocationVariable) assignee.op(); + if (assignee.op() instanceof LocationVariable variable) { if (variable.isGhost()) { return null; } else { diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java index 2547e1f32aa..1e0e53e44ea 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java @@ -1049,7 +1049,7 @@ public TranslatedDependencyContract depends(SLExpression lhs, Term rhs, SLExpres + ", given" + lhs.getTerm().sub(0).op()); } - return new Triple<>((IObserverFunction) lhs.getTerm().op(), rhs, + return new TranslatedDependencyContract((IObserverFunction) lhs.getTerm().op(), rhs, mby == null ? null : mby.getTerm()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TranslatedDependencyContract.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TranslatedDependencyContract.java index 983d03b0f7f..122148732ad 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TranslatedDependencyContract.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TranslatedDependencyContract.java @@ -1,3 +1,6 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.speclang.njml; import de.uka.ilkd.key.logic.Term; @@ -5,7 +8,7 @@ /** * - * @author Alexander Weigl + * @author Alexander Weigl * @version 1 (23.04.24) */ public record TranslatedDependencyContract(IObserverFunction first, Term second, Term third) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/definition/StrategySettingsDefinition.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/definition/StrategySettingsDefinition.java index 5e1ba42bb90..fe7bd9b75a6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/definition/StrategySettingsDefinition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/definition/StrategySettingsDefinition.java @@ -35,7 +35,8 @@ * @see StrategyPropertyValueDefinition */ public class StrategySettingsDefinition { - public record StategySettingEntry(String name, int order, IDefaultStrategyPropertiesFactory factory){} + public record StategySettingEntry(String name, int order, + IDefaultStrategyPropertiesFactory factory) {} private static final ArrayList STD_FURTHER_DEFAULTS; 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 index 9059d07e207..179bb47891a 100644 --- 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 @@ -1028,7 +1028,7 @@ public static SymbolicExecutionState sequentToSEPair(Node node, PosInOccurrence SymbolicExecutionStateWithProgCnt triple = sequentToSETriple(node, pio, services); - return new SymbolicExecutionState(triple.first, triple.second, node); + return new SymbolicExecutionState(triple.symbolicState(), triple.pathCondition(), node); } /** @@ -1099,7 +1099,8 @@ public static ImmutableList sequentsToSEPairs( sequentToSETriple(node, sequentInfo.getPio(), services); result = result.prepend( - new SymbolicExecutionState(partnerSEState.first(), partnerSEState.second(), node)); + new SymbolicExecutionState(partnerSEState.symbolicState(), + partnerSEState.pathCondition(), node)); } return result; diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/SymbolicExecutionStateWithProgCnt.java b/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/SymbolicExecutionStateWithProgCnt.java index f4ec6a50bd3..ea86a015579 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/SymbolicExecutionStateWithProgCnt.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/SymbolicExecutionStateWithProgCnt.java @@ -7,6 +7,7 @@ import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.pp.LogicPrinter; import de.uka.ilkd.key.proof.Node; + import org.jspecify.annotations.Nullable; /** @@ -14,10 +15,14 @@ * parallel update, a path condition in form of a JavaDL formula, and a program counter in form of a * JavaDL formula with non-empty Java Block (and a possible post condition as first, and only, sub * term). - * + * @param symbolicState The symbolic state (parallel update). + * @param pathCondition The path condition (formula). + * @param programCounter The program counter: Formula with non-empty Java block and post + * condition as only sub term. + * @param correspondingNode The node corresponding to this SE state. * @author Dominic Scheurer */ -public record SymbolicExecutionStateWithProgCnt(Term first, Term second, Term third, +public record SymbolicExecutionStateWithProgCnt(Term symbolicState, Term pathCondition, Term programCounter, @Nullable Node correspondingNode) { /** * @param symbolicState The symbolic state (parallel update). @@ -25,43 +30,31 @@ public record SymbolicExecutionStateWithProgCnt(Term first, Term second, Term th * @param programCounter The program counter: Formula with non-empty Java block and post * condition as only sub term. */ - public SymbolicExecutionStateWithProgCnt(Term symbolicState, Term pathCondition, - Term programCounter) { - super(symbolicState, pathCondition, programCounter); + public SymbolicExecutionStateWithProgCnt(Term symbolicState, Term pathCondition, Term programCounter) { + this(symbolicState, pathCondition, programCounter, null); } - /** - * @param symbolicState The symbolic state (parallel update). - * @param pathCondition The path condition (formula). - * @param programCounter The program counter: Formula with non-empty Java block and post - * condition as only sub term. - * @param correspondingNode The node corresponding to this SE state. - */ - public SymbolicExecutionStateWithProgCnt(Term symbolicState, Term pathCondition, - Term programCounter, Node correspondingNode) { - this(symbolicState, pathCondition, programCounter); - this.correspondingNode = correspondingNode; - } + /** * @return The symbolic state. */ public Term getSymbolicState() { - return first; + return symbolicState; } /** * @return The path condition. */ public Term getPathCondition() { - return second; + return pathCondition; } /** * @return The program counter (and post condition). */ public Term getProgramCounter() { - return third; + return programCounter; } /** @@ -71,18 +64,11 @@ public Node getCorrespondingNode() { return correspondingNode; } - /** - * @param correspondingNode The node corresponding to this SE state. - */ - public void setCorrespondingNode(Node correspondingNode) { - this.correspondingNode = correspondingNode; - } - /** * @return The corresponding SE state (without the program counter). */ public SymbolicExecutionState toSymbolicExecutionState() { - return new SymbolicExecutionState(first, second); + return new SymbolicExecutionState(symbolicState, pathCondition); } @Override diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/proverules/ProveRulesTest.java b/key.core/src/test/java/de/uka/ilkd/key/proof/proverules/ProveRulesTest.java index 3d1a1d7aaef..8b03c5694ca 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/proverules/ProveRulesTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/proverules/ProveRulesTest.java @@ -10,7 +10,6 @@ import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.control.KeYEnvironment; import de.uka.ilkd.key.macros.scripts.ProofScriptEngine; -import de.uka.ilkd.key.parser.Location; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.init.Profile; import de.uka.ilkd.key.proof.io.ProblemLoaderException; @@ -19,7 +18,6 @@ import de.uka.ilkd.key.util.HelperClassForTests; import de.uka.ilkd.key.util.LinkedHashMap; -import org.key_project.util.collection.Pair; import org.key_project.util.helper.FindResources; import org.junit.jupiter.api.DynamicTest; diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java index 8966026c803..87d614a794b 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java @@ -11,7 +11,6 @@ import de.uka.ilkd.key.control.KeYEnvironment; import de.uka.ilkd.key.macros.scripts.ProofScriptEngine; import de.uka.ilkd.key.nparser.ProofScriptEntry; -import de.uka.ilkd.key.parser.Location; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.io.AbstractProblemLoader; import de.uka.ilkd.key.proof.io.ProblemLoaderException; @@ -104,12 +103,12 @@ private void runKey(String file, TestProperty testProperty) throws Exception { try { LOGGER.info("({}) Start proving", caseId); // Initialize KeY environment and load proof. - Pair, Pair> pair = + Pair, ProofScriptEntry> pair = load(keyFile); LOGGER.info("({}) Proving done", caseId); env = pair.first; - Pair script = pair.second; + ProofScriptEntry script = pair.second; loadedProof = env.getLoadedProof(); AbstractProblemLoader.ReplayResult replayResult = env.getReplayResult(); @@ -183,14 +182,14 @@ private void reload(File proofFile, Proof loadedProof) throws Exception { * want to use a different strategy. */ private void autoMode(KeYEnvironment env, Proof loadedProof, - Pair script) throws Exception { + ProofScriptEntry script) throws Exception { // Run KeY prover. if (script == null) { // auto mode env.getProofControl().startAndWaitForAutoMode(loadedProof); } else { // ... script - ProofScriptEngine pse = new ProofScriptEngine(script.first, script.second); + ProofScriptEngine pse = new ProofScriptEngine(script.script(), script.location()); pse.execute(env.getUi(), env.getLoadedProof()); } } diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTestFile.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTestFile.java index d7aa7c78ee0..c48a8afeb85 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTestFile.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTestFile.java @@ -28,7 +28,7 @@ public DataRecordingTestFile(TestProperty testProperty, String path, @Override protected void autoMode(KeYEnvironment env, Proof loadedProof, - ProofScriptEntry script) throws Exception { + ProofScriptEntry script) throws Exception { // Run KeY prover. if (script == null) { DataRecordingStrategy strategy = new DataRecordingStrategy(loadedProof, this); diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java index 25d5dedd8fc..af762f4e45a 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java @@ -262,7 +262,7 @@ protected void reload(boolean verbose, File proofFile, Proof loadedProof, boolea * want to use a different strategy. */ protected void autoMode(KeYEnvironment env, Proof loadedProof, - ProofScriptEntry script) throws Exception { + ProofScriptEntry script) throws Exception { // Run KeY prover. if (script == null) { // auto mode diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/StrategySelectionView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/StrategySelectionView.java index b17ae902c0b..0925b8cb48f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/StrategySelectionView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/StrategySelectionView.java @@ -404,7 +404,8 @@ private JPanel createDefaultPanel(StrategySelectionComponents components) { existingPredefs[0] = "Defaults"; int i = 1; - for (StrategySettingsDefinition.StategySettingEntry furtherDefault : DEFINITION.getFurtherDefaults()) { + for (StrategySettingsDefinition.StategySettingEntry furtherDefault : DEFINITION + .getFurtherDefaults()) { existingPredefs[i] = furtherDefault.name(); i++; } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDifference.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDifference.java index 02385e81654..619100c08ea 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDifference.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDifference.java @@ -83,7 +83,7 @@ static String findAndPopNearestMatch(String l, List right) { return current; } - public record QueueEntry(int idxLeft, int idxRight, int distance){} + public record QueueEntry(int idxLeft, int idxRight, int distance) {} static List findPairs(List left, List right) { List pairs = new ArrayList<>(left.size() + right.size()); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java index c0cf68fe6c7..d0d7781110d 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java @@ -20,7 +20,7 @@ import de.uka.ilkd.key.macros.ProofMacroFinishedInfo; import de.uka.ilkd.key.macros.SkipMacro; import de.uka.ilkd.key.macros.scripts.ProofScriptEngine; -import de.uka.ilkd.key.parser.Location; +import de.uka.ilkd.key.nparser.ProofScriptEntry; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.ProofAggregate; @@ -44,7 +44,6 @@ import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; import org.key_project.util.collection.ImmutableSet; -import org.key_project.util.collection.Pair; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -159,13 +158,17 @@ public void taskFinished(TaskFinishedInfo info) { ProblemLoader problemLoader = (ProblemLoader) info.getSource(); if (problemLoader.hasProofScript()) { try { - Pair script = problemLoader.readProofScript(); - ProofScriptEngine pse = new ProofScriptEngine(script.first, script.second); - this.taskStarted(new DefaultTaskStartedInfo(TaskKind.Macro, "Script started", 0)); - pse.execute(this, proof); - // The start and end messages are fake to persuade the system ... - // All this here should refactored anyway ... - this.taskFinished(new ProofMacroFinishedInfo(new SkipMacro(), proof)); + ProofScriptEntry script = problemLoader.readProofScript(); + if (script != null) { + ProofScriptEngine pse = + new ProofScriptEngine(script.script(), script.location()); + this.taskStarted( + new DefaultTaskStartedInfo(TaskKind.Macro, "Script started", 0)); + pse.execute(this, proof); + // The start and end messages are fake to persuade the system ... + // All this here should refactored anyway ... + this.taskFinished(new ProofMacroFinishedInfo(new SkipMacro(), proof)); + } } catch (Exception e) { LOGGER.debug("", e); System.exit(-1); diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/RuleStatistics.java b/keyext.slicing/src/main/java/org/key_project/slicing/RuleStatistics.java index 30ada1c137a..95d7ebc8509 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/RuleStatistics.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/RuleStatistics.java @@ -3,14 +3,14 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.slicing; -import de.uka.ilkd.key.rule.Rule; - import java.util.Comparator; import java.util.HashMap; import java.util.List; import java.util.Map; import java.util.stream.Collectors; +import de.uka.ilkd.key.rule.Rule; + /** * Simple data object to store a mapping of rules to various counters. * @@ -40,7 +40,8 @@ public void addApplication(Rule rule, boolean branches) { StatisticEntry entry = map.computeIfAbsent(name, it -> new StatisticEntry(0, 0, 0)); - map.put(name, new StatisticEntry(entry.numberOfApplications + 1, entry.numberOfUselessApplications, entry.numberOfInitialUselessApplications)); + map.put(name, new StatisticEntry(entry.numberOfApplications + 1, + entry.numberOfUselessApplications, entry.numberOfInitialUselessApplications)); } /** @@ -55,7 +56,8 @@ public void addUselessApplication(Rule rule, boolean branches) { StatisticEntry entry = map.computeIfAbsent(name, it -> new StatisticEntry(0, 0, 0)); - map.put(name, new StatisticEntry(entry.numberOfApplications + 1, entry.numberOfUselessApplications + 1, entry.numberOfInitialUselessApplications)); + map.put(name, new StatisticEntry(entry.numberOfApplications + 1, + entry.numberOfUselessApplications + 1, entry.numberOfInitialUselessApplications)); } /** @@ -70,7 +72,8 @@ public void addInitialUselessApplication(Rule rule, boolean branches) { StatisticEntry entry = map.computeIfAbsent(name, it -> new StatisticEntry(0, 0, 0)); - map.put(name, new StatisticEntry(entry.numberOfApplications + 1, entry.numberOfUselessApplications + 1, entry.numberOfInitialUselessApplications + 1)); + map.put(name, new StatisticEntry(entry.numberOfApplications + 1, + entry.numberOfUselessApplications + 1, entry.numberOfInitialUselessApplications + 1)); } /** @@ -83,8 +86,10 @@ public void addInitialUselessApplication(Rule rule, boolean branches) { */ public List sortBy(Comparator comparator) { return map.entrySet().stream() - .map(entry -> new RuleStatisticEntry(entry.getKey(), entry.getValue().numberOfApplications, - entry.getValue().numberOfUselessApplications, entry.getValue().numberOfInitialUselessApplications)) + .map(entry -> new RuleStatisticEntry(entry.getKey(), + entry.getValue().numberOfApplications, + entry.getValue().numberOfUselessApplications, + entry.getValue().numberOfInitialUselessApplications)) .sorted(comparator) .collect(Collectors.toList()); } @@ -100,21 +105,25 @@ public boolean branches(String rule) { /** * Usage statistic of a rule. *

- * TODO weigl: refactoring task, combine {@link RuleStatisticEntry} with {@link StatisticEntry} to avoid repetition. + * TODO weigl: refactoring task, combine {@link RuleStatisticEntry} with {@link StatisticEntry} + * to avoid repetition. * * @param ruleName * @param numberOfApplications * @param numberOfUselessApplications * @param numberOfInitialUselessApplications */ - public record RuleStatisticEntry(String ruleName, int numberOfApplications, int numberOfUselessApplications, int numberOfInitialUselessApplications) { + public record RuleStatisticEntry(String ruleName, int numberOfApplications, + int numberOfUselessApplications, int numberOfInitialUselessApplications) { } /** * Usage statistic of a rule. + * * @param numberOfApplications * @param numberOfUselessApplications * @param numberOfInitialUselessApplications */ - public record StatisticEntry(int numberOfApplications, int numberOfUselessApplications, int numberOfInitialUselessApplications){} + public record StatisticEntry(int numberOfApplications, int numberOfUselessApplications, + int numberOfInitialUselessApplications) {} } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/analysis/DependencyAnalyzer.java b/keyext.slicing/src/main/java/org/key_project/slicing/analysis/DependencyAnalyzer.java index f01a9de6985..df768c0f273 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/analysis/DependencyAnalyzer.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/analysis/DependencyAnalyzer.java @@ -444,7 +444,7 @@ private void deduplicateRuleApps() { // (for obvious reasons, we don't care about origin labels here -> wrapper) Map, Set> foundDupes = new HashMap<>(); graph.outgoingGraphEdgesOf(node).forEach(t -> { - Node proofNode = t.first; + Node proofNode = t.fromNode(); // this analysis algorithm does not support proofs with State Merging if (proofNode.getAppliedRuleApp() instanceof MergeRuleBuiltInRuleApp @@ -465,7 +465,7 @@ private void deduplicateRuleApps() { } // Only try to deduplicate the addition of new formulas. // It is unlikely that two closed goals are derived using the same formula. - GraphNode produced = t.second; + GraphNode produced = t.toNode(); if (!(produced instanceof TrackedFormula)) { return; } @@ -473,7 +473,7 @@ private void deduplicateRuleApps() { .computeIfAbsent( new EqualsModProofIrrelevancyWrapper<>(proofNode.getAppliedRuleApp()), _a -> new LinkedHashSet<>()) - .add(t.third.getProofStep()); + .add(t.annotation().getProofStep()); }); // scan dupes, try to find a set of mergable rule applications diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java index 320c5d43756..3e4dd6b7851 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java @@ -119,18 +119,26 @@ public Stream incomingEdgesOf(GraphNode node) { return graph.incomingEdgesOf(node).stream().map(AnnotatedEdge::getProofStep); } - public record IncomingEdge(Node first, GraphNode second, AnnotatedEdge third){} + /** + * Represents an edge in the dependency graph. + * + * @param fromNode the outgoing node of the edge + * @param toNode the incoming node of the edge + * @param annotation annotation associated to the edge + */ + public record Edge(Node fromNode, GraphNode toNode, AnnotatedEdge annotation) {} /** * @param node a graph node * @return the incoming (graph edges, graph sources) of that node */ - public Stream incomingGraphEdgesOf(GraphNode node) { + public Stream incomingGraphEdgesOf(GraphNode node) { if (!graph.containsVertex(node)) { return Stream.of(); } return graph.incomingEdgesOf(node).stream() - .map(edge -> new IncomingEdge(edge.getProofStep(), graph.getEdgeSource(edge), edge)); + .map( + edge -> new Edge(edge.getProofStep(), graph.getEdgeSource(edge), edge)); } /** @@ -148,12 +156,13 @@ public Stream outgoingEdgesOf(GraphNode node) { * @param node a graph node * @return the outgoing (graph edges, graph targets) of that node */ - public Stream outgoingGraphEdgesOf(GraphNode node) { + public Stream outgoingGraphEdgesOf(GraphNode node) { if (!graph.containsVertex(node)) { return Stream.of(); } return graph.outgoingEdgesOf(node).stream() - .map(edge -> new IncomingEdge(edge.getProofStep(), graph.getEdgeTarget(edge), edge)); + .map( + edge -> new Edge(edge.getProofStep(), graph.getEdgeTarget(edge), edge)); } /** @@ -281,7 +290,7 @@ public Stream inputsConsumedBy(Node proofStep) { * @return the outgoing edges of that node */ public Stream edgesUsing(GraphNode node) { - return outgoingGraphEdgesOf(node).map(it -> it.third); + return outgoingGraphEdgesOf(node).map(it -> it.annotation); } /** @@ -290,8 +299,8 @@ public Stream edgesUsing(GraphNode node) { */ public Stream edgesConsuming(GraphNode node) { return outgoingGraphEdgesOf(node) - .filter(it -> it.third.replacesInputNode()) - .map(it -> it.third); + .filter(it -> it.annotation.replacesInputNode()) + .map(it -> it.annotation); } /** @@ -300,7 +309,7 @@ public Stream edgesConsuming(GraphNode node) { */ public Stream edgesProducing(GraphNode node) { return incomingGraphEdgesOf(node) - .map(it -> it.third); + .map(it -> it.annotation); } /** @@ -393,12 +402,12 @@ public DependencyGraph removeChains() { // whose hyperedge should not connect more nodes // (otherwise we cannot remove the edge without // making the graph inconsistent) - Node startNode = incoming.get(0).first; + Node startNode = incoming.get(0).fromNode; if (edgesOf(startNode).size() != 1) { continue; } - GraphNode startGraphNode = incoming.get(0).second; - AnnotatedEdge edge = incoming.get(0).third; + GraphNode startGraphNode = incoming.get(0).toNode; + AnnotatedEdge edge = incoming.get(0).annotation; // get real initial node // (in case of repeated shortenings) @@ -412,9 +421,9 @@ public DependencyGraph removeChains() { // whose hyperedge should not connect more nodes // (otherwise we cannot remove the edge without // making the graph inconsistent) - Node endNode = outgoing.get(0).first; - GraphNode endGraphNode = outgoing.get(0).second; - var edge2 = outgoing.get(0).third; + Node endNode = outgoing.get(0).fromNode; + GraphNode endGraphNode = outgoing.get(0).toNode; + var edge2 = outgoing.get(0).annotation; if (edgesOf(endNode).size() != 1) { continue; } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ui/RuleStatisticsDialog.java b/keyext.slicing/src/main/java/org/key_project/slicing/ui/RuleStatisticsDialog.java index ab4b78c1394..ca39d883a20 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ui/RuleStatisticsDialog.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ui/RuleStatisticsDialog.java @@ -3,19 +3,20 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.slicing.ui; +import java.awt.*; +import java.awt.event.KeyAdapter; +import java.awt.event.KeyEvent; +import java.util.*; +import java.util.List; +import javax.swing.*; + import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.configuration.Config; + import org.key_project.slicing.RuleStatistics; import org.key_project.slicing.RuleStatistics.RuleStatisticEntry; import org.key_project.slicing.analysis.AnalysisResults; -import javax.swing.*; -import java.awt.*; -import java.awt.event.KeyAdapter; -import java.awt.event.KeyEvent; -import java.util.List; -import java.util.*; - /** * Dialog that displays the results of the dependency analysis algorithm. * @@ -58,7 +59,7 @@ private void createUI(Window window) { statisticsPane.setBackground(MainWindow.getInstance().getBackground()); statisticsPane.setSize(new Dimension(10, 360)); statisticsPane.setPreferredSize( - new Dimension(statisticsPane.getPreferredSize().width + 15, 360)); + new Dimension(statisticsPane.getPreferredSize().width + 15, 360)); JScrollPane scrollPane = new JScrollPane(statisticsPane); scrollPane.setBorder(BorderFactory.createEmptyBorder()); @@ -66,7 +67,7 @@ private void createUI(Window window) { Font myFont = UIManager.getFont(Config.KEY_FONT_PROOF_TREE); if (myFont != null) { statisticsPane.putClientProperty(JEditorPane.HONOR_DISPLAY_PROPERTIES, - Boolean.TRUE); + Boolean.TRUE); statisticsPane.setFont(myFont); } @@ -77,17 +78,17 @@ private void createUI(Window window) { int w = 50 + Math.max( - scrollPane.getPreferredSize().width, - buttonPane.getPreferredSize().width); + scrollPane.getPreferredSize().width, + buttonPane.getPreferredSize().width); int h = scrollPane.getPreferredSize().height + buttonPane.getPreferredSize().height + 100; setSize(w, h); statisticsPane.setText(genTable( - statistics.sortBy( - Comparator.comparing(RuleStatisticEntry::numberOfApplications) - .reversed()))); + statistics.sortBy( + Comparator.comparing(RuleStatisticEntry::numberOfApplications) + .reversed()))); statisticsPane.setCaretPosition(0); setLocationRelativeTo(window); } @@ -109,25 +110,29 @@ private JPanel constructButtonPanel(JEditorPane statisticsPane) { JButton sortButton1 = new JButton("Sort by name"); sortButton1.addActionListener(event -> { statisticsPane.setText(genTable( - statistics.sortBy(Comparator.comparing(RuleStatisticEntry::ruleName)))); + statistics.sortBy(Comparator.comparing(RuleStatisticEntry::ruleName)))); statisticsPane.setCaretPosition(0); }); JButton sortButton2 = new JButton("Sort by total"); sortButton2.addActionListener(event -> { statisticsPane.setText(genTable( - statistics.sortBy(Comparator.comparing(RuleStatisticEntry::numberOfApplications).reversed()))); + statistics.sortBy( + Comparator.comparing(RuleStatisticEntry::numberOfApplications).reversed()))); statisticsPane.setCaretPosition(0); }); JButton sortButton3 = new JButton("Sort by useless"); sortButton3.addActionListener(event -> { statisticsPane.setText(genTable( - statistics.sortBy(Comparator.comparing(RuleStatisticEntry::numberOfUselessApplications).reversed()))); + statistics.sortBy(Comparator + .comparing(RuleStatisticEntry::numberOfUselessApplications).reversed()))); statisticsPane.setCaretPosition(0); }); JButton sortButton4 = new JButton("Sort by initial useless"); sortButton4.addActionListener(event -> { statisticsPane.setText(genTable( - statistics.sortBy(Comparator.comparing(RuleStatisticEntry::numberOfInitialUselessApplications).reversed()))); + statistics.sortBy( + Comparator.comparing(RuleStatisticEntry::numberOfInitialUselessApplications) + .reversed()))); statisticsPane.setCaretPosition(0); }); @@ -158,26 +163,31 @@ public void keyTyped(KeyEvent e) { */ private String genTable(List rules) { List columns = List.of("Rule name", "Total applications", "Useless applications", - "Initial useless applications"); + "Initial useless applications"); List> rows = new ArrayList<>(); // summary row int uniqueRules = rules.size(); int totalSteps = rules.stream().mapToInt(RuleStatisticEntry::numberOfApplications).sum(); - int uselessSteps = rules.stream().mapToInt(RuleStatisticEntry::numberOfUselessApplications).sum(); - int initialUseless = rules.stream().mapToInt(RuleStatisticEntry::numberOfInitialUselessApplications).sum(); + int uselessSteps = + rules.stream().mapToInt(RuleStatisticEntry::numberOfUselessApplications).sum(); + int initialUseless = + rules.stream().mapToInt(RuleStatisticEntry::numberOfInitialUselessApplications).sum(); rows.add(List.of(String.format("(all %d rules)", uniqueRules), Integer.toString(totalSteps), - Integer.toString(uselessSteps), Integer.toString(initialUseless))); + Integer.toString(uselessSteps), Integer.toString(initialUseless))); // next summary row List rulesBranching = - rules.stream().filter(it -> statistics.branches(it.ruleName())).toList(); + rules.stream().filter(it -> statistics.branches(it.ruleName())).toList(); int uniqueRules2 = rulesBranching.size(); - totalSteps = rulesBranching.stream().mapToInt(RuleStatisticEntry::numberOfApplications).sum(); - uselessSteps = rulesBranching.stream().mapToInt(RuleStatisticEntry::numberOfUselessApplications).sum(); - initialUseless = rulesBranching.stream().mapToInt(RuleStatisticEntry::numberOfInitialUselessApplications).sum(); + totalSteps = + rulesBranching.stream().mapToInt(RuleStatisticEntry::numberOfApplications).sum(); + uselessSteps = + rulesBranching.stream().mapToInt(RuleStatisticEntry::numberOfUselessApplications).sum(); + initialUseless = rulesBranching.stream() + .mapToInt(RuleStatisticEntry::numberOfInitialUselessApplications).sum(); rows.add(List.of(String.format("(%d branching rules)", uniqueRules2), - Integer.toString(totalSteps), Integer.toString(uselessSteps), - Integer.toString(initialUseless))); + Integer.toString(totalSteps), Integer.toString(uselessSteps), + Integer.toString(initialUseless))); rules.forEach(a -> { String name = a.ruleName(); Integer all = a.numberOfApplications(); @@ -186,7 +196,7 @@ private String genTable(List rules) { rows.add(List.of(name, all.toString(), useless.toString(), iua.toString())); }); - return HtmlFactory.generateTable(columns, new boolean[]{false, false, false, false}, - Optional.of(new String[]{null, "right", "right", "right"}), rows, null); + return HtmlFactory.generateTable(columns, new boolean[] { false, false, false, false }, + Optional.of(new String[] { null, "right", "right", "right" }), rows, null); } } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ui/ShowNodeInfoAction.java b/keyext.slicing/src/main/java/org/key_project/slicing/ui/ShowNodeInfoAction.java index 320042ea01b..930ea88a5b8 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ui/ShowNodeInfoAction.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ui/ShowNodeInfoAction.java @@ -18,9 +18,7 @@ import org.key_project.slicing.DependencyTracker; import org.key_project.slicing.analysis.AnalysisResults; -import org.key_project.slicing.graph.AnnotatedEdge; -import org.key_project.slicing.graph.DependencyGraph; -import org.key_project.slicing.graph.DependencyGraph.IncomingEdge; +import org.key_project.slicing.graph.DependencyGraph.Edge; import org.key_project.slicing.graph.GraphNode; import org.key_project.util.collection.Pair; @@ -73,17 +71,17 @@ private void showDialog(Window parentWindow) { List graphNodes = new ArrayList<>(); List proofSteps = new ArrayList<>(); AnalysisResults analysisResults = tracker.getAnalysisResults(); - Function> nodeToTableRow = n -> { - proofSteps.add(n.first()); - graphNodes.add(n.second()); - var ruleName = n.first().getAppliedRuleApp().rule().displayName(); + Function> nodeToTableRow = n -> { + proofSteps.add(n.fromNode()); + graphNodes.add(n.toNode()); + var ruleName = n.fromNode().getAppliedRuleApp().rule().displayName(); return List.of( - Integer.toString(n.first().serialNr()), - analysisResults != null && !analysisResults.usefulSteps.contains(n.first()) + Integer.toString(n.fromNode().serialNr()), + analysisResults != null && !analysisResults.usefulSteps.contains(n.fromNode()) ? "" + ruleName + "" : ruleName, - n.third().replacesInputNode() ? "yes" : "no", - n.second().toString(false, false)); + n.annotation().replacesInputNode() ? "yes" : "no", + n.toNode().toString(false, false)); }; var idxFactory = new IndexFactory(); @@ -100,7 +98,7 @@ private void showDialog(Window parentWindow) { HtmlFactory.generateTable(headers2, clickable, Optional.empty(), outgoing, idxFactory); var useful = analysisResults != null ? tracker.getDependencyGraph().outgoingGraphEdgesOf(node) - .filter(t -> analysisResults.usefulSteps.contains(t.first())).count() + .filter(t -> analysisResults.usefulSteps.contains(t.fromNode())).count() : -1; var extraInfo = useful != -1 ? "

" + useful + " useful rule apps

" : ""; var previousDerivations = 0; diff --git a/keyext.slicing/src/test/java/org/key_project/slicing/DependencyGraphTest.java b/keyext.slicing/src/test/java/org/key_project/slicing/DependencyGraphTest.java index f2b7adc37ff..2b2769523ea 100644 --- a/keyext.slicing/src/test/java/org/key_project/slicing/DependencyGraphTest.java +++ b/keyext.slicing/src/test/java/org/key_project/slicing/DependencyGraphTest.java @@ -58,14 +58,14 @@ void basicTest() { var incomingClosedGoal = graph.incomingGraphEdgesOf(closedGoal).toList(); assertEquals(1, incomingClosedGoal.size()); - assertEquals(formB, incomingClosedGoal.get(0).second); + assertEquals(formB, incomingClosedGoal.get(0).toNode()); var incomingFormB = graph.incomingGraphEdgesOf(formB).toList(); assertEquals(2, incomingFormB.size()); - if (incomingFormB.get(0).second.equals(formA)) { - assertEquals(formC, incomingFormB.get(1).second); + if (incomingFormB.get(0).toNode().equals(formA)) { + assertEquals(formC, incomingFormB.get(1).toNode()); } else { - assertEquals(formA, incomingFormB.get(1).second); + assertEquals(formA, incomingFormB.get(1).toNode()); } assertTrue(graph.containsNode(formA));