Skip to content

Commit

Permalink
Apply spotless
Browse files Browse the repository at this point in the history
  • Loading branch information
@wadoon
wadoon committed Mar 31, 2023
1 parent 3cb2bf9 commit ee6710c
Show file tree
Hide file tree
Showing 1,691 changed files with 5,764 additions and 5,351 deletions.
5 changes: 3 additions & 2 deletions key.core.example/src/main/java/org/key_project/Main.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,6 @@
import java.util.List;
import java.util.Set;

import org.key_project.util.collection.ImmutableSet;

import de.uka.ilkd.key.control.KeYEnvironment;
import de.uka.ilkd.key.java.abstraction.KeYJavaType;
import de.uka.ilkd.key.logic.op.IObserverFunction;
Expand All @@ -20,6 +18,9 @@
import de.uka.ilkd.key.strategy.StrategyProperties;
import de.uka.ilkd.key.util.KeYTypeUtil;
import de.uka.ilkd.key.util.MiscTools;

import org.key_project.util.collection.ImmutableSet;

import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

Expand Down
5 changes: 3 additions & 2 deletions ...e.proof_references/src/main/java/de/uka/ilkd/key/proof_references/ProofReferenceUtil.java
View file
Original file line number Diff line number Diff line change
@@ -1,17 +1,18 @@
package de.uka.ilkd.key.proof_references;

import java.util.LinkedHashSet;

import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.proof.ProofVisitor;
import de.uka.ilkd.key.proof_references.analyst.*;
import de.uka.ilkd.key.proof_references.reference.IProofReference;

import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;
import org.key_project.util.java.CollectionUtil;

import java.util.LinkedHashSet;

