-
Notifications
You must be signed in to change notification settings - Fork 2
Expand file tree
/
Copy pathde.wiesler.SampleParameters(de.wiesler.SampleParameters__oversampling_factor(int)).JML normal_behavior operation contract.0.proof
More file actions
128 lines (122 loc) · 6.34 KB
/
de.wiesler.SampleParameters(de.wiesler.SampleParameters__oversampling_factor(int)).JML normal_behavior operation contract.0.proof
File metadata and controls
128 lines (122 loc) · 6.34 KB
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
\profile "Java Profile";
\settings {
"#Proof-Settings-Config-File
#Tue Apr 05 14:34:26 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
#Tue Apr 05 14:34:26 CEST 2022
contract=de.wiesler.SampleParameters[de.wiesler.SampleParameters\\:\\:oversampling_factor(int)].JML normal_behavior operation contract.0
name=de.wiesler.SampleParameters[de.wiesler.SampleParameters\\:\\:oversampling_factor(int)].JML normal_behavior operation contract.0
class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO
";
\proof {
(keyLog "0" (keyUser "Julian" ) (keyVersion "802059dea3"))
(keyLog "1" (keyUser "Julian" ) (keyVersion "802059dea3"))
(autoModeTime "44")
(branch "dummy ID"
(builtin "One Step Simplification" (formula "1"))
(rule "impRight" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "eqSymm" (formula "4") (term "0,0,1,0,1"))
(rule "assignment" (formula "4") (term "1"))
(builtin "One Step Simplification" (formula "4"))
(rule "methodBodyExpand" (formula "4") (term "1") (newnames "heapBefore_oversampling_factor,savedHeapBefore_oversampling_factor"))
(builtin "One Step Simplification" (formula "4"))
(rule "returnUnfold" (formula "4") (term "1") (inst "#v0=x"))
(rule "variableDeclarationAssign" (formula "4") (term "1"))
(rule "variableDeclaration" (formula "4") (term "1") (newnames "x"))
(rule "compound_division_1" (formula "4") (term "1") (inst "#v=x_1"))
(rule "variableDeclarationAssign" (formula "4") (term "1"))
(rule "variableDeclaration" (formula "4") (term "1") (newnames "x_1"))
(builtin "Use Operation Contract" (formula "4") (newnames "heapBefore_log2,result_0,exc_0") (contract "de.wiesler.Constants[de.wiesler.Constants::log2(int)].JML normal_behavior operation contract.0"))
(branch "Post (log2)"
(builtin "One Step Simplification" (formula "4"))
(builtin "One Step Simplification" (formula "5"))
(rule "andLeft" (formula "4"))
(rule "andLeft" (formula "4"))
(rule "assignment" (formula "6") (term "1"))
(builtin "One Step Simplification" (formula "6"))
(rule "assignmentDivisionInt" (formula "6"))
(branch "Case 1"
(builtin "One Step Simplification" (formula "6"))
(rule "translateJavaDivInt" (formula "6") (term "0,1,0"))
(rule "methodCallReturn" (formula "6") (term "1"))
(rule "assignment" (formula "6") (term "1"))
(builtin "One Step Simplification" (formula "6"))
(rule "methodCallEmpty" (formula "6") (term "1"))
(rule "tryEmpty" (formula "6") (term "1"))
(rule "emptyModality" (formula "6") (term "1"))
(builtin "One Step Simplification" (formula "6"))
(rule "closeTrue" (formula "6"))
)
(branch "Case 2"
(builtin "One Step Simplification" (formula "6"))
(rule "equal_literals" (formula "6") (term "0"))
(builtin "One Step Simplification" (formula "6"))
(rule "closeTrue" (formula "6"))
)
)
(branch "Exceptional Post (log2)"
(builtin "One Step Simplification" (formula "4"))
(builtin "One Step Simplification" (formula "5"))
(rule "andLeft" (formula "4"))
(rule "andLeft" (formula "4"))
(rule "notLeft" (formula "4"))
(rule "close" (formula "6") (ifseqformula "5"))
)
(branch "Pre (log2)"
(builtin "One Step Simplification" (formula "4") (ifInst "" (formula "1")))
(rule "inEqSimp_gtRight" (formula "4"))
(rule "times_zero_1" (formula "1") (term "0,0"))
(rule "add_zero_left" (formula "1") (term "0"))
(rule "inEqSimp_contradInEq1" (formula "1") (ifseqformula "4"))
(rule "qeq_literals" (formula "1") (term "0"))
(builtin "One Step Simplification" (formula "1"))
(rule "closeFalse" (formula "1"))
)
)
}