Skip to content

Commit dbe8815

Browse files
wadoonwadoon
committed
clean and fix tests
1 parent 7c9bf8d commit dbe8815

39 files changed

+611
-422
lines changed

‎build.gradle‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -109,6 +109,7 @@ subprojects {
109109
testImplementation ("org.junit.jupiter:junit-jupiter-params")
110110
testRuntimeOnly ("org.junit.jupiter:junit-jupiter-engine")
111111
testRuntimeOnly ("org.junit.platform:junit-platform-launcher")
112+
testImplementation ("org.assertj:assertj-core:3.26.3")
112113
testImplementation project(':key.util')
113114

114115
}

‎key.core/src/main/java/de/uka/ilkd/key/scripts/AbstractCommand.java‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,7 @@ public List<ProofScriptArgument> getArguments() {
5656
if (parameterClazz == null) {
5757
return new ArrayList<>();
5858
}
59-
return ArgumentsLifter.inferScriptArguments(parameterClazz, this);
59+
return ArgumentsLifter.inferScriptArguments(parameterClazz);
6060
}
6161

6262

@@ -89,10 +89,11 @@ public void execute(ScriptCommandAst args) throws ScriptException, InterruptedEx
8989

9090
@Override
9191
public String getDocumentation() {
92-
if (documentation == null) {
93-
documentation = ArgumentsLifter.extractDocumentation(parameterClazz);
92+
if (documentation == null && parameterClazz != null) {
93+
documentation =
94+
ArgumentsLifter.extractDocumentation(getName(), getClass(), parameterClazz);
9495
}
95-
return documentation;
96+
return Objects.requireNonNullElse(documentation, "");
9697
}
9798

9899
}

