diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java index 9fd345eaf09..ce2d352f6af 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java @@ -19,6 +19,7 @@ import de.uka.ilkd.key.logic.JavaBlock; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.nparser.KeyAst; +import de.uka.ilkd.key.pp.Notation; import de.uka.ilkd.key.proof.*; import de.uka.ilkd.key.proof.mgt.SpecificationRepository; import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo; @@ -243,6 +244,14 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, ProofScriptEngine pse = new ProofScriptEngine(proof); pse.setInitiallySelectedGoal(goal); pse.getStateMap().getUserData().set(USER_DATA_JML_OBTAIN_VAR_MAP, obtainMap); + pse.getStateMap().getValueInjector().addConverter(Integer.class, ObtainAwareTerm.class, + oat -> { + String numberStr = Notation.NumLiteral.printNumberTerm(oat.term); + if (numberStr == null) + throw new ScriptException( + "Expected a number literal, but got: " + oat.term); + return Integer.parseInt(numberStr); + }); pse.getStateMap().getValueInjector().addConverter(JTerm.class, ObtainAwareTerm.class, oat -> oat.resolve(obtainMap, goal.proof().getServices())); // TODO: Perhaps have holes also in JML? @@ -251,6 +260,8 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, oat -> new TermWithHoles(oat.resolve(obtainMap, goal.proof().getServices()))); pse.getStateMap().getValueInjector().addConverter(boolean.class, ObtainAwareTerm.class, oat -> Boolean.parseBoolean(oat.term.toString())); + pse.getStateMap().getValueInjector().addConverter(String.class, ObtainAwareTerm.class, + oat -> oat.term.toString()); LOGGER.debug("---- Script"); LOGGER.debug(renderedProof.stream() .map(ScriptCommandAst::asCommandLine) diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/Notation.java b/key.core/src/main/java/de/uka/ilkd/key/pp/Notation.java index d6f29fcf676..2fac70c0cfc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/Notation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/Notation.java @@ -620,7 +620,7 @@ public void print(JTerm t, LogicPrinter sp) { * The standard concrete syntax for the number literal indicator `Z'. This is only used in the * `Pretty&Untrue' syntax. */ - static final class NumLiteral extends Notation { + public static final class NumLiteral extends Notation { public NumLiteral() { super(120); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/AutoCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/AutoCommand.java index 1b276a3bbf7..ec5a402b429 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/AutoCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/AutoCommand.java @@ -87,8 +87,12 @@ public void execute(ScriptCommandAst args) throws ScriptException, InterruptedEx OriginalValue ov = orgValues.get(entry.getKey()); if (ov != null) { ov.oldValue = activeStrategyProperties.getProperty(ov.settingName); - activeStrategyProperties.setProperty(ov.settingName, - "true".equals(entry.getValue()) ? ov.trueValue : ov.falseValue); + String key = state.getValueInjector().convert(entry.getValue(), String.class); + String value = ov.stringMap.get(key); + if (value == null) { + throw new ScriptException("Invalid value for " + entry.getKey() + ": " + key); + } + activeStrategyProperties.setProperty(ov.settingName, value); } } @@ -132,9 +136,14 @@ public void execute(ScriptCommandAst args) throws ScriptException, InterruptedEx private Map prepareOriginalValues() { var res = new HashMap(); + // Deprecated: Will be removed soon res.put("modelSearch", new OriginalValue(NON_LIN_ARITH_OPTIONS_KEY, NON_LIN_ARITH_COMPLETION, NON_LIN_ARITH_DEF_OPS)); + res.put("arithmetic", + new OriginalValue(NON_LIN_ARITH_OPTIONS_KEY, + Map.of("basic", NON_LIN_ARITH_NONE, "defOps", + NON_LIN_ARITH_DEF_OPS, "modelsearch", NON_LIN_ARITH_COMPLETION))); res.put("expandQueries", new OriginalValue(QUERYAXIOM_OPTIONS_KEY, QUERYAXIOM_ON, QUERYAXIOM_OFF)); res.put("classAxioms", @@ -210,9 +219,28 @@ public static class Parameters implements ValueInjector.VerifyableParameters { public @Nullable String breakpoint = null; @Flag(value = "modelsearch") - @Documentation("Enable model search. Better for some (types of) arithmetic problems. Sometimes a lot worse.") + @Deprecated + @Documentation("Deprecated. Use arithmetic=modelsearch instead.") public boolean modelSearch; + @Option(value = "arithmetic") + @Documentation(""" + Specify the arithmetic strategy to handle division and modulo operations: + - *`basic`*: Basic arithmetic support: + - Simplification of polynomial expressions + - Computation of Gröbner Bases for polynomials in the antecedent + - (Partial) Omega procedure for handling linear inequations" + "" + - *`defOps`*: Automatically expand defined symbols like: `/`, `%`, `jdiv`, `jmod` ..., `int_RANGE`, ... + In addition, inequations are multiplied with each other where the product is bounded by an existing + inequation (restricted such that termination is guaranteed). + - *`modelsearch`*: Support for non-linear inequations and model search. In addition, this performs + (a) multiplication of inequations with each other and (b) systematic case distinctions (cuts). + This method is guaranteed to find counterexamples for invalid goals that only contain polynomial + (in)equations. Such counterexamples turn up as trivially unprovable goals. It is also able to prove many + more valid goals involving (in)equations, but will in general not terminate on such goals. + """) + public @Nullable String arithmetic; + @Flag(value = "expandQueries") @Documentation("Automatically expand occurrences of query symbols using additional modalities on the sequent.") public boolean expandQueries; @@ -259,23 +287,23 @@ public void verifyParameters() throws IllegalArgumentException, InjectionExcepti private static final class OriginalValue { private final String settingName; - private final String trueValue; - private final String falseValue; + private final Map stringMap; private @Nullable String oldValue; private OriginalValue(String settingName, String trueValue, String falseValue) { - this.settingName = settingName; - this.trueValue = trueValue; + this(settingName, Map.of("true", trueValue, "false", falseValue)); + } - this.falseValue = falseValue; + private OriginalValue(String settingName, Map stringMap) { + this.settingName = settingName; + this.stringMap = stringMap; } @Override public String toString() { return "OriginalValue{" + "settingName='" + settingName + '\'' + - ", trueValue='" + trueValue + '\'' + - ", falseValue='" + falseValue + '\'' + + ", stringMap=" + stringMap + ", oldValue='" + oldValue + '\'' + '}'; } diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java index fd1d85147d9..2b24ff31042 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java @@ -185,7 +185,7 @@ public static ProofCollection automaticJavaDL() throws IOException { * pervar g = c.group("- one subprocess is created for each group * perFile-one subprocess is created for each file */ - settings.setForkMode(ForkMode.PERGROUP); + settings.setForkMode(ForkMode.NOFORK); /* * Enable or disable proof reloading. @@ -240,7 +240,7 @@ public static ProofCollection automaticJavaDL() throws IOException { * test can be restricted to these groups (for debugging). */ // runOnlyOn = group1, group2 (the space after each comma is mandatory) - // settings.setRunOnlyOn("performance, performancePOConstruction"); + settings.setRunOnlyOn("example-algos"); settings.setKeySettings(GenerateUnitTestsUtil.loadFromFile("automaticJAVADL.properties")); @@ -415,6 +415,10 @@ public static ProofCollection automaticJavaDL() throws IOException { g.provable("heap/verifyThis11_1_Maximum/project.key"); g.provable("heap/fm12_01_LRS/lcp.key"); g.provable("heap/SemanticSlicing/project.key"); + g.provable("heap/verifyThis26_01_hIndex/compute.key"); + g.provable("heap/verifyThis26_01_hIndex/compute_opt.key"); + g.provable("heap/verifyThis26_01_hIndex/lemma1.key"); + g.provable("heap/verifyThis26_01_hIndex/update.key"); g = c.group("funOfIF"); g.provable("heap/information_flow/ArrayList_contains.key"); diff --git a/key.ui/examples/heap/verifyThis26_01_hIndex/README.txt b/key.ui/examples/heap/verifyThis26_01_hIndex/README.txt new file mode 100644 index 00000000000..9834d42a340 --- /dev/null +++ b/key.ui/examples/heap/verifyThis26_01_hIndex/README.txt @@ -0,0 +1,16 @@ +example.name = H-Index Computation +example.file = hIndex.key +example.additionalFile.1 = src/HIndex.java +example.path = Benchmarks/VerifyThis2026 + +This is a KeY solution to challenge 1 of VerifyThis 2026. + +The h-Index is an (in)famous metrics in research. +This challenge deals with efficient computation and updates of h indices. + +See also challenge.pdf in the example directory. + +The example uses the recently introduced JML proof scripts. +You hence need to run it using the "Script-aware" automation button + +@author Mattias Ulbrich diff --git a/key.ui/examples/heap/verifyThis26_01_hIndex/challenge.pdf b/key.ui/examples/heap/verifyThis26_01_hIndex/challenge.pdf new file mode 100644 index 00000000000..d4a8a81c29f Binary files /dev/null and b/key.ui/examples/heap/verifyThis26_01_hIndex/challenge.pdf differ diff --git a/key.ui/examples/heap/verifyThis26_01_hIndex/compute.key b/key.ui/examples/heap/verifyThis26_01_hIndex/compute.key new file mode 100644 index 00000000000..91180c21a84 --- /dev/null +++ b/key.ui/examples/heap/verifyThis26_01_hIndex/compute.key @@ -0,0 +1,89 @@ +\profile "Java Profile"; + +\settings { + "Choice" : { + "JavaCard" : "JavaCard:on", + "Strings" : "Strings:on", + "assertions" : "assertions:on", + "bigint" : "bigint:on", + "finalFields" : "finalFields:immutable", + "floatRules" : "floatRules:strictfpOnly", + "initialisation" : "initialisation:disableStaticInitialisation", + "intRules" : "intRules:arithmeticSemanticsIgnoringOF", + "integerSimplificationRules" : "integerSimplificationRules:full", + "javaLoopTreatment" : "javaLoopTreatment:efficient", + "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off", + "methodExpansion" : "methodExpansion:modularOnly", + "modelFields" : "modelFields:treatAsAxiom", + "moreSeqRules" : "moreSeqRules:off", + "permissions" : "permissions:off", + "programRules" : "programRules:Java", + "reach" : "reach:on", + "runtimeExceptions" : "runtimeExceptions:ban", + "sequences" : "sequences:on", + "soundDefaultContracts" : "soundDefaultContracts:on" + }, + "Labels" : { + "UseOriginLabels" : true + }, + "NewSMT" : { + + }, + "SMTSettings" : { + "SelectedTaclets" : [ + + ], + "UseBuiltUniqueness" : false, + "explicitTypeHierarchy" : false, + "instantiateHierarchyAssumptions" : true, + "integersMaximum" : 2147483645, + "integersMinimum" : -2147483645, + "invariantForall" : false, + "maxGenericSorts" : 2, + "useConstantsForBigOrSmallIntegers" : true, + "useUninterpretedMultiplication" : true + }, + "Strategy" : { + "ActiveStrategy" : "Modular JavaDL Strategy", + "MaximumNumberOfAutomaticApplications" : 200000, + "Timeout" : -1, + "options" : { + "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF", + "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL", + "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE", + "DEP_OPTIONS_KEY" : "DEP_ON", + "HEAP_REDUCTION_OPTIONS_KEY" : "HEAP_REDUCTION_NORMAL", + "LOOP_OPTIONS_KEY" : "LOOP_INVARIANT", + "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT", + "MPS_OPTIONS_KEY" : "MPS_MERGE", + "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS", + "OSS_OPTIONS_KEY" : "OSS_ON", + "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS", + "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON", + "QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF", + "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED", + "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT", + "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER", + "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF", + "TRIGGERS_OPTIONS_KEY" : "TRIGGERS_BEST", + "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF", + "VBT_PHASE" : "VBT_SYM_EX" + } + } +} + + +\javaSource "src"; + +\proofObligation +// +{ + "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + "contract" : "HIndex[HIndex::compute([I)].JML normal_behavior operation contract.0", + "name" : "HIndex[HIndex::compute([I)].JML normal_behavior operation contract.0" +} + +\proofScript { macro "script-auto"; } + diff --git a/key.ui/examples/heap/verifyThis26_01_hIndex/compute_opt.key b/key.ui/examples/heap/verifyThis26_01_hIndex/compute_opt.key new file mode 100644 index 00000000000..cf10da1e1b0 --- /dev/null +++ b/key.ui/examples/heap/verifyThis26_01_hIndex/compute_opt.key @@ -0,0 +1,89 @@ +\profile "Java Profile"; + +\settings { + "Choice" : { + "JavaCard" : "JavaCard:on", + "Strings" : "Strings:on", + "assertions" : "assertions:on", + "bigint" : "bigint:on", + "finalFields" : "finalFields:immutable", + "floatRules" : "floatRules:strictfpOnly", + "initialisation" : "initialisation:disableStaticInitialisation", + "intRules" : "intRules:arithmeticSemanticsIgnoringOF", + "integerSimplificationRules" : "integerSimplificationRules:full", + "javaLoopTreatment" : "javaLoopTreatment:efficient", + "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off", + "methodExpansion" : "methodExpansion:modularOnly", + "modelFields" : "modelFields:treatAsAxiom", + "moreSeqRules" : "moreSeqRules:off", + "permissions" : "permissions:off", + "programRules" : "programRules:Java", + "reach" : "reach:on", + "runtimeExceptions" : "runtimeExceptions:ban", + "sequences" : "sequences:on", + "soundDefaultContracts" : "soundDefaultContracts:on" + }, + "Labels" : { + "UseOriginLabels" : true + }, + "NewSMT" : { + + }, + "SMTSettings" : { + "SelectedTaclets" : [ + + ], + "UseBuiltUniqueness" : false, + "explicitTypeHierarchy" : false, + "instantiateHierarchyAssumptions" : true, + "integersMaximum" : 2147483645, + "integersMinimum" : -2147483645, + "invariantForall" : false, + "maxGenericSorts" : 2, + "useConstantsForBigOrSmallIntegers" : true, + "useUninterpretedMultiplication" : true + }, + "Strategy" : { + "ActiveStrategy" : "Modular JavaDL Strategy", + "MaximumNumberOfAutomaticApplications" : 200000, + "Timeout" : -1, + "options" : { + "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF", + "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL", + "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE", + "DEP_OPTIONS_KEY" : "DEP_ON", + "HEAP_REDUCTION_OPTIONS_KEY" : "HEAP_REDUCTION_NORMAL", + "LOOP_OPTIONS_KEY" : "LOOP_INVARIANT", + "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT", + "MPS_OPTIONS_KEY" : "MPS_MERGE", + "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS", + "OSS_OPTIONS_KEY" : "OSS_ON", + "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS", + "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON", + "QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF", + "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED", + "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT", + "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER", + "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF", + "TRIGGERS_OPTIONS_KEY" : "TRIGGERS_BEST", + "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF", + "VBT_PHASE" : "VBT_SYM_EX" + } + } +} + + +\javaSource "src"; + +\proofObligation +// +{ + "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + "contract" : "HIndex[HIndex::compute_opt([I)].JML normal_behavior operation contract.0", + "name" : "HIndex[HIndex::compute_opt([I)].JML normal_behavior operation contract.0" +} + +\proofScript { macro "script-auto"; } + diff --git a/key.ui/examples/heap/verifyThis26_01_hIndex/hIndex.key b/key.ui/examples/heap/verifyThis26_01_hIndex/hIndex.key new file mode 100644 index 00000000000..b0726ad3967 --- /dev/null +++ b/key.ui/examples/heap/verifyThis26_01_hIndex/hIndex.key @@ -0,0 +1,80 @@ +\profile "Java Profile"; + +\settings { + "Choice" : { + "JavaCard" : "JavaCard:on", + "Strings" : "Strings:on", + "assertions" : "assertions:on", + "bigint" : "bigint:on", + "finalFields" : "finalFields:immutable", + "floatRules" : "floatRules:strictfpOnly", + "initialisation" : "initialisation:disableStaticInitialisation", + "intRules" : "intRules:arithmeticSemanticsIgnoringOF", + "integerSimplificationRules" : "integerSimplificationRules:full", + "javaLoopTreatment" : "javaLoopTreatment:efficient", + "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off", + "methodExpansion" : "methodExpansion:modularOnly", + "modelFields" : "modelFields:treatAsAxiom", + "moreSeqRules" : "moreSeqRules:off", + "permissions" : "permissions:off", + "programRules" : "programRules:Java", + "reach" : "reach:on", + "runtimeExceptions" : "runtimeExceptions:ban", + "sequences" : "sequences:on", + "soundDefaultContracts" : "soundDefaultContracts:on" + }, + "Labels" : { + "UseOriginLabels" : true + }, + "NewSMT" : { + + }, + "SMTSettings" : { + "SelectedTaclets" : [ + + ], + "UseBuiltUniqueness" : false, + "explicitTypeHierarchy" : false, + "instantiateHierarchyAssumptions" : true, + "integersMaximum" : 2147483645, + "integersMinimum" : -2147483645, + "invariantForall" : false, + "maxGenericSorts" : 2, + "useConstantsForBigOrSmallIntegers" : true, + "useUninterpretedMultiplication" : true + }, + "Strategy" : { + "ActiveStrategy" : "Modular JavaDL Strategy", + "MaximumNumberOfAutomaticApplications" : 200000, + "Timeout" : -1, + "options" : { + "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF", + "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL", + "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE", + "DEP_OPTIONS_KEY" : "DEP_ON", + "HEAP_REDUCTION_OPTIONS_KEY" : "HEAP_REDUCTION_NORMAL", + "LOOP_OPTIONS_KEY" : "LOOP_INVARIANT", + "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT", + "MPS_OPTIONS_KEY" : "MPS_MERGE", + "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS", + "OSS_OPTIONS_KEY" : "OSS_ON", + "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS", + "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON", + "QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF", + "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED", + "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT", + "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER", + "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF", + "TRIGGERS_OPTIONS_KEY" : "TRIGGERS_BEST", + "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF", + "VBT_PHASE" : "VBT_SYM_EX" + } + } +} + + +\javaSource "src"; + +\chooseContract diff --git a/key.ui/examples/heap/verifyThis26_01_hIndex/lemma1.key b/key.ui/examples/heap/verifyThis26_01_hIndex/lemma1.key new file mode 100644 index 00000000000..36d1c53011a --- /dev/null +++ b/key.ui/examples/heap/verifyThis26_01_hIndex/lemma1.key @@ -0,0 +1,86 @@ +\profile "Java Profile"; + +\settings { + "Choice" : { + "JavaCard" : "JavaCard:on", + "Strings" : "Strings:on", + "assertions" : "assertions:on", + "bigint" : "bigint:on", + "finalFields" : "finalFields:immutable", + "floatRules" : "floatRules:strictfpOnly", + "initialisation" : "initialisation:disableStaticInitialisation", + "intRules" : "intRules:arithmeticSemanticsIgnoringOF", + "integerSimplificationRules" : "integerSimplificationRules:full", + "javaLoopTreatment" : "javaLoopTreatment:efficient", + "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off", + "methodExpansion" : "methodExpansion:modularOnly", + "modelFields" : "modelFields:treatAsAxiom", + "moreSeqRules" : "moreSeqRules:off", + "permissions" : "permissions:off", + "programRules" : "programRules:Java", + "reach" : "reach:on", + "runtimeExceptions" : "runtimeExceptions:ban", + "sequences" : "sequences:on", + "soundDefaultContracts" : "soundDefaultContracts:on" + }, + "Labels" : { + "UseOriginLabels" : true + }, + "NewSMT" : { + + }, + "SMTSettings" : { + "SelectedTaclets" : [ + + ], + "UseBuiltUniqueness" : false, + "explicitTypeHierarchy" : false, + "instantiateHierarchyAssumptions" : true, + "integersMaximum" : 2147483645, + "integersMinimum" : -2147483645, + "invariantForall" : false, + "maxGenericSorts" : 2, + "useConstantsForBigOrSmallIntegers" : true, + "useUninterpretedMultiplication" : true + }, + "Strategy" : { + "ActiveStrategy" : "Modular JavaDL Strategy", + "MaximumNumberOfAutomaticApplications" : 200000, + "Timeout" : -1, + "options" : { + "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF", + "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL", + "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE", + "DEP_OPTIONS_KEY" : "DEP_ON", + "HEAP_REDUCTION_OPTIONS_KEY" : "HEAP_REDUCTION_NORMAL", + "LOOP_OPTIONS_KEY" : "LOOP_INVARIANT", + "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT", + "MPS_OPTIONS_KEY" : "MPS_MERGE", + "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS", + "OSS_OPTIONS_KEY" : "OSS_ON", + "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS", + "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON", + "QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF", + "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED", + "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT", + "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER", + "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF", + "TRIGGERS_OPTIONS_KEY" : "TRIGGERS_BEST", + "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF", + "VBT_PHASE" : "VBT_SYM_EX" + } + } +} + + +\javaSource "src"; + +\proofObligation +// +{ + "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + "contract" : "HIndex[HIndex::lemma1(int,[I)].JML normal_behavior operation contract.0", + "name" : "HIndex[HIndex::lemma1(int,[I)].JML normal_behavior operation contract.0" +} diff --git a/key.ui/examples/heap/verifyThis26_01_hIndex/src/HIndex.java b/key.ui/examples/heap/verifyThis26_01_hIndex/src/HIndex.java new file mode 100644 index 00000000000..e9297530e1b --- /dev/null +++ b/key.ui/examples/heap/verifyThis26_01_hIndex/src/HIndex.java @@ -0,0 +1,226 @@ +/** + * This is a KeY solution to challenge 1 of VerifyThis 2026. + * originally proposed by Jean-Christophe Filliâtre∗ and Mário Pereira + * + * Ada is a young researcher who is actively keeping track of her + * citation counts. She keeps them is an array, which is sorted in + * reverse order. These days, it looks as follows: + * + * 12 5 3 3 3 3 2 1 0 0 + * + * In other words, her most cited paper is cited 12 times, the second + * most cited paper is cited 5 times, and so on, for a total of 10 + * papers. Ada notices that she has three papers that are cited at least + * three times each, but that she is not yet famous enough to have four + * papers cited at least four times each. She defines her score as the + * greatest number h such that at least h elements in the array are + * greater or equal to h. Ada just invented the h-index — but luckily for + * her, her administration has not yet come with the same idea. Ada is a + * good programmer, so she quickly writes a C function to compute the h- + * index (function compute in Fig. 1). A moment later, she realizes that + * one of the most fundamental algorithm can be used to compute it more + * efficiently, and she writes a second C function to compute the h-index + * (function compute opt in Fig. 1). Whenever Ada discovers a new + * citation to one of her papers, she updates her array. She locates the + * position in the array corresponding to the paper, increments the value + * at that position, and then moves it to the left until the array is + * sorted again. For instance, if her paper at position 5 (counting from + * 0) gets a new citation, the array ends up in the following state: + * + * 12 5 4 3 3 3 2 1 0 0 + * + * The h-index is still 3, though. If later, the paper at position 4 gets + * a new citation, then the array is updated as follows + * + * 12 5 4 4 3 3 2 1 0 0 + * + * and this times the h-index becomes 4. + * + * Ada figures out that updating both the array and the h-index value can + * be conve- niently done at the same time. This is function update in + * Fig. 1, where parameter h is the current h-index value and i is the + * index of the count to be incremented. The function updates the array + * and returns the new h-index value. + * + * Originally proposed by Jean-Christophe Filliâtre∗ and Mário Pereira, + * curated by Thibault Dardinier and Sacha-Elie Ayoun, + * KeY solution by Mattias Ulbrich (mainly to showcase JML proof scripts). + */ +class HIndex { + + /*@ public normal_behaviour + @ requires (\forall int i,j; 0 <= i < j < a.length; a[i] >= a[j]); + @ ensures (\forall int x; 0 <= x < \result; a[x] > x); + @ ensures (\num_of int i; 0 <= i < a.length; a[i] >= \result) >= \result; + @ ensures (\num_of int i; 0 <= i < a.length; a[i] >= \result + 1) < \result + 1; + @ ensures 0 <= \result <= a.length; + @ ensures \result == a.length || a[\result] <= \result; + @ ensures \result == 0 || a[\result-1] >= \result; + @ assignable \strictly_nothing; + @*/ + static int compute(int a[]) { + int h = 0; + /*@ loop_invariant 0 <= h <= a.length; + @ loop_invariant h == 0 || a[h-1] >= h; + @ loop_invariant (\forall int x; 0 <= x < h; a[x] >= h); + @ loop_invariant (\num_of int i; 0 <= i < h; a[i] >= h) == h; + @ assignable \strictly_nothing; + @ decreases a.length - h + 1; + @*/ + while (h < a.length && h < a[h]) + h++; + + //@ assert h == a.length || a[h] <= h ; + + /*@ assert (\num_of int i; 0 <= i < h; a[i] >= h + 1) <= h \by { + @ oss; + @ rule "bsum_num_of_bounds" occ: 1; + @ auto; + @ }; + @*/ + + /*@ assert (\num_of int i; 0 <= i < a.length; a[i] >= h) == + @ (\num_of int i; 0 <= i < h; a[i] >= h) + + @ (\num_of int i; h <= i < a.length; a[i] >= h); + @*/ + + /*@ assert (\num_of int i; 0 <= i < a.length; a[i] >= h + 1) == + @ (\num_of int i; 0 <= i < h; a[i] >= h + 1) + + @ (\num_of int i; h <= i < a.length; a[i] >= h + 1); + @*/ + + /*@ assert (\num_of int i; 0 <= i < a.length; a[i] >= h) >= h \by { + @ oss; + @ rule "bsum_positive1" occ: 0 on: (\num_of int i; h <= i < a.length; a[i] >= h); + @ auto; + @ }; + @*/ + + //@ assert (\num_of int i; h <= i < a.length; a[i] >= h + 1) == 0; + + return h; + } + + // the same, more efficiently + /*@ public normal_behaviour + @ requires (\forall int i,j; 0 <= i < j < a.length; a[i] >= a[j]); + @ ensures (\forall int x; 0 <= x < \result; a[x] > x); + @ ensures (\num_of int i; 0 <= i < a.length; a[i] >= \result) >= \result; + @ ensures (\num_of int i; 0 <= i < a.length; a[i] >= \result + 1) < \result + 1; + @ ensures \result == a.length || a[\result] <= \result; + @ ensures \result == 0 || a[\result-1] >= \result; + @ assignable \strictly_nothing; + @*/ + static int compute_opt(int a[]) { + int lo = 0, hi = a.length; + + /*@ loop_invariant 0 <= lo <= hi <= a.length; + @ loop_invariant lo == 0 || a[lo-1] >= lo; + @ loop_invariant (\forall int x; 0 <= x < lo; a[x] >= lo); + @ loop_invariant (\forall int x; hi <= x < a.length; a[x] <= hi); + @ assignable \strictly_nothing; + @ decreases hi - lo + 1; + @*/ + while (lo < hi) { + int mid = lo + (hi - lo) / 2; + if (a[mid] <= mid) hi = mid; + else lo = mid + 1; + } + + lemma1(lo, a); + + //@ assert (\num_of int i; 0 <= i < lo; a[i] >= lo) == lo; + + /*@ assert (\num_of int i; 0 <= i < lo; a[i] >= lo + 1) <= lo \by { + @ oss; + @ rule "bsum_num_of_bounds" occ: 1; + @ auto; + @ }; + @*/ + + /*@ assert (\num_of int i; 0 <= i < a.length; a[i] >= lo) == + @ (\num_of int i; 0 <= i < lo; a[i] >= lo) + + @ (\num_of int i; lo <= i < a.length; a[i] >= lo); + @*/ + + /*@ assert (\num_of int i; 0 <= i < a.length; a[i] >= lo + 1) == + @ (\num_of int i; 0 <= i < lo; a[i] >= lo + 1) + + @ (\num_of int i; lo <= i < a.length; a[i] >= lo + 1); + @*/ + + /*@ assert (\num_of int i; 0 <= i < a.length; a[i] >= lo) >= lo \by { + @ oss; + @ rule "bsum_positive1" occ: 0 on: (\num_of int i; lo <= i < a.length; a[i] >= lo); + @ auto; + @ }; + @*/ + + //@ assert (\num_of int i; lo <= i < a.length; a[i] >= lo + 1) == 0; + + return lo; + } + + /*@ public normal_behaviour + @ requires (\forall int i; 0 <= i < lo; a[i] >= lo); + @ requires 0 <= lo <= a.length; + @ ensures (\num_of int i; 0 <= i < lo; a[i] >= lo) == lo; + @ assignable \strictly_nothing; + @*/ + static void lemma1(int lo, int[] a) { + /*@ loop_invariant (\num_of int i; 0 <= i < r; a[i] >= lo) == r; + @ loop_invariant 0 <= r <= lo; + @ decreases lo - r; + @ assignable \strictly_nothing; + @*/ + for(int r = 0; r < lo; r++) {} + } + + /*@ normal_behaviour + @ requires 0 <= i < a.length; + @ requires 0 <= h <= a.length; + @ requires (\forall int i,j; 0 <= i < j < a.length; a[i] >= a[j]); + @ requires h == 0 || a[h-1] >= h; + @ requires h == a.length || a[h] <= h; + @ ensures \result == 0 || a[\result-1] >= \result; + @ ensures \result == a.length || a[\result] <= \result; + @ ensures 0 <= \result <= a.length; + @ ensures (\exists int p; 0 <= p < a.length; \old(a[p] == a[i]) && + @ a[p] == \old(a[p] + 1) && + @ (\forall int q; 0 <= q < a.length && q != p; a[q] == \old(a[q]))); + @ ensures (\forall int i,j; 0 <= i < j < a.length; a[i] >= a[j]); + @ assignable a[*]; + @*/ + static int update(int a[], int h, int i) { + int x = a[i]; + int lo = 0, hi = i; + /*@ loop_invariant 0 <= lo <= hi < a.length; + @ loop_invariant (\forall int f; 0 <= f < lo; a[f] > x); + @ loop_invariant (\forall int g; hi <= g <= i; a[g] == x); + @ loop_invariant a[i] == a[hi]; + @ loop_invariant lo > 0 ==> a[lo-1] > a[i]; + @ assignable \strictly_nothing; + @ decreases hi - lo + 1; + @*/ + while (lo < hi) { + //@ ghost int diff = hi - lo; + + int mid; + //@ ensures \dl_mod(diff,2) == 0 ==> 2*mid == 2*lo + diff; + //@ ensures \dl_mod(diff,2) == 1 ==> 2*mid == 2*lo + diff - 1; + //@ signals (Throwable e) false; + //@ assignable \strictly_nothing; + { mid = lo + (hi-lo) / 2; } + + if (a[mid] == x) hi = mid; + else lo = mid + 1; + } + + a[lo]++; + + if (lo == h && a[lo] == h+1) { + return h+1; + } else { + return h; + } + } +} diff --git a/key.ui/examples/heap/verifyThis26_01_hIndex/update.key b/key.ui/examples/heap/verifyThis26_01_hIndex/update.key new file mode 100644 index 00000000000..10384f1315b --- /dev/null +++ b/key.ui/examples/heap/verifyThis26_01_hIndex/update.key @@ -0,0 +1,85 @@ +\profile "Java Profile"; + +\settings { + "Choice" : { + "JavaCard" : "JavaCard:on", + "Strings" : "Strings:on", + "assertions" : "assertions:on", + "bigint" : "bigint:on", + "finalFields" : "finalFields:immutable", + "floatRules" : "floatRules:strictfpOnly", + "initialisation" : "initialisation:disableStaticInitialisation", + "intRules" : "intRules:arithmeticSemanticsIgnoringOF", + "integerSimplificationRules" : "integerSimplificationRules:full", + "javaLoopTreatment" : "javaLoopTreatment:efficient", + "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off", + "methodExpansion" : "methodExpansion:modularOnly", + "modelFields" : "modelFields:treatAsAxiom", + "moreSeqRules" : "moreSeqRules:off", + "permissions" : "permissions:off", + "programRules" : "programRules:Java", + "reach" : "reach:on", + "runtimeExceptions" : "runtimeExceptions:ban", + "sequences" : "sequences:on", + "soundDefaultContracts" : "soundDefaultContracts:on" + }, + "Labels" : { + "UseOriginLabels" : true + }, + "NewSMT" : { + + }, + "SMTSettings" : { + "SelectedTaclets" : [ + + ], + "UseBuiltUniqueness" : false, + "explicitTypeHierarchy" : false, + "instantiateHierarchyAssumptions" : true, + "integersMaximum" : 2147483645, + "integersMinimum" : -2147483645, + "invariantForall" : false, + "maxGenericSorts" : 2, + "useConstantsForBigOrSmallIntegers" : true, + "useUninterpretedMultiplication" : true + }, + "Strategy" : { + "ActiveStrategy" : "Modular JavaDL Strategy", + "MaximumNumberOfAutomaticApplications" : 200000, + "Timeout" : -1, + "options" : { + "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF", + "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL", + "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE", + "DEP_OPTIONS_KEY" : "DEP_ON", + "HEAP_REDUCTION_OPTIONS_KEY" : "HEAP_REDUCTION_NORMAL", + "LOOP_OPTIONS_KEY" : "LOOP_INVARIANT", + "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT", + "MPS_OPTIONS_KEY" : "MPS_MERGE", + "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS", + "OSS_OPTIONS_KEY" : "OSS_ON", + "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS", + "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON", + "QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF", + "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED", + "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT", + "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER", + "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF", + "TRIGGERS_OPTIONS_KEY" : "TRIGGERS_BEST", + "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF", + "VBT_PHASE" : "VBT_SYM_EX" + } + } +} + + +\javaSource "src"; + +\proofObligation +{ + "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + "contract" : "HIndex[HIndex::update([I,int,int)].JML normal_behavior operation contract.0", + "name" : "HIndex[HIndex::update([I,int,int)].JML normal_behavior operation contract.0" +} diff --git a/key.ui/examples/index/samplesIndex.txt b/key.ui/examples/index/samplesIndex.txt index 666003ded24..4a217f00039 100644 --- a/key.ui/examples/index/samplesIndex.txt +++ b/key.ui/examples/index/samplesIndex.txt @@ -98,6 +98,8 @@ heap/vacid0_01_SparseArray/README.txt ## WeideEtAl heap/WeideEtAl_01_AddAndMultiply/README.txt heap/WeideEtAl_02_BinarySearch/README.txt +## VerifyThis 2026 +heap/verifyThis26_01_hIndex/README.txt # Information Flow heap/information_flow/README-ArrayList.txt