-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathde.wiesler.SampleParameters(de.wiesler.SampleParameters__isValidForLen(int)).JML accessible clause.0.proof
196 lines (190 loc) · 11.1 KB
/
de.wiesler.SampleParameters(de.wiesler.SampleParameters__isValidForLen(int)).JML accessible clause.0.proof
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
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
\profile "Java Profile";
\settings {
"#Proof-Settings-Config-File
#Sun Apr 10 19:50:11 CEST 2022
[NewSMT]NoTypeHierarchy=false
[Labels]UseOriginLabels=true
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_OFF
[NewSMT]Presburger=false
[SMTSettings]invariantForall=false
[Strategy]ActiveStrategy=JavaCardDLStrategy
[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
[Choice]DefaultChoices=JavaCard-JavaCard\\:on , 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\\:on , permissions-permissions\\:off , programRules-programRules\\:Java , reach-reach\\:on , runtimeExceptions-runtimeExceptions\\:ban , sequences-sequences\\:on , wdChecks-wdChecks\\:off , wdOperator-wdOperator\\:L
[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_SCOPE_INV_TACLET
[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
[SMTSettings]UseBuiltUniqueness=false
[SMTSettings]explicitTypeHierarchy=false
[SMTSettings]instantiateHierarchyAssumptions=true
[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_DEF_OPS
[SMTSettings]SelectedTaclets=
[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON
[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
[Strategy]MaximumNumberOfAutomaticApplications=10000
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_DELAYED
[SMTSettings]useConstantsForBigOrSmallIntegers=true
[StrategyProperty]MPS_OPTIONS_KEY=MPS_MERGE
[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
[Strategy]Timeout=-1
[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF
[SMTSettings]useUninterpretedMultiplication=true
[NewSMT]sqrtSMTTranslation=SMT
[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT_INTERNAL
[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT
[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
[NewSMT]identifier=OPEN
[SMTSettings]maxGenericSorts=2
[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON
[NewSMT]Axiomatisations=false
[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED
[SMTSettings]integersMinimum=-2147483645
[StrategyProperty]VBT_PHASE=VBT_SYM_EX
[SMTSettings]integersMaximum=2147483645
"
}
\javaSource "../src";
\proofObligation "#Proof Obligation Settings
#Sun Apr 10 19:50:11 CEST 2022
contract=de.wiesler.SampleParameters[de.wiesler.SampleParameters\\:\\:isValidForLen(int)].JML accessible clause.0
name=de.wiesler.SampleParameters[de.wiesler.SampleParameters\\:\\:isValidForLen(int)].JML accessible clause.0
class=de.uka.ilkd.key.proof.init.DependencyContractPO
";
\proof {
(keyLog "0" (keyUser "Julian" ) (keyVersion "802059dea3"))
(keyLog "1" (keyUser "Julian" ) (keyVersion "82c4308ea5"))
(autoModeTime "128")
(branch "dummy ID"
(builtin "One Step Simplification" (formula "1") (newnames "self,n,anon_heap"))
(rule "impRight" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "notLeft" (formula "3"))
(rule "eqSymm" (formula "8"))
(rule "Class_invariant_axiom_for_de_wiesler_SampleParameters" (formula "6"))
(rule "true_left" (formula "6"))
(rule "Contract_axiom_for_isValidForLen_in_SampleParameters" (formula "7") (term "0"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "7")) (ifInst "" (formula "4")))
(rule "wellFormedAnon" (formula "1") (term "1,0"))
(rule "replace_known_left" (formula "1") (term "0,1,0") (ifseqformula "2"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "3")))
(rule "true_left" (formula "1"))
(rule "Contract_axiom_for_isValidForLen_in_SampleParameters" (formula "7") (term "1"))
(rule "replace_known_left" (formula "1") (term "1,0,0,0") (ifseqformula "2"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "4")) (ifInst "" (formula "7")))
(rule "true_left" (formula "1"))
(rule "Definition_axiom_for_isValidForLen_in_de_wiesler_SampleParameters" (formula "7") (term "1"))
(builtin "One Step Simplification" (formula "7"))
(rule "translateJavaMod" (formula "7") (term "0,1,0,0,1"))
(rule "translateJavaSubInt" (formula "7") (term "0,1,0,1"))
(rule "translateJavaDivInt" (formula "7") (term "1,1,0,0,0,0,0,0,1"))
(rule "translateJavaMulInt" (formula "7") (term "0,0,1,0,1"))
(rule "eqSymm" (formula "7"))
(rule "polySimp_elimSub" (formula "7") (term "0,1,0,0"))
(rule "mul_literals" (formula "7") (term "1,0,1,0,0"))
(rule "polySimp_addComm0" (formula "7") (term "0,1,0,0"))
(rule "translateJavaShiftLeftIntConstant" (formula "7") (term "1,1,1,0,0,0,0"))
(rule "inEqSimp_ltToLeq" (formula "7") (term "1,0,0,0,0,0,0"))
(rule "polySimp_mulComm0" (formula "7") (term "1,0,0,1,0,0,0,0,0,0"))
(rule "inEqSimp_commuteLeq" (formula "7") (term "1,0,0,0,0,0"))
(rule "inEqSimp_commuteLeq" (formula "7") (term "0,0,0,0,0,0,0,0"))
(rule "inEqSimp_commuteLeq" (formula "7") (term "0,1,0,0,0,0"))
(rule "inEqSimp_homoInEq0" (formula "7") (term "1,0,0"))
(rule "polySimp_mulComm0" (formula "7") (term "1,0,1,0,0"))
(rule "polySimp_rightDist" (formula "7") (term "1,0,1,0,0"))
(rule "mul_literals" (formula "7") (term "0,1,0,1,0,0"))
(rule "polySimp_addAssoc" (formula "7") (term "0,1,0,0"))
(rule "polySimp_addComm0" (formula "7") (term "0,0,1,0,0"))
(rule "jmod_axiom" (formula "7") (term "0,1,0,0,0"))
(rule "polySimp_mulLiterals" (formula "7") (term "1,0,1,0,0,0"))
(rule "polySimp_sepNegMonomial" (formula "7") (term "1,0,0,0"))
(rule "polySimp_mulLiterals" (formula "7") (term "0,1,0,0,0"))
(rule "inEqSimp_sepPosMonomial0" (formula "7") (term "1,0,0,0,0,0,0"))
(rule "polySimp_mulComm0" (formula "7") (term "1,1,0,0,0,0,0,0"))
(rule "polySimp_rightDist" (formula "7") (term "1,1,0,0,0,0,0,0"))
(rule "polySimp_mulLiterals" (formula "7") (term "1,1,1,0,0,0,0,0,0"))
(rule "mul_literals" (formula "7") (term "0,1,1,0,0,0,0,0,0"))
(rule "polySimp_elimOne" (formula "7") (term "1,1,1,0,0,0,0,0,0"))
(rule "inEqSimp_sepNegMonomial1" (formula "7") (term "1,0,0"))
(rule "polySimp_mulLiterals" (formula "7") (term "0,1,0,0"))
(rule "polySimp_elimOne" (formula "7") (term "0,1,0,0"))
(rule "javaShiftLeftIntDef" (formula "7") (term "1,1,1,0,0,0,0"))
(rule "mod_axiom" (formula "7") (term "1,0,1,1,1,0,0,0,0"))
(rule "polySimp_mulLiterals" (formula "7") (term "1,1,0,1,1,1,0,0,0,0"))
(rule "div_literals" (formula "7") (term "0,1,1,0,1,1,1,0,0,0,0"))
(rule "times_zero_2" (formula "7") (term "1,1,0,1,1,1,0,0,0,0"))
(rule "add_zero_right" (formula "7") (term "1,0,1,1,1,0,0,0,0"))
(rule "shiftleft_literals" (formula "7") (term "0,1,1,1,0,0,0,0"))
(rule "expand_moduloInteger" (formula "7") (term "1,1,1,0,0,0,0"))
(rule "replace_int_HALFRANGE" (formula "7") (term "0,0,1,1,1,1,0,0,0,0"))
(rule "replace_int_MIN" (formula "7") (term "0,1,1,1,0,0,0,0"))
(rule "replace_int_RANGE" (formula "7") (term "1,1,1,1,1,0,0,0,0"))
(rule "add_literals" (formula "7") (term "0,1,1,1,1,0,0,0,0"))
(rule "mod_axiom" (formula "7") (term "1,1,1,1,0,0,0,0"))
(rule "polySimp_mulLiterals" (formula "7") (term "1,1,1,1,1,0,0,0,0"))
(rule "div_literals" (formula "7") (term "0,1,1,1,1,1,0,0,0,0"))
(rule "times_zero_2" (formula "7") (term "1,1,1,1,1,0,0,0,0"))
(rule "add_zero_right" (formula "7") (term "1,1,1,1,0,0,0,0"))
(rule "add_literals" (formula "7") (term "1,1,1,0,0,0,0"))
(rule "Definition_axiom_for_isValidForLen_in_de_wiesler_SampleParameters" (formula "7") (term "1"))
(builtin "One Step Simplification" (formula "7"))
(rule "translateJavaSubInt" (formula "7") (term "0,1,1"))
(rule "translateJavaMod" (formula "7") (term "0,1,0,1"))
(rule "translateJavaDivInt" (formula "7") (term "1,1,0,0,0,0,0,1"))
(rule "translateJavaMulInt" (formula "7") (term "0,0,1,1"))
(rule "polySimp_elimSub" (formula "7") (term "0,1,1"))
(rule "mul_literals" (formula "7") (term "1,0,1,1"))
(rule "polySimp_addComm0" (formula "7") (term "0,1,1"))
(rule "translateJavaShiftLeftIntConstant" (formula "7") (term "1,1,1,0,0,1"))
(rule "inEqSimp_ltToLeq" (formula "7") (term "1,0,0,0,0,1"))
(rule "polySimp_mulComm0" (formula "7") (term "1,0,0,1,0,0,0,0,1"))
(rule "inEqSimp_commuteLeq" (formula "7") (term "0,1,0,0,1"))
(rule "inEqSimp_commuteLeq" (formula "7") (term "0,0,0,0,0,0,1"))
(rule "inEqSimp_commuteLeq" (formula "7") (term "1,0,0,0,1"))
(rule "inEqSimp_homoInEq0" (formula "7") (term "1,1"))
(rule "polySimp_mulComm0" (formula "7") (term "1,0,1,1"))
(rule "polySimp_rightDist" (formula "7") (term "1,0,1,1"))
(rule "mul_literals" (formula "7") (term "0,1,0,1,1"))
(rule "polySimp_addAssoc" (formula "7") (term "0,1,1"))
(rule "polySimp_addComm0" (formula "7") (term "0,0,1,1"))
(rule "jmod_axiom" (formula "7") (term "0,1,0,1"))
(rule "polySimp_mulLiterals" (formula "7") (term "1,0,1,0,1"))
(rule "polySimp_sepNegMonomial" (formula "7") (term "1,0,1"))
(rule "polySimp_mulLiterals" (formula "7") (term "0,1,0,1"))
(rule "inEqSimp_sepPosMonomial0" (formula "7") (term "1,0,0,0,0,1"))
(rule "polySimp_mulComm0" (formula "7") (term "1,1,0,0,0,0,1"))
(rule "polySimp_rightDist" (formula "7") (term "1,1,0,0,0,0,1"))
(rule "polySimp_mulLiterals" (formula "7") (term "1,1,1,0,0,0,0,1"))
(rule "mul_literals" (formula "7") (term "0,1,1,0,0,0,0,1"))
(rule "polySimp_elimOne" (formula "7") (term "1,1,1,0,0,0,0,1"))
(rule "inEqSimp_sepNegMonomial1" (formula "7") (term "1,1"))
(rule "polySimp_mulLiterals" (formula "7") (term "0,1,1"))
(rule "polySimp_elimOne" (formula "7") (term "0,1,1"))
(rule "javaShiftLeftIntDef" (formula "7") (term "1,1,1,0,0,1"))
(rule "mod_axiom" (formula "7") (term "1,0,1,1,1,0,0,1"))
(rule "polySimp_mulLiterals" (formula "7") (term "1,1,0,1,1,1,0,0,1"))
(rule "div_literals" (formula "7") (term "0,1,1,0,1,1,1,0,0,1"))
(rule "times_zero_2" (formula "7") (term "1,1,0,1,1,1,0,0,1"))
(rule "add_zero_right" (formula "7") (term "1,0,1,1,1,0,0,1"))
(rule "shiftleft_literals" (formula "7") (term "0,1,1,1,0,0,1"))
(rule "expand_moduloInteger" (formula "7") (term "1,1,1,0,0,1"))
(rule "replace_int_RANGE" (formula "7") (term "1,1,1,1,1,0,0,1"))
(rule "replace_int_MIN" (formula "7") (term "0,1,1,1,0,0,1"))
(rule "replace_int_HALFRANGE" (formula "7") (term "0,0,1,1,1,1,0,0,1"))
(rule "add_literals" (formula "7") (term "0,1,1,1,1,0,0,1"))
(rule "mod_axiom" (formula "7") (term "1,1,1,1,0,0,1"))
(rule "polySimp_mulLiterals" (formula "7") (term "1,1,1,1,1,0,0,1"))
(rule "div_literals" (formula "7") (term "0,1,1,1,1,1,0,0,1"))
(rule "times_zero_2" (formula "7") (term "1,1,1,1,1,0,0,1"))
(rule "add_zero_right" (formula "7") (term "1,1,1,1,0,0,1"))
(rule "add_literals" (formula "7") (term "1,1,1,0,0,1"))
(builtin "One Step Simplification" (formula "7"))
(rule "closeTrue" (formula "7"))
)
}