‎key.core/src/main/java/de/uka/ilkd/key/scripts/AssertCommand.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ public AssertCommand() {
2525

2626
@Override
2727
public void execute(ScriptCommandAst arguments) throws ScriptException, InterruptedException {
28-
var args = state().getValueInjector().inject(this, new Parameters(), arguments);
28+
var args = state().getValueInjector().inject(new Parameters(), arguments);
2929

3030
if (args.goals == null) {
3131
throw new ScriptException("No parameter specified!");

‎key.core/src/main/java/de/uka/ilkd/key/scripts/AssumeCommand.java‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,8 @@
77
import de.uka.ilkd.key.rule.NoPosTacletApp;
88
import de.uka.ilkd.key.rule.Taclet;
99
import de.uka.ilkd.key.rule.TacletApp;
10-
import de.uka.ilkd.key.scripts.meta.Option;
10+
import de.uka.ilkd.key.scripts.meta.Argument;
11+
import de.uka.ilkd.key.scripts.meta.Documentation;
1112

1213
import org.key_project.logic.Name;
1314
import org.key_project.logic.op.sv.SchemaVariable;
@@ -45,7 +46,7 @@ public String getDocumentation() {
4546

4647
public void execute(ScriptCommandAst arguments) throws ScriptException, InterruptedException {
4748
var parameter = state().getValueInjector()
48-
.inject(this, new FormulaParameter(), arguments);
49+
.inject(new FormulaParameter(), arguments);
4950
Taclet cut =
5051
state.getProof().getEnv().getInitConfigForEnvironment().lookupActiveTaclet(TACLET_NAME);
5152
TacletApp app = NoPosTacletApp.createNoPosTacletApp(cut);
@@ -57,8 +58,8 @@ public void execute(ScriptCommandAst arguments) throws ScriptException, Interrup
5758
}
5859

5960
public static class FormulaParameter {
60-
@Option(value = "#2", help = "The formula to be assumed.")
61-
@MonotonicNonNull
62-
public JTerm formula;
61+
@Argument
62+
@Documentation("The formula to be assumed.")
63+
public @MonotonicNonNull JTerm formula;
6364
}
6465
}

‎key.core/src/main/java/de/uka/ilkd/key/scripts/AutoCommand.java‎

Lines changed: 29 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@
1313
import de.uka.ilkd.key.proof.init.Profile;
1414
import de.uka.ilkd.key.prover.impl.ApplyStrategy;
1515
import de.uka.ilkd.key.scripts.meta.Documentation;
16+
import de.uka.ilkd.key.scripts.meta.Flag;
1617
import de.uka.ilkd.key.scripts.meta.Option;
1718
import de.uka.ilkd.key.strategy.FocussedBreakpointRuleApplicationManager;
1819
import de.uka.ilkd.key.strategy.StrategyProperties;
@@ -53,7 +54,7 @@ public String getDocumentation() {
5354

5455
@Override
5556
public void execute(ScriptCommandAst args) throws ScriptException, InterruptedException {
56-
var arguments = state().getValueInjector().inject(this, new AutoCommand.Parameters(), args);
57+
var arguments = state().getValueInjector().inject(new AutoCommand.Parameters(), args);
5758
final Services services = state().getProof().getServices();
5859
final Profile profile = services.getProfile();
5960

@@ -175,50 +176,47 @@ private void setupFocussedBreakpointStrategy(final String maybeMatchesRegEx,
175176
changes.""")
176177
public static class Parameters {
177178
// @ TODO Deprecated with the higher order proof commands?
178-
@Option(value = "all", required = false,
179-
help = "Apply the strategy on all open goals. There is a better syntax for that now.")
179+
@Flag(value = "all")
180+
@Documentation("Apply the strategy on all open goals. There is a better syntax for that now.")
180181
public boolean onAllOpenGoals = false;
181182

182-
@Option(value = "steps", required = false,
183-
help = "The maximum number of steps to be performed.")
183+
@Option(value = "steps")
184+
@Documentation("The maximum number of steps to be performed.")
184185
public int maxSteps = -1;
185186

186187
/**
187188
* Run on formula matching the given regex
188189
*/
189-
@Option(value = "matches", required = false,
190-
help = "Run on formula matching the given regex.")
190+
@Option(value = "matches")
191+
@Documentation("Run on formula matching the given regex.")
191192
public @Nullable String matches = null;
192193

193194
/**
194195
* Run on formula matching the given regex
195196
*/
196-
@Option(value = "breakpoint", required = false,
197-
help = "Run on formula matching the given regex.")
197+
@Option(value = "breakpoint")
198+
@Documentation("Run on formula matching the given regex.")
198199
public @Nullable String breakpoint = null;
199200

200-
@Option(value = "modelsearch", required = false,
201-
help = "Enable model search. Better for some types of arithmetic problems. Sometimes a lot worse")
202-
@Nullable
203-
public Boolean modelSearch;
204-
205-
@Option(value = "expandQueries", required = false, help = "Expand queries by modalities.")
206-
@Nullable
207-
public Boolean expandQueries;
208-
209-
@Option(value = "classAxioms", required = false,
210-
help = "Enable class axioms. This expands model methods and fields and invariants quite eagerly. "
211-
+
212-
"May lead to divergence.")
213-
@Nullable
214-
public Boolean classAxioms;
215-
216-
@Option(value = "dependencies", required = false,
217-
help = "Enable dependency reasoning. In modular reasoning, the value of symbols may stay the same, "
218-
+
219-
"without that its definition is known. May be an enabler, may be a showstopper.")
220-
@Nullable
221-
public Boolean dependencies;
201+
@Flag(value = "modelsearch")
202+
@Documentation("Enable model search. Better for some types of arithmetic problems. Sometimes a lot worse")
203+
public boolean modelSearch;
204+
205+
@Flag(value = "expandQueries")
206+
@Documentation("Expand queries by modalities.")
207+
public boolean expandQueries;
208+
209+
@Flag(value = "classAxioms")
210+
@Documentation("""
211+
Enable class axioms. This expands model methods and fields and invariants quite eagerly. \
212+
May lead to divergence.""")
213+
public boolean classAxioms;
214+
215+
@Flag(value = "dependencies")
216+
@Documentation("""
217+
Enable dependency reasoning. In modular reasoning, the value of symbols may stay the same, \
218+
without that its definition is known. May be an enabler, may be a showstopper.""")
219+
public boolean dependencies;
222220

223221
public int getSteps() {
224222
return maxSteps;

‎key.core/src/main/java/de/uka/ilkd/key/scripts/AxiomCommand.java‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8,11 +8,13 @@
88
import de.uka.ilkd.key.rule.NoPosTacletApp;
99
import de.uka.ilkd.key.rule.Taclet;
1010
import de.uka.ilkd.key.rule.TacletApp;
11-
import de.uka.ilkd.key.scripts.meta.Option;
11+
import de.uka.ilkd.key.scripts.meta.Argument;
1212

1313
import org.key_project.logic.Name;
1414
import org.key_project.logic.op.sv.SchemaVariable;
1515

16+
import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
17+
1618
/**
1719
* The axiom command takes one argument: a formula to which the command is applied.
1820
*
@@ -33,7 +35,7 @@ public String getName() {
3335

3436
@Override
3537
public void execute(ScriptCommandAst args) throws ScriptException, InterruptedException {
36-
var parameter = state().getValueInjector().inject(this, new FormulaParameter(), args);
38+
var parameter = state().getValueInjector().inject(new FormulaParameter(), args);
3739

3840
Taclet cut = state().getProof().getEnv()
3941
.getInitConfigForEnvironment().lookupActiveTaclet(TACLET_NAME);
@@ -46,7 +48,7 @@ public void execute(ScriptCommandAst args) throws ScriptException, InterruptedEx
4648
}
4749

4850
public static class FormulaParameter {
49-
@Option("#2")
50-
public JTerm formula;
51+
@Argument
52+
public @MonotonicNonNull JTerm formula;
5153
}
5254
}

‎key.core/src/main/java/de/uka/ilkd/key/scripts/CutCommand.java‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8,11 +8,13 @@
88
import de.uka.ilkd.key.rule.NoPosTacletApp;
99
import de.uka.ilkd.key.rule.Taclet;
1010
import de.uka.ilkd.key.rule.TacletApp;
11-
import de.uka.ilkd.key.scripts.meta.Option;
11+
import de.uka.ilkd.key.scripts.meta.Argument;
1212

1313
import org.key_project.logic.Name;
1414
import org.key_project.logic.op.sv.SchemaVariable;
1515

16+
import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
17+
1618
/**
1719
* The command object CutCommand has as scriptcommand name "cut" As parameters: a formula with the
1820
* id "#2"
@@ -42,7 +44,7 @@ public String getDocumentation() {
4244
public void execute(AbstractUserInterfaceControl uiControl, ScriptCommandAst arguments,
4345
EngineState state)
4446
throws ScriptException, InterruptedException {
45-
var args = state.getValueInjector().inject(this, new Parameters(), arguments);
47+
var args = state.getValueInjector().inject(new Parameters(), arguments);
4648
execute(state, args);
4749
}
4850

@@ -58,8 +60,8 @@ static void execute(EngineState state, Parameters args) throws ScriptException {
5860
}
5961

6062
public static class Parameters {
61-
@Option("#2")
62-
public JTerm formula;
63+
@Argument
64+
public @MonotonicNonNull JTerm formula;
6365
}
6466

6567
}

‎key.core/src/main/java/de/uka/ilkd/key/scripts/EchoCommand.java‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,9 @@
55

66

77
import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
8-
import de.uka.ilkd.key.scripts.meta.Option;
8+
import de.uka.ilkd.key.scripts.meta.Argument;
9+
10+
import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
911

1012
/**
1113
* A simple "echo" command for giving feedback to human observers during lengthy executions.
@@ -24,7 +26,7 @@ public String getName() {
2426
public void execute(AbstractUserInterfaceControl uiControl, ScriptCommandAst args,
2527
EngineState state)
2628
throws ScriptException, InterruptedException {
27-
var params = state.getValueInjector().inject(this, new Parameters(), args);
29+
var params = state.getValueInjector().inject(new Parameters(), args);
2830

2931
var obs = state.getObserver();
3032
if (obs != null) {
@@ -36,8 +38,8 @@ public static class Parameters {
3638
/**
3739
* The message to show.
3840
*/
39-
@Option("#2")
40-
public String message;
41+
@Argument
42+
public @MonotonicNonNull String message;
4143
}
4244

4345
}

‎key.core/src/main/java/de/uka/ilkd/key/scripts/FocusCommand.java‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@
1313
import de.uka.ilkd.key.rule.Taclet;
1414
import de.uka.ilkd.key.rule.TacletApp;
1515
import de.uka.ilkd.key.rule.inst.SVInstantiations;
16-
import de.uka.ilkd.key.scripts.meta.Option;
16+
import de.uka.ilkd.key.scripts.meta.Argument;
1717

1818
import org.key_project.logic.Name;
1919
import org.key_project.logic.PosInTerm;
@@ -24,6 +24,8 @@
2424
import org.key_project.prover.sequent.SequentFormula;
2525
import org.key_project.util.collection.ImmutableList;
2626

27+
import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
28+
2729
import static de.uka.ilkd.key.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY;
2830

2931
/**
@@ -47,13 +49,13 @@ public FocusCommand() {
4749
}
4850

4951
static class Parameters {
50-
@Option("#2")
51-
public Sequent toKeep;
52+
@Argument
53+
public @MonotonicNonNull Sequent toKeep;
5254
}
5355

5456
@Override
5557
public void execute(ScriptCommandAst args) throws ScriptException, InterruptedException {
56-
var s = state().getValueInjector().inject(this, new Parameters(), args);
58+
var s = state().getValueInjector().inject(new Parameters(), args);
5759

5860
Sequent toKeep = s.toKeep;
5961
hideAll(toKeep);

‎key.core/src/main/java/de/uka/ilkd/key/scripts/HideCommand.java‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@
99
import de.uka.ilkd.key.rule.NoPosTacletApp;
1010
import de.uka.ilkd.key.rule.Taclet;
1111
import de.uka.ilkd.key.rule.TacletApp;
12-
import de.uka.ilkd.key.scripts.meta.Option;
12+
import de.uka.ilkd.key.scripts.meta.Argument;
1313

1414
import org.key_project.logic.Name;
1515
import org.key_project.logic.PosInTerm;
@@ -20,6 +20,8 @@
2020
import org.key_project.prover.sequent.Sequent;
2121
import org.key_project.prover.sequent.SequentFormula;
2222

23+
import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
24+
2325
import static de.uka.ilkd.key.logic.equality.TermLabelsProperty.TERM_LABELS_PROPERTY;
2426

2527
/**
@@ -47,7 +49,7 @@ public HideCommand() {
4749

4850
@Override
4951
public void execute(ScriptCommandAst arguments) throws ScriptException, InterruptedException {
50-
var args = state().getValueInjector().inject(this, new Parameters(), arguments);
52+
var args = state().getValueInjector().inject(new Parameters(), arguments);
5153

5254
Goal goal = state().getFirstOpenAutomaticGoal();
5355

@@ -98,7 +100,8 @@ public String getName() {
98100
}
99101

100102
public static class Parameters {
101-
@Option("#2")
103+
@Argument
104+
@MonotonicNonNull
102105
public Sequent sequent;
103106
}
104107

0 commit comments

Comments
 (0)