From 1fd187de823d1bd01ece95d434bd0570307f3e29 Mon Sep 17 00:00:00 2001
From: Mattias Ulbrich <ulbrich@kit.edu>
Date: Fri, 14 Jun 2024 17:03:39 +0200
Subject: [PATCH] proof script for ArrayList.add

needs a new key version ...
---
 ...normal_behavior operation contract.0.proof | 92 +++++++++++++++++++
 ArrayList/src/ArrayList.java                  |  6 +-
 2 files changed, 94 insertions(+), 4 deletions(-)
 create mode 100644 ArrayList/proofs/ArrayList(List__add(int)).JML normal_behavior operation contract.0.proof

diff --git a/ArrayList/proofs/ArrayList(List__add(int)).JML normal_behavior operation contract.0.proof b/ArrayList/proofs/ArrayList(List__add(int)).JML normal_behavior operation contract.0.proof
new file mode 100644
index 0000000..4eeb310
--- /dev/null
+++ b/ArrayList/proofs/ArrayList(List__add(int)).JML normal_behavior operation contract.0.proof	
@@ -0,0 +1,92 @@
+\profile "Java Profile";
+
+\settings // Proof-Settings-Config-File
+{ 
+    "Choice" : { 
+        "JavaCard" : "JavaCard:off",
+        "Strings" : "Strings:on",
+        "assertions" : "assertions:safe",
+        "bigint" : "bigint:on",
+        "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:on",
+        "permissions" : "permissions:off",
+        "programRules" : "programRules:Java",
+        "reach" : "reach:on",
+        "runtimeExceptions" : "runtimeExceptions:ban",
+        "sequences" : "sequences:on",
+        "wdChecks" : "wdChecks:off",
+        "wdOperator" : "wdOperator:L"
+     },
+    "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" : "JavaCardDLStrategy",
+        "MaximumNumberOfAutomaticApplications" : 10000,
+        "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",
+            "INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE",
+            "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_OFF",
+            "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",
+            "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 
+// Proof-Obligation settings
+{ 
+    "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO",
+    "contract" : "ArrayList[List::add(int)].JML normal_behavior operation contract.0",
+    "name" : "ArrayList[List::add(int)].JML normal_behavior operation contract.0"
+ }
+
+
+\proofScript "
+  macro autopilot;
+  rule Class_invariant_axiom_for_ArrayList;
+  macro split-prop;
+  auto all=true steps=10000;"
diff --git a/ArrayList/src/ArrayList.java b/ArrayList/src/ArrayList.java
index a53ae01..54da122 100644
--- a/ArrayList/src/ArrayList.java
+++ b/ArrayList/src/ArrayList.java
@@ -15,7 +15,7 @@ public class ArrayList implements List {
       @*/
 
     /*@ public normal_behaviour
-      @   ensures seq == \seq_empty && \fresh(footprint);
+      @   ensures seq == \seq() && \fresh(footprint);
       @*/
     public /*@ pure @*/ ArrayList() {
         this.array = new int[10];
@@ -124,8 +124,6 @@ private void swap(int a, int b) {
         int t = array[a];
         array[a] = array[b];
         array[b] = t;
-	//@ set seq = \dl_seqSwap(seq, a, b);
-        // @ set seq = \seq_upd(seq, a, array[a]);
-        // @ set seq = \seq_upd(seq, b, array[b]);
+        //@ set seq = \dl_seqSwap(seq, a, b);
     }
 }