diff --git a/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdWhileInvariantRule.java b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdWhileInvariantRule.java index 49ba53d71a6..bd88f9bb377 100644 --- a/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdWhileInvariantRule.java +++ b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdWhileInvariantRule.java @@ -17,7 +17,6 @@ import org.jspecify.annotations.NonNull; import org.jspecify.annotations.NullMarked; -import org.jspecify.annotations.Nullable; @NullMarked @@ -38,11 +37,6 @@ public Name name() { return NAME; } - @Override - public @Nullable String getOrigin() { - return super.getOrigin(); - } - protected static class WdWhileInvariantRuleApplier extends WhileInvariantRuleApplier { public WdWhileInvariantRuleApplier(Goal goal, LoopInvariantBuiltInRuleApp ruleApp) { super(goal, ruleApp); diff --git a/key.core/src/main/antlr4/KeYParser.g4 b/key.core/src/main/antlr4/KeYParser.g4 index 5832a7238f7..cf96837f214 100644 --- a/key.core/src/main/antlr4/KeYParser.g4 +++ b/key.core/src/main/antlr4/KeYParser.g4 @@ -90,17 +90,18 @@ 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 | parametric_sort_decl) (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 | parametric_sort_decl) (EXTENDS sortExt=extends_sorts)? SEMI | ALIAS simple_ident_dots EQUALS sortId SEMI ) ; parametric_sort_decl : + DOC_COMMENT? simple_ident_dots formal_sort_param_decls ; @@ -115,6 +116,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 : @@ -139,7 +147,7 @@ prog_var_decls LBRACE ( kjt = keyjavatype - var_names = simple_ident_comma_list + var_names = simple_ident_comma_list_with_docs SEMI )* RBRACE @@ -161,6 +169,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 @@ -259,6 +271,7 @@ datatype_decl: ; datatype_constructor: + doc=DOC_COMMENT? name=simple_ident ( LPAREN @@ -341,7 +354,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/java/loader/JP2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java index b2985ea025e..5447b1b2675 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java @@ -1736,13 +1736,13 @@ public Object handleSpecialFunctionInvocation(Node n, String name, "Requested to find the default value of an unknown sort '%s'.", sortName)); } - var doc = sort.getDocumentation(); - + String doc = services.getNamespaces().docs().findDocumentation(sort); + String origin = services.getNamespaces().docs().findOrigin(sort); if (doc == null) { return reportError(n, format("Requested to find the default value for the sort '%s', " + "which does not have a documentary comment. The sort is defined at %s. ", - sortName, sort.getOrigin())); + sortName, origin)); } int pos = doc.indexOf(DEFVALUE); @@ -1754,7 +1754,7 @@ public Object handleSpecialFunctionInvocation(Node n, String name, return reportError(n, format( "Forgotten closing parenthesis on @defaultValue annotation for sort '%s' in '%s'", - sortName, sort.getOrigin())); + sortName, origin)); } // set this as the function name, as the user had written \dl_XXX diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/JTerm.java b/key.core/src/main/java/de/uka/ilkd/key/logic/JTerm.java index dc84ea2b302..3513d8c1584 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/JTerm.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/JTerm.java @@ -16,7 +16,6 @@ import org.key_project.util.collection.ImmutableSet; import org.jspecify.annotations.NonNull; -import org.jspecify.annotations.Nullable; /** * In contrast to the distinction of formulas and terms as made by most of the inductive definitions @@ -118,9 +117,4 @@ public interface JTerm * non-empty {@link JavaBlock}, {@code false} no {@link JavaBlock} available. */ boolean containsJavaBlockRecursive(); - - /** - * Returns a human-readable source of this term. For example the filename with line and offset. - */ - default @Nullable String getOrigin() { return null; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/LabeledTermImpl.java b/key.core/src/main/java/de/uka/ilkd/key/logic/LabeledTermImpl.java index cebf29cce99..4f1dba590ea 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/LabeledTermImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/LabeledTermImpl.java @@ -52,7 +52,7 @@ public class LabeledTermImpl extends TermImpl { public LabeledTermImpl(Operator op, ImmutableArray subs, ImmutableArray boundVars, ImmutableArray labels, String origin) { - super(op, subs, boundVars, origin); + super(op, subs, boundVars); assert labels != null : "Term labels must not be null"; assert !labels.isEmpty() : "There must be at least one term label"; this.labels = labels; @@ -69,7 +69,7 @@ public LabeledTermImpl(Operator op, ImmutableArray subs, public LabeledTermImpl(Operator op, ImmutableArray subs, ImmutableArray boundVars, ImmutableArray labels) { - super(op, subs, boundVars, ""); + super(op, subs, boundVars); assert labels != null : "Term labels must not be null"; assert !labels.isEmpty() : "There must be at least one term label"; this.labels = labels; diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/MetaSpace.java b/key.core/src/main/java/de/uka/ilkd/key/logic/MetaSpace.java new file mode 100644 index 00000000000..7f334d7ca86 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/MetaSpace.java @@ -0,0 +1,89 @@ +/* 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.HasMeta; + +import org.jspecify.annotations.NullMarked; +import org.jspecify.annotations.Nullable; + +/// MetaSpace is a namespace for storing additional information +/// +/// @author weigl +@NullMarked +public class MetaSpace { + public static final String SPACE_PREFIX_DOC = "doc/"; + public static final String SPACE_PREFIX_ORIGIN = "origin/"; + + private @Nullable MetaSpace parent; + private final Map metadata = new TreeMap<>(); + + public MetaSpace() { + } + + public MetaSpace(Map documentation) { + this.metadata.putAll(documentation); + } + + public MetaSpace(MetaSpace parent) { + this.parent = parent; + } + + private @Nullable Object findMetadata(String key) { + return metadata.get(key); + } + + public @Nullable String findDocumentation(HasMeta entity) { + if (entity.getDocumentation() != null) { + return entity.getDocumentation(); + } + return (String) findMetadata(SPACE_PREFIX_DOC + entity.getMetaKey()); + } + + /** + * Returns a human-readable source of this term. For example the filename with line and offset. + */ + public @Nullable String findOrigin(HasMeta entity) { + return (String) findMetadata(SPACE_PREFIX_ORIGIN + entity.getMetaKey()); + } + + public void add(MetaSpace space) { + this.metadata.putAll(space.metadata); + } + + public @Nullable MetaSpace parent() { + return parent; + } + + public void setDocumentation(HasMeta entity, @Nullable String doc) { + if (doc != null && doc.isBlank()) { + return; + } + setMetadata(SPACE_PREFIX_DOC, entity, doc); + } + + public void setOrigin(HasMeta entity, @Nullable String origin) { + if (origin != null && origin.isBlank()) { + return; + } + setMetadata(SPACE_PREFIX_ORIGIN, entity, origin); + } + + private void setMetadata(String prefix, HasMeta entity, @Nullable Object val) { + var key = prefix + entity.getMetaKey(); + if (val == null) { + metadata.remove(key); + } else { + metadata.put(key, val); + } + } + + + public MetaSpace copy() { + return new MetaSpace(metadata); + } +} 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 2da81a7abb9..f23613c8845 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,7 @@ package de.uka.ilkd.key.logic; + import de.uka.ilkd.key.logic.op.IProgramVariable; import de.uka.ilkd.key.logic.op.ParametricFunctionDecl; import de.uka.ilkd.key.logic.sort.ParametricSortDecl; @@ -18,33 +19,52 @@ import org.key_project.logic.sort.Sort; import org.key_project.prover.rules.RuleSet; -import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.NullMarked; import org.jspecify.annotations.Nullable; + +@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 SortAlias> sortAliases = new Namespace<>(); - private Namespace<@NonNull ParametricSortDecl> parametricSortNS = new Namespace<>(); - private Namespace<@NonNull ParametricFunctionDecl> parametricFuncNS = 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 sortAliases = new Namespace<>(); + private Namespace parametricSortNS = new Namespace<>(); + private Namespace parametricFuncNS = new Namespace<>(); + private Namespace choiceNS = new Namespace<>(); + private MetaSpace documentation = new MetaSpace(); public NamespaceSet() { } - public NamespaceSet(Namespace<@NonNull QuantifiableVariable> varNS, - Namespace<@NonNull Function> funcNS, - Namespace<@NonNull Sort> sortNS, Namespace<@NonNull SortAlias> sortAliases, - Namespace<@NonNull RuleSet> ruleSetNS, - Namespace<@NonNull ParametricSortDecl> parametricSortNS, - Namespace<@NonNull ParametricFunctionDecl> parametricFuncNS, - Namespace<@NonNull Choice> choiceNS, - Namespace<@NonNull IProgramVariable> programVarNS) { + public NamespaceSet(Namespace varNS, + Namespace funcNS, + Namespace sortNS, + Namespace sortAliases, + Namespace ruleSetNS, + Namespace parametricSortNS, + Namespace parametricFuncNS, + Namespace choiceNS, + Namespace programVarNS) { + this(varNS, funcNS, sortNS, sortAliases, ruleSetNS, + parametricSortNS, parametricFuncNS, + choiceNS, programVarNS, new MetaSpace()); + } + + public NamespaceSet(Namespace varNS, + Namespace funcNS, + Namespace sortNS, + Namespace sortAliases, + Namespace ruleSetNS, + Namespace parametricSortNS, + Namespace parametricFuncNS, + Namespace choiceNS, + Namespace programVarNS, + MetaSpace documentation) { this.varNS = varNS; this.progVarNS = programVarNS; this.funcNS = funcNS; @@ -54,21 +74,23 @@ public NamespaceSet(Namespace<@NonNull QuantifiableVariable> varNS, this.choiceNS = choiceNS; this.parametricSortNS = parametricSortNS; this.parametricFuncNS = parametricFuncNS; + this.documentation = documentation; } + public NamespaceSet copy() { return new NamespaceSet(variables().copy(), functions().copy(), sorts().copy(), sortAliases().copy(), ruleSets().copy(), parametricSortNS.copy(), parametricFuncNS.copy(), choices().copy(), - programVariables().copy()); + programVariables().copy(), + documentation.copy()); } public NamespaceSet shallowCopy() { return new NamespaceSet(variables(), functions(), sorts(), sortAliases(), ruleSets(), parametricSorts(), parametricFunctions(), - choices(), - programVariables()); + choices(), programVariables(), new MetaSpace(documentation)); } // TODO MU: Rename into sth with wrap or similar @@ -77,79 +99,80 @@ public NamespaceSet copyWithParent() { new Namespace<>(functions()), new Namespace<>(sorts()), new Namespace<>(sortAliases()), new Namespace<>(ruleSets()), new Namespace<>(parametricSorts()), new Namespace<>(parametricFunctions()), new Namespace<>(choices()), - new Namespace<>(programVariables())); + new Namespace<>(programVariables()), + new MetaSpace(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 SortAlias> sortAliases() { + public Namespace sortAliases() { return sortAliases; } - public void setSortAliases(Namespace<@NonNull SortAlias> sortAliases) { + public void setSortAliases(Namespace sortAliases) { this.sortAliases = sortAliases; } - public Namespace<@NonNull ParametricSortDecl> parametricSorts() { + public Namespace parametricSorts() { return parametricSortNS; } - public void setParametricSorts(Namespace<@NonNull ParametricSortDecl> parametricSortNS) { + public void setParametricSorts(Namespace parametricSortNS) { this.parametricSortNS = parametricSortNS; } - public Namespace<@NonNull ParametricFunctionDecl> parametricFunctions() { + public Namespace parametricFunctions() { return parametricFuncNS; } public void setParametricFunctions( - Namespace<@NonNull ParametricFunctionDecl> parametricFuncNS) { + Namespace parametricFuncNS) { this.parametricFuncNS = parametricFuncNS; } - 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; } @@ -286,7 +309,7 @@ public NamespaceSet getCompression() { return new NamespaceSet(varNS.compress(), funcNS.compress(), sortNS.compress(), sortAliases.compress(), ruleSetNS.compress(), parametricSortNS.compress(), parametricFuncNS.compress(), - choiceNS.compress(), progVarNS.compress()); + choiceNS.compress(), progVarNS.compress(), documentation); } public void flushToParent() { @@ -299,7 +322,10 @@ public NamespaceSet getParent() { return new NamespaceSet(varNS.parent(), funcNS.parent(), sortNS.parent(), sortAliases.parent(), ruleSetNS.parent(), parametricSortNS.parent(), parametricFuncNS.parent(), - choiceNS.parent(), progVarNS.parent()); + choiceNS.parent(), progVarNS.parent(), documentation.parent()); } + public MetaSpace docs() { + return documentation; + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/TermFactory.java b/key.core/src/main/java/de/uka/ilkd/key/logic/TermFactory.java index ad9935f7a92..bdd83aacbe3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/TermFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/TermFactory.java @@ -121,7 +121,7 @@ private JTerm doCreateTerm(Operator op, ImmutableArray subs, final TermImpl newTerm = (labels == null || labels.isEmpty() - ? new TermImpl(op, subs, boundVars, origin) + ? new TermImpl(op, subs, boundVars) : new LabeledTermImpl(op, subs, boundVars, labels, origin)); // Check if caching is possible. It is not possible if a non-empty JavaBlock is available // in the term or in one of its children because the meta information like PositionInfos diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java b/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java index 42063167176..c35c8c9ab9c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java @@ -21,7 +21,6 @@ import org.key_project.util.collection.ImmutableSet; import org.jspecify.annotations.NonNull; -import org.jspecify.annotations.Nullable; /** @@ -81,10 +80,6 @@ private enum ThreeValuedTruth { */ private ThreeValuedTruth containsJavaBlockRecursive = ThreeValuedTruth.UNKNOWN; - // ------------------------------------------------------------------------- - // constructors - // ------------------------------------------------------------------------- - /** * Constructs a term for the given operator, with the given sub terms, bounded variables and (if * applicable) the code block on this term. @@ -95,37 +90,14 @@ private enum ThreeValuedTruth { * @param boundVars the bounded variables (if applicable), e.g., for quantifiers */ public TermImpl(Operator op, ImmutableArray subs, - ImmutableArray boundVars, - String origin) { + ImmutableArray boundVars) { assert op != null; assert subs != null; this.op = op; this.subs = subs.isEmpty() ? EMPTY_TERM_LIST : subs; this.boundVars = boundVars == null ? EMPTY_VAR_LIST : boundVars; - this.origin = origin; } - TermImpl(Operator op, ImmutableArray subs, - ImmutableArray boundVars) { - this(op, subs, boundVars, ""); - } - - /** - * For which feature is this information needed? - * What is the difference from {@link de.uka.ilkd.key.logic.label.OriginTermLabel}? - */ - private final String origin; - - @Override - public @Nullable String getOrigin() { - return origin; - } - - // ------------------------------------------------------------------------- - // internal methods - // ------------------------------------------------------------------------- - - private ImmutableSet determineFreeVars() { ImmutableSet localFreeVars = DefaultImmutableSet.nil(); 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..4e3d3a9feda 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.HasMeta; 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, HasMeta, /* 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 getMetaKey() { + 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/ParametricFunctionDecl.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionDecl.java index 78b7a6a1c49..e6d4a0f19c8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionDecl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionDecl.java @@ -5,6 +5,7 @@ import de.uka.ilkd.key.logic.GenericParameter; +import org.key_project.logic.HasMeta; import org.key_project.logic.Name; import org.key_project.logic.Named; import org.key_project.logic.Sorted; @@ -18,8 +19,8 @@ /// The abstract declaration of a parametric function, e.g., `append<[E]>(List<[E]>, List<[E]>)`. /// /// To get an instantiated instance, use [ParametricFunctionInstance#get(ParametricFunctionDecl, -/// ImmutableList, Services)]. -public final class ParametricFunctionDecl implements Named, Sorted { +/// ImmutableList, de.uka.ilkd.key.java.Services)]. +public final class ParametricFunctionDecl implements Named, Sorted, HasMeta { private final Name name; private final ImmutableList parameters; private final ImmutableArray argSorts; @@ -76,4 +77,9 @@ public ImmutableList getParameters() { public @NonNull Name name() { return name; } + + @Override + public String getMetaKey() { + return "pfun/" + name(); + } } 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..3856d6acda8 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 getMetaKey() { + return super.getMetaKey(); + } } 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 cbddb2bc76d..803535ed5ca 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 61afd860737..5d44293d457 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,15 @@ 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) throws GenericSupersortException { - super(name, ext, false, documentation, origin); + super(name, ext, false); this.oneOf = oneOf; checkSupersorts(); } - public GenericSort(Name name, ImmutableSet ext, ImmutableSet oneOf) - throws GenericSupersortException { - 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..bd53d514e65 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/ParametricSortDecl.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortDecl.java index a0484a75d9f..43b593c222c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortDecl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortDecl.java @@ -6,6 +6,7 @@ import de.uka.ilkd.key.ldt.JavaDLTheory; import de.uka.ilkd.key.logic.GenericParameter; +import org.key_project.logic.HasMeta; import org.key_project.logic.Name; import org.key_project.logic.Named; import org.key_project.logic.sort.Sort; @@ -19,23 +20,18 @@ /// /// Get instantiated versions using [ParametricSortInstance#get(ParametricSortDecl, ImmutableList, /// Services)]. -public class ParametricSortDecl implements Named { +public class ParametricSortDecl implements Named, HasMeta { private final Name name; private final boolean isAbstract; - private final String documentation; - private final ImmutableList parameters; private final ImmutableSet extendedSorts; - private final String origin; public ParametricSortDecl(Name name, boolean isAbstract, ImmutableSet ext, - ImmutableList sortParams, String documentation, String origin) { + ImmutableList sortParams) { this.name = name; this.isAbstract = isAbstract; this.extendedSorts = ext.isEmpty() ? ImmutableSet.singleton(JavaDLTheory.ANY) : ext; - this.documentation = documentation; this.parameters = sortParams; - this.origin = origin; assert Immutables.isDuplicateFree(parameters) : "The caller should have made sure that generic sorts are not duplicated"; } @@ -57,11 +53,8 @@ public ImmutableSet getExtendedSorts() { return extendedSorts; } - public String getDocumentation() { - return documentation; - } - - public String getOrigin() { - return origin; + @Override + public String getMetaKey() { + return "psort/" + name(); } } 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 4e644442ee7..b5fd16060bb 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 @@ -255,7 +255,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..c5196d3e5f0 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) { + super(name, ext, false); } 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 3ead17776fe..7e1bb555638 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 @@ -11,50 +11,27 @@ import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableSet; -import org.jspecify.annotations.Nullable; - /** * 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) { 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, boolean 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,16 +65,6 @@ public String declarationString() { return name().toString(); } - @Override - public @Nullable String getDocumentation() { - return documentation; - } - - @Override - public @Nullable String getOrigin() { - return origin; - } - @Override public boolean containsGenericSort() { return false; diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/ConfigurationBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/ConfigurationBuilder.java index 146723fcf0d..3e9cddbefbd 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/ConfigurationBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/ConfigurationBuilder.java @@ -34,6 +34,9 @@ public String visitCkey(KeYParser.CkeyContext ctx) { @Override public String visitCsymbol(KeYParser.CsymbolContext ctx) { + if (ctx.getText().equals("null")) { + return null; + } return ctx.IDENT().getText(); } 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 22a4e64f10d..61b92c54b87 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 @@ -191,6 +191,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 b9d4c467101..edf31221501 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 @@ -4,6 +4,8 @@ package de.uka.ilkd.key.nparser.builder; 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.ast.abstraction.KeYJavaType; @@ -13,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.HasMeta; import org.key_project.logic.Name; import org.key_project.logic.Named; import org.key_project.logic.sort.Sort; @@ -63,16 +65,15 @@ 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); List typeParameters = accept(ctx.formal_sort_param_decls()); if (typeParameters == null) { - var s = new SortImpl(new Name(name), ImmutableSet.empty(), false, doc, origin); + var s = new SortImpl(new Name(name), ImmutableSet.empty(), false); sorts().addSafely(s); + docsSpace().setDocumentation(s, doc); + docsSpace().setOrigin(s, origin); } else { var doubled = CollectionUtil.findDuplicates(typeParameters); if (!doubled.isEmpty()) { @@ -81,22 +82,25 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { doubled.getFirst()); } var s = new ParametricSortDecl(new Name(name), false, ImmutableSet.empty(), - ImmutableList.fromList(typeParameters), doc, origin); + ImmutableList.fromList(typeParameters)); namespaces().parametricSorts().addSafely(s); + docsSpace().setDocumentation(s, doc); + docsSpace().setOrigin(s, origin); } 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); @@ -104,8 +108,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 { @@ -120,21 +124,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().setDocumentation(new HasMeta.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().setDocumentation(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; } @@ -154,7 +167,7 @@ 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()); + var sectionDoc = processDocumentation(ctx.DOC_COMMENT()); ImmutableSet ext = sortExt == null ? ImmutableSet.empty() : Immutables.createSetFrom(sortExt); @@ -176,8 +189,8 @@ public Object visitOne_sort_decl(KeYParser.One_sort_declContext ctx) { } if (ctx.sortIds != null) { - for (var idCtx : ctx.sortIds.simple_ident_dots()) { - String sortId = accept(idCtx); + for (var idCtx : ctx.sortIds.simple_ident_dots_with_docs()) { + String sortId = accept(idCtx.simple_ident_dots()); Name sortName = new Name(sortId); @@ -190,9 +203,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, - BuilderHelpers.getPosition(idCtx)); - s = gs; + s = new GenericSort(sortName, ext, oneOf); } catch (GenericSupersortException e) { semanticError(ctx, "Illegal sort given"); } @@ -200,16 +211,18 @@ 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)); - s = ps; + s = new ProxySort(sortName, ext); } else { - var si = new SortImpl(sortName, ext, isAbstractSort, - documentation, BuilderHelpers.getPosition(idCtx)); - s = si; + s = new SortImpl(sortName, ext, isAbstractSort); } } assert s != null; + String doc = processDocumentation(idCtx.DOC_COMMENT()); + String origin = BuilderHelpers.getPosition(idCtx); + docsSpace().setOrigin(s, origin); + docsSpace().setDocumentation(s, + Stream.of(doc, sectionDoc).filter(Objects::nonNull) + .collect(Collectors.joining("\n"))); sorts().add(s); createdSorts.add(s); } else { @@ -220,7 +233,7 @@ public Object visitOne_sort_decl(KeYParser.One_sort_declContext ctx) { "Sort declaration of {} in {} is ignored due to collision (already " + "present in {}).", sortName, BuilderHelpers.getPosition(ctx), - existingSort.getOrigin()); + docsSpace().findOrigin(existingSort)); } } } else { @@ -243,9 +256,13 @@ public Object visitOne_sort_decl(KeYParser.One_sort_declContext ctx) { "Cannot declare parametric sort %s, as a sort of the same name has already been declared", sortName); } - var sortDecl = new ParametricSortDecl(sortName, isAbstractSort, ext, params, - documentation, BuilderHelpers.getPosition(declCtx)); + var sortDecl = new ParametricSortDecl(sortName, isAbstractSort, ext, params); namespaces().parametricSorts().addSafely(sortDecl); + docsSpace().setOrigin(sortDecl, BuilderHelpers.getPosition(declCtx)); + var doc = processDocumentation(declCtx.DOC_COMMENT()); + docsSpace().setDocumentation(sortDecl, + Stream.of(doc, sectionDoc).filter(Objects::nonNull) + .collect(Collectors.joining("\n"))); } return createdSorts; } @@ -268,10 +285,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().setDocumentation(h, doc); } } return null; @@ -283,5 +303,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 4ecd37159ca..2c724b43c09 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; @@ -34,6 +36,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; import org.jspecify.annotations.Nullable; /** @@ -278,6 +282,11 @@ protected Namespace choices() { return namespaces().choices(); } + protected MetaSpace docsSpace() { + return namespaces().docs(); + } + + @Override public String visitString_value(KeYParser.String_valueContext ctx) { return ctx.getText().substring(1, ctx.getText().length() - 1); @@ -487,4 +496,28 @@ public Object visitFuncpred_name(KeYParser.Funcpred_nameContext ctx) { } return new GenericParameter((GenericSort) paramSort, variance); } + + + 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 344ab2ef9be..96a38da988f 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 @@ -83,6 +83,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; @@ -106,10 +107,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); @@ -128,10 +127,12 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { if (genericParams == null) { var fn = new JFunction(name, sort, args, null, true, false); functions().addSafely(fn); + docsSpace().setDocumentation(fn, doc); } else { var fn = new ParametricFunctionDecl(name, genericParams, new ImmutableArray<>(args), sort, null, true, true, false); namespaces().parametricFunctions().add(fn); + docsSpace().setDocumentation(fn, doc); } } if (genericParams != null) { @@ -147,6 +148,7 @@ public Object visitPred_decl(KeYParser.Pred_declContext ctx) { String pred_name = accept(ctx.funcpred_name()); List params = ctx.formal_sort_param_decls() == null ? null : visitFormal_sort_param_decls(ctx.formal_sort_param_decls()); + 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()) { @@ -198,6 +200,7 @@ public Object visitPred_decl(KeYParser.Pred_declContext ctx) { if (lookup(p.name()) == null) { functions().add(p); + docsSpace().setDocumentation(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 47f7a06730e..8c05a24b604 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,9 +172,11 @@ public Taclet visitTaclet(KeYParser.TacletContext ctx) { b.setName(new Name(name)); b.setChoices(choices); b.setAnnotations(tacletAnnotations); - b.setOrigin(BuilderHelpers.getPosition(ctx)); Taclet r = b.getTaclet(); - registerTaclet(ctx, r); + String doc = processDocumentation(ctx.doc); + String origin = BuilderHelpers.getPosition(ctx); + + registerTaclet(ctx, r, doc, origin); currentTBuilder.pop(); return r; } @@ -187,9 +189,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()) { @@ -218,10 +219,11 @@ public Taclet visitTaclet(KeYParser.TacletContext ctx) { accept(ctx.modifiers()); b.setChoices(choices); b.setAnnotations(tacletAnnotations); - b.setOrigin(BuilderHelpers.getPosition(ctx)); + String origin = BuilderHelpers.getPosition(ctx); try { Taclet r = peekTBuilder().getTaclet(); - registerTaclet(ctx, r); + String doc = processDocumentation(ctx.doc); + registerTaclet(ctx, r, doc, origin); setSchemaVariables(schemaVariables().parent()); currentTBuilder.pop(); return r; @@ -238,8 +240,11 @@ 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, @Nullable String origin) { taclet2Builder.put(taclet, peekTBuilder()); + docsSpace().setDocumentation(taclet, documentation); + docsSpace().setOrigin(taclet, origin); LOGGER.trace("Taclet announced: \"{}\" from {}:{}", taclet.name(), ctx.start.getTokenSource().getSourceName(), ctx.start.getLine()); } @@ -457,7 +462,7 @@ private TacletBuilder createAxiomTaclet( var cases = ctx.datatype_constructor().stream() .map(it -> createQuantifiedFormula(it, qvar, tb.var(phi), sort)) - .collect(Collectors.toList()); + .toList(); for (var c : cases) { if (c.vars == null) @@ -584,10 +589,6 @@ public Object visitModifiers(KeYParser.ModifiersContext ctx) { b.setDisplayName(Objects.requireNonNull(accept(ctx.dname))); } - if (ctx.HELPTEXT() != null) { // last entry - b.setHelpText(accept(ctx.htext)); - } - mapOf(ctx.triggers()); return null; } @@ -801,7 +802,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()); @@ -850,29 +850,32 @@ public ImmutableList visitTacletlist(KeYParser.TacletlistContext ctx) { private @NonNull TacletBuilder createTacletBuilderFor(Object find, ApplicationRestriction applicationRestriction, ParserRuleContext ctx) { - if (find == null) { - return new NoFindTacletBuilder(); - } else if (find instanceof JTerm) { - return new RewriteTacletBuilder<>().setFind((JTerm) find) - .setApplicationRestriction(applicationRestriction); - } else if (find instanceof Sequent findSeq) { - if (findSeq.isEmpty()) { + switch (find) { + case null -> { return new NoFindTacletBuilder(); - } else if (findSeq.antecedent().size() == 1 && findSeq.succedent().isEmpty()) { - AntecTacletBuilder b = new AntecTacletBuilder(); - b.setFind(findSeq); - b.setApplicationRestriction(applicationRestriction); - return b; - } else if (findSeq.antecedent().isEmpty() && findSeq.succedent().size() == 1) { - SuccTacletBuilder b = new SuccTacletBuilder(); - b.setFind(findSeq); - b.setApplicationRestriction(applicationRestriction); - return b; - } else { - semanticError(ctx, "Unknown find-sequent (perhaps null?):" + findSeq); } - } else { - semanticError(ctx, "Unknown find class type: %s", find.getClass().getName()); + case JTerm jTerm -> { + return new RewriteTacletBuilder<>().setFind(jTerm) + .setApplicationRestriction(applicationRestriction); + } + case Sequent findSeq -> { + if (findSeq.isEmpty()) { + return new NoFindTacletBuilder(); + } else if (findSeq.antecedent().size() == 1 && findSeq.succedent().isEmpty()) { + AntecTacletBuilder b = new AntecTacletBuilder(); + b.setFind(findSeq); + b.setApplicationRestriction(applicationRestriction); + return b; + } else if (findSeq.antecedent().isEmpty() && findSeq.succedent().size() == 1) { + SuccTacletBuilder b = new SuccTacletBuilder(); + b.setFind(findSeq); + b.setApplicationRestriction(applicationRestriction); + return b; + } else { + semanticError(ctx, "Unknown find-sequent (perhaps null?):" + findSeq); + } + } + default -> semanticError(ctx, "Unknown find class type: %s", find.getClass().getName()); } throw new IllegalArgumentException( 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 054ff20a142..a7f5a630aee 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/ProblemInitializer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java index cdd3c8653d4..146cf413dc4 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 @@ -34,6 +34,7 @@ import de.uka.ilkd.key.rule.RewriteTaclet; 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; @@ -53,6 +54,7 @@ import org.key_project.util.collection.ImmutableSet; import org.key_project.util.java.StringUtil; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -69,6 +71,7 @@ public final class ProblemInitializer { */ private FileRepo fileRepo; private ImmutableSet warnings = DefaultImmutableSet.nil(); + private @Nullable Configuration additionalProfileOptions; // ------------------------------------------------------------------------- // constructors @@ -82,13 +85,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,7 +455,7 @@ private InitConfig createInitConfigFor(EnvInput envInput) throws ProofInputExcep for (RuleSource tacletBase : tacletBases) { KeYFile tacletBaseFile = new KeYFile( "taclet base (%s)".formatted(tacletBase.file().getFileName()), - tacletBase, progMon, profile); + tacletBase, progMon, profile, null); readEnvInput(tacletBaseFile, config); } } @@ -605,9 +617,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, - services); + if (pv instanceof LocationVariable lv) { + heapLDT.getFieldSymbolForPV(lv, initConfig.getServices()); } } } 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 851cfa8320b..3e60e3ea712 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,36 +65,6 @@ 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(); - } - - } - /** * The file or folder to load. */ @@ -859,4 +829,34 @@ public void setLoadSingleJavaFile(boolean loadSingleJavaFile) { public void setIgnoreWarnings(boolean ignoreWarnings) { this.ignoreWarnings = ignoreWarnings; } + + 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 028a83a33c4..856ccb44329 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/BuiltInRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/BuiltInRule.java index cac17c592b7..f59d007bbb1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/BuiltInRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/BuiltInRule.java @@ -40,9 +40,4 @@ public interface BuiltInRule extends Rule, RuleExecutor { default RuleExecutor getExecutor() { return this; } - - @Override - default @Nullable String getOrigin() { - return "defined in Java: " + getClass().getName(); - } } 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 c04e03ef185..a999b12b13f 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 7c9c327582e..a64659f4de7 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 @@ -42,6 +42,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; @@ -683,4 +684,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..0b691486a8c 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,17 @@ package de.uka.ilkd.key.rule; -import org.key_project.logic.HasOrigin; +import org.key_project.logic.HasMeta; + +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, HasMeta { + @Override + default @NonNull String getMetaKey() { + return "rule/" + this.name(); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java b/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java index 6c2660bd593..248736f25d7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java @@ -32,8 +32,6 @@ import org.checkerframework.checker.nullness.qual.EnsuresNonNull; import org.jspecify.annotations.NonNull; -import org.jspecify.annotations.Nullable; - /** @@ -519,23 +517,6 @@ public enum TacletOperation { public abstract @NonNull Taclet setName(@NonNull String s); - /** - * Information about the origin of the taclet. Should be a location where the user can find the - * declaration of the taclet. - *

