diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java index 52faa9af592..e56d8566542 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java @@ -325,4 +325,9 @@ public static boolean isTruthValueEvaluationEnabled(Profile profile) { return false; } } + + @Override + public String displayName() { + return NAME; + } } 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 82850b88104..ae8cb696a91 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 @@ -27,7 +27,6 @@ import de.uka.ilkd.key.rule.BuiltInRule; import de.uka.ilkd.key.rule.OneStepSimplifier; import de.uka.ilkd.key.rule.Taclet; -import de.uka.ilkd.key.rule.tacletbuilder.TacletBuilder; import de.uka.ilkd.key.settings.ProofSettings; import de.uka.ilkd.key.strategy.StrategyProperties; import de.uka.ilkd.key.symbolic_execution.profile.SimplifyTermProfile; @@ -817,9 +816,7 @@ protected ImmutableList computeTermLabelConfiguration() ? new ProofSettings(sourceInitConfig.getSettings()) : null; initConfig.setSettings(clonedSettings); - initConfig.setTaclet2Builder( - (HashMap>) sourceInitConfig.getTaclet2Builder() - .clone()); + initConfig.setTaclet2Builder(new HashMap<>(sourceInitConfig.getTaclet2Builder())); initConfig.setTaclets(sourceInitConfig.getTaclets()); // Create new ProofEnvironment and initialize it with values from initial one. ProofEnvironment env = new ProofEnvironment(initConfig); diff --git a/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdProfile.java b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdProfile.java index e5f650a2b08..40fd625c061 100644 --- a/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdProfile.java +++ b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdProfile.java @@ -15,11 +15,14 @@ import de.uka.ilkd.key.proof.io.RuleSourceFactory; import de.uka.ilkd.key.proof.mgt.SpecificationRepository; import de.uka.ilkd.key.rule.*; +import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.util.KeYResourceManager; import org.key_project.logic.Name; import org.key_project.util.collection.ImmutableList; +import org.jspecify.annotations.Nullable; + /** * @author Alexander Weigl * @version 1 (7/27/25) @@ -97,9 +100,19 @@ public RuleCollection getStandardRules() { return wdStandardRules; } + /// {@inheritDoc} + /// + /// @param additionalProfileOptions a string representing the choice of `wdOperator` @Override - public void prepareInitConfig(InitConfig baseConfig) { + public void prepareInitConfig(InitConfig baseConfig, + @Nullable Configuration additionalProfileOptions) { var wdChoice = baseConfig.choiceNS().lookup(new Name("wdChecks:on")); baseConfig.activateChoice(wdChoice); + + if (additionalProfileOptions != null) { + var wdOperator = + baseConfig.choiceNS().lookup(new Name(additionalProfileOptions.toString())); + baseConfig.activateChoice(wdOperator); + } } } diff --git a/key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdHeader.key b/key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdHeader.key index 75c567a0e8b..0081871d19e 100644 --- a/key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdHeader.key +++ b/key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdHeader.key @@ -2,6 +2,51 @@ * KeY is licensed under the GNU General Public License Version 2 * SPDX-License-Identifier: GPL-2.0-only */ +\optionsDecl { + /*! + Treatment of formulas and terms for welldefinedness checks: + */ + wdOperator: { + /*! + More intuitive for software developers and along the lines of + runtime assertion semantics. Well-Definedness checks will be + stricter using this operator, since the order of terms/formulas + matters. It is based on McCarthy logic. + Cf. "Are the Logical Foundations of Verifying Compiler + Prototypes Matching User Expectations?" by Patrice Chalin. + + @choiceDefaultOption + */ + L, + /*! + Complete and along the lines of classical logic, where the + order of terms/formulas is irrelevant. This operator is + equivalent to the D-operator, but more efficient. + Cf. "Efficient Well-Definedness Checking" by Ádám Darvas, + Farhad Mehta, and Arsenii Rudich. + */ + Y, + /*! + Complete and along the lines of classical logic, where the + order of terms/formulas is irrelevant. This operator is not as + strict as the L-operator, based on strong Kleene logic. To be + used with care, since formulas may blow up exponentially. + Cf. "Well Defined B" by Patrick Behm, Lilian Burdy, and + Jean-Marc Meynadier*/ + D + }; + + /*! + Welldefinedness checks of JML specifications can be turned on/off. + This includes class invariants, operation contracts, model fields + as well as JML (annotation) statements as loop invariants and + block contracts. The former ones are checked "on-the-fly", i.e., + directly when they are applied in the code while proving an operation + contract, since the context is needed. + */ + wdChecks: {off, on}; +} + \transformers { \formula wd(any); \formula WD(\formula); diff --git a/key.core/src/main/antlr4/KeYParser.g4 b/key.core/src/main/antlr4/KeYParser.g4 index f111efcedec..19ac344e83e 100644 --- a/key.core/src/main/antlr4/KeYParser.g4 +++ b/key.core/src/main/antlr4/KeYParser.g4 @@ -90,11 +90,11 @@ one_sort_decl : doc=DOC_COMMENT? ( - GENERIC sortIds=simple_ident_dots_comma_list + GENERIC sortIds=simple_ident_dots_comma_list_with_docs (ONEOF sortOneOf = oneof_sorts)? (EXTENDS sortExt = extends_sorts)? SEMI - | PROXY sortIds=simple_ident_dots_comma_list (EXTENDS sortExt=extends_sorts)? SEMI - | ABSTRACT? sortIds=simple_ident_dots_comma_list (EXTENDS sortExt=extends_sorts)? SEMI + | PROXY sortIds=simple_ident_dots_comma_list_with_docs (EXTENDS sortExt=extends_sorts)? SEMI + | ABSTRACT? sortIds=simple_ident_dots_comma_list_with_docs (EXTENDS sortExt=extends_sorts)? SEMI ) ; @@ -108,6 +108,13 @@ simple_ident_dots_comma_list simple_ident_dots (COMMA simple_ident_dots)* ; +simple_ident_dots_comma_list_with_docs +: + simple_ident_dots_with_docs (COMMA simple_ident_dots_with_docs)* +; + +simple_ident_dots_with_docs: DOC_COMMENT? simple_ident_dots; + extends_sorts : @@ -132,7 +139,7 @@ prog_var_decls LBRACE ( kjt = keyjavatype - var_names = simple_ident_comma_list + var_names = simple_ident_comma_list_with_docs SEMI )* RBRACE @@ -154,6 +161,10 @@ simple_ident_comma_list id = simple_ident (COMMA id = simple_ident )* ; +simple_ident_comma_list_with_docs +: + id+=simple_ident_with_doc (COMMA id+=simple_ident_with_doc)* +; schema_var_decls : SCHEMAVARIABLES LBRACE @@ -250,6 +261,7 @@ datatype_decl: ; datatype_constructor: + doc=DOC_COMMENT? name=simple_ident ( LPAREN @@ -321,7 +333,12 @@ where_to_bind: ruleset_decls : - HEURISTICSDECL LBRACE (doc+=DOC_COMMENT? id+=simple_ident SEMI)* RBRACE + HEURISTICSDECL LBRACE (id+=simple_ident_with_doc SEMI)* RBRACE +; + +simple_ident_with_doc +: + doc=DOC_COMMENT? id=simple_ident ; sortId diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/TermLabelVisibilityManager.java b/key.core/src/main/java/de/uka/ilkd/key/control/TermLabelVisibilityManager.java index 4e04c3bec13..a248b1e0761 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/TermLabelVisibilityManager.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/TermLabelVisibilityManager.java @@ -157,7 +157,7 @@ public TermLabelVisibilityManagerListener[] getTermLabelVisibilityManagerListene /** * Fires the event - * {@link TermLabelVisibilityManagerListener#visibleLabelsChanged( TermLabelVisibilityManagerEvent)} + * {@link TermLabelVisibilityManagerListener#visibleLabelsChanged(TermLabelVisibilityManagerEvent)} * to all listeners. * * @param e The event object. diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java index 02cb218f130..092d72380cf 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java @@ -762,7 +762,7 @@ public DLEmbeddedExpression convert(EscapeExpression e) { sortName, e.getStartPosition())); } - var doc = sort.getDocumentation(); + var doc = namespaceSet.docs().find(sort); if (doc == null) { throw new ConvertException( diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/FinalHeapResolution.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/FinalHeapResolution.java index 72a3736dd7e..08c0e9d3519 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/FinalHeapResolution.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/FinalHeapResolution.java @@ -3,6 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.ldt; +import java.util.Objects; + import de.uka.ilkd.key.proof.init.InitConfig; import de.uka.ilkd.key.settings.ProofSettings; @@ -51,8 +53,8 @@ public static boolean isFinalEnabled(@NonNull InitConfig initConfig) { * @return true if final fields are treated as immutable */ public static boolean isFinalEnabled(@NonNull ProofSettings settings) { - return settings.getChoiceSettings().getDefaultChoices().get(SETTING) - .equals(IMMUTABLE_OPTION); + return Objects.equals(settings.getChoiceSettings().getDefaultChoices().get(SETTING), + IMMUTABLE_OPTION); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/DocSpace.java b/key.core/src/main/java/de/uka/ilkd/key/logic/DocSpace.java new file mode 100644 index 00000000000..3457be0300b --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/DocSpace.java @@ -0,0 +1,69 @@ +/* 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.logic; + +import java.util.Map; +import java.util.TreeMap; + +import org.key_project.logic.HasDocumentation; + +import org.jspecify.annotations.NullMarked; +import org.jspecify.annotations.Nullable; + +@NullMarked +public class DocSpace { + private @Nullable DocSpace parent; + private final Map documentation = new TreeMap<>(); + + public DocSpace() {} + + public DocSpace(Map documentation) { + this.documentation.putAll(documentation); + } + + public DocSpace(DocSpace parent) { + this.parent = parent; + } + + public DocSpace(@Nullable DocSpace parent, Map documentation) { + this(documentation); + this.parent = parent; + } + + public @Nullable String find(String key) { + var value = documentation.get(key); + if (value != null) + return value; + if (parent != null) + return parent.find(key); + return null; + } + + public @Nullable String find(HasDocumentation entity) { + var doc = entity.getDocumentation(); + if (doc != null) { + return doc; + } + return find(entity.getDocumentationKey()); + } + + public void add(DocSpace space) { + this.documentation.putAll(space.documentation); + } + + public @Nullable DocSpace parent() { + return parent; + } + + public void describe(HasDocumentation entity, @Nullable String doc) { + if (doc == null) { + return; + } + documentation.put(entity.getDocumentationKey(), doc); + } + + public DocSpace copy() { + return new DocSpace(parent, documentation); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/NamespaceSet.java b/key.core/src/main/java/de/uka/ilkd/key/logic/NamespaceSet.java index e87be8f8072..bf78a24494e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/NamespaceSet.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/NamespaceSet.java @@ -4,6 +4,8 @@ package de.uka.ilkd.key.logic; +import java.util.Objects; + import de.uka.ilkd.key.logic.op.IProgramVariable; import org.key_project.logic.Choice; @@ -15,44 +17,56 @@ import org.key_project.logic.sort.Sort; import org.key_project.prover.rules.RuleSet; -import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.NullMarked; +@NullMarked public class NamespaceSet { - private Namespace<@NonNull QuantifiableVariable> varNS = new Namespace<>(); - private Namespace<@NonNull IProgramVariable> progVarNS = new Namespace<>(); + private Namespace varNS = new Namespace<>(); + private Namespace progVarNS = new Namespace<>(); // TODO: Operators should not be local to goals - private Namespace<@NonNull Function> funcNS = new Namespace<>(); - private Namespace<@NonNull RuleSet> ruleSetNS = new Namespace<>(); - private Namespace<@NonNull Sort> sortNS = new Namespace<>(); - private Namespace<@NonNull Choice> choiceNS = new Namespace<>(); + private Namespace funcNS = new Namespace<>(); + private Namespace ruleSetNS = new Namespace<>(); + private Namespace sortNS = new Namespace<>(); + private Namespace choiceNS = new Namespace<>(); + private DocSpace documentation = new DocSpace(); public NamespaceSet() { } - public NamespaceSet(Namespace<@NonNull QuantifiableVariable> varNS, - Namespace<@NonNull Function> funcNS, - Namespace<@NonNull Sort> sortNS, Namespace<@NonNull RuleSet> ruleSetNS, - Namespace<@NonNull Choice> choiceNS, - Namespace<@NonNull IProgramVariable> programVarNS) { + public NamespaceSet(Namespace varNS, + Namespace funcNS, + Namespace sortNS, Namespace ruleSetNS, + Namespace choiceNS, + Namespace programVarNS) { + this(varNS, funcNS, sortNS, ruleSetNS, choiceNS, programVarNS, new DocSpace()); + } + + public NamespaceSet(Namespace varNS, + Namespace funcNS, + Namespace sortNS, Namespace ruleSetNS, + Namespace choiceNS, + Namespace programVarNS, + DocSpace documentation) { this.varNS = varNS; this.progVarNS = programVarNS; this.funcNS = funcNS; this.sortNS = sortNS; this.ruleSetNS = ruleSetNS; this.choiceNS = choiceNS; + this.documentation = Objects.requireNonNull(documentation); } public NamespaceSet copy() { return new NamespaceSet(variables().copy(), functions().copy(), sorts().copy(), - ruleSets().copy(), choices().copy(), programVariables().copy()); + ruleSets().copy(), choices().copy(), programVariables().copy(), + documentation.copy()); } public NamespaceSet shallowCopy() { return new NamespaceSet(variables(), functions(), sorts(), ruleSets(), - choices(), - programVariables()); + choices(), programVariables(), new DocSpace(documentation)); } // TODO MU: Rename into sth with wrap or similar @@ -60,54 +74,55 @@ public NamespaceSet copyWithParent() { return new NamespaceSet(new Namespace<>(variables()), new Namespace<>(functions()), new Namespace<>(sorts()), new Namespace<>(ruleSets()), new Namespace<>(choices()), - new Namespace<>(programVariables())); + new Namespace<>(programVariables()), + new DocSpace(documentation)); } - public Namespace<@NonNull QuantifiableVariable> variables() { + public Namespace variables() { return varNS; } - public void setVariables(Namespace<@NonNull QuantifiableVariable> varNS) { + public void setVariables(Namespace varNS) { this.varNS = varNS; } - public Namespace<@NonNull IProgramVariable> programVariables() { + public Namespace programVariables() { return progVarNS; } - public void setProgramVariables(Namespace<@NonNull IProgramVariable> progVarNS) { + public void setProgramVariables(Namespace progVarNS) { this.progVarNS = progVarNS; } - public Namespace<@NonNull Function> functions() { + public Namespace functions() { return funcNS; } - public void setFunctions(Namespace<@NonNull Function> funcNS) { + public void setFunctions(Namespace funcNS) { this.funcNS = funcNS; } - public Namespace<@NonNull RuleSet> ruleSets() { + public Namespace ruleSets() { return ruleSetNS; } - public void setRuleSets(Namespace<@NonNull RuleSet> ruleSetNS) { + public void setRuleSets(Namespace ruleSetNS) { this.ruleSetNS = ruleSetNS; } - public Namespace<@NonNull Sort> sorts() { + public Namespace sorts() { return sortNS; } - public void setSorts(Namespace<@NonNull Sort> sortNS) { + public void setSorts(Namespace sortNS) { this.sortNS = sortNS; } - public Namespace<@NonNull Choice> choices() { + public Namespace choices() { return choiceNS; } - public void setChoices(Namespace<@NonNull Choice> choiceNS) { + public void setChoices(Namespace choiceNS) { this.choiceNS = choiceNS; } @@ -211,12 +226,12 @@ public boolean isEmpty() { // create a namespace public NamespaceSet simplify() { return new NamespaceSet(varNS.simplify(), funcNS.simplify(), sortNS.simplify(), - ruleSetNS.simplify(), choiceNS.simplify(), progVarNS.simplify()); + ruleSetNS.simplify(), choiceNS.simplify(), progVarNS.simplify(), documentation); } public NamespaceSet getCompression() { return new NamespaceSet(varNS.compress(), funcNS.compress(), sortNS.compress(), - ruleSetNS.compress(), choiceNS.compress(), progVarNS.compress()); + ruleSetNS.compress(), choiceNS.compress(), progVarNS.compress(), documentation); } public void flushToParent() { @@ -227,7 +242,10 @@ public void flushToParent() { public NamespaceSet getParent() { return new NamespaceSet(varNS.parent(), funcNS.parent(), sortNS.parent(), - ruleSetNS.parent(), choiceNS.parent(), progVarNS.parent()); + ruleSetNS.parent(), choiceNS.parent(), progVarNS.parent(), documentation.parent()); } + public DocSpace docs() { + return documentation; + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabel.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabel.java index 05bea742469..fce39fbae7e 100755 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabel.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabel.java @@ -59,12 +59,12 @@ public class OriginTermLabel implements TermLabel { /** * Display name for {@link OriginTermLabel}s. */ - public final static Name NAME = new Name("origin"); + public static final Name NAME = new Name("origin"); /** * @see #getTLChildCount() */ - public final static int CHILD_COUNT = 2; + public static final int CHILD_COUNT = 2; public static final Sort[] EMPTY_SORTS = new Sort[0]; @@ -559,9 +559,13 @@ private static SubTermOriginData getSubTermOriginData(final ImmutableArray origins; /** @@ -775,6 +779,18 @@ public boolean equals(Object obj) { } } + @Override + public @Nullable String getDocumentation() { + return """ + This label saves a term's origin in the JML specification as well as the origins of all of its subterms and former subterms. + + For example, if the file "Example.java" contains the clause "requires R" at line 20, then every JavaDL term that is generated from R will have the origin + "requires @ Example.java @ line 20". + + Origin labels are not printed in the sequent view. To see a term's origin, you can mouse over it while holding the ALT button. If you want more detailed information, left click on the term and then on "Show Origin". + """; + } + /** * A {@code SpecType} is any type of JML specification which gets translated into JavaDL. * diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/ParameterlessTermLabel.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/ParameterlessTermLabel.java index 596410ce3e8..e57b7a35622 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/ParameterlessTermLabel.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/ParameterlessTermLabel.java @@ -7,6 +7,8 @@ import org.key_project.logic.Name; +import org.jspecify.annotations.Nullable; + /** * The Class {@link ParameterlessTermLabel} can be used to define labels without parameters. * @@ -56,12 +58,22 @@ public final class ParameterlessTermLabel implements TermLabel { */ public static final Name SHORTCUT_EVALUATION_LABEL_NAME = new Name("SC"); + public static final String SHORTCUT_EVALUATION_LABEL_DOC = + """ + The term label SC is used to indicate that a logical operator has originally been "shortcut" operator. + + For instance, both conjunction operators in JML (i.e., && and &) are translated to the same function in JavaDL. To differentiate between the two, the translation of && adds the label SC. + + This is relevant for welldefinedness checks. + """; + /** * Label attached to a term with the logical operator '{@literal ||}' or '{@literal &&}' to * distinguish from '{@literal |}' or '{@literal &}' respectively. */ public static final TermLabel SHORTCUT_EVALUATION_LABEL = - new ParameterlessTermLabel(SHORTCUT_EVALUATION_LABEL_NAME); + new ParameterlessTermLabel(SHORTCUT_EVALUATION_LABEL_NAME, + SHORTCUT_EVALUATION_LABEL_DOC); /** * Name of {@link #UNDEFINED_VALUE_LABEL}. @@ -115,6 +127,8 @@ public final class ParameterlessTermLabel implements TermLabel { */ private final Name name; + private final @Nullable String documentation; + /** * Instantiates a new simple term label. * @@ -122,8 +136,13 @@ public final class ParameterlessTermLabel implements TermLabel { * null. */ public ParameterlessTermLabel(Name name) { + this(name, null); + } + + public ParameterlessTermLabel(Name name, @Nullable String doc) { assert name != null; this.name = name; + this.documentation = doc; } @Override @@ -181,4 +200,9 @@ public boolean equals(Object obj) { public int hashCode() { return name.hashCode(); } + + @Override + public @Nullable String getDocumentation() { + return documentation; + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/SingletonLabelFactory.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/SingletonLabelFactory.java index 025d5cf4208..b9b6b32542e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/SingletonLabelFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/SingletonLabelFactory.java @@ -7,6 +7,8 @@ import de.uka.ilkd.key.logic.TermServices; +import org.jspecify.annotations.Nullable; + /** * A factory for creating singleton {@link TermLabel}. * @@ -33,6 +35,11 @@ public SingletonLabelFactory(T singletonLabel) { this.singletonLabel = singletonLabel; } + @Override + public @Nullable String getDocumentation() { + return singletonLabel.getDocumentation(); + } + /** * {@inheritDoc} * diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabel.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabel.java index 389a84ab4f0..86c774f7c5b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabel.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabel.java @@ -16,6 +16,7 @@ import de.uka.ilkd.key.rule.label.TermLabelRefactoring.RefactoringScope; import de.uka.ilkd.key.rule.label.TermLabelUpdate; +import org.key_project.logic.HasDocumentation; import org.key_project.logic.Name; import org.key_project.logic.Named; import org.key_project.logic.TerminalSyntaxElement; @@ -151,7 +152,8 @@ * @see TermLabelManager */ // spotless:on -public interface TermLabel extends Named, /* TODO: Remove */ TerminalSyntaxElement { +public interface TermLabel + extends Named, HasDocumentation, /* TODO: Remove */ TerminalSyntaxElement { /** * Retrieves the i-th parameter object of this term label. @@ -183,4 +185,9 @@ public interface TermLabel extends Named, /* TODO: Remove */ TerminalSyntaxEleme default boolean isProofRelevant() { return true; } + + @Override + default String getDocumentationKey() { + return "termlabel/" + name(); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelFactory.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelFactory.java index a8fd1cecafe..2375c964987 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelFactory.java @@ -7,6 +7,8 @@ import de.uka.ilkd.key.logic.TermServices; +import org.jspecify.annotations.Nullable; + /** * A factory for creating TermLabel objects. * @@ -45,4 +47,8 @@ public interface TermLabelFactory { * @throws TermLabelException if the parameters were illegally formatted */ T parseInstance(List arguments, TermServices services) throws TermLabelException; + + default @Nullable String getDocumentation() { + return null; + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelManager.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelManager.java index f08bb194f98..a9438317abb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelManager.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelManager.java @@ -71,8 +71,7 @@ public class TermLabelManager { /** * {@link Map}s the {@link Name} of a {@link TermLabel} to its {@link TermLabelFactory}. */ - private final Map> factoryMap = - new LinkedHashMap<>(); + private final Map> factoryMap = new LinkedHashMap<>(); /** * {@link Map}s the {@link Name} of a {@link TermLabel} to its {@link TermLabelPolicy} applied @@ -1493,6 +1492,10 @@ protected RefactoringsContainer computeRefactorings(TermLabelState state, Servic return refactorings; } + public Map> getFactories() { + return Collections.unmodifiableMap(factoryMap); + } + /** * Utility class used by * {@link TermLabelManager#computeRefactorings(TermLabelState, Services, PosInOccurrence, JTerm, Rule, Goal, Object, JTerm)} diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermLabelSV.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermLabelSV.java index ca2f315c10d..c892c952df9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermLabelSV.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/TermLabelSV.java @@ -31,4 +31,9 @@ public int getTLChildCount() { public Object getTLChild(int i) { throw new IndexOutOfBoundsException(); } + + @Override + public String getDocumentationKey() { + return super.getDocumentationKey(); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ArraySort.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ArraySort.java index 22fcd5e166c..d481e0ebe3b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ArraySort.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ArraySort.java @@ -42,7 +42,7 @@ public final class ArraySort extends SortImpl { private ArraySort(ImmutableSet extendsSorts, SortKey sk) { super(new Name((sk.elemType != null ? sk.elemType.getName() : sk.elemSort.name()) + "[]"), - extendsSorts, false, "", ""); + extendsSorts, false, ""); if (extendsSorts.isEmpty()) { throw new IllegalArgumentException("An ArraySort extends typically three sorts" diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/GenericSort.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/GenericSort.java index f714f27c47d..6a2be3f9291 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/GenericSort.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/GenericSort.java @@ -46,22 +46,21 @@ public final class GenericSort extends SortImpl { * @param ext supersorts of this sort, which have to be either concrete sorts or plain generic * sorts (i.e. not collection sorts of generic sorts) */ - public GenericSort(Name name, ImmutableSet ext, ImmutableSet oneOf, - String documentation, String origin) + public GenericSort(Name name, ImmutableSet ext, ImmutableSet oneOf, String origin) throws GenericSupersortException { - super(name, ext, false, documentation, origin); + super(name, ext, false, origin); this.oneOf = oneOf; checkSupersorts(); } public GenericSort(Name name, ImmutableSet ext, ImmutableSet oneOf) throws GenericSupersortException { - this(name, ext, oneOf, "", ""); + this(name, ext, oneOf, ""); } public GenericSort(Name name) { - super(name, DefaultImmutableSet.nil(), false, "", ""); + super(name, DefaultImmutableSet.nil(), false, ""); this.oneOf = DefaultImmutableSet.nil(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/NullSort.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/NullSort.java index c181b22e9c7..cf68e666b45 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/NullSort.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/NullSort.java @@ -35,7 +35,7 @@ public final class NullSort extends SortImpl { public NullSort(Sort objectSort) { - super(NAME, null, false, "", ""); + super(NAME, null, false, ""); assert objectSort != null; this.objectSort = objectSort; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java index c56513e2fb4..8182bb15eef 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java @@ -279,7 +279,7 @@ public boolean canStandFor(ProgramElement pe, Services services) { // -------------------------------------------------------------------------- protected ProgramSVSort(Name name) { - super(name, DefaultImmutableSet.nil(), false, "", ""); + super(name, DefaultImmutableSet.nil(), false, ""); NAME2SORT.put(name, this); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProxySort.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProxySort.java index fca9856c8a9..c6954a6ed35 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProxySort.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProxySort.java @@ -9,12 +9,11 @@ import org.key_project.util.collection.ImmutableSet; public class ProxySort extends SortImpl { - - public ProxySort(Name name, ImmutableSet ext, String documentation, String origin) { - super(name, ext, false, documentation, origin); + public ProxySort(Name name, ImmutableSet ext, String origin) { + super(name, ext, false, origin); } public ProxySort(Name name) { - this(name, DefaultImmutableSet.nil(), "", ""); + this(name, DefaultImmutableSet.nil(), ""); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/SortImpl.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/SortImpl.java index 40f5a1bba5b..60a5e6e82dd 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/SortImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/SortImpl.java @@ -17,44 +17,36 @@ * Abstract base class for implementations of the Sort interface. */ public class SortImpl extends AbstractSort { - /** - * Documentation for this sort given by the associated documentation comment. - * - * @see de.uka.ilkd.key.nparser.KeYParser.One_sort_declContext#doc - */ - private final String documentation; - /** Information of the origin of this sort */ private final String origin; + private ImmutableSet ext; - public SortImpl(Name name, ImmutableSet ext, boolean isAbstract, String documentation, - String origin) { + public SortImpl(Name name, ImmutableSet ext, boolean isAbstract, String origin) { super(name, isAbstract); this.ext = ext; - this.documentation = documentation; this.origin = origin; } - public SortImpl(Name name, ImmutableSet ext, String documentation, String origin) { - this(name, ext, false, documentation, origin); + public SortImpl(Name name, ImmutableSet ext, String origin) { + this(name, ext, false, origin); } public SortImpl(Name name, ImmutableSet ext, boolean isAbstract) { - this(name, ext, isAbstract, "", ""); + this(name, ext, isAbstract, ""); } public SortImpl(Name name, ImmutableSet ext) { - this(name, ext, false, "", ""); + this(name, ext, false, ""); } public SortImpl(Name name, Sort ext) { - this(name, DefaultImmutableSet.nil().add(ext), false, "", ""); + this(name, DefaultImmutableSet.nil().add(ext), false, ""); } public SortImpl(Name name) { - this(name, DefaultImmutableSet.nil(), "", ""); + this(name, DefaultImmutableSet.nil(), ""); } @Override @@ -88,11 +80,6 @@ public String declarationString() { return name().toString(); } - @Override - public @Nullable String getDocumentation() { - return documentation; - } - @Override public @Nullable String getOrigin() { return origin; 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 e3e50418712..e2692298a92 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 @@ -201,6 +201,16 @@ public Configuration asConfiguration() { throw new RuntimeException("Error in configuration. Source: " + ctx.start.getTokenSource().getSourceName()); } + + public List asConfigurationList() { + final var cfg = new ConfigurationBuilder(); + List res = cfg.visitCfile(ctx); + if (!res.isEmpty()) + return (List) res.getFirst(); + else + throw new RuntimeException("Error in configuration. Source: " + + ctx.start.getTokenSource().getSourceName()); + } } public static class SetStatementContext extends KeyAst { diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java index 30d94ea933c..c45cba03a17 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java @@ -3,10 +3,9 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.nparser.builder; -import java.util.HashMap; -import java.util.LinkedList; -import java.util.List; -import java.util.Map; +import java.util.*; +import java.util.stream.Collectors; +import java.util.stream.Stream; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.abstraction.KeYJavaType; @@ -16,9 +15,9 @@ import de.uka.ilkd.key.logic.op.ProgramVariable; import de.uka.ilkd.key.logic.sort.*; import de.uka.ilkd.key.nparser.KeYParser; -import de.uka.ilkd.key.nparser.ParsingFacade; import org.key_project.logic.Choice; +import org.key_project.logic.HasDocumentation; import org.key_project.logic.Name; import org.key_project.logic.Named; import org.key_project.logic.sort.Sort; @@ -64,27 +63,26 @@ public Object visitDecls(KeYParser.DeclsContext ctx) { @Override public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { - // boolean freeAdt = ctx.FREE() != null; var name = ctx.name.getText(); - var doc = ctx.DOC_COMMENT() != null - ? ctx.DOC_COMMENT().getText() - : null; + var doc = processDocumentation(ctx.doc); var origin = BuilderHelpers.getPosition(ctx); - var s = new SortImpl(new Name(name), ImmutableSet.empty(), false, doc, origin); + var s = new SortImpl(new Name(name), ImmutableSet.empty(), false, origin); sorts().addSafely(s); + docsSpace().describe(s, doc); return null; } @Override public Object visitProg_var_decls(KeYParser.Prog_var_declsContext ctx) { - for (int i = 0; i < ctx.simple_ident_comma_list().size(); i++) { - List varNames = accept(ctx.simple_ident_comma_list(i)); + for (int i = 0; i < ctx.simple_ident_comma_list_with_docs().size(); i++) { + var c = ctx.simple_ident_comma_list_with_docs(i); + List varNames = c.simple_ident_with_doc() + .stream().map(it -> (String) accept(it.simple_ident())).toList(); KeYJavaType kjt = accept(ctx.keyjavatype(i)); assert varNames != null; for (String varName : varNames) { if (varName.equals("null")) { - semanticError(ctx.simple_ident_comma_list(i), - "Function '" + varName + "' is already defined!"); + semanticError(c, "Function '" + varName + "' is already defined!"); } ProgramElementName pvName = new ProgramElementName(varName); Named name = lookup(pvName); @@ -92,8 +90,8 @@ public Object visitProg_var_decls(KeYParser.Prog_var_declsContext ctx) { // commented out as pv do not have unique name (at the moment) // throw new AmbigiousDeclException(varName, getSourceName(), getLine(), // getColumn()) - if (!(name instanceof ProgramVariable) - || !((ProgramVariable) name).getKeYJavaType().equals(kjt)) { + if (!(name instanceof ProgramVariable pv) + || !(pv.getKeYJavaType().equals(kjt))) { programVariables().add(new LocationVariable(pvName, kjt)); } } else { @@ -108,21 +106,30 @@ public Object visitProg_var_decls(KeYParser.Prog_var_declsContext ctx) { @Override public Object visitChoice(KeYParser.ChoiceContext ctx) { String cat = ctx.category.getText(); + String catDoc = processDocumentation(ctx.maindoc); + docsSpace().describe(new HasDocumentation.OptionCategory(cat), catDoc); + for (KeYParser.OptionDeclContext optdecl : ctx.optionDecl()) { Token catctx = optdecl.IDENT; String name = cat + ":" + catctx.getText(); + Choice c = choices().lookup(new Name(name)); if (c == null) { c = new Choice(catctx.getText(), cat); choices().add(c); + + var doc = processDocumentation(optdecl.DOC_COMMENT); + docsSpace().describe(c, doc); } category2Default.putIfAbsent(cat, name); } + category2Default.computeIfAbsent(cat, it -> { - choices().add(new Choice("On", cat)); - choices().add(new Choice("Off", cat)); + choices().add(new Choice(cat + ":On", cat)); + choices().add(new Choice(cat + ":Off", cat)); return cat + ":On"; }); + return null; } @@ -142,9 +149,9 @@ public Object visitOne_sort_decl(KeYParser.One_sort_declContext ctx) { boolean isProxySort = ctx.PROXY() != null; boolean isAbstractSort = ctx.ABSTRACT() != null; List createdSorts = new LinkedList<>(); - var documentation = ParsingFacade.getValueDocumentation(ctx.DOC_COMMENT()); - for (var idCtx : ctx.sortIds.simple_ident_dots()) { - String sortId = accept(idCtx); + var sectionDoc = processDocumentation(ctx.DOC_COMMENT()); + for (var idCtx : ctx.sortIds.simple_ident_dots_with_docs()) { + String sortId = accept(idCtx.simple_ident_dots()); Name sortName = new Name(sortId); ImmutableSet ext = sortExt == null ? ImmutableSet.empty() @@ -158,7 +165,7 @@ public Object visitOne_sort_decl(KeYParser.One_sort_declContext ctx) { Sort s = null; if (isGenericSort) { try { - var gs = new GenericSort(sortName, ext, oneOf, documentation, + var gs = new GenericSort(sortName, ext, oneOf, BuilderHelpers.getPosition(idCtx)); s = gs; } catch (GenericSupersortException e) { @@ -168,16 +175,19 @@ public Object visitOne_sort_decl(KeYParser.One_sort_declContext ctx) { s = JavaDLTheory.ANY; } else { if (isProxySort) { - var ps = new ProxySort(sortName, ext, documentation, - BuilderHelpers.getPosition(idCtx)); + var ps = new ProxySort(sortName, ext, BuilderHelpers.getPosition(idCtx)); s = ps; } else { var si = new SortImpl(sortName, ext, isAbstractSort, - documentation, BuilderHelpers.getPosition(idCtx)); + BuilderHelpers.getPosition(idCtx)); s = si; } } assert s != null; + String doc = processDocumentation(idCtx.DOC_COMMENT()); + docsSpace().describe(s, + Stream.of(doc, sectionDoc).filter(Objects::nonNull) + .collect(Collectors.joining("\n"))); sorts().add(s); createdSorts.add(s); } else { @@ -210,10 +220,13 @@ public List visitOneof_sorts(KeYParser.Oneof_sortsContext ctx) { @Override public Object visitRuleset_decls(KeYParser.Ruleset_declsContext ctx) { - for (String id : this.mapOf(ctx.simple_ident())) { + for (KeYParser.Simple_ident_with_docContext iddoc : ctx.simple_ident_with_doc()) { + String id = accept(iddoc.simple_ident()); + String doc = processDocumentation(iddoc.DOC_COMMENT()); RuleSet h = new RuleSet(new Name(id)); if (ruleSets().lookup(new Name(id)) == null) { ruleSets().add(h); + docsSpace().describe(h, doc); } } return null; @@ -225,5 +238,4 @@ public Object visitOptions_choice(KeYParser.Options_choiceContext ctx) { return null; } - } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java index 059f24f1696..efc54b0418f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java @@ -7,6 +7,8 @@ import java.util.Collection; import java.util.List; import java.util.ResourceBundle; +import java.util.regex.Pattern; +import java.util.stream.Collectors; import de.uka.ilkd.key.java.JavaInfo; import de.uka.ilkd.key.java.Services; @@ -33,6 +35,8 @@ import org.key_project.util.collection.Pair; import org.antlr.v4.runtime.ParserRuleContext; +import org.antlr.v4.runtime.Token; +import org.antlr.v4.runtime.tree.TerminalNode; /** * Helper class for are visitor that requires a namespaces and services. Also it provides the @@ -256,6 +260,11 @@ protected Namespace choices() { return namespaces().choices(); } + protected DocSpace docsSpace() { + return namespaces().docs(); + } + + @Override public String visitString_value(KeYParser.String_valueContext ctx) { return ctx.getText().substring(1, ctx.getText().length() - 1); @@ -408,4 +417,28 @@ public KeYJavaType visitKeyjavatype(KeYParser.KeyjavatypeContext ctx) { public Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx) { return ctx.getText(); } + + + protected String processDocumentation(TerminalNode terminalNode) { + if (terminalNode != null) + return processDocumentation(terminalNode.getSymbol()); + return null; + } + + protected String processDocumentation(List maindoc) { + return maindoc.stream().map(this::processDocumentation).collect(Collectors.joining("\n\n")); + } + + protected String processDocumentation(Token doc) { + if (doc == null) { + return null; + } + + var text = doc.getText(); + int prefix = doc.getCharPositionInLine() + 2; + Pattern REMOVE_INDENT = Pattern.compile("^[ ]{1," + prefix + "}", Pattern.MULTILINE); + text = text.strip().substring(3, text.length() - 2); + return REMOVE_INDENT.matcher(text).replaceAll("").trim(); + } + } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java index d9454ff4591..6e88eafd282 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java @@ -55,7 +55,6 @@ public Object visitDecls(KeYParser.DeclsContext ctx) { @Override public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { // weigl: all datatypes are free ==> functions are unique! - // boolean freeAdt = ctx.FREE() != null; var sort = sorts().lookup(ctx.name.getText()); var dtNamespace = new Namespace(); for (KeYParser.Datatype_constructorContext constructorContext : ctx @@ -63,6 +62,7 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { Name name = new Name(constructorContext.name.getText()); Sort[] args = new Sort[constructorContext.sortId().size()]; var argNames = constructorContext.argName; + var doc = processDocumentation(constructorContext.doc); for (int i = 0; i < args.length; i++) { Sort argSort = accept(constructorContext.sortId(i)); args[i] = argSort; @@ -79,10 +79,8 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { || !alreadyDefinedFn.argSorts().equals(ImmutableList.of(sort)))) { // The condition checks whether there is already a function with the same name // but different signature. This is necessarily true if there is a globally - // defined function - // of the same name and may or may not be true if there is another constructor - // argument of the - // same name. + // defined function of the same name and may or may not be true if there + // is another constructor argument of the same name. semanticError(argNames.get(i), "Name already in namespace: %s" + ". Identifiers in datatype definitions must be unique (also wrt. global functions).", argName); @@ -93,6 +91,7 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { } Function function = new JFunction(name, sort, args, null, true, false); namespaces().functions().addSafely(function); + docsSpace().describe(function, doc); } namespaces().functions().addSafely(dtNamespace.allElements()); return null; @@ -101,6 +100,7 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { @Override public Object visitPred_decl(KeYParser.Pred_declContext ctx) { String pred_name = accept(ctx.funcpred_name()); + String doc = processDocumentation(ctx.doc); List whereToBind = accept(ctx.where_to_bind()); List argSorts = accept(ctx.arg_sorts()); if (whereToBind != null && whereToBind.size() != argSorts.size()) { @@ -130,6 +130,7 @@ public Object visitPred_decl(KeYParser.Pred_declContext ctx) { if (lookup(p.name()) == null) { functions().add(p); + docsSpace().describe(p, doc); } else { // weigl: agreement on KaKeY meeting: this should be an error. semanticError(ctx, "Predicate '" + p.name() + "' is already defined!"); diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java index 7964520a468..98cbe47035b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java @@ -172,7 +172,8 @@ public Taclet visitTaclet(KeYParser.TacletContext ctx) { b.setAnnotations(tacletAnnotations); b.setOrigin(BuilderHelpers.getPosition(ctx)); Taclet r = b.getTaclet(); - registerTaclet(ctx, r); + String doc = processDocumentation(ctx.doc); + registerTaclet(ctx, r, doc); currentTBuilder.pop(); return r; } @@ -185,9 +186,8 @@ public Taclet visitTaclet(KeYParser.TacletContext ctx) { ifSeq = accept(ctx.ifSeq); } - @Nullable Object find = accept(ctx.find); - Sequent seq = find instanceof Sequent ? (Sequent) find : null; + Sequent seq = (find instanceof Sequent s) ? s : null; var applicationRestriction = ApplicationRestriction.NONE; if (!ctx.SAMEUPDATELEVEL().isEmpty()) { @@ -219,7 +219,8 @@ public Taclet visitTaclet(KeYParser.TacletContext ctx) { b.setOrigin(BuilderHelpers.getPosition(ctx)); try { Taclet r = peekTBuilder().getTaclet(); - registerTaclet(ctx, r); + String doc = processDocumentation(ctx.doc); + registerTaclet(ctx, r, doc); setSchemaVariables(schemaVariables().parent()); currentTBuilder.pop(); return r; @@ -236,8 +237,10 @@ private void registerTaclet(KeYParser.Datatype_declContext ctx, TacletBuilder ctx.start.getTokenSource().getSourceName(), ctx.start.getLine()); } - private void registerTaclet(ParserRuleContext ctx, Taclet taclet) { + private void registerTaclet(ParserRuleContext ctx, Taclet taclet, + @Nullable String documentation) { taclet2Builder.put(taclet, peekTBuilder()); + docsSpace().describe(taclet, documentation); LOGGER.trace("Taclet announced: \"{}\" from {}:{}", taclet.name(), ctx.start.getTokenSource().getSourceName(), ctx.start.getLine()); } @@ -742,7 +745,6 @@ public Object visitGoalspec(KeYParser.GoalspecContext ctx) { ImmutableSLList addRList = ImmutableSLList.nil(); DefaultImmutableSet addpv = DefaultImmutableSet.nil(); - @Nullable Object rwObj = accept(ctx.replacewith()); if (ctx.add() != null) { addSeq = accept(ctx.add()); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractPO.java index 3f2ef79bbeb..f2398bf4d05 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractPO.java @@ -292,7 +292,6 @@ private Vertex getVertexFor(Pair vertexCore, ClassAxiom */ private void registerClassAxiomTaclets(KeYJavaType selfKJT, InitConfig proofConfig) { final ImmutableSet axioms = selectClassAxioms(selfKJT); - var choices = Collections.unmodifiableSet(proofConfig.getActivatedChoices().toSet()); for (ClassAxiom axiom : axioms) { final Vertex node = getVertexFor(axiom.getKJT().getSort(), axiom.getTarget(), axiom); if (node.index == -1) { @@ -305,9 +304,9 @@ private void registerClassAxiomTaclets(KeYJavaType selfKJT, InitConfig proofConf proofConfig.getServices())) { assert axiomTaclet != null : "class axiom returned null taclet: " + axiom.getName(); // only include if choices are appropriate - if (axiomTaclet.getChoices().eval(choices)) { - register(axiomTaclet, proofConfig); - } + // weigl: register always! choices are evaluated as late as possible. + // This would technically allow to change Taclet options after loading. + register(axiomTaclet, proofConfig); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java index 50f39d98e64..289b974cef2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java @@ -28,12 +28,12 @@ import org.key_project.logic.sort.Sort; import org.key_project.prover.rules.RuleApp; import org.key_project.prover.rules.RuleSet; -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.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; /** * an instance of this class describes the initial configuration of the prover. This includes sorts, @@ -49,32 +49,35 @@ public class InitConfig { private RuleJustificationInfo justifInfo = new RuleJustificationInfo(); - + /// List of all known taclets. private ImmutableList taclets = ImmutableSLList.nil(); /** - * maps categories to their default choice (both represented as Strings), which is used if no - * other choice is specified in the problemfile + * Map of categories to their default choice. The choices are overridden in activateChoice + * by settings given in the {@link KeYUserProblemFile} or + * {@link Profile#prepareInitConfig(InitConfig, Object)}. */ - private Map category2DefaultChoice = new LinkedHashMap<>(); + private final Map category2DefaultChoice; - /** - * maps taclets to their TacletBuilders. This information is needed when a taclet contains - * GoalTemplates annotated with taclet-options because in this case a new taclet has to be - * created containing only those GoalTemplates whose options are activated and those who don't - * belong to any specific option. - */ - private HashMap> taclet2Builder = new LinkedHashMap<>(); /** * Set of the rule options activated for the current proof. The rule options ({@link Choice}s) * allow to use different ruleset modelling or skipping certain features (e.g. nullpointer * checks when resolving references) */ - private ImmutableSet activatedChoices = DefaultImmutableSet.nil(); + private final Map activatedChoices = new TreeMap<>(); + + + /** + * maps taclets to their TacletBuilders. This information is needed when a taclet contains + * GoalTemplates annotated with taclet-options because in this case a new taclet has to be + * created containing only those GoalTemplates whose options are activated and those who don't + * belong to any specific option. + */ + private Map> taclet2Builder = new LinkedHashMap<>(); /** HashMap for quick lookups taclet name->taclet */ - private Map activatedTacletCache = null; + private @Nullable Map activatedTacletCache = null; /** the fileRepo which is responsible for consistency between source code and proof */ private FileRepo fileRepo; @@ -83,29 +86,23 @@ public class InitConfig { private ProofSettings settings; - - - // ------------------------------------------------------------------------- - // constructors - // ------------------------------------------------------------------------- - public InitConfig(Services services) { this.services = services; - category2DefaultChoice = new HashMap<>( - ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices()); - } - - - // ------------------------------------------------------------------------- - // internal methods - // ------------------------------------------------------------------------- + var currentDefaultChoices = + ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices(); + var defaults = new TreeMap(); + for (final String s : currentDefaultChoices.values()) { + final Choice c = choiceNS().lookup(new Name(s)); + if (c != null) { + defaults.put(c.category(), c); + } + } - // ------------------------------------------------------------------------- - // public interface - // ------------------------------------------------------------------------- + category2DefaultChoice = defaults; + } /** * returns the Services of this initial configuration providing access to the used program model @@ -122,32 +119,28 @@ public Profile getProfile() { } - /** - * Adds a default option for a category. It does override previous default choices. - * - * @return true if the default was successfully set - */ - public boolean addCategoryDefaultChoice(@NonNull String category, @NonNull String choice) { - if (!category2DefaultChoice.containsKey(category)) { - category2DefaultChoice.put(category, choice); - return true; - } - return false; - } - /** * Adds default choices given in {@code init}. Not overriding previous default choices. */ public void addCategory2DefaultChoices(@NonNull Map init) { boolean changed = false; for (final Map.Entry entry : init.entrySet()) { - changed = addCategoryDefaultChoice(entry.getKey(), entry.getValue()) || changed; + final Choice c = choiceNS().lookup(new Name(entry.getValue())); + if (c != null && !category2DefaultChoice.containsKey(c.category())) { + changed = true; + category2DefaultChoice.put(c.category(), c); + } } + if (changed) { // FIXME weigl: I do not understand why the default choices are back progragated! // For me this is a design flaw. - Map clone = - new HashMap<>(category2DefaultChoice); + // weigl(2026): This is the way, how the settings are getting updated by the current + // known choices. This is not good! + Map clone = new HashMap<>(); + for (Map.Entry entry : category2DefaultChoice.entrySet()) { + clone.put(entry.getKey(), entry.getValue().name().toString()); + } ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().setDefaultChoices(clone); // invalidate active taclet cache activatedTacletCache = null; @@ -155,7 +148,7 @@ public void addCategory2DefaultChoices(@NonNull Map init) { } - public void setTaclet2Builder(HashMap> taclet2Builder) { + public void setTaclet2Builder(Map> taclet2Builder) { this.taclet2Builder = taclet2Builder; } @@ -167,7 +160,7 @@ public void setTaclet2Builder(HashMap> t * * @return the map from a taclet to its builder */ - public HashMap> getTaclet2Builder() { + public Map> getTaclet2Builder() { return taclet2Builder; } @@ -177,37 +170,22 @@ public HashMap> getTaclet2Builder() { * specified choice the default choice contained in category2DefaultChoice is added. */ public void setActivatedChoices(ImmutableSet activatedChoices) { - category2DefaultChoice = - ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices(); - - HashMap c2DC = new HashMap<>(category2DefaultChoice); - for (final Choice c : activatedChoices) { - c2DC.remove(c.category()); - } - - ImmutableList category2DefaultChoiceList = ImmutableSLList.nil(); - for (final String s : c2DC.values()) { - final Choice c = choiceNS().lookup(new Name(s)); - if (c != null) { - category2DefaultChoiceList = category2DefaultChoiceList.prepend(c); - } + this.activatedChoices.clear(); + for (Choice choice : activatedChoices) { + this.activatedChoices.put(choice.category(), choice); } - this.activatedChoices = activatedChoices - .union( - DefaultImmutableSet.fromImmutableList(category2DefaultChoiceList)); // invalidate active taclet cache activatedTacletCache = null; } - /** - * Returns the choices which are currently active. For getting the active choices for a specific - * proof, getChoices in de.uka.ilkd.key.proof.Proof - * has to be used. + * Returns the effective activated choices. */ public ImmutableSet getActivatedChoices() { - return activatedChoices; + var effectiveMap = new TreeMap<>(category2DefaultChoice); + effectiveMap.putAll(activatedChoices); + return ImmutableSet.from(effectiveMap.values()); } @@ -259,7 +237,8 @@ private void fillActiveTacletCache() { return; } final LinkedHashMap tacletCache = new LinkedHashMap<>(); - var choices = Collections.unmodifiableSet(activatedChoices.toSet()); + var choices = Collections.unmodifiableSet(getActivatedChoices().toSet()); + for (Taclet t : taclets) { TacletBuilder b = taclet2Builder.get(t); @@ -425,16 +404,14 @@ public InitConfig deepCopy() { * returns a copy of this initial configuration copying the namespaces, the contained JavaInfo * while using the immutable set of taclets in the copy */ - @SuppressWarnings("unchecked") public InitConfig copyWithServices(Services services) { InitConfig ic = new InitConfig(services); if (settings != null) { ic.setSettings(new ProofSettings(settings)); } - ic.setActivatedChoices(activatedChoices); - ic.category2DefaultChoice = new HashMap<>(category2DefaultChoice); - ic.setTaclet2Builder( - (HashMap>) taclet2Builder.clone()); + ic.category2DefaultChoice.putAll(category2DefaultChoice); + ic.activatedChoices.putAll(activatedChoices); + ic.setTaclet2Builder(new HashMap<>(taclet2Builder)); ic.taclets = taclets; ic.originalKeYFileName = originalKeYFileName; ic.justifInfo = justifInfo.copy(); @@ -460,10 +437,26 @@ public void setFileRepo(FileRepo fileRepo) { /// Enforce the given choice. Remove choices of the same category from the current set. public void activateChoice(Choice choice) { - setActivatedChoices( - getActivatedChoices() - .stream().filter(it -> choice.category().equals(it.category())) - .collect(ImmutableSet.collector()) - .add(choice)); + activatedChoices.put(choice.category(), choice); + // invalidate active taclet cache + activatedTacletCache = null; + } + + public boolean isChoiceActive(String choice) { + var c = choiceNS().lookup(choice); + return isChoiceActive(c); + } + + public boolean isChoiceActive(@Nullable Choice c) { + if (c == null) { + return false; + } + + if (activatedChoices.containsValue(c)) { + return true; + } + + return !activatedChoices.containsKey(c.category()) + && category2DefaultChoice.containsValue(c); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java index 1b7b6fa1ed0..716ff8f5aa4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java @@ -32,6 +32,7 @@ import de.uka.ilkd.key.rule.BuiltInRule; import de.uka.ilkd.key.rule.Rule; import de.uka.ilkd.key.rule.Taclet; +import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.settings.ProofIndependentSettings; import de.uka.ilkd.key.settings.ProofSettings; import de.uka.ilkd.key.speclang.PositionedString; @@ -49,6 +50,7 @@ import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSet; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; import recoder.io.PathList; @@ -68,6 +70,7 @@ public final class ProblemInitializer { */ private FileRepo fileRepo; private ImmutableSet warnings = DefaultImmutableSet.nil(); + private @Nullable Configuration additionalProfileOptions; // ------------------------------------------------------------------------- // constructors @@ -81,13 +84,22 @@ public ProblemInitializer(ProgressMonitor mon, Services services, } public ProblemInitializer(Profile profile) { - if (profile == null) { - throw new IllegalArgumentException("Given profile is null"); - } + this(null, new Services(Objects.requireNonNull(profile, "Given profile is null")), null); + } + + public ProblemInitializer(Profile profile, @Nullable Configuration additionalProfileOptions) { + this(profile); + this.additionalProfileOptions = additionalProfileOptions; + } + + /// An arbitrary object which is passed to the provided profile, during construction of the + /// `initConfig`. + public @Nullable Configuration getAdditionalProfileOptions() { + return additionalProfileOptions; + } - this.progMon = null; - this.listener = null; - this.services = new Services(Objects.requireNonNull(profile)); + public void setAdditionalProfileOptions(@Nullable Configuration additionalProfileOptions) { + this.additionalProfileOptions = additionalProfileOptions; } private void progressStarted(Object sender) { @@ -443,14 +455,14 @@ public InitConfig prepare(EnvInput envInput) throws ProofInputException { for (var tacletBase : tacletBases) { KeYFile tacletBaseFile = new KeYFile( "taclet base (%s)".formatted(tacletBase.file().getFileName()), - tacletBase, progMon, profile); + tacletBase, progMon, profile, null); readEnvInput(tacletBaseFile, currentBaseConfig); } } // remove traces of the generic sorts within the base configuration cleanupNamespaces(currentBaseConfig); - profile.prepareInitConfig(currentBaseConfig); + profile.prepareInitConfig(currentBaseConfig, additionalProfileOptions); baseConfig = currentBaseConfig; } @@ -543,9 +555,8 @@ private InitConfig prepare(EnvInput envInput, InitConfig referenceConfig) if (type instanceof ClassDeclaration || type instanceof InterfaceDeclaration) { for (Field f : javaInfo.getAllFields((TypeDeclaration) type)) { final ProgramVariable pv = (ProgramVariable) f.getProgramVariable(); - if (pv instanceof LocationVariable) { - heapLDT.getFieldSymbolForPV((LocationVariable) pv, - initConfig.getServices()); + if (pv instanceof LocationVariable lv) { + heapLDT.getFieldSymbolForPV(lv, initConfig.getServices()); } } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/Profile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/Profile.java index 9316c659d0e..ef22751d63e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/Profile.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/Profile.java @@ -12,6 +12,7 @@ import de.uka.ilkd.key.rule.Rule; import de.uka.ilkd.key.rule.UseDependencyContractRule; import de.uka.ilkd.key.rule.UseOperationContractRule; +import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.strategy.StrategyFactory; import org.key_project.logic.Name; @@ -22,6 +23,7 @@ import org.key_project.util.collection.ImmutableSet; import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; /** *

