Jerboa-KeY-case-study/fr.up.xlim.sic.ig.jerboa.jme.model.JMELoop(fr.up.xlim.sic.ig.jerboa.jme.model.JMEArc__getDimension()).JML normal_behavior operation contract.0.proof at master · KeYProject/Jerboa-KeY-case-study · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
\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" : "fr.up.xlim.sic.ig.jerboa.jme.model.JMELoop[fr.up.xlim.sic.ig.jerboa.jme.model.JMEArc::getDimension()].JML normal_behavior operation contract.0",
    "name" : "fr.up.xlim.sic.ig.jerboa.jme.model.JMELoop[fr.up.xlim.sic.ig.jerboa.jme.model.JMEArc::getDimension()].JML normal_behavior operation contract.0"
 }

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

(autoModeTime "154")

(branch "dummy ID"
(rule "impRight" (formula "1") (newnames "heapAtPre,o,f"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "notLeft" (formula "2"))
(rule "eqSymm" (formula "7") (term "0,0,1,0,1"))
(rule "eqSymm" (formula "7") (term "0,0,0,0,1"))
(rule "assignment" (formula "7") (term "1"))
 (builtin "One Step Simplification" (formula "7"))
(rule "methodBodyExpand" (formula "7") (term "1") (newnames "heapBefore_getDimension,savedHeapBefore_getDimension"))
 (builtin "One Step Simplification" (formula "7"))
(rule "returnUnfold" (formula "7") (term "1") (inst "#v0=i"))
(rule "variableDeclarationAssign" (formula "7") (term "1"))
(rule "variableDeclaration" (formula "7") (term "1") (newnames "i"))
(rule "assignment_read_attribute_this_final" (formula "7"))
 (builtin "One Step Simplification" (formula "7"))
(rule "methodCallReturn" (formula "7") (term "1"))
(rule "assignment" (formula "7") (term "1"))
 (builtin "One Step Simplification" (formula "7"))
(rule "methodCallEmpty" (formula "7") (term "1"))
(rule "tryEmpty" (formula "7") (term "1"))
(rule "emptyModality" (formula "7") (term "1"))
 (builtin "One Step Simplification" (formula "7") (ifInst ""  (formula "5")))
(rule "closeTrue" (formula "7"))
)
}