up.jerboa.core.JerboaOrbit(up.jerboa.core.JerboaOrbit__get(int)).JML normal_behavior operation contract.0.proof

\profile "Java Profile";

\settings // Proof-Settings-Config-File
{ 
    "Choice" : { 
        "JavaCard" : "JavaCard:off",
        "Strings" : "Strings:on",
        "assertions" : "assertions:safe",
        "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",
        "wdChecks" : "wdChecks:off",
        "wdOperator" : "wdOperator:L"
     },
    "Labels" : { 
        "UseOriginLabels" : true
     },
    "NewSMT" : { 
        "Axiomatisations" : "false",
        "Presburger" : "false",
        "sqrtSMTTranslation" : "SMT"
     },
    "SMTSettings" : { 
        "SelectedTaclets" : [ 
            
         ],
        "UseBuiltUniqueness" : false,
        "explicitTypeHierarchy" : false,
        "instantiateHierarchyAssumptions" : true,
        "integersMaximum" : 2147483645,
        "integersMinimum" : -2147483645,
        "invariantForall" : false,
        "maxGenericSorts" : 2,
        "useConstantsForBigOrSmallIntegers" : true,
        "useUninterpretedMultiplication" : true
     },
    "Strategy" : { 
        "ActiveStrategy" : "JavaCardDLStrategy",
        "MaximumNumberOfAutomaticApplications" : 20000,
        "Timeout" : -1,
        "options" : { 
            "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
            "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
            "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_DELAYED",
            "DEP_OPTIONS_KEY" : "DEP_ON",
            "INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE",
            "LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET",
            "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_ON",
            "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"
         }
     }
 } 


\bootclasspath "bootclasspath";
\javaSource "src/main/java";
\include "rules.key";\proofObligation 
// 
{ 
    "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO",
    "contract" : "up.jerboa.core.JerboaOrbit[up.jerboa.core.JerboaOrbit::get(int)].JML normal_behavior operation contract.0",
    "name" : "up.jerboa.core.JerboaOrbit[up.jerboa.core.JerboaOrbit::get(int)].JML normal_behavior operation contract.0"
 }

\proof {
(keyLog "0" (keyUser "arne" ) (keyVersion "a2f03f4b8f29184dd8b0d107edb6876965b02f95"))

(autoModeTime "74")

(branch "dummy ID"
 (builtin "One Step Simplification" (formula "1") (newnames "heapAtPre,o,f"))
(rule "impRight" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "3"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "4"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "notLeft" (formula "2"))
(rule "eqSymm" (formula "9") (term "0,0,0,0,1"))
(rule "eqSymm" (formula "9") (term "0,0,1,0,1"))
(rule "inEqSimp_ltToLeq" (formula "6"))
(rule "polySimp_mulComm0" (formula "6") (term "1,0,0"))
(rule "polySimp_addComm1" (formula "6") (term "0"))
(rule "inEqSimp_commuteLeq" (formula "5"))
(rule "assignment" (formula "9") (term "1"))
 (builtin "One Step Simplification" (formula "9"))
(rule "inEqSimp_sepNegMonomial0" (formula "6"))
(rule "polySimp_mulLiterals" (formula "6") (term "0"))
(rule "polySimp_elimOne" (formula "6") (term "0"))
(rule "methodBodyExpand" (formula "9") (term "1") (newnames "heapBefore_get,savedHeapBefore_get"))
 (builtin "One Step Simplification" (formula "9"))
(rule "returnUnfold" (formula "9") (term "1") (inst "#v0=i_1"))
(rule "variableDeclarationAssign" (formula "9") (term "1"))
(rule "variableDeclaration" (formula "9") (term "1") (newnames "i_1"))
(rule "eval_order_array_access4" (formula "9") (term "1") (inst "#v0=i_arr"))
(rule "variableDeclarationAssign" (formula "9") (term "1"))
(rule "variableDeclaration" (formula "9") (term "1") (newnames "i_arr"))
(rule "assignment_read_attribute_this_final" (formula "9"))
 (builtin "One Step Simplification" (formula "9"))
(rule "assignment_array2" (formula "9"))
(branch "Normal Execution (i_arr != null)"
    (builtin "One Step Simplification" (formula "9"))
   (rule "methodCallReturn" (formula "9") (term "1"))
   (rule "assignment" (formula "9") (term "1"))
    (builtin "One Step Simplification" (formula "9"))
   (rule "methodCallEmpty" (formula "9") (term "1"))
   (rule "tryEmpty" (formula "9") (term "1"))
   (rule "emptyModality" (formula "9") (term "1"))
    (builtin "One Step Simplification" (formula "9") (ifInst ""  (formula "7")))
   (rule "closeTrue" (formula "9"))
)
(branch "Null Reference (i_arr = null)"
   (rule "false_right" (formula "10"))
    (builtin "One Step Simplification" (formula "1"))
   (rule "applyEq" (formula "7") (term "0,0") (ifseqformula "1"))
   (rule "Class_invariant_axiom_for_up_jerboa_core_JerboaOrbit" (formula "8") (inst "i=i_2") (ifseqformula "9"))
   (rule "andLeft" (formula "8"))
   (rule "andLeft" (formula "8"))
   (rule "notLeft" (formula "8"))
   (rule "close" (formula "10") (ifseqformula "1"))
)
(branch "Index Out of Bounds (i_arr != null, but _i Out of Bounds!)"
   (rule "false_right" (formula "10"))
    (builtin "One Step Simplification" (formula "1"))
   (rule "andLeft" (formula "1"))
   (rule "notLeft" (formula "1"))
   (rule "inEqSimp_ltToLeq" (formula "1") (term "1"))
   (rule "times_zero_1" (formula "1") (term "1,0,0,1"))
   (rule "add_zero_right" (formula "1") (term "0,0,1"))
   (rule "inEqSimp_sepPosMonomial0" (formula "1") (term "1"))
   (rule "mul_literals" (formula "1") (term "1,1"))
   (rule "inEqSimp_contradInEq1" (formula "1") (term "1") (ifseqformula "6"))
   (rule "qeq_literals" (formula "1") (term "0,1"))
    (builtin "One Step Simplification" (formula "1"))
   (rule "inEqSimp_contradInEq1" (formula "1") (ifseqformula "7"))
   (rule "andLeft" (formula "1"))
   (rule "inEqSimp_homoInEq1" (formula "1"))
   (rule "polySimp_pullOutFactor1b" (formula "1") (term "0"))
   (rule "add_literals" (formula "1") (term "1,1,0"))
   (rule "times_zero_1" (formula "1") (term "1,0"))
   (rule "add_zero_right" (formula "1") (term "0"))
   (rule "leq_literals" (formula "1"))
   (rule "closeFalse" (formula "1"))
)
)
}