@@ -180,8 +182,13 @@ default UseOperationContractRule getUseOperationContractRule() { /// Taclet base has been loaded, but before Java sources are loaded or the environment is /// established. /// + /// @param baseConfig a initial configuration which can be modified, e.g., forcing Taclet + /// options. + /// @param additionalProfileOptions a nullable object representing selected options in the UI or + /// command line. /// @see ProblemInitializer - default void prepareInitConfig(InitConfig baseConfig) { + default void prepareInitConfig(InitConfig baseConfig, + @Nullable Configuration additionalProfileOptions) { } } 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 167aff7270c..5cf57810f95 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 @@ -65,35 +65,10 @@ public abstract class AbstractProblemLoader { */ private boolean loadSingleJavaFile = false; - public static class ReplayResult { - - private final Node node; - private final List errors; - private final String status; - - public ReplayResult(String status, List errors, Node node) { - this.status = status; - this.errors = errors; - this.node = node; - } - - public Node getNode() { - return node; - } - - public String getStatus() { - return status; - } - - public List getErrorList() { - return errors; - } - - public boolean hasErrors() { - return errors != null && !errors.isEmpty(); - } - - } + /** + * + */ + private @Nullable Configuration additionalProfileOptions; /** * The file or folder to load. @@ -552,6 +527,7 @@ protected EnvInput createEnvInput(FileRepo fileRepo) throws IOException { protected ProblemInitializer createProblemInitializer(FileRepo fileRepo) { Profile profile = forceNewProfileOfNewProofs ? profileOfNewProofs : envInput.getProfile(); ProblemInitializer pi = new ProblemInitializer(control, new Services(profile), control); + pi.setAdditionalProfileOptions(additionalProfileOptions); pi.setFileRepo(fileRepo); return pi; } @@ -859,4 +835,45 @@ public void setLoadSingleJavaFile(boolean loadSingleJavaFile) { public void setIgnoreWarnings(boolean ignoreWarnings) { this.ignoreWarnings = ignoreWarnings; } + + public void setAdditionalProfileOptions(@Nullable Configuration additionalProfileOptions) { + this.additionalProfileOptions = additionalProfileOptions; + } + + /// An arbitrary object representing additional options for the given profile. + /// @see ProblemInitializer + public Configuration getAdditionalProfileOptions() { + return additionalProfileOptions; + } + + + public static class ReplayResult { + + private final Node node; + private final List errors; + private final String status; + + public ReplayResult(String status, List errors, Node node) { + this.status = status; + this.errors = errors; + this.node = node; + } + + public Node getNode() { + return node; + } + + public String getStatus() { + return status; + } + + public List getErrorList() { + return errors; + } + + public boolean hasErrors() { + return errors != null && !errors.isEmpty(); + } + + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java index 604d4720b17..a751362709a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java @@ -276,4 +276,18 @@ public String toString() { + (excVar != null ? "Validity Branch: exceptionVar=" + excVar.name() : ""); } } + + @Override + public @Nullable String getDocumentation() { + return """ + Like methods, statement blocks can be annotated with contracts. The application of the Block Contract rules then gives rise to subgoals which roughly correspond to those of the Use Operation Contract rule (see there). + Three properties have to be shown: + + 1. Validity of block contract + + 2. Precondition of contract holds + + 3. Postcondition holds after block terminates + """; + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java b/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java index 5f5d6cb4986..65ca1e5ae7a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java @@ -795,4 +795,28 @@ public String toString() { public boolean isApplicableOnSubTerms() { return false; } + + + @Override + public String getDocumentation() { + return """ + The One Step Simplifier (OSS) aggregates the application of simplification rules into a single rule. This is done to make the calculus more efficient. + + You can activate/deactivate the simplifier by toggling the menu entry Options->One Step Simplifier. An active OSS makes the proof faster, a deactivated more transparent. + + In particular, the OSS performs normalisation and simplification on updated terms: + * Updates on terms without modality are resolved. + * Updates without effects are dropped. + * Sequential updates are merged into one parallel update. + + Technical Information: + The OSS aggregates the rules from the following heuristics (-> Taclet Base): + concrete, + update_elim, + update_apply_on_update, + update_apply, + update_join, + elimQuantifier + """; + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/QueryExpand.java b/key.core/src/main/java/de/uka/ilkd/key/rule/QueryExpand.java index f13302128c9..1cccf5f1996 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/QueryExpand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/QueryExpand.java @@ -39,6 +39,7 @@ import org.key_project.util.collection.Pair; import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -680,4 +681,15 @@ public DefaultBuiltInRuleApp createApp(PosInOccurrence pos, TermServices service public boolean isApplicableOnSubTerms() { return true; } + + @Override + public @Nullable String getDocumentation() { + return """ + The QueryExpand rule allows to apply contracts or to symbolically execute a query + expression in the logic. It replaces the query expression by a new constant and + constructs a box formula in the antecedent 'defining' the constant as the result of + a method call. The method call is encoded directly as a method call in the box modality. + The query is invoked in a context equal to the container type of the query method. + """; + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/Rule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/Rule.java index a2c53678b42..b7480176bef 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/Rule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/Rule.java @@ -4,11 +4,18 @@ package de.uka.ilkd.key.rule; +import org.key_project.logic.HasDocumentation; import org.key_project.logic.HasOrigin; +import org.jspecify.annotations.NonNull; + /** * This interface has to be implemented by all classes that want to act as a rule in the calculus. */ -public interface Rule extends org.key_project.prover.rules.Rule, HasOrigin { +public interface Rule extends org.key_project.prover.rules.Rule, HasOrigin, HasDocumentation { + @Override + default @NonNull String getDocumentationKey() { + return "rule/" + this.name(); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/UseDependencyContractRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/UseDependencyContractRule.java index 8c30fb92ed2..8982128fca3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/UseDependencyContractRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/UseDependencyContractRule.java @@ -605,4 +605,15 @@ public UseDependencyContractApp createApp(PosInOccurrence pos, TermServices serv public boolean isApplicableOnSubTerms() { return true; } + + @Override + public @Nullable String getDocumentation() { + return """ + Methods and model fields may be annotated with an accessible clause. This defines a dependency contract describing the heap locations its value may depend on. + + If the heap changes in locations the symbol does not depend on, its value remains unchanged. This rules adds an according implication for a heap-dependent symbol to the sequent's antecedent. + + In automatic strategy, this rule is applied lazily (only once all other means of advancing the proof have been exhausted) to avoid endless loops. + """; + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/UseOperationContractRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/UseOperationContractRule.java index 5daaa777ad5..5fe81292435 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/UseOperationContractRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/UseOperationContractRule.java @@ -956,4 +956,20 @@ protected JTerm getFinalPreTerm() { return finalPreTerm; } } + + @Override + public @Nullable String getDocumentation() { + return """ + When symbolic execution reaches a method call, the according method can be approximated by its specified contract (more precisely, one or more of its contracts). + + This rule gives rise to three or four subgoals: + 1. Pre: It must be established that the pre-condition of the method holds prior to the method call. + + 2. Post: The method terminates normally, the post-condition of the method can be assumed and symbolic execution continues. + + 3. Exceptional Post: The method terminates abruptly with an exception, the exceptional post-condition is assumed, and symbolic execution continues with this exception thrown. + + 4. Null reference: The receiver of the call can be null. This case is considered on this branch. If KeY can figure out automatically that this cannot be the case, this branch is suppressed. + """; + } } 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 bae9c49e129..c673c18be4e 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 @@ -699,4 +699,19 @@ protected void prepareUseCaseBranch(Goal useGoal) { ruleApp.posInOccurrence()); } } + + @Override + public @Nullable String getDocumentation() { + return """ + Loops can be handled by expanding or by using a loop invariant. + An invariant can be created manually or supplied by the JML specification. + Use of this rule creates three subgoals, two of which are new proof obligations: + + 1. It must be shown that the loop invariant is initially valid. + + 2. The loop body needs to preserve the invariant. + + In the third subgoal, the loop invariant can be used. + """; + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java index 7f7888731c5..7bf6824e286 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java @@ -176,7 +176,7 @@ public long getLong(String name, long defaultValue) { * @throws NullPointerException if no such value entry exists */ public boolean getBool(String name) { - return get(name, Boolean.class); + return Boolean.TRUE.equals(get(name, Boolean.class)); } /** @@ -350,7 +350,7 @@ private ConfigurationMeta getOrCreateMeta(String name) { /** * @see #getTable(String) */ - public Configuration getSection(String name) { + public @Nullable Configuration getSection(String name) { return getTable(name); } @@ -365,39 +365,39 @@ public Configuration getSection(String name, boolean createIfNotExists) { return getSection(name); } - public Object set(String name, Object obj) { + public @Nullable Object set(String name, @Nullable Object obj) { return data.put(name, obj); } - public Object set(String name, Boolean obj) { + public @Nullable Object set(String name, @Nullable Boolean obj) { return set(name, (Object) obj); } - public Object set(String name, String obj) { + public @Nullable Object set(String name, @Nullable String obj) { return set(name, (Object) obj); } - public Object set(String name, Long obj) { + public @Nullable Object set(String name, @Nullable Long obj) { return set(name, (Object) obj); } - public Object set(String name, int obj) { + public @Nullable Object set(String name, int obj) { return set(name, (long) obj); } - public Object set(String name, Double obj) { + public @Nullable Object set(String name, @Nullable Double obj) { return set(name, (Object) obj); } - public Object set(String name, Configuration obj) { + public @Nullable Object set(String name, @Nullable Configuration obj) { return set(name, (Object) obj); } - public Object set(String name, List obj) { + public @Nullable Object set(String name, @Nullable List obj) { return set(name, (Object) obj); } - public Object set(String name, String[] seq) { + public @Nullable Object set(String name, @Nullable String[] seq) { return set(name, (Object) Arrays.asList(seq)); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/PathConfig.java b/key.core/src/main/java/de/uka/ilkd/key/settings/PathConfig.java index 040aa15ba23..f1bdbaab0bd 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/PathConfig.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/PathConfig.java @@ -14,8 +14,8 @@ * Keeps some central paths to files and directories. *

*

- * By default all KeY configurations are stored in a directory named ".key" inside the user's home - * directory. In Microsoft windows operating systems this is directly the hard disc that contains + * By default, all KeY configurations are stored in a directory named ".key" inside the user's home + * directory. In Microsoft Windows operating systems this is directly the hard disc that contains * the KeY code. But the eclipse integration requires to change the default location. This is * possible via {@link #setKeyConfigDir(String)} which should be called once before something is * done with KeY (e.g. before the {@code MainWindow} is opened). @@ -81,7 +81,6 @@ public static Path getKeyConfigDir() { */ public static void setKeyConfigDir(String keyConfigDir) { PathConfig.keyConfigDir = Paths.get(keyConfigDir); - recentFileStorage = getKeyConfigDir().resolve("recentFiles.json"); proofIndependentSettings = getKeyConfigDir().resolve("proofIndependentSettings.props"); logDirectory = getKeyConfigDir().resolve("logs"); diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java index 9d7c698c9a4..04c2d4e34a3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java @@ -347,10 +347,7 @@ private ImmutableSet createSpecs(SpecExtractor specExtractor) && !declaringType.getFullName().equals("java.lang.Object") && !pm.isImplicit()) { specRepos.addContract(specExtractor.createDefaultContract(pm, - initConfig.getActivatedChoices().exists( - choice -> choice.category().equals("soundDefaultContracts") - && choice.name().toString() - .equals("soundDefaultContracts:on")))); + initConfig.isChoiceActive("soundDefaultContracts:on"))); } addLoopInvariants(specExtractor, specRepos, kjt, pm); diff --git a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/GenericRemovingLemmaGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/GenericRemovingLemmaGenerator.java index 778914c8cdc..6e4c961d4f8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/GenericRemovingLemmaGenerator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/GenericRemovingLemmaGenerator.java @@ -70,7 +70,7 @@ protected Sort replaceSort(Sort sort, TermServices services) { } ImmutableSet extSorts = replaceSorts(sort.extendsSorts(), services); - ProxySort result = new ProxySort(sort.name(), extSorts, "", ""); + ProxySort result = new ProxySort(sort.name(), extSorts, ""); sortMap.put(sort, result); return result; diff --git a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/TacletLoader.java b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/TacletLoader.java index 0618c9668f2..ac7cb117a9a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/TacletLoader.java +++ b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/TacletLoader.java @@ -6,7 +6,7 @@ import java.io.File; import java.nio.file.Path; import java.util.Collection; -import java.util.HashMap; +import java.util.Map; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.proof.Proof; @@ -83,7 +83,7 @@ public void manageAvailableTaclets(InitConfig initConfig, Taclet tacletToProve) ImmutableList sysTaclets = initConfig.getTaclets(); ImmutableList newTaclets = ImmutableSLList.nil(); - HashMap> map = initConfig.getTaclet2Builder(); + Map> map = initConfig.getTaclet2Builder(); boolean tacletfound = false; for (Taclet taclet : sysTaclets) { if (taclet.equals(tacletToProve)) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/UserDefinedSymbols.java b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/UserDefinedSymbols.java index 318f99bb81b..fd43d930ade 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/UserDefinedSymbols.java +++ b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/UserDefinedSymbols.java @@ -123,7 +123,7 @@ public void replaceGenericByProxySorts() { for (Sort sort : usedExtraSorts) { if (sort instanceof GenericSort genSort) { ProxySort proxySort = new ProxySort(genSort.name(), genSort.extendsSorts(), - "", ""); + ""); result.add(proxySort); } else { result.add(sort); diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java b/key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java index d49b8cc496b..8a6c4212c69 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java @@ -161,6 +161,7 @@ private static String getNiceMessageInternal(IntStream inputStream, return token == null ? null : new Location( + // FIXME weigl: This does not work on Windows. Illegal characters. Paths.get(Paths.get("").toString(), exc.getInputStream().getSourceName()) .normalize().toUri(), Position.fromToken(token)); diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/SideProofUtil.java b/key.core/src/main/java/de/uka/ilkd/key/util/SideProofUtil.java index 75c1cda207b..7b2dd56c94c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/SideProofUtil.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/SideProofUtil.java @@ -16,7 +16,6 @@ import de.uka.ilkd.key.rule.BuiltInRule; import de.uka.ilkd.key.rule.OneStepSimplifier; import de.uka.ilkd.key.rule.Taclet; -import de.uka.ilkd.key.rule.tacletbuilder.TacletBuilder; import de.uka.ilkd.key.settings.ProofSettings; import org.key_project.logic.Choice; @@ -63,9 +62,7 @@ public static ProofEnvironment cloneProofEnvironmentWithOwnOneStepSimplifier( ? new ProofSettings(sourceInitConfig.getSettings()) : null; initConfig.setSettings(clonedSettings); - initConfig.setTaclet2Builder( - (HashMap>) sourceInitConfig.getTaclet2Builder() - .clone()); + initConfig.setTaclet2Builder(new HashMap<>(sourceInitConfig.getTaclet2Builder())); initConfig.setTaclets(sourceInitConfig.getTaclets()); // Create new ProofEnvironment and initialize it with values from initial one. ProofEnvironment env = new ProofEnvironment(initConfig); diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heap.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heap.key index 87896efa8da..a24947b5743 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heap.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heap.key @@ -14,9 +14,37 @@ \functions { // select/store alpha alpha::select(Heap, Object, Field); + + + /*! This function modifies a heap by changing the value in one location. It takes four arguments: + + 1. The heap h which is to be modified + 2. The object o reference of the location which is to be modified + 3. The field of the location which is to be modified + 4. The value v which is to be written in the designated location. + + The result is a heap which coincides with h in all locations but in (o,f), where v is stored. + In the theory of arrays, store is somtimes called "write". + The field java.lang.Object::<created> cannot be updated using store; use "create". */ Heap store(Heap, Object, Field, any); + + /*! This function modifies a heap by changing the createdness of one object. + It takes two arguments: + 1. The heap h which is to be modified + 2. The object reference o for the object which is to be set created. + The result is a heap which coincides with h in all locations but in (o,java.lang.Object::), + which has been set to true. There is no means to modify a heap by setting the createdness of an object to false. + */ Heap create(Heap, Object); Heap anon(Heap, LocSet, Heap); + + /*! This function modifies a heap by changing the value in one location. It takes three arguments: + 1. The heap h which is to be modified + 2. The location set s whose locations are to be modified + 3. The value v which is to be written in the designated locations. + + The result is a heap which coincides with h in all locations but in the locations in s where v is stored. + The field java.lang.Object::<created> cannot be updated using memset; use "create". */ Heap memset(Heap, LocSet, any); // default value for a field @@ -26,6 +54,16 @@ alpha alpha::final(Object, Field); // fields + + /*! + This function turns an integer into a field reference. + + Integers are used to access the entries of entries within arrays stored on the heap. This + function provides the injection of the integer domain into that of the type Field. It is + ensured that this image of arr is disjoint from any defined field constant. + + The array access a[i], for instance for an int-array a, becomes int::select(heap, a, arr(i)). + */ \unique Field arr(int); \unique Field java.lang.Object::; \unique Field java.lang.Object::; @@ -36,16 +74,38 @@ \unique Field alpha::; // static \unique Field alpha::; // static - // array length + /*! array length + + The length of an array is not stored on the heap but is an inherent property of the object reference which denotes the array. + Hence, this functions takes only one argument: the object reference whose length (as an array) is to be retrieved. + This function always results in a non-negative value. + */ int length(Object); - // null + /*! A constant holding the object reference pointing to the Java null object. + Quite the same as the keyword "null" in Java. */ Null null; } \predicates { + /*! This predicate takes an argument of type Heap. It is true if the following conditions hold for its the argument: + 1. Every location contains a reference to a created (in this heap) object or null. + 2. Every location set stored on the heap contains only created objects. + 3. Every location belonging to a declared Java field holds a value compatible with its type. + 4. Only finitely many objects are created on the heap. + */ wellFormed(Heap); + + /*! + This predicate is true if the described array update is valid in Java. + + Java has the peculiarity of covariant array types. They allow an array assignment to fail at runtime (with an ArrayStoreException). This predicate deals with the issue in the logic. + + (tbd) + */ arrayStoreValid(any, any); + + nonNull(Heap, Object, int); // can be used to formulate assignable proof obligations in JML assert statements (via \dl_ escapes) @@ -53,5 +113,11 @@ } \programVariables { - Heap heap, savedHeap, permissions; + Heap + /*! This program variable holds to the current heap state. + Its type is Heap. Any assignment statement in a modality modifies the value of this program variable + and any expression reading from the heap within a Java modality refers to the heap stored + in this program variable. */ + heap, + savedHeap, permissions; } diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaHeader.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaHeader.key index 810c4692342..50e40d4503e 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaHeader.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaHeader.key @@ -26,6 +26,12 @@ \functions { alpha alpha::cast(any); + + /*! A boolean function which is true iff the dynamic type of its argument is + precisely the type which is part of the function name. */ boolean alpha::exactInstance(any); + + /*! A boolean function which is true iff the dynamic type of its argument is a + subtype of the type which is part of the function name. */ boolean alpha::instance(any); } diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locSets.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locSets.key index b1a2a9a2cd4..be74f91a6dc 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locSets.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locSets.key @@ -11,18 +11,48 @@ \functions { // unique function symbols + /*! The empty location set which does not contain any elements. */ \unique LocSet empty; + + /*! The unique location set containing all locations, i.e. elementOf(o, f, allLocs) + will always return true for an arbitrary Field f and Object o. */ \unique LocSet allLocs; // other constructors + /*! Converts a single location to a locations set with one element. */ LocSet singleton(Object, Field); + + /*! Union between two location sets. */ LocSet union(LocSet, LocSet); + + /*! Intersection between two location sets. */ LocSet intersect(LocSet, LocSet); + + /*! Realizes relative complement (a.k.a. set difference) between two locations sets. It takes as arguments + two location sets and returns another location set which contains all elements from the first argument + except those that are elements of the second argument. */ LocSet setMinus(LocSet, LocSet); + + /*! Takes as argument a term of type LocSet, which may contain a free variable. The term represents a family + of locations sets, which is parameterized by the unbound variable. The returned location set is the union + over all members of the parameterized family. */ LocSet infiniteUnion {true}(LocSet); + + /*! The set that contains all locations which belong to the object o given as argument. + + A location (a,b) is in the set allFields(o) iff a=o. + In JML, the function corresponds to `o.*`. */ LocSet allFields(Object); + + /*! The set of all locations that belong to a particular field f given as argument. + + A location (a,b) is in the set allObjects(f) iff b=f. */ LocSet allObjects(Field); + + /*! The set of locations which are fresh (that is not created) w.r.t. the heap h given as argument. + A location (a,b) is in the set freshLocs(h) iff o.<created>@h = FALSE. */ LocSet arrayRange(Object, int, int); + LocSet freshLocs(Heap); // work-a-round LocSet allElementsOfArray(Heap, Object, LocSet); @@ -30,8 +60,21 @@ } \predicates { + /*! This is the set theoretic membership predicate to be used for location sets. + + It takes three arguments: The first two (an Object and a Field) make up the location and the + third is the location set against which membership is tested. */ elementOf(Object, Field, LocSet); + + /*! This is the set theoretic subset predicate to be used for location sets. + + A location set A is subset of another location set B iff every element of A is also element of B.*/ subset(LocSet, LocSet); + + /*! This binary predicate models disjointness of location sets. + + disjoint(A,B) is true iff A and B have an empty intersection, + it is thus equivalent to intersect(A,B) = empty.*/ disjoint(LocSet, LocSet); createdInHeap(LocSet, Heap); } diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/map.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/map.key index baa1cb64421..0fff5bdf9c7 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/map.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/map.key @@ -13,30 +13,47 @@ Abstract datatype of (untyped) partial maps. Map; } + + \functions { - /*! - Return a value from the given Map. - If value is undefined, `mapUndef` is used. - */ + /*! Return a value from the given Map. If value is undefined, `mapUndef` is used. */ any mapGet(Map, any); - /*! - - */ + /*! A unique value, which is returned by mapGet in case no mapping value is declared for the specified key. */ \unique any mapUndef; // constructors + /*! Generalized quantifier for maps. This is a generic constructor for maps. */ Map mapForeach {true, true}(boolean, any); + + /*! The empty map, which does not contain any entries. */ Map mapEmpty; + + /*! A map, which contains only one entry. */ Map mapSingleton(any, any); + + /*! Takes as arguments two maps and creates a new map from their entries. In case their domains overlap, + entries of the second map are used for keys from the intersection. */ Map mapOverride(Map, Map); + + /*! Converts a sequence to a map. The map domain consists of exactly those integers, which are inside the sequence bounds. */ Map seq2map(Seq); + + /*! Adds an entry to a map or overwrites an existing one. */ Map mapUpdate(Map, any, any); + + /*! Removes an entry from a map. */ Map mapRemove(Map, any); } \predicates { + /*! Takes two arguments: key ∈ any and map ∈ Map. Returns true iff key is in the domain of map. */ inDomain(Map, any); + + /*! Returns true iff the domain of the specified map contains only objects that are ; + in the implicit heap (additional non-object values may also be part of the domain). This can be used + in a JML specification as an invariant to ensure, that non-created objects are not (yet) part + of the domain of a map. */ inDomainImpliesCreated(Map); } diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/optionsDeclarations.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/optionsDeclarations.key index 6b4660adff5..e251ef5f86e 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/optionsDeclarations.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/optionsDeclarations.key @@ -160,48 +160,7 @@ integerSimplificationRules: {full, /*! @choiceIncomplete */ minimal}; // TODO: further refine this option permissions: {off, on}; - /*! - Treatment of formulas and terms for welldefinedness checks: - */ - wdOperator: { - /*! - More intuitive for software developers and along the lines of - runtime assertion semantics. Well-Definedness checks will be - stricter using this operator, since the order of terms/formulas - matters. It is based on McCarthy logic. - Cf. "Are the Logical Foundations of Verifying Compiler - Prototypes Matching User Expectations?" by Patrice Chalin. - - @choiceDefaultOption - */ - L, - /*! - Complete and along the lines of classical logic, where the - order of terms/formulas is irrelevant. This operator is - equivalent to the D-operator, but more efficient. - Cf. "Efficient Well-Definedness Checking" by Ádám Darvas, - Farhad Mehta, and Arsenii Rudich. - */ - Y, - /*! - Complete and along the lines of classical logic, where the - order of terms/formulas is irrelevant. This operator is not as - strict as the L-operator, based on strong Kleene logic. To be - used with care, since formulas may blow up exponentially. - Cf. "Well Defined B" by Patrick Behm, Lilian Burdy, and - Jean-Marc Meynadier*/ - D - }; - /*! - Welldefinedness checks of JML specifications can be turned on/off. - This includes class invariants, operation contracts, model fields - as well as JML (annotation) statements as loop invariants and - block contracts. The former ones are checked "on-the-fly", i.e., - directly when they are applied in the code while proving an operation - contract, since the context is needed. - */ - wdChecks: {off, on}; /*! Specifies whether a special goal "Joined node is weakening" should be generated as a child of the partner node of a join operation. diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/seq.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/seq.key index e9fa73b1381..432776504de 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/seq.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/seq.key @@ -19,24 +19,59 @@ \functions { // getters + /*! Return the element at a position within a sequence. The type read from the sequence is part of the function name. */ alpha alpha::seqGet(Seq, int); + + /*! Return the length of a sequence. */ int seqLen(Seq); + + /*! Return the first index in a sequence that holds a value. */ int seqIndexOf(Seq, any); + /*! The underspecified error value if a sequence is accessed outside its idnex range. */ any seqGetOutside; // constructors + /*! The empty sequence. */ Seq seqEmpty; + /*! A singleton sequence that has the argument as only entry.*/ Seq seqSingleton(any); + + /*! Concatenates two sequences. */ Seq seqConcat(Seq, Seq); + + /*! Takes a subsequence from a sequence. + The first argument is the original sequence, + the second is the first index to consider (inclusive) and + the third is the last index to consider (!exclusive!). */ Seq seqSub(Seq, int, int); + + /*! Reverses a sequence. The result has the same entries as the argument but in reverse order. */ Seq seqReverse(Seq); Seq seqUpd(Seq, int, any); + + /*! This function binds an integer variable and evaluates an expression over this variable + for a range of values to obtain the entries of a sequence. + + The sequence + `seqDef{int i;}(-2, 3, i*i)` + has, for instance, the entries + `[ 4, 1, 0, 1, 4 ]`. + + The first and second argument give the range over which the variable goes. Again, the right-hand bound is exclusive. + + seqDef is related to the lambda operator in lambda calculus. */ Seq seqDef {false, false, true}(int, int, any); + /*! Takes a sequence and two indices. The elements at the specified indices are exchanged in the resulting sequence. In case one of the indices is out of bounds, the sequence is left unchanged.*/ Seq seqSwap(Seq, int, int); + + /*! Takes a sequence and removes the element at the specified index. In case the index is out of bounds, the sequence is left unchanged. */ Seq seqRemove(Seq, int); + + /*! Takes a sequence of naturals (zero included) and treats it as a permutation. The resulting sequence is the inverse permutation of the original one. */ Seq seqNPermInv(Seq); + /*! Convert a Java array to a JavaDL sequence. */ Seq array2seq(Heap, Object); // placeholder for values in enhanced for loop diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wellfound.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wellfound.key index 629a7daf6e7..8c8cefff393 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wellfound.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wellfound.key @@ -26,8 +26,13 @@ \functions { // The constructor is unique which makes it also an injection. + /*! Return the (unique) ordered pair of two specified elements. */ \unique Pair pair(any, any); + + /*! Return the first element of an ordered pair. */ any first(Pair); + + /*! Return the second element of an ordered pair. */ any second(Pair); } diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/RuleSet.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/RuleSet.java index 73a341b5e6e..35770ca02bf 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/RuleSet.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/RuleSet.java @@ -3,6 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.prover.rules; +import org.key_project.logic.HasDocumentation; import org.key_project.logic.Name; import org.key_project.logic.Named; @@ -14,7 +15,7 @@ /// /// Rulesets had been originally called heuristics. /// -public record RuleSet(Name name) implements Named { +public record RuleSet(Name name) implements Named, HasDocumentation { /// creates a ruleset /// /// @param name the [Name] of the ruleset @@ -44,4 +45,9 @@ public boolean equals(@Nullable Object other) { /// toString public String toString() { return name.toString(); } + + @Override + public String getDocumentationKey() { + return "heuristic/" + name; + } } diff --git a/key.ncore/src/main/java/org/key_project/logic/Choice.java b/key.ncore/src/main/java/org/key_project/logic/Choice.java index 09c1d2a9482..d01c4fb3e3e 100644 --- a/key.ncore/src/main/java/org/key_project/logic/Choice.java +++ b/key.ncore/src/main/java/org/key_project/logic/Choice.java @@ -13,7 +13,7 @@ /// A choice is represented by a string, where the category is separated by the option with a colon. /// /// Choices can be declared within KeY files. They influence the activation of taclets. -public class Choice implements Named { +public class Choice implements Named, HasDocumentation { private final @NonNull Name name; private final @NonNull String category; @@ -58,4 +58,9 @@ public int hashCode() { public String toString() { return name.toString(); } + + @Override + public String getDocumentationKey() { + return "choice/" + name; + } } diff --git a/key.ncore/src/main/java/org/key_project/logic/HasDocumentation.java b/key.ncore/src/main/java/org/key_project/logic/HasDocumentation.java new file mode 100644 index 00000000000..cc30145b1ac --- /dev/null +++ b/key.ncore/src/main/java/org/key_project/logic/HasDocumentation.java @@ -0,0 +1,20 @@ +/* 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 org.key_project.logic; + +import org.jspecify.annotations.Nullable; + +public interface HasDocumentation { + String getDocumentationKey(); + + default @Nullable String getDocumentation() { + return null; + } + + record OptionCategory(String name) implements HasDocumentation { + public String getDocumentationKey() { + return "category/" + name; + } + } +} diff --git a/key.ncore/src/main/java/org/key_project/logic/op/Operator.java b/key.ncore/src/main/java/org/key_project/logic/op/Operator.java index 0a3d0c99ac1..e5d045b94ff 100644 --- a/key.ncore/src/main/java/org/key_project/logic/op/Operator.java +++ b/key.ncore/src/main/java/org/key_project/logic/op/Operator.java @@ -3,13 +3,10 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.logic.op; -import org.key_project.logic.Named; -import org.key_project.logic.SyntaxElement; -import org.key_project.logic.Term; -import org.key_project.logic.TermCreationException; +import org.key_project.logic.*; import org.key_project.logic.sort.Sort; -public interface Operator extends Named, SyntaxElement { +public interface Operator extends Named, HasDocumentation, SyntaxElement { /// the arity of this operator int arity(); @@ -41,4 +38,9 @@ default boolean hasModifier(Modifier mod) { /// /// @throws TermCreationException if a construction error was recognised void validTopLevelException(T term) throws TermCreationException; + + @Override + default String getDocumentationKey() { + return "operator/" + name(); + } } diff --git a/key.ncore/src/main/java/org/key_project/logic/sort/AbstractSort.java b/key.ncore/src/main/java/org/key_project/logic/sort/AbstractSort.java index d536defdf29..e1b9781a04b 100644 --- a/key.ncore/src/main/java/org/key_project/logic/sort/AbstractSort.java +++ b/key.ncore/src/main/java/org/key_project/logic/sort/AbstractSort.java @@ -5,18 +5,11 @@ import org.key_project.logic.Name; -import org.jspecify.annotations.Nullable; - - /// Abstract base class for implementations of the Sort interface. public abstract class AbstractSort implements Sort { private final Name name; private final boolean isAbstract; - /// Documentation for this sort given by the associated documentation comment. - /// //@see de.uka.ilkd.key.nparser.KeYParser.One_sort_declContext#doc - private @Nullable String documentation; - protected AbstractSort(Name name, boolean isAbstract) { this.name = name; this.isAbstract = isAbstract; @@ -40,13 +33,4 @@ public final String toString() { public String declarationString() { return name.toString(); } - - public void setDocumentation(@Nullable String documentation) { - this.documentation = documentation; - } - - @Override - public @Nullable String getDocumentation() { - return documentation; - } } diff --git a/key.ncore/src/main/java/org/key_project/logic/sort/Sort.java b/key.ncore/src/main/java/org/key_project/logic/sort/Sort.java index 41a94bdc81e..adae6056850 100644 --- a/key.ncore/src/main/java/org/key_project/logic/sort/Sort.java +++ b/key.ncore/src/main/java/org/key_project/logic/sort/Sort.java @@ -3,14 +3,14 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.logic.sort; +import org.key_project.logic.HasDocumentation; import org.key_project.logic.HasOrigin; import org.key_project.logic.LogicServices; import org.key_project.logic.Named; import org.key_project.util.collection.ImmutableSet; -import org.jspecify.annotations.Nullable; -public interface Sort extends Named, HasOrigin { +public interface Sort extends Named, HasOrigin, HasDocumentation { /// @return the direct supersorts of this sort. Not supported by `NullSort`. ImmutableSet extendsSorts(); @@ -27,7 +27,8 @@ default ImmutableSet extendsSorts(Service String declarationString(); - /// Returns a human explainable text describing this sort. This field is typical set by the - /// parser, who captures the documentation comments. - default @Nullable String getDocumentation() { return null; } + @Override + default String getDocumentationKey() { + return "sort/" + name(); + } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTree.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTree.java deleted file mode 100644 index 6918c7339ba..00000000000 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTree.java +++ /dev/null @@ -1,40 +0,0 @@ -/* 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.gui; - -import javax.swing.JTree; -import javax.swing.tree.DefaultMutableTreeNode; -import javax.swing.tree.DefaultTreeModel; - -/** - * This class is used by {@link InfoView} to display its contents. - * - * @author Kai Wallisch - */ -public class InfoTree extends JTree { - - /** - * - */ - private static final long serialVersionUID = 2018185104131516569L; - - InfoTree() { - DefaultMutableTreeNode root = new DefaultMutableTreeNode(); - root.add(new InfoTreeNode("No proof loaded", - "In this pane, the available logical rules will be displayed and/or explained.")); - setModel(new DefaultTreeModel(root)); - setShowsRootHandles(true); - setRootVisible(false); - } - - /* - * This function is expected to return only {@link InfoTreeNode} instances. The super method - * returns {@link DefaultMutableTreeNode} instances. - */ - @Override - public InfoTreeNode getLastSelectedPathComponent() { - return (InfoTreeNode) super.getLastSelectedPathComponent(); - } - -} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTreeModel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTreeModel.java deleted file mode 100644 index e5c2656b37e..00000000000 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTreeModel.java +++ /dev/null @@ -1,220 +0,0 @@ -/* 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.gui; - -import java.util.*; -import javax.swing.tree.DefaultTreeModel; - -import de.uka.ilkd.key.proof.Goal; -import de.uka.ilkd.key.proof.mgt.RuleJustification; -import de.uka.ilkd.key.rule.BuiltInRule; -import de.uka.ilkd.key.rule.NoPosTacletApp; -import de.uka.ilkd.key.rule.OneStepSimplifier; -import de.uka.ilkd.key.rule.Taclet; -import de.uka.ilkd.key.util.MiscTools; -import de.uka.ilkd.key.util.XMLResources; - -import org.key_project.logic.Name; - -/** - * Extension of {@link DefaultTreeModel} used by {@link InfoTree}. - * - * @author Kai Wallisch - */ -public class InfoTreeModel extends DefaultTreeModel { - - /** - * - */ - private static final long serialVersionUID = 2093787874117871875L; - private static final String LEMMAS = "Lemmas"; - private static final String TACLET_BASE = "Taclet Base"; - - public InfoTreeModel(Goal goal, XMLResources xmlResources, MainWindow mainWindow) { - super(new InfoTreeNode()); - insertAsLast(new RulesNode(xmlResources.getRuleExplanations(), goal), (InfoTreeNode) root); - insertAsLast(new TermLabelsNode(mainWindow, xmlResources.getTermLabelExplanations()), - (InfoTreeNode) root); - insertAsLast(new FunctionsNode(xmlResources.getFunctionExplanations()), - (InfoTreeNode) root); - } - - private void insertAsLast(InfoTreeNode ins, InfoTreeNode parent) { - insertNodeInto(ins, parent, parent.getChildCount()); - } - - private class FunctionsNode extends InfoTreeNode { - - /** - * - */ - private static final long serialVersionUID = -5546552277804988834L; - private static final String COLLECTION = - "This node stands for a category of symbols; expand it to browse the symbols " - + "in the category."; - private static final String DEFAULT_FUNCTIONS_LABEL = - "Display descriptions for documented interpreted function and predicate symbols."; - - FunctionsNode(Properties functionExplanations) { - super("Function Symbols", DEFAULT_FUNCTIONS_LABEL); - - Map categoryMap = new HashMap<>(); - - List sortedKeys = - new ArrayList<>(functionExplanations.stringPropertyNames()); - java.util.Collections.sort(sortedKeys); - - for (String key : sortedKeys) { - String[] parts = key.split("/", 2); - if (parts.length == 1) { - // no "/" - insertAsLast(new InfoTreeNode(key, functionExplanations), this); - } else { - String category = parts[0]; - InfoTreeNode categoryNode = categoryMap.get(category); - if (categoryNode == null) { - categoryNode = new InfoTreeNode(category, COLLECTION); - categoryMap.put(category, categoryNode); - insertAsLast(categoryNode, this); - } - String description = functionExplanations.getProperty(key); - insertAsLast(new InfoTreeNode(parts[1], description), categoryNode); - } - } - } - } - - private class TermLabelsNode extends InfoTreeNode { - - /** - * - */ - private static final long serialVersionUID = 7447092361863294242L; - - TermLabelsNode(MainWindow mainWindow, Properties termLabelExplanations) { - super("Term Labels", "Show descriptions for currently available term labels."); - - List labelNames = mainWindow.getSortedTermLabelNames(); - for (Name name : labelNames) { - insertAsLast(new InfoTreeNode(name.toString(), termLabelExplanations), this); - } - } - } - - private class RulesNode extends InfoTreeNode { - - /** - * - */ - private static final long serialVersionUID = 7622830441420768861L; - - RulesNode(Properties ruleExplanations, Goal goal) { - super("Rules", "Browse descriptions for currently available rules."); - - InfoTreeNode builtInRoot = new InfoTreeNode("Built-In", ruleExplanations); - insertAsLast(builtInRoot, this); - InfoTreeNode axiomTacletRoot = new InfoTreeNode(TACLET_BASE, ruleExplanations); - insertAsLast(axiomTacletRoot, this); - InfoTreeNode proveableTacletsRoot = new InfoTreeNode(LEMMAS, ruleExplanations); - insertAsLast(proveableTacletsRoot, this); - - if (goal != null && goal.proof() != null && goal.proof().mgt() != null) { - for (final BuiltInRule br : goal.ruleAppIndex().builtInRuleAppIndex() - .builtInRuleIndex().rules()) { - insertAsLast(new InfoTreeNode(br, ruleExplanations), builtInRoot); - } - Set set = goal.ruleAppIndex().tacletIndex().allNoPosTacletApps(); - OneStepSimplifier simplifier = MiscTools.findOneStepSimplifier(goal.proof()); - if (simplifier != null && !simplifier.isShutdown()) { - set.addAll(simplifier.getCapturedTaclets()); - } - - for (final NoPosTacletApp app : sort(set)) { - RuleJustification just = goal.proof().mgt().getJustification(app); - if (just == null) { - continue; // do not break system because of this - } - if (just.isAxiomJustification()) { - insertAndGroup(new InfoTreeNode(app.taclet()), axiomTacletRoot, - ruleExplanations); - } else { - insertAndGroup(new InfoTreeNode(app.taclet()), proveableTacletsRoot, - ruleExplanations); - } - } - } - - axiomTacletRoot - .setUserObject(TACLET_BASE + " (" + getChildCount(axiomTacletRoot) + ")"); - proveableTacletsRoot - .setUserObject(LEMMAS + " (" + getChildCount(proveableTacletsRoot) + ")"); - } - - private int getChildCount(InfoTreeNode root) { - int res = 0; - for (int i = 0; i < root.getChildCount(); i++) { - final InfoTreeNode child = (InfoTreeNode) root.getChildAt(i); - // there is no deeper nesting - final int grandchildren = child.getChildCount(); - res += grandchildren == 0 ? 1 : grandchildren; - } - return res; - } - - /** - * groups subsequent insertions with the same name under a new node - */ - private void insertAndGroup(InfoTreeNode ins, InfoTreeNode parent, - Properties ruleExplanations) { - InfoTreeNode insNode = ins; - if (parent.getChildCount() > 0) { - InfoTreeNode lastNode = - (InfoTreeNode) parent.getChildAt(parent.getChildCount() - 1); - if (getName(insNode).equals(getName(lastNode))) { - if (lastNode.getChildCount() == 0) { - removeNodeFromParent(lastNode); - InfoTreeNode oldParent = parent; - parent = new InfoTreeNode(getName(insNode), ruleExplanations); - insNode.setTitleToAltName(); - lastNode.setTitleToAltName(); - insertAsLast(parent, oldParent); - insertAsLast(lastNode, parent); - } else { - parent = lastNode; - insNode.setTitleToAltName(); - } - } - } - insertAsLast(ins, parent); - } - - private String getName(InfoTreeNode t1) { - if (t1.getUserObject() instanceof Taclet) { - return ((Taclet) t1.getUserObject()).displayName(); - } else { - String title = t1.toString(); - - // strip number of taclets - int parenIdx = title.lastIndexOf('('); - if (parenIdx >= 0) { - return title.substring(0, parenIdx - 1).intern(); - } else { - return title; - } - } - } - - private List sort(Set set) { - final ArrayList l = new ArrayList<>(set); - - l.sort((o1, o2) -> { - final Taclet t1 = o1.taclet(); - final Taclet t2 = o2.taclet(); - return t1.displayName().compareTo(t2.displayName()); - }); - return l; - } - } - -} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTreeNode.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTreeNode.java deleted file mode 100644 index 86909fc9f95..00000000000 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTreeNode.java +++ /dev/null @@ -1,97 +0,0 @@ -/* 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.gui; - -import java.util.Properties; -import javax.swing.tree.DefaultMutableTreeNode; - -import de.uka.ilkd.key.pp.LogicPrinter; -import de.uka.ilkd.key.pp.NotationInfo; -import de.uka.ilkd.key.rule.BuiltInRule; -import de.uka.ilkd.key.rule.Rule; -import de.uka.ilkd.key.rule.Taclet; - -/** - * Every node of {@link InfoTree} is an instance of this class. - * - * @author Kai Wallisch - */ -public class InfoTreeNode extends DefaultMutableTreeNode { - - private static final long serialVersionUID = 4187650510339169399L; - // the original rule name - private final String altName; - private String description; - - private Rule rule; - - /* - * This constructor should only be used for the invisible root node of {@link InfoTreeModel}. - */ - InfoTreeNode() { - super("root node"); - altName = null; - description = "This is the root node of InfoTreeModel. It should not be visible."; - } - - /** - * @param title The name of the node. - * @param explanations An XML resource containing node descriptions. - */ - InfoTreeNode(String title, Properties explanations) { - super(title); - - altName = null; - String desc = explanations.getProperty(title); - - if (desc == null) { - description = "No description available for " + title + "."; - } else { - description = desc; - } - - } - - InfoTreeNode(Taclet taclet) { - super(taclet.displayName()); - this.rule = taclet; - altName = taclet.name().toString(); - LogicPrinter lp = LogicPrinter.purePrinter(new NotationInfo(), null); - lp.printTaclet(taclet); - description = lp.result() + "\n\n Defined at:" + taclet.getOrigin() - + "\n\n under options:" + taclet.getChoices(); - } - - InfoTreeNode(String title, String description) { - super(title); - altName = null; - this.description = description; - } - - public InfoTreeNode(BuiltInRule br, Properties ruleExplanations) { - this(br.displayName(), ruleExplanations); - rule = br; - description = "Defined at: " + br.getOrigin(); - } - - String getTitle() { - return (String) getUserObject(); - } - - /** - * switch title to alternative name (i.e., internal rule name) - */ - void setTitleToAltName() { - assert altName != null; - userObject = altName; - } - - String getDescription() { - return description; - } - - public Rule getRule() { - return rule; - } -} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoView.java index 27200a52ac8..c84687ff1fa 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoView.java @@ -7,27 +7,50 @@ import java.awt.event.ComponentListener; import java.awt.event.MouseAdapter; import java.awt.event.MouseEvent; +import java.util.*; +import java.util.function.Supplier; +import java.util.stream.Collectors; +import java.util.stream.Stream; import javax.swing.*; -import javax.swing.event.TreeSelectionEvent; -import javax.swing.event.TreeSelectionListener; +import javax.swing.tree.DefaultMutableTreeNode; +import javax.swing.tree.DefaultTreeModel; +import javax.swing.tree.MutableTreeNode; import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.core.KeYSelectionEvent; import de.uka.ilkd.key.core.KeYSelectionListener; -import de.uka.ilkd.key.core.KeYSelectionModel; -import de.uka.ilkd.key.gui.extension.api.DefaultContextMenuKind; +import de.uka.ilkd.key.gui.InfoView.InfoNodeFactory.InfoTreeNode; import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; import de.uka.ilkd.key.gui.extension.api.TabPanel; import de.uka.ilkd.key.gui.extension.impl.KeYGuiExtensionFacade; import de.uka.ilkd.key.gui.fonticons.IconFactory; +import de.uka.ilkd.key.gui.utilities.LexerHighlighter; +import de.uka.ilkd.key.logic.DocSpace; +import de.uka.ilkd.key.logic.label.TermLabelManager; +import de.uka.ilkd.key.pp.LogicPrinter; +import de.uka.ilkd.key.pp.NotationInfo; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.event.ProofDisposedEvent; import de.uka.ilkd.key.proof.event.ProofDisposedListener; -import de.uka.ilkd.key.rule.Rule; -import de.uka.ilkd.key.util.ThreadUtilities; -import de.uka.ilkd.key.util.XMLResources; +import de.uka.ilkd.key.proof.init.InitConfig; +import de.uka.ilkd.key.proof.mgt.RuleJustification; +import de.uka.ilkd.key.rule.BuiltInRule; +import de.uka.ilkd.key.rule.NoPosTacletApp; +import de.uka.ilkd.key.rule.OneStepSimplifier; +import de.uka.ilkd.key.rule.Taclet; +import de.uka.ilkd.key.util.MiscTools; + +import org.key_project.logic.Choice; +import org.key_project.logic.Name; +import org.key_project.logic.Namespace; +import org.key_project.logic.op.Function; +import org.key_project.logic.sort.Sort; +import org.key_project.prover.rules.RuleApp; +import org.key_project.util.collection.ImmutableList; + +import org.jspecify.annotations.Nullable; /** * Class for info contents displayed in {@link MainWindow}. @@ -35,24 +58,41 @@ * @author Kai Wallisch */ public class InfoView extends JSplitPane implements TabPanel { - - private static final long serialVersionUID = -6944612837850368411L; public static final Icon INFO_ICON = IconFactory.INFO_VIEW.get(MainWindow.TAB_ICON_SIZE); - private final InfoTree infoTree; - private final InfoViewContentPane contentPane; - private final XMLResources xmlResources; + private final JTree infoTree = new JTree(); + private final JTextPane contentPane = createInfoArea(); private final ProofDisposedListener proofDisposedListener; - private final KeYSelectionListener selectionListener = new InfoViewSelectionListener(); - private Node lastShownGoalNode; - private MainWindow mainWindow; + private final InfoNodeFactory nodeFactory = new InfoNodeFactory(); + + private LexerHighlighter lexerHighlighter = new LexerHighlighter.KeYLexerHighlighter(); + + + private final KeYSelectionListener selectionListener = new KeYSelectionListener() { + public void selectedProofChanged(KeYSelectionEvent e) { + SwingUtilities.invokeLater(() -> { + if (mediator.getSelectedGoal() != null) { + updateModel(mediator.getSelectedGoal()); + } else if (mediator.getSelectedProof() != null) { + try { + updateModel(mediator.getSelectedProof().openGoals().head()); + } catch (NoSuchElementException ex) { + // nothing possible to do + } + } + }); + } + }; + + private @Nullable Node lastShownGoalNode; private KeYMediator mediator; - public InfoView() { + public InfoView(KeYMediator mediator) { super(VERTICAL_SPLIT); - xmlResources = new XMLResources(); + + setMediator(mediator); // initial placement of the divider setDividerLocation(300); @@ -63,18 +103,13 @@ public InfoView() { // Setting a name for this causes PreferenceSaver to include this class. setName("infoViewPane"); - infoTree = new InfoTree(); - infoTree.addTreeSelectionListener(new TreeSelectionListener() { - @Override - public void valueChanged(TreeSelectionEvent e) { - InfoTreeNode node = infoTree.getLastSelectedPathComponent(); - if (node != null) { - contentPane.setNode(node); - } else { - contentPane.clear(); - } - } - }); + + DefaultMutableTreeNode root = new DefaultMutableTreeNode(); + root.add(nodeFactory.create("No proof loaded", + "In this pane, the available logical rules will be displayed and/or explained.")); + infoTree.setModel(new DefaultTreeModel(root)); + infoTree.setShowsRootHandles(true); + infoTree.setRootVisible(false); lastShownGoalNode = null; @@ -124,37 +159,46 @@ public void mousePressed(MouseEvent e) { } private void checkPopup(MouseEvent e) { - if (e.isPopupTrigger()) { - Rule selected = infoTree.getLastSelectedPathComponent().getRule(); - JPopupMenu menu = KeYGuiExtensionFacade.createContextMenu( - DefaultContextMenuKind.TACLET_INFO, selected, mediator); - if (menu.getComponentCount() > 0) { - menu.show(InfoView.this, e.getX(), e.getY()); - } - } + /* + * if (e.isPopupTrigger()) { + * Rule selected = ((InfoTreeNode) + * infoTree.getLastSelectedPathComponent()).getRule(); + * JPopupMenu menu = KeYGuiExtensionFacade.createContextMenu( + * DefaultContextMenuKind.TACLET_INFO, selected, mediator); + * if (menu.getComponentCount() > 0) { + * menu.show(InfoView.this, e.getX(), e.getY()); + * } + * } + */ } }); - - contentPane = new InfoViewContentPane(); + infoTree.addTreeSelectionListener(e -> { + InfoTreeNode node = (InfoTreeNode) infoTree.getLastSelectedPathComponent(); + if (node != null) { + contentPane.setText(node.getDescription()); + lexerHighlighter.highlightPaneMarkdown(contentPane); + } else { + contentPane.setText(""); + } + }); setLeftComponent(new JScrollPane(infoTree)); - setRightComponent(contentPane); + setRightComponent(new JScrollPane(contentPane)); KeYGuiExtensionFacade.installKeyboardShortcuts(mediator, this, KeYGuiExtension.KeyboardShortcuts.INFO_VIEW); } - public InfoView(MainWindow window, KeYMediator mediator) { - this(); - setMainWindow(window); - setMediator(mediator); - } - + @Override + public void updateUI() { + // create new lexer highlighter for updating dark/light color + lexerHighlighter = new LexerHighlighter.KeYLexerHighlighter(); + super.updateUI(); + } public void setMediator(KeYMediator m) { - assert m != null; if (mediator != null) { mediator.removeKeYSelectionListener(selectionListener); } @@ -162,9 +206,6 @@ public void setMediator(KeYMediator m) { mediator = m; } - public void setMainWindow(MainWindow w) { - mainWindow = w; - } @Override public String getTitle() { @@ -181,52 +222,236 @@ public JComponent getComponent() { return this; } - private void updateModel(Goal g) { + private void updateModel(@Nullable Goal g) { if (g == null || lastShownGoalNode != g.node()) { if (lastShownGoalNode != null) { lastShownGoalNode.proof().removeProofDisposedListener(proofDisposedListener); } - final InfoTreeModel model; if (g != null) { - model = new InfoTreeModel(g, xmlResources, mainWindow); + infoTree.setModel(new DefaultTreeModel(nodeFactory.createInfoTreeRoot(g))); g.proof().addProofDisposedListener(proofDisposedListener); lastShownGoalNode = g.node(); } else { - model = null; + infoTree.setModel(null); lastShownGoalNode = null; } - contentPane.clear(); - infoTree.setModel(model); + contentPane.setText(""); } } - private class InfoViewSelectionListener implements KeYSelectionListener { + private JTextPane createInfoArea() { + var description = new JTextPane(); + description.setEditable(false); + description.setBorder(BorderFactory.createTitledBorder("")); + description.setCaretPosition(0); + return description; + } + + + public static class InfoNodeFactory { + private static final String LEMMAS = "Lemmas"; + private static final String TACLET_BASE = "Taclet Base"; + + private static final String COLLECTION = + "This node stands for a category of symbols; expand it to browse the symbols " + + "in the category."; + private static final String DEFAULT_FUNCTIONS_LABEL = + "Display descriptions for documented interpreted function and predicate symbols."; - /** - * focused node has changed - */ - @Override - public void selectedNodeChanged(KeYSelectionEvent e) { + + private DefaultMutableTreeNode createInfoTreeRoot(Goal g) { + InfoTreeNode root = create( + "This is the root node of InfoTreeModel. It should not be visible.", ""); + + DocSpace docs = g.proof().getServices().getNamespaces().docs(); + + root.add(createNodeRules(docs, g)); + root.add(createNodeTermLabels(docs, g.proof())); + root.add(createNodeFunctions(docs, g.proof().getNamespaces().functions())); + root.add(createNodeTacletOptions(docs, g.proof().getInitConfig())); + return root; } - /** - * the selected proof has changed (e.g. a new proof has been loaded) - */ - @Override - public void selectedProofChanged(KeYSelectionEvent e) { - final KeYSelectionModel selectionModel = e.getSource(); - Runnable action = () -> { - if (isVisible()) { - if (selectionModel.getSelectedProof() == null) { - updateModel(null); - } else if (selectionModel.getSelectedGoal() != null) { - // keep old view if an inner node has been selected - updateModel(selectionModel.getSelectedGoal()); - } + private InfoTreeNode createNodeRules(DocSpace docs, Goal g) { + var tlRoot = create("Rules", "Browse descriptions for currently available rules."); + + List set = + new ArrayList<>(g.ruleAppIndex().tacletIndex().allNoPosTacletApps()); + OneStepSimplifier simplifier = MiscTools.findOneStepSimplifier(g.proof()); + if (simplifier != null && !simplifier.isShutdown()) { + set.addAll(simplifier.getCapturedTaclets()); + } + set.sort(Comparator.comparing(RuleApp::displayName)); + + tlRoot.add(createNodeBuiltInRules(docs, g)); + tlRoot.add(createNodeAxiom(docs, + set.stream().filter(it -> { + RuleJustification just = g.proof().mgt().getJustification(it); + return just != null && just.isAxiomJustification(); + }))); + + tlRoot.add(createNodeLemmas(docs, set.stream().filter(it -> { + RuleJustification just = g.proof().mgt().getJustification(it); + return just != null && !just.isAxiomJustification(); + }))); + + return tlRoot; + } + + private MutableTreeNode createNodeBuiltInRules(DocSpace docs, Goal g) { + InfoTreeNode builtInRoot = create("Built-In", + "Some logical rules are implemented in Java code. This is because their semantics " + + + "cannot easily be expressed in KeY's Taclet language."); + ImmutableList rules = + g.ruleAppIndex().builtInRuleAppIndex().builtInRuleIndex().rules(); + for (BuiltInRule br : rules) { + builtInRoot.add(create(br, docs)); + } + return builtInRoot; + } + + private MutableTreeNode createNodeAxiom(DocSpace docs, Stream seq) { + InfoTreeNode axiomTacletRoot = create(TACLET_BASE, """ + Most logical rules are implemented as Taclets. + + Taclets are schematic logical rules formulated in the Taclet Language.\s + The language is defined and explained in the KeY book. + """); + Map> ruleAppIndex = new TreeMap<>(); + seq.forEach(it -> ruleAppIndex.computeIfAbsent(it.displayName(), k -> new ArrayList<>()) + .add(it)); + + ruleAppIndex.forEach((key, value) -> { + if (value.size() > 1) { + InfoTreeNode group = create("%s (%d)".formatted(key, value.size()), ""); + axiomTacletRoot.add(group); + value.forEach(it -> group.add(create(it.rule(), docs))); + } else { + value.forEach(it -> axiomTacletRoot.add(create(it.rule(), docs))); } - }; - ThreadUtilities.invokeOnEventQueue(action); + }); + var count = ruleAppIndex.values().stream().mapToInt(List::size).sum(); + axiomTacletRoot.setUserObject("%s (%d)".formatted(TACLET_BASE, count)); + return axiomTacletRoot; + } + + private MutableTreeNode createNodeLemmas(DocSpace docs, Stream seq) { + InfoTreeNode proveableTacletsRoot = create(LEMMAS, + """ + Taclets which have been introduced using File->Load User-Defined Taclets are filed here. + + Loading User Defined Taclets opens side branches on which the soundness of the lemma taclets must be established. + """); + seq.forEach(it -> proveableTacletsRoot.add(create(it.rule(), docs))); + return proveableTacletsRoot; + } + + private MutableTreeNode createNodeTermLabels(DocSpace docs, Proof proof) { + var tlRoot = + create("Term Labels", "Show descriptions for currently available term labels."); + var mgr = TermLabelManager.getTermLabelManager(proof.getServices()); + var factories = mgr.getFactories(); + + var labelNames = new ArrayList<>(factories.keySet()); + labelNames.sort(Comparator.comparing(Name::toString)); + + for (Name name : labelNames) { + tlRoot.add(new InfoTreeNode(name.toString(), + () -> factories.get(name).getDocumentation())); + } + return tlRoot; } + private InfoTreeNode createNodeFunctions(DocSpace docs, Namespace functions) { + var fnRoot = create("Function Symbols", DEFAULT_FUNCTIONS_LABEL); + var fnByName = create("By Name", DEFAULT_FUNCTIONS_LABEL); + var fnByReturnType = create("By Return Type", DEFAULT_FUNCTIONS_LABEL); + + fnRoot.add(fnByName); + fnRoot.add(fnByReturnType); + + var seq = new ArrayList<>(functions.allElements()); + seq.sort(Comparator.comparing(it -> it.name().toString())); + + var byReturn = new TreeMap>( + Comparator.comparing(it -> it.name().toString())); + + for (var fn : seq) { + var fnName = "%s(%s) : %s".formatted( + fn.name(), + fn.argSorts().stream().map(it -> it.name().toString()) + .collect(Collectors.joining(", ")), + fn.sort().name()); + var fnSort = fn.sort(); + + // flat list: + Supplier stringSupplier = () -> docs.find(fn); + fnByName.add(new InfoTreeNode(fnName, stringSupplier)); + + // by return type + byReturn.putIfAbsent(fnSort, new ArrayList<>()); + byReturn.get(fnSort).add(new InfoTreeNode(fnName, stringSupplier)); + } + + for (var entry : byReturn.entrySet()) { + var node = create(entry.getKey().name().toString(), ""); + entry.getValue().forEach(node::add); + fnByReturnType.add(node); + } + + return fnRoot; + } + + private InfoTreeNode createNodeTacletOptions(DocSpace docs, InitConfig initConfig) { + InfoTreeNode localRoot = + create("Active Taclet Options", "Shows the activated Taclet options"); + for (Choice activatedChoice : initConfig.getActivatedChoices()) { + localRoot.add( + create(activatedChoice.name().toString(), + docs.find(activatedChoice))); + } + return localRoot; + } + + + public InfoTreeNode create(Taclet taclet, DocSpace docs) { + LogicPrinter lp = LogicPrinter.purePrinter(new NotationInfo(), null); + lp.printTaclet(taclet); + return create(taclet.name().toString(), + () -> Stream.of(docs.find(taclet), "```key\n" + lp.result() + "\n```", + "Defined at:" + taclet.getOrigin() + "under options:" + taclet.getChoices()) + .filter(Objects::nonNull) + .collect(Collectors.joining("\n\n"))); + } + + public InfoTreeNode create(BuiltInRule br, DocSpace docs) { + var description = "Defined at: " + br.getOrigin(); + return create(br.displayName(), () -> Stream.of(docs.find(br), description) + .filter(Objects::nonNull) + .collect(Collectors.joining("\n\n"))); + } + + public InfoTreeNode create(String title, String description) { + return create(title, () -> description); + } + + public InfoTreeNode create(String title, Supplier description) { + return new InfoTreeNode(title, description); + } + + + public static class InfoTreeNode extends DefaultMutableTreeNode { + private final Supplier description; + + public InfoTreeNode(String name, Supplier description) { + super(name); + this.description = description; + } + + public String getDescription() { + return description.get(); + } + } } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoViewContentPane.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoViewContentPane.java deleted file mode 100644 index 3f61f68933e..00000000000 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoViewContentPane.java +++ /dev/null @@ -1,42 +0,0 @@ -/* 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.gui; - -import javax.swing.BorderFactory; -import javax.swing.JScrollPane; -import javax.swing.JTextArea; - -/** - * This class is used to display descriptions in {@link InfoView}. - * - * @author Kai Wallisch - */ -public class InfoViewContentPane extends JScrollPane { - - /** - * - */ - private static final long serialVersionUID = -7609483136106706196L; - private final JTextArea description; - - InfoViewContentPane() { - description = new JTextArea("", 15, 30); - description.setEditable(false); - description.setLineWrap(true); - description.setWrapStyleWord(true); - setViewportView(description); - } - - public void setNode(InfoTreeNode node) { - setBorder(BorderFactory.createTitledBorder(node.getTitle())); - description.setText(node.getDescription()); - description.setCaretPosition(0); - } - - public void clear() { - setBorder(BorderFactory.createTitledBorder("Description")); - description.setText(""); - } - -} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/KeYFileChooserLoadingOptions.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/KeYFileChooserLoadingOptions.java index c6e35409d7e..73a8a919a25 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/KeYFileChooserLoadingOptions.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/KeYFileChooserLoadingOptions.java @@ -3,21 +3,24 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui; -import java.util.Arrays; -import java.util.Objects; +import java.util.ArrayList; +import java.util.Map; import java.util.ServiceLoader; import javax.swing.*; +import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; +import de.uka.ilkd.key.gui.extension.impl.KeYGuiExtensionFacade; import de.uka.ilkd.key.gui.settings.SettingsPanel; -import de.uka.ilkd.key.proof.init.AbstractProfile; import de.uka.ilkd.key.proof.init.DefaultProfileResolver; import de.uka.ilkd.key.proof.init.Profile; +import de.uka.ilkd.key.settings.Configuration; import net.miginfocom.layout.AC; import net.miginfocom.layout.CC; import net.miginfocom.layout.LC; import net.miginfocom.swing.MigLayout; import org.checkerframework.checker.nullness.qual.Nullable; +import org.jspecify.annotations.NonNull; public class KeYFileChooserLoadingOptions extends JPanel { private final JLabel lblProfile = new JLabel("Profile:"); @@ -39,6 +42,11 @@ public class KeYFileChooserLoadingOptions extends JPanel { Mark this checkbox to only load the selected Java file. """); + private final Map additionalOptionPanels = + KeYGuiExtensionFacade.createAdditionalOptionPanels(); + + + private KeYGuiExtension.@Nullable OptionPanel currentOptionPanel = null; public KeYFileChooserLoadingOptions(KeYFileChooser chooser) { setLayout(new MigLayout(new LC().fillX().wrapAfter(3).maxWidth("400"), @@ -48,16 +56,23 @@ public KeYFileChooserLoadingOptions(KeYFileChooser chooser) { lblProfileInfo.setWrapStyleWord(true); lblProfileInfo.setLineWrap(true); - var items = ServiceLoader.load(DefaultProfileResolver.class) - .stream().map(it -> it.get().getDefaultProfile()) - .map(ProfileWrapper::new) - .toArray(ProfileWrapper[]::new); + var profiles = + new ArrayList<>(ServiceLoader.load(DefaultProfileResolver.class) + .stream().map(it -> it.get().getDefaultProfile()) + .map(ProfileWrapper::new) + .toList()); + + final var legacyMode = new ProfileWrapper("Respect profile given in file", "", + "Usable on KeY file which defines \\profile inside the file. " + + "If no KeY file is loaded, falls back to legacy behavior", + null); + + profiles.addFirst(legacyMode); + + var items = profiles.toArray(ProfileWrapper[]::new); + cboProfile.setModel(new DefaultComboBoxModel<>(items)); - cboProfile.setSelectedItem( - Arrays.stream(items) - .filter(it -> it.profile.equals(AbstractProfile.getDefaultProfile())) - .findFirst() - .orElse(null)); + cboProfile.setSelectedItem(legacyMode); cboProfile.addItemListener(evt -> updateProfileInfo()); updateProfileInfo(); @@ -78,34 +93,56 @@ private void updateProfileInfo() { } private void updateProfileInfo(@Nullable ProfileWrapper selectedItem) { + if (currentOptionPanel != null) { + currentOptionPanel.deinstall(this); + } + if (selectedItem == null) { lblProfileInfo.setText(""); } else { - lblProfileInfo.setText(selectedItem.profile.description()); + lblProfileInfo.setText(selectedItem.description()); + if (additionalOptionPanels.containsKey(selectedItem.profile)) { + currentOptionPanel = additionalOptionPanels.get(selectedItem.profile); + currentOptionPanel.install(this); + } } } public @Nullable Profile getSelectedProfile() { - var selected = getSelectedProfileName(); - var items = ServiceLoader.load(DefaultProfileResolver.class) - .stream().filter(it -> Objects.equals(selected, it.get().getProfileName())) - .findFirst(); - return items.map(it -> it.get().getDefaultProfile()) - .orElse(null); + var selected = (ProfileWrapper) cboProfile.getSelectedItem(); + if (selected == null) { + return null; + } + return selected.profile(); + } + + public @Nullable Configuration getAdditionalProfileOptions() { + if (currentOptionPanel == null) { + return null; + } + return currentOptionPanel.getResult(); } public @Nullable String getSelectedProfileName() { - return ((ProfileWrapper) cboProfile.getSelectedItem()).profile().ident(); + final var selectedItem = (ProfileWrapper) cboProfile.getSelectedItem(); + if (selectedItem == null) + return null; + return selectedItem.ident(); } public boolean isOnlyLoadSingleJavaFile() { return lblSingleJava.isSelected(); } - record ProfileWrapper(Profile profile) { + record ProfileWrapper(String name, String ident, String description, + @Nullable Profile profile) { + ProfileWrapper(Profile profile) { + this(profile.displayName(), profile.ident(), profile.description(), profile); + } + @Override - public String toString() { - return profile.displayName(); + public @NonNull String toString() { + return name; } } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index de53db7ca84..f8b3a672420 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java @@ -56,11 +56,9 @@ import de.uka.ilkd.key.gui.sourceview.SourceViewFrame; import de.uka.ilkd.key.gui.utilities.LruCached; import de.uka.ilkd.key.proof.*; +import de.uka.ilkd.key.proof.init.Profile; import de.uka.ilkd.key.proof.io.ProblemLoader; -import de.uka.ilkd.key.settings.FeatureSettings; -import de.uka.ilkd.key.settings.GeneralSettings; -import de.uka.ilkd.key.settings.ProofIndependentSettings; -import de.uka.ilkd.key.settings.ViewSettings; +import de.uka.ilkd.key.settings.*; import de.uka.ilkd.key.smt.SolverTypeCollection; import de.uka.ilkd.key.smt.solvertypes.SolverType; import de.uka.ilkd.key.ui.AbstractMediatorUserInterfaceControl; @@ -81,6 +79,7 @@ import com.formdev.flatlaf.FlatLightLaf; import com.formdev.flatlaf.util.SystemInfo; import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -326,7 +325,7 @@ private MainWindow() { recentFileMenu = new RecentFileMenu(mediator); proofTreeView = new ProofTreeView(mediator); - infoView = new InfoView(this, mediator); + infoView = new InfoView(mediator); strategySelectionView = new StrategySelectionView(this, mediator); openGoalsView = new GoalList(mediator); @@ -1389,8 +1388,11 @@ public NotificationManager getNotificationManager() { * * @see RecentFileMenu#addRecentFile(String) */ - public void addRecentFile(@NonNull String absolutePath) { - recentFileMenu.addRecentFile(absolutePath); + public void addRecentFile(@NonNull String absolutePath, + @Nullable Profile profile, + boolean singleJava, + @Nullable Configuration additionalOption) { + recentFileMenu.addRecentFile(absolutePath, profile, singleJava, additionalOption); } public void openExamples() { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindowTabbedPane.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindowTabbedPane.java index 5e24a53fe68..28a93432cbc 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindowTabbedPane.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindowTabbedPane.java @@ -32,7 +32,7 @@ public class MainWindowTabbedPane extends JTabbedPane { assert mainWindow != null; proofTreeView = new ProofTreeView(mediator); - InfoView infoView = new InfoView(mainWindow, mediator); + InfoView infoView = new InfoView(mediator); StrategySelectionView strategySelectionView = new StrategySelectionView(mainWindow, mediator); GoalList openGoalsView = new GoalList(mediator); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java index b38d85ef33d..efbacb4917d 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java @@ -3,19 +3,24 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui; -import java.awt.event.ActionListener; -import java.io.*; +import java.awt.event.ActionEvent; +import java.io.File; +import java.io.FileNotFoundException; +import java.io.IOException; import java.nio.file.Files; import java.nio.file.Path; import java.nio.file.Paths; -import java.util.HashMap; -import java.util.LinkedHashMap; -import java.util.Map; -import java.util.stream.Collectors; +import java.util.ArrayList; +import java.util.List; +import java.util.Objects; +import java.util.Optional; import javax.swing.*; import de.uka.ilkd.key.core.KeYMediator; +import de.uka.ilkd.key.gui.actions.KeyAction; import de.uka.ilkd.key.gui.fonticons.IconFactory; +import de.uka.ilkd.key.nparser.ParsingFacade; +import de.uka.ilkd.key.proof.init.Profile; import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.settings.PathConfig; @@ -23,6 +28,8 @@ import org.slf4j.Logger; import org.slf4j.LoggerFactory; +import static de.uka.ilkd.key.gui.actions.QuickSaveAction.QUICK_SAVE_PATH; + /** * This class offers a mechanism to manage recent files; it adds the necessary menu items to a menu * or even can provide that menu itself. also it offers a way to read the recent files from a @@ -40,6 +47,8 @@ public class RecentFileMenu { */ private static final int MAX_RECENT_FILES = 8; + private final KeYMediator mediator; + /** * this is the maximal number of recent files. */ @@ -50,19 +59,10 @@ public class RecentFileMenu { */ private final JMenu menu; - /** - * the actionListener to be notified of mouse-clicks or other actionevents on the menu items - */ - private final ActionListener lissy; - - /** - * recent files, unique by path - */ - private final Map pathToRecentFile = new LinkedHashMap<>(); /** * Mapping from menu item to entry */ - private final HashMap menuItemToRecentFile; + private final List recentFiles = new ArrayList<>(); private RecentFileEntry mostRecentFile; @@ -72,96 +72,75 @@ public class RecentFileMenu { * @param mediator Key mediator */ public RecentFileMenu(final KeYMediator mediator) { + this.mediator = mediator; this.menu = new JMenu("Recent Files"); - this.lissy = e -> { - String absPath = getAbsolutePath((JMenuItem) e.getSource()); - Path file = Paths.get(absPath); - - // special case proof bundles -> allow to select the proof to load - if (ProofSelectionDialog.isProofBundle(file)) { - Path proofPath = ProofSelectionDialog.chooseProofToLoad(file); - if (proofPath == null) { - // canceled by user! - } else { - mediator.getUI().loadProofFromBundle(file, proofPath); - } - } else { - mediator.getUI().loadProblem(file); - } - }; this.maxNumberOfEntries = MAX_RECENT_FILES; - this.menuItemToRecentFile = new LinkedHashMap<>(); - - menu.setEnabled(menu.getItemCount() != 0); + // menu.setEnabled(menu.getItemCount() != 0); menu.setIcon(IconFactory.recentFiles(16)); loadFrom(PathConfig.getRecentFileStorage()); } private void insertFirstEntry(RecentFileEntry entry) { - menu.insert(entry.getMenuItem(), 0); + menu.insert(entry.createMenuItem(), 0); mostRecentFile = entry; } /** * add path to the menu */ - private void addNewToModelAndView(final String path) { + private void addNewToModelAndView(final String path, + @Nullable Profile profile, + boolean singleJava, @Nullable Configuration additionalOption) { // do not add quick save location to recent files - if (de.uka.ilkd.key.gui.actions.QuickSaveAction.QUICK_SAVE_PATH.endsWith(path)) { + if (QUICK_SAVE_PATH.endsWith(path)) { return; } if (new File(path).exists()) { - final RecentFileEntry entry = new RecentFileEntry(path); - pathToRecentFile.put(entry.getAbsolutePath(), entry); + var entry = new RecentFileEntry(path, profile != null ? profile.displayName() : null, + singleJava, additionalOption); // Recalculate unique names - final String[] paths = pathToRecentFile.keySet().toArray(String[]::new); + final String[] paths = + recentFiles.stream().map(RecentFileEntry::getAbsolutePath).toArray(String[]::new); final ShortUniqueFileNames.Name[] names = ShortUniqueFileNames.makeUniqueNames(paths); + // Set the names for (ShortUniqueFileNames.Name name : names) { - pathToRecentFile.get(name.getPath()).setName(name.getName()); + // TODO pathToRecentFile.get(name.getPath()).setName(name.getName()); } - // Insert the menu item - final JMenuItem item = entry.getMenuItem(); - menuItemToRecentFile.put(item, entry); - item.addActionListener(lissy); - insertFirstEntry(entry); } } - /** - * - */ - private String getAbsolutePath(JMenuItem item) { - return menuItemToRecentFile.get(item).getAbsolutePath(); - } - - private void addRecentFileNoSave(final String path) { + private void addRecentFileNoSave(final String path, + @Nullable Profile profile, + boolean singleJava, + @Nullable Configuration additionalOption) { LOGGER.trace("Adding file: {}", path); - final RecentFileEntry existingEntry = pathToRecentFile.get(path); + + Optional existingEntry = recentFiles.stream() + .filter(it -> path.equals(it.getAbsolutePath())).findFirst(); // Add the path to the recentFileList: // check whether this path is already there - if (existingEntry != null) { - menu.remove(existingEntry.getMenuItem()); - insertFirstEntry(existingEntry); + if (existingEntry.isPresent()) { + var entry = existingEntry.get(); + recentFiles.remove(entry); + menu.remove(entry.createMenuItem()); + insertFirstEntry(entry); return; } // if appropriate, remove the last entry. if (menu.getItemCount() == maxNumberOfEntries) { - final JMenuItem item = menu.getItem(menu.getItemCount() - 1); - final RecentFileEntry entry = menuItemToRecentFile.get(item); - menuItemToRecentFile.remove(entry.getMenuItem()); - pathToRecentFile.remove(entry.getAbsolutePath()); - menu.remove(entry.getMenuItem()); + var lastEntry = recentFiles.removeLast(); + menu.remove(lastEntry.createMenuItem()); } - addNewToModelAndView(path); + addNewToModelAndView(path, profile, singleJava, additionalOption); menu.setEnabled(menu.getItemCount() != 0); } @@ -172,9 +151,12 @@ private void addRecentFileNoSave(final String path) { * the end. (set the maximum number with the {@link #setMaxNumberOfEntries(int i)} method). * * @param path the path of the file. + * @param singleJava */ - public void addRecentFile(final String path) { - addRecentFileNoSave(path); + public void addRecentFile(final String path, + @Nullable Profile profile, boolean singleJava, + @Nullable Configuration additionalOption) { + addRecentFileNoSave(path, profile, singleJava, additionalOption); save(); } @@ -204,8 +186,17 @@ public JMenu getMenu() { */ public final void loadFrom(Path filename) { try { - var c = Configuration.load(filename); - c.getStringList("recentFiles").forEach(this::addRecentFileNoSave); + var file = ParsingFacade.parseConfigurationFile(filename); + List recent = file.asConfigurationList(); + this.recentFiles.clear(); + for (var c : recent) { + final var e = new RecentFileEntry(c); + if (mostRecentFile != null) { + mostRecentFile = e; + } + recentFiles.add(e); + menu.add(e.createMenuItem()); + } } catch (FileNotFoundException ex) { LOGGER.debug("Could not read RecentFileList. Did not find file {}", filename); } catch (IOException ioe) { @@ -226,14 +217,11 @@ public String getMostRecent() { * exists) and then re-written so no information will be lost. */ public void store(Path filename) { - Configuration c = new Configuration(); - var seq = menuItemToRecentFile.values().stream() - .map(RecentFileEntry::getAbsolutePath) - .collect(Collectors.toList()); - c.set("recentFiles", seq); - + List config = + recentFiles.stream().map(RecentFileEntry::asConfiguration).toList(); try (var fin = Files.newBufferedWriter(filename)) { - c.save(fin, ""); + var writer = new Configuration.ConfigurationWriter(fin); + writer.printValue(config); } catch (IOException ex) { LOGGER.info("Could not write recent files list ", ex); } @@ -243,37 +231,80 @@ public void save() { store(PathConfig.getRecentFileStorage()); } - private static class RecentFileEntry { - /** - * full path - */ - private final String absolutePath; - /** - * the associated menu item - */ - private final JMenuItem menuItem; - - public RecentFileEntry(String absolutePath) { - this.menuItem = new JMenuItem(); - this.menuItem.setToolTipText(absolutePath); - this.absolutePath = absolutePath; + public class RecentFileEntry { + public static final String KEY_PATH = "path"; + public static final String KEY_PROFILE = "profile"; + public static final String KEY_OPTIONS = "options"; + private static final String KEY_LOAD_SINGLE_JAVA = "singleJava"; + + private @Nullable JMenuItem menuItem; + + private final String path; + private final @Nullable String profile; + private final boolean singleJava; + private final @Nullable Configuration additionalOption; + + public RecentFileEntry(String path, @Nullable String profile, boolean singleJava, + @Nullable Configuration additionalOption) { + this.additionalOption = additionalOption; + this.path = path; + this.profile = profile; + this.singleJava = singleJava; } - public String getAbsolutePath() { - return absolutePath; + public RecentFileEntry(Configuration options) { + this(Objects.requireNonNull(options.getString(KEY_PATH)), + options.getString(KEY_PROFILE), + options.getBool(KEY_LOAD_SINGLE_JAVA, false), + options.getTable(KEY_OPTIONS)); } - public void setName(String name) { - this.menuItem.setText(name); + public Configuration asConfiguration() { + Configuration config = new Configuration(); + config.set(KEY_PATH, path); + config.set(KEY_PROFILE, profile); + config.set(KEY_LOAD_SINGLE_JAVA, singleJava); + config.set(KEY_OPTIONS, additionalOption); + return config; } - public JMenuItem getMenuItem() { + public String getAbsolutePath() { + return path; + } + + public JMenuItem createMenuItem() { + if (menuItem == null) { + menuItem = new JMenuItem(new RecentFileAction(this)); + } return menuItem; } + } + + private class RecentFileAction extends KeyAction { + private final RecentFileEntry recentFileEntry; + + public RecentFileAction(RecentFileEntry recentFileEntry) { + this.recentFileEntry = recentFileEntry; + setName(recentFileEntry.getAbsolutePath()); + setTooltip(recentFileEntry.getAbsolutePath()); + } @Override - public String toString() { - return absolutePath; + public void actionPerformed(ActionEvent actionEvent) { + String absPath = recentFileEntry.getAbsolutePath(); + Path file = Paths.get(absPath); + + // special case proof bundles -> allow to select the proof to load + if (ProofSelectionDialog.isProofBundle(file)) { + Path proofPath = ProofSelectionDialog.chooseProofToLoad(file); + if (proofPath == null) { + // canceled by user! + } else { + mediator.getUI().loadProofFromBundle(file, proofPath); + } + } else { + mediator.getUI().loadProblem(file); + } } } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java index 3b530ba32c0..ab44f1001cf 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java @@ -97,9 +97,12 @@ public boolean isAutoModeSupported(Proof proof) { public void loadProblem(Path file, Consumer configure) { - mainWindow.addRecentFile(file.toAbsolutePath().toString()); ProblemLoader problemLoader = getProblemLoader(file, null, null, null, getMediator()); configure.accept(problemLoader); + mainWindow.addRecentFile(file.toAbsolutePath().toString(), + problemLoader.getProfileOfNewProofs(), + problemLoader.isLoadSingleJavaFile(), + problemLoader.getAdditionalProfileOptions()); problemLoader.runAsynchronously(); } @@ -112,16 +115,14 @@ public void loadProblem(Path file, Consumer configure) { */ public void loadProblem(Path file, @Nullable List classPath, @Nullable Path bootClassPath, @Nullable List includes) { - mainWindow.addRecentFile(file.toAbsolutePath().toString()); + mainWindow.addRecentFile(file.toAbsolutePath().toString(), null, false, null); ProblemLoader problemLoader = getProblemLoader(file, classPath, bootClassPath, includes, getMediator()); problemLoader.runAsynchronously(); } public void loadProblem(Path file, Profile profile) { - loadProblem(file, (pl) -> { - pl.setProfileOfNewProofs(profile); - }); + loadProblem(file, (pl) -> pl.setProfileOfNewProofs(profile)); } @Override @@ -131,7 +132,7 @@ public void loadProblem(Path file) { @Override public void loadProofFromBundle(Path proofBundle, Path proofFilename) { - mainWindow.addRecentFile(proofBundle.toAbsolutePath().toString()); + mainWindow.addRecentFile(proofBundle.toAbsolutePath().toString(), null, false, null); ProblemLoader problemLoader = getProblemLoader(proofBundle, null, null, null, getMediator()); problemLoader.setProofPath(proofFilename); @@ -369,7 +370,8 @@ public AbstractProblemLoader load(Profile profile, Path file, List classPa boolean forceNewProfileOfNewProofs, Consumer callback) throws ProblemLoaderException { if (file != null) { - mainWindow.getRecentFiles().addRecentFile(file.toAbsolutePath().toString()); + mainWindow.getRecentFiles().addRecentFile(file.toAbsolutePath().toString(), profile, + false, null); } try { getMediator().stopInterface(true); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenFileAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenFileAction.java index c0682f40938..aa2393717b2 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenFileAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenFileAction.java @@ -10,6 +10,7 @@ import de.uka.ilkd.key.core.Main; import de.uka.ilkd.key.gui.KeYFileChooser; +import de.uka.ilkd.key.gui.KeYFileChooserLoadingOptions; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.ProofSelectionDialog; import de.uka.ilkd.key.gui.fonticons.IconFactory; @@ -29,7 +30,7 @@ public OpenFileAction(MainWindow mainWindow) { public void actionPerformed(ActionEvent e) { KeYFileChooser fc = new KeYFileChooser(lastSelectedPath); fc.setDialogTitle("Select file to load proof or problem"); - var options = fc.addLoadingOptions(); + KeYFileChooserLoadingOptions options = fc.addLoadingOptions(); fc.addBookmarkPanel(); fc.prepare(); fc.setFileFilter(KeYFileChooser.DEFAULT_FILTER); @@ -64,9 +65,11 @@ public void actionPerformed(ActionEvent e) { } var selectedProfile = options.getSelectedProfile(); + var additionalProfileOptions = options.getAdditionalProfileOptions(); mainWindow.loadProblem(file, pl -> { if (selectedProfile != null) { pl.setProfileOfNewProofs(selectedProfile); + pl.setAdditionalProfileOptions(additionalProfileOptions); } pl.setLoadSingleJavaFile(options.isOnlyLoadSingleJavaFile()); }); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenSingleJavaFileAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenSingleJavaFileAction.java index c97ab4b2aed..4206b2da39f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenSingleJavaFileAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenSingleJavaFileAction.java @@ -39,7 +39,8 @@ public void actionPerformed(ActionEvent e) { if (result == JFileChooser.APPROVE_OPTION) { Path file = fc.getSelectedFile().toPath(); - mainWindow.addRecentFile(file.toAbsolutePath().toString()); + mainWindow.addRecentFile(file.toAbsolutePath().toString(), + null, true, null); WindowUserInterfaceControl ui = mainWindow.getUserInterface(); ProblemLoader pl = ui.getProblemLoader(file, Collections.emptyList(), null, diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java index ef94d9dc7df..2f19c8534dc 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java @@ -7,23 +7,24 @@ import java.lang.annotation.RetentionPolicy; import java.util.Collection; import java.util.List; +import java.util.function.Supplier; import javax.swing.Action; import javax.swing.JComponent; import javax.swing.JMenu; import javax.swing.JToolBar; import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.gui.GoalList; -import de.uka.ilkd.key.gui.InfoView; -import de.uka.ilkd.key.gui.MainWindow; -import de.uka.ilkd.key.gui.StrategySelectionView; +import de.uka.ilkd.key.gui.*; import de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager; import de.uka.ilkd.key.gui.nodeviews.SequentView; import de.uka.ilkd.key.gui.prooftree.ProofTreeView; import de.uka.ilkd.key.gui.settings.SettingsProvider; import de.uka.ilkd.key.gui.sourceview.SourceView; import de.uka.ilkd.key.pp.PosInSequent; +import de.uka.ilkd.key.proof.init.Profile; +import de.uka.ilkd.key.settings.Configuration; +import org.checkerframework.checker.nullness.qual.Nullable; import org.jspecify.annotations.NonNull; /** @@ -272,4 +273,43 @@ default int getTermLabelPriority() { return 0; } } + + /// A {@link LoadOptionPanel} provides additional UI components in the file selection dialog + /// dependent on the selected profile. + /// + /// Implementing this interface requires to provide an {@link OptionPanel}, and associated + /// {@link Profile}. + /// + /// @author weigl + interface LoadOptionPanel extends Supplier { + Profile getProfile(); + } + + /// A provider of UI components for additional options w.r.t. specific profiles. + /// **Lifecycle:** For each {@link Profile} an {@link OptionPanel} is constructed, when the + /// {@link KeYFileChooser} + /// is instantiated. *On selected of a profile*, the current {@link OptionPanel} is + /// `deinstall`ed, and the + /// {@link OptionPanel} for the selected profile is `install`ed. + /// + /// @author weigl + /// @see KeYFileChooserLoadingOptions + interface OptionPanel { + /// Installs the UI components in the given {@link KeYFileChooserLoadingOptions} instance. + /// UI components + /// can be reused, to keep the temporary state. + /// {@link KeYFileChooserLoadingOptions} uses the {@link net.miginfocom.swing.MigLayout} to + /// manage the layout. + void install(KeYFileChooserLoadingOptions panel); + + /// Removes all *installed* UI components from the panel. + void deinstall(KeYFileChooserLoadingOptions panel); + + /// Returning an arbitrary object, representing the selected option in the UI components. + /// The object needs to compatible with the assigned profile in {@link LoadOptionPanel}. + /// + /// @see Profile#prepareInitConfig(InitConfig, Object) + @Nullable + Configuration getResult(); + } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java index 199a32b428d..ee19c119022 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java @@ -17,9 +17,12 @@ import de.uka.ilkd.key.gui.actions.KeyAction; import de.uka.ilkd.key.gui.extension.api.ContextMenuKind; import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; +import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension.LoadOptionPanel; +import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension.OptionPanel; import de.uka.ilkd.key.gui.extension.api.TabPanel; import de.uka.ilkd.key.pp.PosInSequent; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.init.Profile; /** * Facade for retrieving the GUI extensions. @@ -403,6 +406,19 @@ public static Stream getTermInfoStrings(MainWindow mainWindow, PosInSequ .flatMap(it -> it.getTermInfoStrings(mainWindow, mousePos).stream()); } + /** + * Helper methods that finds matches {@link Profile} and {@link OptionPanel} together. + * This information are provided by {@link LoadOptionPanel} interface. + */ + public static Map createAdditionalOptionPanels() { + List items = getExtensionInstances(LoadOptionPanel.class); + HashMap map = HashMap.newHashMap(4); + for (LoadOptionPanel item : items) { + map.put(item.getProfile(), item.get()); + } + return map; + } + /** * Disables the clazz from further loading. *

diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/InnerNodeView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/InnerNodeView.java index 2ea3152d913..1166fe79f2b 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/InnerNodeView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/InnerNodeView.java @@ -15,6 +15,7 @@ import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.colors.ColorSettings; +import de.uka.ilkd.key.gui.utilities.LexerHighlighter; import de.uka.ilkd.key.pp.*; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; @@ -56,7 +57,7 @@ public final class InnerNodeView extends SequentView implements ProofDisposedLis private final InnerNodeViewListener listener; - private JTextArea tacletInfo = new JTextArea(); + private JTextPane tacletInfo = new JTextPane(); private Node node; private final RuleApp ruleApp; @@ -244,9 +245,13 @@ public synchronized void printSequent() { } private void updateTacletInfo() { - tacletInfo.setText( + final var tacletDescription = TacletDescriber.getTacletDescription(getMainWindow().getMediator(), ruleApp, - getLineWidth())); + getLineWidth()); + tacletInfo.setText(tacletDescription); + LexerHighlighter lh = new LexerHighlighter.KeYLexerHighlighter(); + lh.highlightPaneAll(tacletInfo, tacletDescription.indexOf('\n'), -1); + tacletInfo.setBackground(getBackground()); tacletInfo.setBorder(new CompoundBorder(new MatteBorder(3, 0, 0, 0, Color.black), new EmptyBorder(new Insets(4, 0, 0, 0)))); @@ -260,7 +265,7 @@ public void makeTacletInfoVisible(boolean visible) { tacletInfo.setVisible(visible); } - public JTextArea getTacletInfo() { + public JTextPane getTacletInfo() { return tacletInfo; } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java index 009a53a28de..2e65f9fe9e5 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java @@ -153,14 +153,21 @@ private void loadProof(Proof selectedProof) throws RuntimeException { lblStatus.setText("Javac runs"); lblStatus.setIcon(ICON_WAIT.get(16)); - CompletableFuture> task = - JavaCompilerCheckFacade.check(mediator.getUI(), bootClassPath, classpath, javaPath); + try { - task.thenAccept(it -> SwingUtilities.invokeLater(() -> { - lblStatus.setText("Javac finished"); - data.issues = it; - updateLabel(data); - })).get(); + try { + CompletableFuture> task = + JavaCompilerCheckFacade.check(mediator.getUI(), bootClassPath, classpath, + javaPath); + + task.thenAccept(it -> SwingUtilities.invokeLater(() -> { + lblStatus.setText("Javac finished"); + data.issues = it; + updateLabel(data); + })).get(); + } catch (IllegalArgumentException iae) { + LOGGER.error("Javac check failed {}", iae.getMessage()); + } } catch (InterruptedException | ExecutionException ex) { throw new RuntimeException(ex); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/profileloading/WDLoadDialogOptionPanel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/profileloading/WDLoadDialogOptionPanel.java new file mode 100644 index 00000000000..5504aef26b4 --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/profileloading/WDLoadDialogOptionPanel.java @@ -0,0 +1,118 @@ +/* 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.gui.profileloading; + +import java.awt.*; +import javax.swing.*; + +import de.uka.ilkd.key.gui.KeYFileChooserLoadingOptions; +import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; +import de.uka.ilkd.key.proof.init.Profile; +import de.uka.ilkd.key.settings.Configuration; +import de.uka.ilkd.key.wd.WdProfile; + +import net.miginfocom.layout.CC; +import org.checkerframework.checker.nullness.qual.Nullable; + +/// Additional UI components for the selection of the WD semantics. +/// +/// @author weigl +@KeYGuiExtension.Info(experimental = false) +public class WDLoadDialogOptionPanel implements KeYGuiExtension, KeYGuiExtension.LoadOptionPanel { + @Override + public OptionPanel get() { + return new WDLoadDialogOptionPanelImpl(); + } + + @Override + public Profile getProfile() { + return WdProfile.INSTANCE; + } + + public static class WDLoadDialogOptionPanelImpl implements OptionPanel { + private final JRadioButton rdbWDL = new JRadioButton("L"); + private final JRadioButton rdbWDY = new JRadioButton("Y"); + private final JRadioButton rdbWDD = new JRadioButton("D"); + + private final JLabel lblHeader = new JLabel("WD options"); + private final JLabel lblSemantics = new JLabel("Semantics:"); + private final JSeparator sepHeader = new JSeparator(); + + private static final String DESCRIPTION_L_WD_SEMANTIC = """ + More intuitive for software developers and along the lines of + runtime assertion semantics. Well-Definedness checks will be + stricter using this operator, since the order of terms/formulas + matters. It is based on McCarthy logic. + Cf. "Are the Logical Foundations of Verifying Compiler + Prototypes Matching User Expectations?" by Patrice Chalin. + """; + + private static final String DESCRIPTION_D_WD_SEMANTIC = """ + Complete and along the lines of classical logic, where the + order of terms/formulas is irrelevant. This operator is + equivalent to the D-operator, but more efficient. + Cf. "Efficient Well-Definedness Checking" by Ádám Darvas, + Farhad Mehta, and Arsenii Rudich. + """; + + + private static final String DESCRIPTION_Y_WD_SEMANTIC = """ + Complete and along the lines of classical logic, where the + order of terms/formulas is irrelevant. This operator is not as + strict as the L-operator, based on strong Kleene logic. To be + used with care, since formulas may blow up exponentially. + Cf. "Well Defined B" by Patrick Behm, Lilian Burdy, and + Jean-Marc Meynadier + """; + + public WDLoadDialogOptionPanelImpl() { + lblHeader.setFont(lblHeader.getFont().deriveFont(Font.BOLD)); + + rdbWDL.setToolTipText(DESCRIPTION_L_WD_SEMANTIC); + rdbWDD.setToolTipText(DESCRIPTION_D_WD_SEMANTIC); + rdbWDY.setToolTipText(DESCRIPTION_Y_WD_SEMANTIC); + + ButtonGroup btnGrp = new ButtonGroup(); + btnGrp.add(rdbWDD); + btnGrp.add(rdbWDL); + btnGrp.add(rdbWDY); + + rdbWDL.setSelected(true); + } + + @Override + public void install(KeYFileChooserLoadingOptions panel) { + panel.add(lblHeader); + panel.add(sepHeader, new CC().wrap().span(2).growX()); + + panel.add(lblSemantics); + panel.add(rdbWDD, new CC().span(2).split(3)); + panel.add(rdbWDY); + panel.add(rdbWDL); + } + + @Override + public void deinstall(KeYFileChooserLoadingOptions panel) { + panel.remove(lblHeader); + panel.remove(sepHeader); + panel.remove(lblSemantics); + panel.remove(rdbWDL); + panel.remove(rdbWDD); + panel.remove(rdbWDY); + } + + @Override + public @Nullable Configuration getResult() { + Configuration configuration = new Configuration(); + configuration.set("wdOperator", "wdOperator:L"); + if (rdbWDD.isSelected()) { + configuration.set("wdOperator", "wdOperator:D"); + } + if (rdbWDY.isSelected()) { + configuration.set("wdOperator", "wdOperator:Y"); + } + return configuration; + } + } +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/LexerHighlighter.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/LexerHighlighter.java new file mode 100644 index 00000000000..5a3c0ea6b15 --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/LexerHighlighter.java @@ -0,0 +1,189 @@ +/* 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.gui.utilities; + +import java.awt.*; +import java.util.regex.Matcher; +import java.util.regex.Pattern; +import javax.swing.*; +import javax.swing.text.*; + +import de.uka.ilkd.key.gui.colors.ColorSettings; +import de.uka.ilkd.key.nparser.ParsingFacade; + +import org.antlr.v4.runtime.CharStreams; +import org.antlr.v4.runtime.Token; +import org.jspecify.annotations.NullMarked; +import org.jspecify.annotations.Nullable; + +import static de.uka.ilkd.key.nparser.KeYLexer.*; + +/** + * Utilities for highlighting of text based on ANTLR-based Lexers. + * + * @author Alexander Weigl + * @version 1 (2/17/26) + */ +@NullMarked +public abstract class LexerHighlighter { + protected abstract @Nullable AttributeSet getStyle(int tokenType); + + private final StyleContext styleContext = new StyleContext(); + + protected AttributeSet define(Color fgColor, boolean bold, boolean italic) { + AttributeSet aset = + styleContext.addAttribute(SimpleAttributeSet.EMPTY, StyleConstants.Foreground, fgColor); + aset = styleContext.addAttribute(aset, StyleConstants.FontFamily, Font.MONOSPACED); + aset = styleContext.addAttribute(aset, StyleConstants.Bold, bold); + aset = styleContext.addAttribute(aset, StyleConstants.Italic, italic); + return aset; + } + + public final void highlightPaneMarkdown(JTextPane contentPane) { + String text = contentPane.getText(); + Pattern pattern = getMarkdownPattern(); + + Matcher match = pattern.matcher(text); + var sd = contentPane.getStyledDocument(); + + while (match.find()) { + var lexer = ParsingFacade.createLexer(CharStreams.fromString(match.group(1))); + var toks = lexer.getAllTokens(); + int startIdx = match.start() + "```key".length(); + for (var tok : toks) { + highlightToken(sd, startIdx, tok); + } + } + contentPane.invalidate(); + contentPane.repaint(); + contentPane.repaint(); + } + + public final void highlightPaneAll(JTextPane contentPane, int startIdx, int stopIdx) { + String text = contentPane.getText(); + + if (stopIdx < 0) { + stopIdx = text.length(); + } + + text = text.substring(startIdx, stopIdx); + + var sd = contentPane.getStyledDocument(); + var lexer = ParsingFacade.createLexer(CharStreams.fromString(text)); + var toks = lexer.getAllTokens(); + for (var tok : toks) { + highlightToken(sd, startIdx, tok); + } + contentPane.invalidate(); + contentPane.repaint(); + contentPane.repaint(); + } + + public final void highlightPaneAll(JTextPane contentPane) { + highlightPaneAll(contentPane, 0, -1); + } + + + private void highlightToken(StyledDocument sd, int startIdx, Token tok) { + var attribute = getStyle(tok.getType()); + sd.setCharacterAttributes(startIdx + tok.getStartIndex(), + 1 + tok.getStopIndex() - tok.getStartIndex(), + attribute, true); + } + + protected abstract Pattern getMarkdownPattern(); + + public static class KeYLexerHighlighter extends LexerHighlighter { + public static final ColorSettings.ColorProperty COLOR_KEYWORD = + ColorSettings.define("syntax.keyword", "", Color.BLUE, Color.ORANGE); + + public static final ColorSettings.ColorProperty COLOR_IDENTIFIER = + ColorSettings.define("syntax.identifier", "", Color.BLACK, Color.WHITE); + + public static final ColorSettings.ColorProperty COLOR_COMMENT = + ColorSettings.define("syntax.comment", "", Color.GREEN, Color.GREEN); + + public static final ColorSettings.ColorProperty COLOR_OPERATORS = + ColorSettings.define("syntax.operators", "", Color.BLACK, Color.ORANGE); + + public static final ColorSettings.ColorProperty COLOR_ERROR = + ColorSettings.define("syntax.error", "", Color.RED, Color.WHITE); + + public static final ColorSettings.ColorProperty COLOR_LITERALS = + ColorSettings.define("syntax.literals", "", Color.GREEN, Color.GREEN); + + + private final AttributeSet STYLE_OPERATORS = define(COLOR_OPERATORS.get(), false, false); + private final AttributeSet STYLE_ERROR = define(COLOR_ERROR.get(), false, false); + private final AttributeSet STYLE_LITERALS = define(COLOR_LITERALS.get(), false, true); + private final AttributeSet STYLE_KEYWORDS = define(COLOR_KEYWORD.get(), true, false); + private final AttributeSet STYLE_IDENTIFIER = define(COLOR_IDENTIFIER.get(), true, false); + private final AttributeSet STYLE_COMMENT = define(COLOR_COMMENT.get(), false, true); + private final AttributeSet STYLE_DEFAULT = define(COLOR_IDENTIFIER.get(), false, false); + + private final Pattern MARKDOWN = Pattern.compile("```key(.*?)```", + Pattern.MULTILINE | Pattern.DOTALL | Pattern.CASE_INSENSITIVE); + + @Override + protected @Nullable AttributeSet getStyle(int tokType) { + return switch (tokType) { + case TERMLABEL, MODIFIABLE, PROGRAMVARIABLES, STORE_TERM_IN, STORE_STMT_IN, + HAS_INVARIANT, GET_INVARIANT, GET_FREE_INVARIANT, GET_VARIANT, + IS_LABELED, SAME_OBSERVER, VARCOND, APPLY_UPDATE_ON_RIGID, + DEPENDINGON, DISJOINTMODULONULL, DROP_EFFECTLESS_ELEMENTARIES, + DROP_EFFECTLESS_STORES, SIMPLIFY_IF_THEN_ELSE_UPDATE, ENUM_CONST, + FREELABELIN, HASSORT, FIELDTYPE, FINAL, ELEMSORT, HASLABEL, + HASSUBFORMULAS, ISARRAY, ISARRAYLENGTH, ISCONSTANT, ISENUMTYPE, + ISINDUCTVAR, ISLOCALVARIABLE, ISOBSERVER, DIFFERENT, METADISJOINT, + ISTHISREFERENCE, DIFFERENTFIELDS, ISREFERENCE, ISREFERENCEARRAY, + ISSTATICFIELD, ISMODELFIELD, ISINSTRICTFP, ISSUBTYPE, EQUAL_UNIQUE, + NEW, NEW_TYPE_OF, NEW_DEPENDING_ON, NEW_LOCAL_VARS, HAS_ELEMENTARY_SORT, + NEWLABEL, CONTAINS_ASSIGNMENT, NOT_, NOTFREEIN, SAME, STATIC, + STATICMETHODREFERENCE, MAXEXPANDMETHOD, STRICT, TYPEOF, INSTANTIATE_GENERIC, + FORALL, EXISTS, SUBST, IF, IFEX, THEN, ELSE, INCLUDE, + INCLUDELDTS, CLASSPATH, BOOTCLASSPATH, NODEFAULTCLASSES, JAVASOURCE, + WITHOPTIONS, OPTIONSDECL, KEYSETTINGS, PROFILE, + SAMEUPDATELEVEL, INSEQUENTSTATE, ANTECEDENTPOLARITY, SUCCEDENTPOLARITY, + CLOSEGOAL, HEURISTICSDECL, NONINTERACTIVE, DISPLAYNAME, + HELPTEXT, REPLACEWITH, ADDRULES, ADDPROGVARS, HEURISTICS, + FIND, ADD, ASSUMES, TRIGGER, AVOID, PREDICATES, + FUNCTIONS, DATATYPES, TRANSFORMERS, UNIQUE, FREE, + RULES, AXIOMS, PROBLEM, CHOOSECONTRACT, PROOFOBLIGATION, + PROOF, PROOFSCRIPT, CONTRACTS, INVARIANTS, LEMMA, + IN_TYPE, IS_ABSTRACT_OR_INTERFACE, IS_FINAL, CONTAINERTYPE, + SCHEMAVAR, FORMULA, + COMMENT_END, DOC_COMMENT, ML_COMMENT, MODALITYD, MODALITYB, + MODALITYBB, MODAILITYGENERIC1, MODAILITYGENERIC2, MODAILITYGENERIC3, + MODAILITYGENERIC4, MODAILITYGENERIC5, MODAILITYGENERIC6, MODAILITYGENERIC7, + MODALITYD_END, MODALITYD_STRING, MODALITYD_CHAR, MODALITYG_END, + MODALITYB_END, MODALITYBB_END -> + STYLE_KEYWORDS; + + case AT, PARALLEL, OR, AND, NOT, IMP, + EQUALS, NOT_EQUALS, SEQARROW, EXP, TILDE, PERCENT, + STAR, MINUS, PLUS, GREATER, GREATEREQUAL, + LESS, LESSEQUAL, LGUILLEMETS, RGUILLEMETS, EQV, + UTF_PRECEDES, UTF_IN, UTF_EMPTY, UTF_UNION, UTF_INTERSECT, + UTF_SUBSET_EQ, UTF_SUBSEQ, UTF_SETMINUS, SEMI, SLASH, + COLON, DOUBLECOLON, ASSIGN, DOT, DOTRANGE, COMMA, + LPAREN, RPAREN, LBRACE, RBRACE, LBRACKET, RBRACKET, + EMPTYBRACKETS -> + STYLE_OPERATORS; + case ERROR_UKNOWN_ESCAPE, ERROR_CHAR -> STYLE_ERROR; + case IDENT -> STYLE_IDENTIFIER; + case COMMENT, SL_COMMENT -> STYLE_COMMENT; + case CHAR_LITERAL, QUOTED_STRING_LITERAL, TRUE, FALSE, + STRING_LITERAL, BIN_LITERAL, HEX_LITERAL, INT_LITERAL, FLOAT_LITERAL, + DOUBLE_LITERAL, REAL_LITERAL -> + STYLE_LITERALS; + default -> STYLE_DEFAULT; + }; + } + + @Override + protected Pattern getMarkdownPattern() { + return MARKDOWN; + } + } +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/util/XMLResources.java b/key.ui/src/main/java/de/uka/ilkd/key/util/XMLResources.java deleted file mode 100644 index 3c50b745530..00000000000 --- a/key.ui/src/main/java/de/uka/ilkd/key/util/XMLResources.java +++ /dev/null @@ -1,66 +0,0 @@ -/* 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.util; - -import java.io.FileNotFoundException; -import java.io.IOException; -import java.io.InputStream; -import java.util.Properties; - -import org.slf4j.Logger; -import org.slf4j.LoggerFactory; - -/** - * An instance of this class loads several XML files, whose contents are displayed in - * {@link de.uka.ilkd.key.gui.InfoView}. - * - * @author Kai Wallisch - */ -public class XMLResources { - - private static final String RULE_RESOURCE = "/de/uka/ilkd/key/gui/help/ruleExplanations.xml"; - private static final Logger LOGGER = LoggerFactory.getLogger(XMLResources.class); - protected final Properties ruleExplanations; - - private static final String LABEL_RESOURCE = - "/de/uka/ilkd/key/gui/help/termLabelExplanations.xml"; - protected final Properties termLabelExplanations; - - static final String FUNCTION_RESOURCE = "/de/uka/ilkd/key/gui/help/functionExplanations.xml"; - protected final Properties functionExplanations; - - public XMLResources() { - ruleExplanations = getResource(RULE_RESOURCE); - termLabelExplanations = getResource(LABEL_RESOURCE); - functionExplanations = getResource(FUNCTION_RESOURCE); - } - - public Properties getRuleExplanations() { - return ruleExplanations; - } - - public Properties getTermLabelExplanations() { - return termLabelExplanations; - } - - public Properties getFunctionExplanations() { - return functionExplanations; - } - - private static Properties getResource(String xmlFile) { - Properties ret = new Properties(); - - try (InputStream is = XMLResources.class.getResourceAsStream(xmlFile)) { - if (is == null) { - throw new FileNotFoundException("Descriptions file " + xmlFile + " not found."); - } - ret.loadFromXML(is); - } catch (IOException e) { - LOGGER.error("Cannot not load help messages in info view", e); - } - - return ret; - } - -} diff --git a/key.ui/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension b/key.ui/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension index 3906585323c..646d2f4c102 100644 --- a/key.ui/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension +++ b/key.ui/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension @@ -6,7 +6,7 @@ de.uka.ilkd.key.gui.KeyboardTacletExtension de.uka.ilkd.key.gui.nodeviews.ShowHashcodesExtension de.uka.ilkd.key.gui.LogView de.uka.ilkd.key.gui.plugins.javac.JavacExtension -de.uka.ilkd.key.gui.plugins.caching.CachingExtension de.uka.ilkd.key.gui.utilities.HeapStatusExt de.uka.ilkd.key.gui.JmlEnabledKeysIndicator -de.uka.ilkd.key.gui.extension.impl.ProfileNameInStatusBar \ No newline at end of file +de.uka.ilkd.key.gui.extension.impl.ProfileNameInStatusBar +de.uka.ilkd.key.gui.profileloading.WDLoadDialogOptionPanel \ No newline at end of file diff --git a/key.ui/src/main/resources/de/uka/ilkd/key/gui/help/functionExplanations.xml b/key.ui/src/main/resources/de/uka/ilkd/key/gui/help/functionExplanations.xml deleted file mode 100644 index abf9f4d10d4..00000000000 --- a/key.ui/src/main/resources/de/uka/ilkd/key/gui/help/functionExplanations.xml +++ /dev/null @@ -1,181 +0,0 @@ - - - - - - Put descriptions for JavaDL function and predicate symbols in here. - - -The length of an array is not stored on the heap but is an inherent property of the object reference which denotes the array. -Hence, this functions takes only one argument: the object reference whose length (as an array) is to be retrieved. -This function always results in a non-negative value. - -This predicate is true if the described array update is valid in Java. - -Java has the peculiarity of covariant array types. They allow an array assignment to fail at runtime (with an ArrayStoreException). This predicate deals with the issue in the logic. - -(tbd) - - -This function turns an integer into a field reference. - -Integers are used to access the entries of entries within arrays stored on the heap. This function provides the injection of the integer domain into that of the type Field. It is ensured that this image of arr is disjoint from any defined field constant. - -The array access a[i], for instance for an int-array a, becomes int::select(heap, a, arr(i)). - -tbd -tbd -tbd -tbd -tbd -tbd -tbd -tbd - -This program variable holds to the current heap state. Its type is Heap. Any assignment statement in a modality modifies the value of this program variable and any expression reading from the heap within a Java modality refers to the heap stored in this program variable. - -This predicate takes an argument of type Heap. It is true if the following conditions hold for its the argument: -1. Every location contains a reference to a created (in this heap) object or null. -2. Every location set stored on the heap contains only created objects. -3. Every location belonging to a declared Java field holds a value compatible with its type. -4. Only finitely many objects are created on the heap. - -This function modifies a heap by changing the value in one location. -It takes four arguments: -1. The heap h which is to be modified -2. The object o reference of the location which is to be modified -3. The field of the location which is to be modified -4. The value v which is to be written in the designated location. -The result is a heap which coincides with h in all locations but in (o,f), where v is stored. -In the theory of arrays, store is somtimes called "write". -The field java.lang.Object::<created> cannot be updated using store; use "create". - -This function modifies a heap by changing the createdness of one object. -It takes two arguments: -1. The heap h which is to be modified -2. The object reference o for the object which is to be set created. -The result is a heap which coincides with h in all locations but in (o,java.lang.Object::<created>), which has been set to true. -There is no means to modify a heap by setting the createdness of an object to false. - -tbd - -This function modifies a heap by changing the value in one location. -It takes three arguments: -1. The heap h which is to be modified -2. The location set s whose locations are to be modified -4. The value v which is to be written in the designated locations. -The result is a heap which coincides with h in all locations but in the locations in s where v is stored. -The field java.lang.Object::<created> cannot be updated using memset; use "create". - -tbd - -The empty location set which does not contain any elements. - -The unique location set containing all locations, i.e. elementOf(o, f, allLocs) will always return true for an arbitrary Field f and Object o. - -Converts a single location to a locations set with one element. - -Union between two location sets. - -Intersection between two location sets. - -Realizes relative complement (a.k.a. set difference) between two locations sets. It takes as arguments two location sets and returns another location set which contains all elements from the first argument except those that are elements of the second argument. - -Takes as argument a term of type LocSet, which may contain a free variable. The term represents a family of locations sets, which is parameterized by the unbound variable. The returned location set is the union over all members of the parameterized family. - -The set that contains all locations which belong to the object o given as argument. - -A location (a,b) is in the set allFields(o) iff a=o. -In JML, the function corresponds to o.*. - -The set of all locations that belong to a particular field f given as argument. - -A location (a,b) is in the set allObjects(f) iff b=f. - -tbd - -The set of locations which are fresh (that is not created) w.r.t. the heap h given as argument. -A location (a,b) is in the set freshLocs(h) iff o.<created>@h = FALSE. - -tbd - -tbd - -This is the set theoretic membership predicate to be used for location sets. - -It takes three arguments: The first two (an Object and a Field) make up the location and the third is the location set against which membership is tested. - -This is the set theoretic subset predicate to be used for location sets. - -A location set A is subset of another location set B iff every element of A is also element of B. - -This binary predicate models disjointness of location sets. - -disjoint(A,B) is true iff A and B have an empty intersection, -it is thus equivalent to intersect(A,B) = empty. - -tbd - -Retrieve the mapping value of a key. -A unique value, which is returned by mapGet in case no mapping value is declared for the specified key. -Generalized quantifier for maps. This is a generic constructor for maps. -The empty map, which does not contain any entries. -A map, which contains only one entry. -Takes as arguments two maps and creates a new map from their entries. In case their domains overlap, entries of the second map are used for keys from the intersection. -Converts a sequence to a map. The map domain consists of exactly those integers, which are inside the sequence bounds. -Adds an entry to a map or overwrites an existing one. -Removes an entry from a map. -Returns the number of entries of a map. -Returns true iff the specified map contains a finite amount of entries. -Takes two arguments: key ∈ any and map ∈ Map. Returns true iff key is in the domain of map. -Returns true iff the domain of the specified map contains only objects that are <created> in the implicit heap (additional non-object values may also be part of the domain). This can be used in a JML specification as an invariant to ensure, that non-created objects are not (yet) part of the domain of a map. - -Return the length of a sequence. -Return the element at a position within a sequence. The type read from the sequence is part of the function name. -Return the first index in a sequence that holds a value. -The underspecified error value if a sequence is accessed outside its idnex range. -The empty sequence. -A singleton sequence that has the argument as only entry. -Concatenates two sequences. -Takes a subsequence from a sequence. -The first argument is the original sequence, -the second is the first index to consider (inclusive) and -the third is the last index to consider (!exclusive!). - -Reverses a sequence. The result has the same entries as the argument but in reverse order. -This function binds an integer variable and evaluates an expression over this variable for a range of values to obtain the entries of a sequence. - -The sequence - seqDef{int i;}(-2, 3, i*i) -has, for instance, the entries - [ 4, 1, 0, 1, 4 ]. - -The first and second argument give the range over which the variable goes. Again, the right-hand bound is exclusive. - -seqDef is related to the lambda operator in lambda calculus. - - -Takes a sequence and two indices. The elements at the specified indices are exchanged in the resulting sequence. In case one of the indices is out of bounds, the sequence is left unchanged. -Takes a sequence and removes the element at the specified index. In case the index is out of bounds, the sequence is left unchanged. -Takes a sequence of naturals (zero included) and treats it as a permutation. The resulting sequence is the inverse permutation of the original one. -Convert a Java array to a JavaDL sequence. - -Return the (unique) ordered pair of two specified elements. -Return the first element of an ordered pair. -Return the second element of an ordered pair. - -A boolean function which is true iff the dynamic type of its argument is precisely the type which is part of the function name. - -A boolean function which is true iff the dynamic type of its argument is a subtype of the type which is part of the function name. - -tbd - -A constant holding the object reference pointing to the Java null object. -Quite the same as the keyword "null" in Java. - -tbd - -tbd - - - diff --git a/key.ui/src/main/resources/de/uka/ilkd/key/gui/help/ruleExplanations.xml b/key.ui/src/main/resources/de/uka/ilkd/key/gui/help/ruleExplanations.xml deleted file mode 100644 index a2f5e92de30..00000000000 --- a/key.ui/src/main/resources/de/uka/ilkd/key/gui/help/ruleExplanations.xml +++ /dev/null @@ -1,98 +0,0 @@ - - - - - - These properties define the help comments which are to be displayed - in the view pane when selecting tree elements for built-in rules. - - - -Some logical rules are implemented in Java code. This is because their semantics cannot easily be expressed in KeY's Taclet language. - - - -Most logical rules are implemented as Taclets. - -Taclets are schematic logical rules formulated in the Taclet Language. -The language is defined and explained in the KeY book. - - - -Taclets which have been introduced using File->Load User-Defined Taclets are filed here. - -Loading User Defined Taclets opens side branches on which the soundness of the lemma taclets must be established. - - - -When symbolic execution reaches a method call, the according method can be approximated by its specified contract (more precisely, one or more of its contracts). - -This rule gives rise to three or four subgoals: -1. Pre: It must be established that the pre-condition of the method holds prior to the method call. - -2. Post: The method terminates normally, the post-condition of the method can be assumed and symbolic execution continues. - -3. Exceptional Post: The method terminates abruptly with an exception, the exceptional post-condition is assumed, and symbolic execution continues with this exception thrown. - -4. Null reference: The receiver of the call can be null. This case is considered on this branch. If KeY can figure out automatically that this cannot be the case, this branch is suppressed. - - - -The QueryExpand rule allows to apply contracts or to symbolically execute a query -expression in the logic. It replaces the query expression by a new constant and -constructs a box formula in the antecedent 'defining' the constant as the result of -a method call. The method call is encoded directly as a method call in the box modality. -The query is invoked in a context equal to the container type of the query method. - - -The One Step Simplifier (OSS) aggregates the application of simplification rules into a single rule. This is done to make the calculus more efficient. - -You can activate/deactivate the simplifier by toggling the menu entry Options->One Step Simplifier. An active OSS makes the proof faster, a deactivated more transparent. - -In particular, the OSS performs normalisation and simplification on updated terms: - * Updates on terms without modality are resolved. - * Updates without effects are dropped. - * Sequential updates are merged into one parallel update. - -Technical Information: -The OSS aggregates the rules from the following heuristics (-> Taclet Base): - concrete, - update_elim, - update_apply_on_update, - update_apply - update_join, - elimQuantifier - - - -Methods and model fields may be annotated with an accessible clause. This defines a dependency contract describing the heap locations its value may depend on. - -If the heap changes in locations the symbol does not depend on, its value remains unchanged. This rules adds an according implication for a heap-dependent symbol to the sequent's antecedent. - -In automatic strategy, this rule is applied lazily (only once all other means of advancing the proof have been exhausted) to avoid endless loops. - - -Like methods, statement blocks can be annotated with contracts. The application of the Block Contract rules then gives rise to subgoals which roughly correspond to those of the Use Operation Contract rule (see there). -Three properties have to be shown: - -1. Validity of block contract - -2. Precondition of contract holds - -3. Postcondition holds after block terminates - - - -Loops can be handled by expanding or by using a loop invariant. -An invariant can be created manually or supplied by the JML specification. -Use of this rule creates three subgoals, two of which are new proof obligations: - -1. It must be shown that the loop invariant is initially valid. - -2. The loop body needs to preserve the invariant. - -In the third subgoal, the loop invariant can be used. - - - - diff --git a/key.ui/src/main/resources/de/uka/ilkd/key/gui/help/termLabelExplanations.xml b/key.ui/src/main/resources/de/uka/ilkd/key/gui/help/termLabelExplanations.xml deleted file mode 100644 index 86bb2ffa51d..00000000000 --- a/key.ui/src/main/resources/de/uka/ilkd/key/gui/help/termLabelExplanations.xml +++ /dev/null @@ -1,27 +0,0 @@ - - - - - - These properties define the help comments which are to be displayed - in the view pane when selecting term label tree elements. - - - -The term label SC is used to indicate that a logical operator has originally been "shortcut" operator. - -For instance, both conjunction operators in JML (i.e., && and &) are translated to the same function in JavaDL. To differentiate between the two, the translation of && adds the label SC. - -This is relevant for welldefinedness checks. - - - -This label saves a term's origin in the JML specification as well as the origins of all of its subterms and former subterms. - -For example, if the file "Example.java" contains the clause "requires R" at line 20, then every JavaDL term that is generated from R will have the origin -"requires @ Example.java @ line 20". - -Origin labels are not printed in the sequent view. To see a term's origin, you can mouse over it while holding the ALT button. If you want more detailed information, left click on the term and then on "Show Origin". - - - diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableSet.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableSet.java index 7eab97f1b7a..1786e0e32c6 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableSet.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableSet.java @@ -43,6 +43,12 @@ public interface ImmutableSet return DefaultImmutableSet.nil(); } + /// Creates an immutable set populated with the given values. + static ImmutableSet from(Collection values) { + var set = ImmutableSet.empty(); + return set.add(values); + } + /** * @return a {@code Set} containing the same elements as this {@code ImmutableSet} */ diff --git a/keyext.caching/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension b/keyext.caching/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension new file mode 100644 index 00000000000..37763eb246e --- /dev/null +++ b/keyext.caching/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension @@ -0,0 +1 @@ +de.uka.ilkd.key.gui.plugins.caching.CachingExtension