m4ndeb2r · mattulbrich · Aug 7, 2021 · Aug 7, 2021 · Aug 7, 2021 · Aug 9, 2021
diff --git a/README.md b/README.md
@@ -67,6 +67,17 @@ Now, the class can be loaded in KeY.
 
 Note: The KeY plugin Eclipse complains about the `remove` method on line 979 (Cycle detected). However, this does not seem to be a real problem. Threrefore, it is ignored. 
 
+## Start the stand-alone KeY tool
+Version 2.7 of the stand-alone KeY tool is provided in the directory key2.7 this repository. First, unzip the file `key.zip` in your working directory of you choice. Then, start the tool in one of the following ways:
+* On the command line, type: 
+  `$ cd ./key/key`
+  `$ ./gradlew :key.ui:run --parallel`
+  or
+* `$ cd ./key/key`
+  `$ ./gradlew shadowJar`
+  `$ java -Xmx8G -jar ./key.ui/build/libs/key-2.9-exe.jar` 
+
+The second option allows you to claim extra memory resources (in this example, 8GB). 
+
 ## Load VerifiedIdentityHashMap in KeY
-* select your project, and right-click on it for the context menu
-* from the context menu, choose Load Project.
+* Open the `IdentityHashMap.key` file that is available in the root of the project.
diff --git a/jre/java/lang/Object.java b/jre/java/lang/Object.java
@@ -7,12 +7,11 @@ public class Object {
    /**
     * @generated
     */
-   /*@ public behavior
-     @ requires true;
-     @ ensures true;
-     @ assignable \everything;
+   /*@ public normal_behavior
+     @   requires true;
+     @   ensures \result == this.equals(param0);
      @*/
-   public Object();
+   public /*@ helper strictly_pure @*/ boolean equals(/*@ nullable */ java.lang.Object param0);
 
    /**
     * @generated
@@ -22,7 +21,7 @@ public class Object {
      @ ensures true;
      @ assignable \everything;
      @*/
-   protected java.lang.Object[] clone();
+   protected java.lang.Object clone() throws java.lang.CloneNotSupportedException;
 
    /**
     * @generated
@@ -32,7 +31,7 @@ public class Object {
      @ ensures true;
      @ assignable \everything;
      @*/
-   public boolean equals(java.lang.Object param0);
+   public final java.lang.Class getClass();
 
    /**
     * @generated
@@ -54,16 +53,6 @@ public class Object {
      @*/
    public java.lang.String toString();
 
-   /**
-    * @generated
-    */
-   /*@ public behavior
-     @ requires true;
-     @ ensures true;
-     @ assignable \everything;
-     @*/
-   public final java.lang.Class getClass();
-
    /**
     * @generated
     */
@@ -123,4 +112,4 @@ public class Object {
      @ assignable \everything;
      @*/
    protected void finalize() throws java.lang.Throwable;
-}
+}
diff --git a/key2.7/key.zip b/key2.7/key.zip
diff --git a/...il.VerifiedIdentityHashMap__capacity(int)).JML normal_behavior operation contract.0.proof b/...il.VerifiedIdentityHashMap__capacity(int)).JML normal_behavior operation contract.0.proof
diff --git a/...l.VerifiedIdentityHashMap(java.util.Map__clear()).JML behavior operation contract.0.proof b/...l.VerifiedIdentityHashMap(java.util.Map__clear()).JML behavior operation contract.0.proof
diff --git a/...ava.util.VerifiedIdentityHashMap__clear()).JML normal_behavior operation contract.0.proof b/...ava.util.VerifiedIdentityHashMap__clear()).JML normal_behavior operation contract.0.proof
diff --git a/...ityHashMap__containsKey(java.lang.Object)).JML normal_behavior operation contract.0.proof b/...ityHashMap__containsKey(java.lang.Object)).JML normal_behavior operation contract.0.proof
diff --git a/...dentityHashMap__VerifiedIdentityHashMap()).JML normal_behavior operation contract.0.proof b/...dentityHashMap__VerifiedIdentityHashMap()).JML normal_behavior operation contract.0.proof
diff --git a/...a.util.VerifiedIdentityHashMap__init(int)).JML normal_behavior operation contract.0.proof b/...a.util.VerifiedIdentityHashMap__init(int)).JML normal_behavior operation contract.0.proof
diff --git a/...VerifiedIdentityHashMap(java.util.Map__isEmpty()).JML behavior operation contract.0.proof b/...VerifiedIdentityHashMap(java.util.Map__isEmpty()).JML behavior operation contract.0.proof
@@ -2,7 +2,7 @@
 
 \settings {
 "#Proof-Settings-Config-File
-#Fri Jun 18 12:43:59 CEST 2021
+#Sat Aug 28 15:04:36 CEST 2021
 [Labels]UseOriginLabels=true
 [StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON
 [SMTSettings]invariantForall=false
@@ -11,7 +11,7 @@
 [StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
 [StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
 [Choice]DefaultChoices=assertions-assertions\\:safe , initialisation-initialisation\\:disableStaticInitialisation , intRules-intRules\\:javaSemantics , programRules-programRules\\:Java , runtimeExceptions-runtimeExceptions\\:ban , JavaCard-JavaCard\\:on , Strings-Strings\\:on , modelFields-modelFields\\:treatAsAxiom , bigint-bigint\\:on , sequences-sequences\\:on , moreSeqRules-moreSeqRules\\:off , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , permissions-permissions\\:off , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\\:off , methodExpansion-methodExpansion\\:modularOnly , javaLoopTreatment-javaLoopTreatment\\:efficient
-[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_NONE
+[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_SCOPE_INV_TACLET
 [StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
 [SMTSettings]UseBuiltUniqueness=false
 [SMTSettings]explicitTypeHierarchy=false
@@ -20,7 +20,7 @@
 [SMTSettings]SelectedTaclets=
 [StrategyProperty]DEP_OPTIONS_KEY=DEP_ON
 [StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
-[Strategy]MaximumNumberOfAutomaticApplications=100000
+[Strategy]MaximumNumberOfAutomaticApplications=50000
 [StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
 [StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_DELAYED
 [SMTSettings]useConstantsForBigOrSmallIntegers=true
@@ -49,7 +49,7 @@
 \include "../../../../functions.key";
 
 \proofObligation "#Proof Obligation Settings
-#Fri Jun 18 12:43:59 CEST 2021
+#Sat Aug 28 15:04:36 CEST 2021
 contract=java.util.VerifiedIdentityHashMap[java.util.Map\\:\\:isEmpty()].JML behavior operation contract.0
 name=java.util.VerifiedIdentityHashMap[java.util.Map\\:\\:isEmpty()].JML behavior operation contract.0
 class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO
@@ -58,7 +58,7 @@ class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO
 \proof {
 (keyLog "0" (keyUser "martindeboer" ) (keyVersion "a6034b00a3"))
 
-(autoModeTime "149")
+(autoModeTime "46")
 
 (branch "dummy ID"
 (rule "instanceof_static_type" (formula "1") (term "0,0,0,1,1,0,0,1,1") (newnames "self,result,exc,heapAtPre,o,f"))

diff --git a/...a.util.VerifiedIdentityHashMap__isEmpty()).JML normal_behavior operation contract.0.proof b/...a.util.VerifiedIdentityHashMap__isEmpty()).JML normal_behavior operation contract.0.proof
@@ -2,7 +2,7 @@
 
 \settings {
 "#Proof-Settings-Config-File
-#Fri Jun 18 12:44:57 CEST 2021
+#Sat Aug 28 15:05:05 CEST 2021
 [Labels]UseOriginLabels=true
 [StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON
 [SMTSettings]invariantForall=false
@@ -11,7 +11,7 @@
 [StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
 [StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
 [Choice]DefaultChoices=assertions-assertions\\:safe , initialisation-initialisation\\:disableStaticInitialisation , intRules-intRules\\:javaSemantics , programRules-programRules\\:Java , runtimeExceptions-runtimeExceptions\\:ban , JavaCard-JavaCard\\:on , Strings-Strings\\:on , modelFields-modelFields\\:treatAsAxiom , bigint-bigint\\:on , sequences-sequences\\:on , moreSeqRules-moreSeqRules\\:off , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , permissions-permissions\\:off , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\\:off , methodExpansion-methodExpansion\\:modularOnly , javaLoopTreatment-javaLoopTreatment\\:efficient
-[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_NONE
+[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_SCOPE_INV_TACLET
 [StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
 [SMTSettings]UseBuiltUniqueness=false
 [SMTSettings]explicitTypeHierarchy=false
@@ -20,7 +20,7 @@
 [SMTSettings]SelectedTaclets=
 [StrategyProperty]DEP_OPTIONS_KEY=DEP_ON
 [StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
-[Strategy]MaximumNumberOfAutomaticApplications=100000
+[Strategy]MaximumNumberOfAutomaticApplications=50000
 [StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
 [StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_DELAYED
 [SMTSettings]useConstantsForBigOrSmallIntegers=true
@@ -49,7 +49,7 @@
 \include "../../../../functions.key";
 
 \proofObligation "#Proof Obligation Settings
-#Fri Jun 18 12:44:57 CEST 2021
+#Sat Aug 28 15:05:05 CEST 2021
 contract=java.util.VerifiedIdentityHashMap[java.util.VerifiedIdentityHashMap\\:\\:isEmpty()].JML normal_behavior operation contract.0
 name=java.util.VerifiedIdentityHashMap[java.util.VerifiedIdentityHashMap\\:\\:isEmpty()].JML normal_behavior operation contract.0
 class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO
@@ -58,7 +58,7 @@ class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO
 \proof {
 (keyLog "0" (keyUser "martindeboer" ) (keyVersion "a6034b00a3"))
 
-(autoModeTime "96")
+(autoModeTime "56")
 
 (branch "dummy ID"
 (rule "impRight" (formula "1") (newnames "self,result,exc,heapAtPre,o,f"))

diff --git a/...entityHashMap__maskNull(java.lang.Object)).JML normal_behavior operation contract.0.proof b/...entityHashMap__maskNull(java.lang.Object)).JML normal_behavior operation contract.0.proof
@@ -2,7 +2,7 @@
 
 \settings {
 "#Proof-Settings-Config-File
-#Fri Jun 04 15:11:07 CEST 2021
+#Sat Aug 28 15:02:53 CEST 2021
 [Labels]UseOriginLabels=true
 [StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON
 [SMTSettings]invariantForall=false
@@ -11,7 +11,7 @@
 [StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
 [StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
 [Choice]DefaultChoices=assertions-assertions\\:safe , initialisation-initialisation\\:disableStaticInitialisation , intRules-intRules\\:javaSemantics , programRules-programRules\\:Java , runtimeExceptions-runtimeExceptions\\:ban , JavaCard-JavaCard\\:on , Strings-Strings\\:on , modelFields-modelFields\\:treatAsAxiom , bigint-bigint\\:on , sequences-sequences\\:on , moreSeqRules-moreSeqRules\\:off , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , permissions-permissions\\:off , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\\:off , methodExpansion-methodExpansion\\:modularOnly , javaLoopTreatment-javaLoopTreatment\\:efficient
-[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_NONE
+[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_SCOPE_INV_TACLET
 [StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
 [SMTSettings]UseBuiltUniqueness=false
 [SMTSettings]explicitTypeHierarchy=false
@@ -20,7 +20,7 @@
 [SMTSettings]SelectedTaclets=
 [StrategyProperty]DEP_OPTIONS_KEY=DEP_ON
 [StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
-[Strategy]MaximumNumberOfAutomaticApplications=100000
+[Strategy]MaximumNumberOfAutomaticApplications=50000
 [StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
 [StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_DELAYED
 [SMTSettings]useConstantsForBigOrSmallIntegers=true
@@ -49,16 +49,17 @@
 \include "../../../../functions.key";
 
 \proofObligation "#Proof Obligation Settings
-#Fri Jun 04 15:11:07 CEST 2021
+#Sat Aug 28 15:02:53 CEST 2021
 contract=java.util.VerifiedIdentityHashMap[java.util.VerifiedIdentityHashMap\\:\\:maskNull(java.lang.Object)].JML normal_behavior operation contract.0
 name=java.util.VerifiedIdentityHashMap[java.util.VerifiedIdentityHashMap\\:\\:maskNull(java.lang.Object)].JML normal_behavior operation contract.0
 class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO
 ";
 
 \proof {
 (keyLog "0" (keyUser "martindeboer" ) (keyVersion "a6034b00a3"))
+(keyLog "1" (keyUser "martindeboer" ) (keyVersion "a6034b00a3"))
 
-(autoModeTime "93")
+(autoModeTime "67")
 
 (branch "dummy ID"
 (rule "impRight" (formula "1") (newnames "key,result,exc,heapAtPre,o,f"))