- * This field is set by the parser with [url]:[lineNumber] - */ - private @Nullable String origin; - - @Override - public @Nullable String getOrigin() { - return origin; - } - - public void setOrigin(@Nullable String origin) { - this.origin = origin; - } - StringBuffer toStringAttribs(StringBuffer sb) { // if (noninteractive()) sb = sb.append(" \\noninteractive"); sb.append("\nChoices: ").append(choices); 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 ec6b10b9f4b..73bbb048127 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 3780c359933..cf3426d24a2 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 @@ -970,4 +970,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 e727678997f..cc29101fd1f 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/rule/tacletbuilder/AntecTacletBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/AntecTacletBuilder.java index 9359af7621b..b2bb64eda58 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/AntecTacletBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/AntecTacletBuilder.java @@ -92,7 +92,6 @@ public AntecTaclet getAntecTaclet() { goals, ruleSets, attrs, (Sequent) find, prefixBuilder.getPrefixMap(), choices, tacletAnnotations); - t.setOrigin(origin); return t; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/NoFindTacletBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/NoFindTacletBuilder.java index e2d1f630b39..4cddf086024 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/NoFindTacletBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/NoFindTacletBuilder.java @@ -39,7 +39,6 @@ public NoFindTaclet getNoFindTaclet() { varsNewDependingOn, variableConditions), goals, ruleSets, attrs, prefixBuilder.getPrefixMap(), choices, tacletAnnotations); - t.setOrigin(origin); return t; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/RewriteTacletBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/RewriteTacletBuilder.java index bc5ab5239b2..35bee170e56 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/RewriteTacletBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/RewriteTacletBuilder.java @@ -55,7 +55,6 @@ public T getRewriteTaclet() { variableConditions), goals, ruleSets, attrs, (JTerm) find, prefixBuilder.getPrefixMap(), choices, surviveSmbExec, tacletAnnotations); - t.setOrigin(origin); return (T) t; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/SuccTacletBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/SuccTacletBuilder.java index 1954f7713b1..cb768b69dea 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/SuccTacletBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/SuccTacletBuilder.java @@ -76,7 +76,6 @@ public SuccTaclet getSuccTaclet() { goals, ruleSets, attrs, (Sequent) find, prefixBuilder.getPrefixMap(), choices, tacletAnnotations); - t.setOrigin(origin); return t; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletBuilder.java index bcfd38f2692..f78e9cecb9f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletBuilder.java @@ -32,7 +32,6 @@ import org.key_project.util.collection.ImmutableSet; import org.jspecify.annotations.NonNull; -import org.jspecify.annotations.Nullable; /** * abstract taclet builder class to be inherited from taclet builders specialised for their concrete @@ -63,7 +62,6 @@ public abstract class TacletBuilder { protected ChoiceExpr choices = ChoiceExpr.TRUE; protected ImmutableSet tacletAnnotations = DefaultImmutableSet.nil(); - protected String origin; public void setAnnotations(ImmutableSet tacletAnnotations) { this.tacletAnnotations = tacletAnnotations; @@ -326,21 +324,7 @@ public T getTacletWithoutInactiveGoalTemplates(Set active) { } } - public void setOrigin(String origin) { - this.origin = origin; - } - - public void setHelpText(@Nullable Object accept) { - // throw new RuntimeException("To be implemented"); - } - public static class TacletBuilderException extends IllegalArgumentException { - - - /** - * - */ - private static final long serialVersionUID = -6710383705714015291L; private final Name tacletname; private final String errorMessage; 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 31acea8acba..11bf0d4c1b6 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 @@ -88,7 +88,8 @@ public boolean exists(String name) { * @see #getTable(String) */ public boolean exists(String name, Class clazz) { - return data.containsKey(name) && clazz.isAssignableFrom(data.get(name).getClass()); + return data.containsKey(name) && data.get(name) != null + && clazz.isAssignableFrom(data.get(name).getClass()); } /** @@ -184,7 +185,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)); } /** @@ -215,8 +216,7 @@ public double getDouble(String name) { * @param name property name * @throws ClassCastException if the entry is not a {@link String} */ - @Nullable - public String getString(String name) { + public @Nullable String getString(String name) { return get(name, String.class); } @@ -358,7 +358,7 @@ private ConfigurationMeta getOrCreateMeta(String name) { /** * @see #getTable(String) */ - public Configuration getSection(String name) { + public @Nullable Configuration getSection(String name) { return getTable(name); } @@ -373,39 +373,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)); } @@ -544,7 +544,7 @@ public ConfigurationWriter printValue(Object value) { } else if (value instanceof Enum) { printValue(value.toString()); } else if (value == null) { - printValue("null"); + out.write("null"); } else { throw new IllegalArgumentException("Unexpected object: " + value); } @@ -552,7 +552,7 @@ public ConfigurationWriter printValue(Object value) { } private ConfigurationWriter printMap(Map value) { - out.format("{ "); + out.format("{"); indent += 4; newline().printIndent(); for (Iterator> iterator = @@ -579,7 +579,7 @@ private ConfigurationWriter print(String s) { } private ConfigurationWriter printSeq(Collection value) { - out.format("[ "); + out.print("["); indent += 4; newline(); printIndent(); @@ -598,13 +598,13 @@ private ConfigurationWriter printSeq(Collection value) { } indent -= 4; newline().printIndent(); - out.format("]"); + out.print("]"); return this; } private ConfigurationWriter printKey(String key) { printValue(key); - out.format(" : "); + out.print(" : "); return this; } } 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/taclettranslation/lemma/GenericRemovingLemmaGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/GenericRemovingLemmaGenerator.java index 778914c8cdc..7aebd45fcfc 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..d0392bf44b1 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 @@ -122,8 +122,7 @@ public void replaceGenericByProxySorts() { Set result = new HashSet<>(); for (Sort sort : usedExtraSorts) { if (sort instanceof GenericSort genSort) { - ProxySort proxySort = new ProxySort(genSort.name(), genSort.extendsSorts(), - "", ""); + 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 39c7bc8c851..c7b5cacc8ec 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 @@ -7,8 +7,11 @@ import java.net.MalformedURLException; import java.net.URI; import java.net.URISyntaxException; +import java.nio.file.Paths; +import java.util.regex.Matcher; import java.util.regex.Pattern; +import de.uka.ilkd.key.java.Position; import de.uka.ilkd.key.parser.Location; import de.uka.ilkd.key.proof.io.ProblemLoaderException; import de.uka.ilkd.key.util.parsing.HasLocation; @@ -39,17 +42,17 @@ public final class ExceptionTools { public static final Pattern TOKEN_MGR_ERR_PATTERN = Pattern.compile("^Lexical error at line (\\d+), column (\\d+)\\."); - private ExceptionTools() {} + private ExceptionTools() { + } /** * Get the throwable's message. This will return a nicer error message for * certain ANTLR exceptions. * - * @param throwable - * a throwable + * @param throwable a throwable * @return message for the exception */ - public static String getMessage(Throwable throwable) { + public static String getMessage(@Nullable Throwable throwable) { if (throwable == null) { return ""; } else if (throwable instanceof ParseCancellationException @@ -108,15 +111,13 @@ private static String getNiceMessageInternal(IntStream inputStream, * Tries to resolve the location (i.e., file name, line, and column) from a parsing exception. * Result may be null. * - * @param exc - * the Throwable to extract the Location from + * @param exc the Throwable to extract the Location from * @return the Location stored inside the Throwable or null if no such can be found - * @throws MalformedURLException - * if the no URL can be parsed from the String stored inside the + * @throws MalformedURLException if the no URL can be parsed from the String stored inside the * given Throwable can not be successfully converted to a URL and thus no Location can * be created */ - public static Location getLocation(@NonNull Throwable exc) + public static @Nullable Location getLocation(@NonNull Throwable exc) throws MalformedURLException { if (exc instanceof HasLocation) { return ((HasLocation) exc).getLocation(); @@ -141,14 +142,14 @@ private static URI parseFileName(String filename) throws MalformedURLException { } } - // TODO javaparser this was not unused - @Nullable - private static Location getLocation(RecognitionException exc) throws MalformedURLException { - // ANTLR 3 - Recognition Exception. - if (exc.input != null) { - // ANTLR has 0-based column numbers - return new Location(parseFileName(exc.input.getSourceName()), exc.position); - } - return null; + private static @Nullable Location getLocation(InputMismatchException exc) { + var token = exc.getOffendingToken(); + + 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(), + de.uka.ilkd.key.java.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 1cf51d30c4b..1243a772423 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::#$transient; \unique Field java.lang.Object::#$transactionConditionallyUpdated; @@ -36,16 +74,38 @@ \unique Field alpha::#$classInitializationInProgress; // static \unique Field alpha::#$classErroneous; // 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/locset/locSets.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locset/locSets.key index b1a2a9a2cd4..be74f91a6dc 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locset/locSets.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locset/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 903b3fde087..cb279fdcba7 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/sequence/seq.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/sequence/seq.key index e9fa73b1381..432776504de 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/sequence/seq.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/sequence/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.core/src/test/java/de/uka/ilkd/key/logic/TestTermFactory.java b/key.core/src/test/java/de/uka/ilkd/key/logic/TestTermFactory.java index 80489f2a6ae..5203ffc935d 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/logic/TestTermFactory.java +++ b/key.core/src/test/java/de/uka/ilkd/key/logic/TestTermFactory.java @@ -66,8 +66,8 @@ public class TestTermFactory { @BeforeEach public void setUp() { - JTerm et_x = new TermImpl(x, new ImmutableArray<>(), null, null); - JTerm et_px = new TermImpl(p, new ImmutableArray<>(et_x), null, null); + JTerm et_x = new TermImpl(x, new ImmutableArray<>(), null); + JTerm et_px = new TermImpl(p, new ImmutableArray<>(et_x), null); et1 = et_px; TB = TacletForTests.services().getTermBuilder(); tf = TB.tf(); @@ -130,7 +130,7 @@ public void testWrongArity() { @Test public void testWithInvalidSubformulae() { JTerm invalidBuilt = new TermImpl(p, - new ImmutableArray<>(new TermImpl(y, new ImmutableArray<>(), null, null)), null, null); + new ImmutableArray<>(new TermImpl(y, new ImmutableArray<>(), null)), null); try { JTerm t_px_or_py = tf.createTerm(Junctor.OR, invalidBuilt, t1()); } catch (Exception e) { @@ -141,27 +141,27 @@ public void testWithInvalidSubformulae() { @Test public void testConstantTrue() { JTerm t_true = tf.createTerm(Junctor.TRUE); - assertEquals(t_true, new TermImpl(Junctor.TRUE, new ImmutableArray<>(), null, null)); + assertEquals(t_true, new TermImpl(Junctor.TRUE, new ImmutableArray<>(), null)); } @Test public void testQuantifierTerm() { JTerm t_forallx_px = TB.all(ImmutableSLList.nil().append(x), t1()); assertEquals(t_forallx_px, new TermImpl(Quantifier.ALL, new ImmutableArray<>(t1()), - new ImmutableArray<>(x), null)); + new ImmutableArray<>(x))); } @Test public void testJunctorTerm() { JTerm t_px_imp_ryw = tf.createTerm(Junctor.IMP, t1(), t2()); assertEquals(t_px_imp_ryw, - new TermImpl(Junctor.IMP, new ImmutableArray<>(t1(), t2()), null, null)); + new TermImpl(Junctor.IMP, new ImmutableArray<>(t1(), t2()), null)); } @Test public void testNegationTerm() { JTerm t_not_ryw = tf.createTerm(Junctor.NOT, t2()); - assertEquals(t_not_ryw, new TermImpl(Junctor.NOT, new ImmutableArray<>(t2()), null, null)); + assertEquals(t_not_ryw, new TermImpl(Junctor.NOT, new ImmutableArray<>(t2()), null)); } @Test @@ -188,7 +188,7 @@ public void testBoxTerm() { public void testSubstitutionTerm() { JTerm t_x_subst_fy_in_px = TB.subst(WarySubstOp.SUBST, x, t3(), t1()); assertEquals(new TermImpl(WarySubstOp.SUBST, new ImmutableArray<>(t3(), t1()), - new ImmutableArray<>(x), null), t_x_subst_fy_in_px); + new ImmutableArray<>(x)), t_x_subst_fy_in_px); } diff --git a/key.core/src/test/java/de/uka/ilkd/key/logic/sort/TestAlias.java b/key.core/src/test/java/de/uka/ilkd/key/logic/sort/TestAlias.java index 858f5dcd541..4636d680497 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/logic/sort/TestAlias.java +++ b/key.core/src/test/java/de/uka/ilkd/key/logic/sort/TestAlias.java @@ -57,8 +57,7 @@ public void testAliasOfParametric() { var pSet = new ParametricSortDecl(new Name("PSet"), false, ImmutableSet.empty(), ImmutableList.of( new GenericParameter(new GenericSort(new Name("A")), - GenericParameter.Variance.INVARIANT)), - "", ""); + GenericParameter.Variance.INVARIANT))); nss.parametricSorts().add(pSet); ParametricSortInstance intSet = ParametricSortInstance.get(pSet, ImmutableList.of(new GenericArgument(nss.lookupSortOrAlias("int"))), services); diff --git a/key.core/src/test/java/de/uka/ilkd/key/logic/sort/TestParametricSorts.java b/key.core/src/test/java/de/uka/ilkd/key/logic/sort/TestParametricSorts.java index e6f2e32576b..c8d544db6d4 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/logic/sort/TestParametricSorts.java +++ b/key.core/src/test/java/de/uka/ilkd/key/logic/sort/TestParametricSorts.java @@ -62,8 +62,8 @@ private ParametricSortDecl addParametricSort(String name, GenericSort genSort = (GenericSort) nss.sorts().lookup("G" + (i + 1)); params = params.prepend(new GenericParameter(genSort, varia)); } - ParametricSortDecl psd = new ParametricSortDecl(new Name(name), false, ImmutableSet.empty(), - params, "", ""); + ParametricSortDecl psd = + new ParametricSortDecl(new Name(name), false, ImmutableSet.empty(), params); nss.parametricSorts().add(psd); return psd; } 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..e5b36ec4f58 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.HasMeta; 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, HasMeta { /// 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 getMetaKey() { + return "heuristic/" + name; + } } diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/Taclet.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/Taclet.java index 9a8c547a060..c9e39964a63 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/Taclet.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/Taclet.java @@ -5,6 +5,7 @@ import java.util.Iterator; +import org.jspecify.annotations.NonNull; import org.key_project.logic.ChoiceExpr; import org.key_project.logic.Name; import org.key_project.logic.SyntaxElement; @@ -23,7 +24,6 @@ import org.checkerframework.checker.calledmethods.qual.RequiresCalledMethods; import org.checkerframework.checker.initialization.qual.UnderInitialization; import org.checkerframework.checker.nullness.qual.EnsuresNonNull; -import org.jspecify.annotations.NonNull; import org.jspecify.annotations.Nullable; import static org.key_project.util.Strings.formatAsList; @@ -44,7 +44,7 @@ public abstract class Taclet implements Rule { protected final @Nullable SyntaxElement find; /// The restriction(s) for applying this update. [ApplicationRestriction]. - protected final @NonNull ApplicationRestriction applicationRestriction; + protected final ApplicationRestriction applicationRestriction; /// the assumes sequent of the taclet protected final Sequent assumesSequent; @@ -75,7 +75,7 @@ public abstract class Taclet implements Rule { /// list /// of all variables that may appear free in the instantiation of the schemavariable (a bit more /// complicated for rewrite taclets, see paper of M:Giese) - protected final ImmutableMap<@NonNull SchemaVariable, org.key_project.prover.rules.TacletPrefix> prefixMap; + protected final ImmutableMap prefixMap; /// cache; contains set of all bound variables protected @Nullable ImmutableSet boundVariables = null; @@ -101,10 +101,10 @@ public abstract class Taclet implements Rule { // but all at once for a given term. /// The taclet matcher - protected @NonNull TacletMatcher matcher; + protected TacletMatcher matcher; /// The taclet executor - protected @NonNull TacletExecutor, ? extends @NonNull RuleApp> executor; + protected TacletExecutor, ? extends RuleApp> executor; /// creates a Taclet (originally known as Schematic Theory Specific Rules) /// @@ -121,7 +121,7 @@ protected Taclet(Name name, SyntaxElement find, TacletApplPart applPart, ImmutableList goalTemplates, ImmutableList ruleSets, TacletAttributes attrs, - ImmutableMap<@NonNull SchemaVariable, TacletPrefix> prefixMap, ChoiceExpr choices, + ImmutableMap prefixMap, ChoiceExpr choices, ImmutableSet tacletAnnotations) { this.tacletAnnotations = tacletAnnotations; this.name = name; @@ -167,7 +167,7 @@ public boolean hasTrigger() { } @RequiresCalledMethods(value = "this", methods = "createAndInitializeMatcher") - public final TacletMatcher getMatcher() { + public final @Nullable TacletMatcher getMatcher() { return matcher; } @@ -227,13 +227,13 @@ public ImmutableList getVariableConditions() { /// @return the name of the Taclet @Override - public @NonNull Name name() { + public Name name() { return name; } /// @return the display name of the taclet, or, if not specified -- the canonical name @Override - public @NonNull String displayName() { + public String displayName() { return displayName; } @@ -243,7 +243,7 @@ public Sequent assumesSequent() { } /// @return the application restrictions of the Taclet. - public ApplicationRestriction applicationRestriction() { + public @Nullable ApplicationRestriction applicationRestriction() { return applicationRestriction; } @@ -266,7 +266,7 @@ public ImmutableList goalTemplates() { return goalTemplates; } - public ImmutableMap<@NonNull SchemaVariable, TacletPrefix> prefixMap() { + public ImmutableMap prefixMap() { return prefixMap; } @@ -440,8 +440,8 @@ public String toString() { } @SuppressWarnings("unchecked") - public @NonNull > TacletExecutor<@NonNull G, ?> getExecutor() { - return (TacletExecutor<@NonNull G, ?>) executor; + public > TacletExecutor<@NonNull G, ?> getExecutor() { + return (TacletExecutor) executor; } public abstract Taclet setName(String 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..c4ab2bb05a7 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, HasMeta { 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 getMetaKey() { + return "choice/" + name; + } } diff --git a/key.ncore/src/main/java/org/key_project/logic/HasMeta.java b/key.ncore/src/main/java/org/key_project/logic/HasMeta.java new file mode 100644 index 00000000000..36ecf0f508c --- /dev/null +++ b/key.ncore/src/main/java/org/key_project/logic/HasMeta.java @@ -0,0 +1,24 @@ +/* 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; + +/// Mark items of the namespace which can have entries in the {@link +/// de.uka.ilkd.key.logic.MetaSpace}. +/// +/// @author weigl +public interface HasMeta { + String getMetaKey(); + + default @Nullable String getDocumentation() { + return null; + } + + record OptionCategory(String name) implements HasMeta { + public String getMetaKey() { + return "category/" + name; + } + } +} diff --git a/key.ncore/src/main/java/org/key_project/logic/HasOrigin.java b/key.ncore/src/main/java/org/key_project/logic/HasOrigin.java deleted file mode 100644 index 50b2b5f1477..00000000000 --- a/key.ncore/src/main/java/org/key_project/logic/HasOrigin.java +++ /dev/null @@ -1,21 +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 org.key_project.logic; - -import org.jspecify.annotations.Nullable; - -/// Classes with this interface provides a simple human-readable String where they came from. -/// -/// @author Alexander Weigl -/// @version 1 (12/30/21) -public interface HasOrigin { - /// Information about the origin of the rule. - /// - /// Should be a human-readable location where the user can find the declaration of the rule. - /// - /// This field is set by the parser with \[url]:\[lineNumber] - default @Nullable String getOrigin() { - return null; - } -} 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..d05a643c630 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, HasMeta, 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 getMetaKey() { + 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 68799506339..bc29701c640 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,13 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.logic.sort; -import org.key_project.logic.HasOrigin; +import org.key_project.logic.HasMeta; 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, HasMeta { /// @return the direct supersorts of this sort. Not supported by `NullSort`. ImmutableSet extendsSorts(); @@ -27,9 +26,10 @@ 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 getMetaKey() { + return "sort/" + name(); + } /// Whether this sort is or contains an uninstantiated generic sort. boolean containsGenericSort(); 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 index e5c2656b37e..bf1a05eddbc 100644 --- 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 @@ -6,16 +6,20 @@ import java.util.*; import javax.swing.tree.DefaultTreeModel; +import de.uka.ilkd.key.logic.MetaSpace; +import de.uka.ilkd.key.logic.NamespaceSet; +import de.uka.ilkd.key.logic.label.TermLabelManager; import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.proof.Proof; 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; +import org.key_project.logic.op.Function; /** * Extension of {@link DefaultTreeModel} used by {@link InfoTree}. @@ -31,13 +35,12 @@ public class InfoTreeModel extends DefaultTreeModel { private static final String LEMMAS = "Lemmas"; private static final String TACLET_BASE = "Taclet Base"; - public InfoTreeModel(Goal goal, XMLResources xmlResources, MainWindow mainWindow) { + public InfoTreeModel(Goal goal, MetaSpace meta, 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()), + insertAsLast(new RulesNode(meta, goal), (InfoTreeNode) root); + insertAsLast(new TermLabelsNode(goal.proof(), meta), (InfoTreeNode) root); + insertAsLast(new FunctionsNode(meta, goal.getLocalNamespaces()), (InfoTreeNode) root); } private void insertAsLast(InfoTreeNode ins, InfoTreeNode parent) { @@ -56,31 +59,25 @@ private class FunctionsNode extends InfoTreeNode { private static final String DEFAULT_FUNCTIONS_LABEL = "Display descriptions for documented interpreted function and predicate symbols."; - FunctionsNode(Properties functionExplanations) { + FunctionsNode(MetaSpace functionExplanations, NamespaceSet nss) { 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); + var sortedKeys = new ArrayList<>(nss.functions().allElements()); + sortedKeys.sort(Comparator.comparing(it -> it.name().toString())); + + for (Function function : sortedKeys) { + var key = function.name().toString(); + var category = function.sort().name().toString(); + var doc = functionExplanations.findDocumentation(function); + InfoTreeNode categoryNode = categoryMap.get(category); + if (categoryNode == null) { + categoryNode = new InfoTreeNode(category, COLLECTION); + categoryMap.put(category, categoryNode); + insertAsLast(categoryNode, this); } + insertAsLast(new InfoTreeNode(key, doc), categoryNode); } } } @@ -92,12 +89,19 @@ private class TermLabelsNode extends InfoTreeNode { */ private static final long serialVersionUID = 7447092361863294242L; - TermLabelsNode(MainWindow mainWindow, Properties termLabelExplanations) { + TermLabelsNode(Proof proof, MetaSpace meta) { super("Term Labels", "Show descriptions for currently available term labels."); - List labelNames = mainWindow.getSortedTermLabelNames(); + 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) { - insertAsLast(new InfoTreeNode(name.toString(), termLabelExplanations), this); + var item = + new InfoTreeNode(name.toString(), factories.get(name).getDocumentation()); + insertAsLast(item, this); } } } @@ -109,20 +113,20 @@ private class RulesNode extends InfoTreeNode { */ private static final long serialVersionUID = 7622830441420768861L; - RulesNode(Properties ruleExplanations, Goal goal) { + RulesNode(MetaSpace meta, Goal goal) { super("Rules", "Browse descriptions for currently available rules."); - InfoTreeNode builtInRoot = new InfoTreeNode("Built-In", ruleExplanations); + InfoTreeNode builtInRoot = new InfoTreeNode("Built-In", ""); insertAsLast(builtInRoot, this); - InfoTreeNode axiomTacletRoot = new InfoTreeNode(TACLET_BASE, ruleExplanations); + InfoTreeNode axiomTacletRoot = new InfoTreeNode(TACLET_BASE, ""); insertAsLast(axiomTacletRoot, this); - InfoTreeNode proveableTacletsRoot = new InfoTreeNode(LEMMAS, ruleExplanations); + InfoTreeNode proveableTacletsRoot = new InfoTreeNode(LEMMAS, ""); 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); + insertAsLast(new InfoTreeNode(br, meta), builtInRoot); } Set set = goal.ruleAppIndex().tacletIndex().allNoPosTacletApps(); OneStepSimplifier simplifier = MiscTools.findOneStepSimplifier(goal.proof()); @@ -136,11 +140,10 @@ private class RulesNode extends InfoTreeNode { continue; // do not break system because of this } if (just.isAxiomJustification()) { - insertAndGroup(new InfoTreeNode(app.taclet()), axiomTacletRoot, - ruleExplanations); + insertAndGroup(new InfoTreeNode(app.taclet(), meta), axiomTacletRoot, ""); } else { - insertAndGroup(new InfoTreeNode(app.taclet()), proveableTacletsRoot, - ruleExplanations); + insertAndGroup(new InfoTreeNode(app.taclet(), meta), proveableTacletsRoot, + ""); } } } @@ -166,7 +169,7 @@ private int getChildCount(InfoTreeNode root) { * groups subsequent insertions with the same name under a new node */ private void insertAndGroup(InfoTreeNode ins, InfoTreeNode parent, - Properties ruleExplanations) { + String ruleExplanations) { InfoTreeNode insNode = ins; if (parent.getChildCount() > 0) { InfoTreeNode lastNode = 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 index 86909fc9f95..c6511723b98 100644 --- 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 @@ -6,6 +6,7 @@ import java.util.Properties; import javax.swing.tree.DefaultMutableTreeNode; +import de.uka.ilkd.key.logic.MetaSpace; import de.uka.ilkd.key.pp.LogicPrinter; import de.uka.ilkd.key.pp.NotationInfo; import de.uka.ilkd.key.rule.BuiltInRule; @@ -53,13 +54,13 @@ public class InfoTreeNode extends DefaultMutableTreeNode { } - InfoTreeNode(Taclet taclet) { + InfoTreeNode(Taclet taclet, MetaSpace metaSpace) { 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() + description = lp.result() + "\n\n Defined at:" + metaSpace.findOrigin(taclet) + "\n\n under options:" + taclet.getChoices(); } @@ -69,10 +70,10 @@ public class InfoTreeNode extends DefaultMutableTreeNode { this.description = description; } - public InfoTreeNode(BuiltInRule br, Properties ruleExplanations) { - this(br.displayName(), ruleExplanations); + public InfoTreeNode(BuiltInRule br, MetaSpace ruleExplanations) { + this(br.displayName(), ruleExplanations.findDocumentation(br)); rule = br; - description = "Defined at: " + br.getOrigin(); + description = "Defined at: " + br.getClass(); } String getTitle() { 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 46ba554d74a..1852e5d9659 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 @@ -27,7 +27,6 @@ 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; /** * Class for info contents displayed in {@link MainWindow}. @@ -43,7 +42,6 @@ public class InfoView extends JSplitPane implements TabPanel { private final InfoTree infoTree; private final InfoViewContentPane contentPane; - private final XMLResources xmlResources; private final ProofDisposedListener proofDisposedListener; private final KeYSelectionListener selectionListener = new InfoViewSelectionListener(); private Node lastShownGoalNode; @@ -52,7 +50,6 @@ public class InfoView extends JSplitPane implements TabPanel { public InfoView() { super(VERTICAL_SPLIT); - xmlResources = new XMLResources(); // initial placement of the divider setDividerLocation(300); @@ -188,7 +185,8 @@ private void updateModel(Goal g) { } final InfoTreeModel model; if (g != null) { - model = new InfoTreeModel(g, xmlResources, mainWindow); + var metaSpace = g.proof().getServices().getNamespaces().docs(); + model = new InfoTreeModel(g, metaSpace, mainWindow); g.proof().addProofDisposedListener(proofDisposedListener); lastShownGoalNode = g.node(); } else { 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/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 7fafa339ec6..00000000000 --- a/key.ui/src/main/resources/de/uka/ilkd/key/gui/help/functionExplanations.xml +++ /dev/null @@ -1,180 +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/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java b/keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java index 3138256f05b..6643ea9a430 100644 --- a/keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java @@ -54,10 +54,13 @@ public static ClosedBy findPreviousProof(List previousProofs, Node newNod var newTacletIndex = newNode.proof().allGoals().head().ruleAppIndex().tacletIndex(); Set newTaclets = newTacletIndex.allNoPosTacletApps(); var tacletsOk = true; - for (var taclet : tacletIndex.allNoPosTacletApps().stream() - .filter(x -> x.taclet().getOrigin() != null - && x.taclet().getOrigin().contains(proofFile)) - .toList()) { + final var list = tacletIndex.allNoPosTacletApps().stream() + .filter(x -> { + var origin = p.getServices().getNamespaces().docs().findOrigin(x.taclet()); + return origin != null && origin.contains(proofFile); + }) + .toList(); + for (NoPosTacletApp taclet : list) { if (newTaclets.stream().noneMatch(newTaclet -> Objects .equals(taclet.taclet().toString(), newTaclet.taclet().toString()))) { tacletsOk = false;