/**
* <p>
* This class provides static methods to compute proof references. A proof reference is a source
Expand Down
6 changes: 3 additions & 3 deletions ...e/uka/ilkd/key/proof_references/analyst/ClassAxiomAndInvariantProofReferencesAnalyst.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,6 @@
import java.util.Iterator;
import java.util.LinkedHashSet;

import org.key_project.util.collection.DefaultImmutableSet;
import org.key_project.util.collection.ImmutableSet;

import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.java.abstraction.KeYJavaType;
import de.uka.ilkd.key.logic.Name;
Expand All @@ -23,6 +20,9 @@
import de.uka.ilkd.key.util.MiscTools;
import de.uka.ilkd.key.util.Pair;

import org.key_project.util.collection.DefaultImmutableSet;
import org.key_project.util.collection.ImmutableSet;

/**
* Extracts used {@link ClassAxiom} and {@link ClassInvariant}s.
*
Expand Down
6 changes: 3 additions & 3 deletions .../main/java/de/uka/ilkd/key/proof_references/analyst/MethodCallProofReferencesAnalyst.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,6 @@

import java.util.LinkedHashSet;

import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.collection.ImmutableSLList;

import de.uka.ilkd.key.java.JavaTools;
import de.uka.ilkd.key.java.ProgramElement;
import de.uka.ilkd.key.java.Services;
Expand All @@ -30,6 +27,9 @@
import de.uka.ilkd.key.rule.RuleApp;
import de.uka.ilkd.key.util.MiscTools;

import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.collection.ImmutableSLList;

/**
* Extracts called methods.
*
Expand Down
6 changes: 3 additions & 3 deletions ...ences/src/main/java/de/uka/ilkd/key/proof_references/reference/DefaultProofReference.java
View file
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
package de.uka.ilkd.key.proof_references.reference;

import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof;

import java.util.Collection;
import java.util.LinkedHashSet;
import java.util.Objects;

import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof;

/**
* Default implementation of {@link IProofReference}.
*
Expand Down
13 changes: 7 additions & 6 deletions ...c/test/java/de/uka/ilkd/key/proof_references/testcase/AbstractProofReferenceTestCase.java
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,11 @@
package de.uka.ilkd.key.proof_references.testcase;

import java.io.File;
import java.util.HashMap;
import java.util.Iterator;
import java.util.LinkedHashSet;
import java.util.function.Predicate;

import de.uka.ilkd.key.control.KeYEnvironment;
import de.uka.ilkd.key.java.abstraction.KeYJavaType;
import de.uka.ilkd.key.logic.Choice;
Expand All @@ -18,19 +24,14 @@
import de.uka.ilkd.key.speclang.FunctionalOperationContract;
import de.uka.ilkd.key.strategy.StrategyProperties;
import de.uka.ilkd.key.util.HelperClassForTests;

import org.key_project.util.collection.DefaultImmutableSet;
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.helper.FindResources;
import org.key_project.util.java.CollectionUtil;

import java.io.File;
import java.util.HashMap;
import java.util.Iterator;
import java.util.LinkedHashSet;
import java.util.function.Predicate;

import static org.junit.jupiter.api.Assertions.*;

/**
Expand Down
1 change: 1 addition & 0 deletions ...f_references/src/test/java/de/uka/ilkd/key/proof_references/testcase/TestKeYTypeUtil.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.java.abstraction.KeYJavaType;
import de.uka.ilkd.key.util.KeYTypeUtil;

import org.junit.jupiter.api.Assertions;
import org.junit.jupiter.api.Test;

Expand Down
8 changes: 5 additions & 3 deletions ...ences/src/test/java/de/uka/ilkd/key/proof_references/testcase/TestProofReferenceUtil.java
View file
Original file line number Diff line number Diff line change
@@ -1,18 +1,20 @@
package de.uka.ilkd.key.proof_references.testcase;

import java.io.File;
import java.util.LinkedHashSet;

import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.proof_references.ProofReferenceUtil;
import de.uka.ilkd.key.proof_references.analyst.ContractProofReferencesAnalyst;
import de.uka.ilkd.key.proof_references.analyst.IProofReferencesAnalyst;
import de.uka.ilkd.key.proof_references.analyst.MethodBodyExpandProofReferencesAnalyst;
import de.uka.ilkd.key.proof_references.reference.IProofReference;
import org.junit.jupiter.api.Test;

import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;

import java.io.File;
import java.util.LinkedHashSet;
import org.junit.jupiter.api.Test;

/**
* Tests for {@link ProofReferenceUtil}.
Expand Down
1 change: 1 addition & 0 deletions ...y/proof_references/testcase/analyst/TestClassAxiomAndInvariantProofReferencesAnalyst.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
import de.uka.ilkd.key.proof_references.analyst.ClassAxiomAndInvariantProofReferencesAnalyst;
import de.uka.ilkd.key.proof_references.reference.IProofReference;
import de.uka.ilkd.key.proof_references.testcase.AbstractProofReferenceTestCase;

import org.junit.jupiter.api.Test;

/**
Expand Down
1 change: 1 addition & 0 deletions ...de/uka/ilkd/key/proof_references/testcase/analyst/TestContractProofReferencesAnalyst.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
import de.uka.ilkd.key.proof_references.analyst.ContractProofReferencesAnalyst;
import de.uka.ilkd.key.proof_references.reference.IProofReference;
import de.uka.ilkd.key.proof_references.testcase.AbstractProofReferenceTestCase;

import org.junit.jupiter.api.Test;

/**
Expand Down
1 change: 1 addition & 0 deletions ...lkd/key/proof_references/testcase/analyst/TestMethodBodyExpandProofReferencesAnalyst.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
import de.uka.ilkd.key.proof_references.analyst.MethodBodyExpandProofReferencesAnalyst;
import de.uka.ilkd.key.proof_references.reference.IProofReference;
import de.uka.ilkd.key.proof_references.testcase.AbstractProofReferenceTestCase;

import org.junit.jupiter.api.Test;

/**
Expand Down
1 change: 1 addition & 0 deletions .../uka/ilkd/key/proof_references/testcase/analyst/TestMethodCallProofReferencesAnalyst.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
import de.uka.ilkd.key.proof_references.analyst.MethodCallProofReferencesAnalyst;
import de.uka.ilkd.key.proof_references.reference.IProofReference;
import de.uka.ilkd.key.proof_references.testcase.AbstractProofReferenceTestCase;

import org.junit.jupiter.api.Test;

/**
Expand Down
1 change: 1 addition & 0 deletions .../uka/ilkd/key/proof_references/testcase/analyst/TestProgramVariableReferencesAnalyst.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
import de.uka.ilkd.key.proof_references.analyst.ProgramVariableReferencesAnalyst;
import de.uka.ilkd.key.proof_references.reference.IProofReference;
import de.uka.ilkd.key.proof_references.testcase.AbstractProofReferenceTestCase;

import org.junit.jupiter.api.Test;

/**
Expand Down
7 changes: 4 additions & 3 deletions key.core.symbolic_execution.example/src/main/java/org/key_project/example/Main.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,6 @@
import java.util.HashMap;
import java.util.List;

import org.key_project.util.collection.ImmutableSLList;
import org.key_project.util.java.StringUtil;

import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
import de.uka.ilkd.key.control.KeYEnvironment;
import de.uka.ilkd.key.java.abstraction.KeYJavaType;
Expand All @@ -29,6 +26,10 @@
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionEnvironment;
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
import de.uka.ilkd.key.util.MiscTools;

import org.key_project.util.collection.ImmutableSLList;
import org.key_project.util.java.StringUtil;

import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

Expand Down
5 changes: 3 additions & 2 deletions ...cution/src/main/java/de/uka/ilkd/key/rule/label/BlockContractValidityTermLabelUpdate.java
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
package de.uka.ilkd.key.rule.label;

import java.util.Set;

import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.JavaBlock;
import de.uka.ilkd.key.logic.Name;
Expand All @@ -15,13 +17,12 @@
import de.uka.ilkd.key.rule.Rule;
import de.uka.ilkd.key.rule.RuleApp;
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;

import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;
import org.key_project.util.java.CollectionUtil;

import java.util.Set;

/**
* Makes sure that {@link BlockContractValidityTermLabel} is introduced when a
* {@link BlockContractInternalRule} is applied.
Expand Down
3 changes: 0 additions & 3 deletions ...e.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelMerger.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,8 @@

import java.util.ArrayList;
import java.util.Arrays;
import java.util.LinkedList;
import java.util.List;

import org.key_project.util.java.CollectionUtil;

import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.label.FormulaTermLabel;
Expand Down
5 changes: 3 additions & 2 deletions ...bolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelRefactoring.java
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
package de.uka.ilkd.key.rule.label;

import java.util.*;

import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.*;
import de.uka.ilkd.key.logic.label.FormulaTermLabel;
Expand All @@ -11,11 +13,10 @@
import de.uka.ilkd.key.rule.SyntacticalReplaceVisitor;
import de.uka.ilkd.key.rule.merge.CloseAfterMerge;
import de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil;

import org.key_project.util.collection.ImmutableList;
import org.key_project.util.java.CollectionUtil;

import java.util.*;

/**
* The {@link TermLabelRefactoring} used to label predicates with a {@link FormulaTermLabel} on
* applied loop invariants or operation contracts.
Expand Down
13 changes: 7 additions & 6 deletions ...e.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,11 @@
package de.uka.ilkd.key.rule.label;

import java.util.Collections;
import java.util.LinkedHashMap;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Set;

import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.*;
import de.uka.ilkd.key.logic.label.FormulaTermLabel;
Expand All @@ -15,16 +21,11 @@
import de.uka.ilkd.key.rule.Taclet.TacletLabelHint.TacletOperation;
import de.uka.ilkd.key.rule.TacletApp;
import de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil;

import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.java.CollectionUtil;

import java.util.Collections;
import java.util.LinkedHashMap;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Set;

/**
* The {@link TermLabelUpdate} used to label predicates with a {@link FormulaTermLabel} of add
* clauses which were not labeled before.
Expand Down
8 changes: 4 additions & 4 deletions ....symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/LoopBodyTermLabelUpdate.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,10 +2,6 @@

import java.util.Set;

import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;

import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.JavaBlock;
import de.uka.ilkd.key.logic.Name;
Expand All @@ -20,6 +16,10 @@
import de.uka.ilkd.key.rule.WhileInvariantRule;
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;

import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;

/**
* Makes sure that {@link SymbolicExecutionUtil#LOOP_BODY_LABEL} is introduced when a
* {@link WhileInvariantRule} is applied.
Expand Down
8 changes: 4 additions & 4 deletions .../src/main/java/de/uka/ilkd/key/rule/label/LoopInvariantNormalBehaviorTermLabelUpdate.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,10 +2,6 @@

import java.util.Set;

import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;

import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.JavaBlock;
import de.uka.ilkd.key.logic.Name;
Expand All @@ -20,6 +16,10 @@
import de.uka.ilkd.key.rule.WhileInvariantRule;
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;

import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;

/**
* Makes sure that {@link SymbolicExecutionUtil#LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL} is introduced
* when a {@link WhileInvariantRule} is applied.
Expand Down
6 changes: 3 additions & 3 deletions ...n/src/main/java/de/uka/ilkd/key/rule/label/RemoveInCheckBranchesTermLabelRefactoring.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,6 @@
import java.util.Iterator;
import java.util.List;

import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;

import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.Name;
import de.uka.ilkd.key.logic.PosInOccurrence;
Expand All @@ -22,6 +19,9 @@
import de.uka.ilkd.key.rule.UseOperationContractRule;
import de.uka.ilkd.key.rule.WhileInvariantRule;

import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;

/**
* This {@link TermLabelRefactoring} removes the supported {@link TermLabel} in check branches.
* These are:
Expand Down
9 changes: 5 additions & 4 deletions ...olic_execution/src/main/java/de/uka/ilkd/key/rule/label/StayOnFormulaTermLabelPolicy.java
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,9 @@
package de.uka.ilkd.key.rule.label;

import java.util.Deque;
import java.util.LinkedHashSet;
import java.util.Set;

import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.JavaBlock;
import de.uka.ilkd.key.logic.PosInOccurrence;
Expand All @@ -13,13 +17,10 @@
import de.uka.ilkd.key.rule.Taclet.TacletLabelHint;
import de.uka.ilkd.key.rule.Taclet.TacletLabelHint.TacletOperation;
import de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil;

import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.java.CollectionUtil;

import java.util.Deque;
import java.util.LinkedHashSet;
import java.util.Set;

/**
* This {@link TermLabelPolicy} maintains a {@link FormulaTermLabel} on predicates.
*
Expand Down

0 comments on commit ee6710c

Please sign in to comment.