Skip to content

Commit 96a6a98

Browse files
mattulbrichmattulbrich
committed
The Boyer-Moore example now runs on scripts
1 parent 594f407 commit 96a6a98

8 files changed

Lines changed: 360 additions & 12 deletions

File tree

‎key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java‎

Lines changed: 6 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -355,15 +355,12 @@ public static ProofCollection automaticJavaDL() throws IOException {
355355
g.provable("heap/removeDups/contains.key");
356356
g.provable("heap/removeDups/removeDup.key");
357357
g.provable("heap/saddleback_search/Saddleback_search.key");
358-
// TODO: Make BoyerMoore run automatically, not only loading proofs. Need proofs scripts for
359-
// that.
360-
g.loadable("heap/BoyerMoore/BM(BM__bm((I)).JML normal_behavior operation contract.0.proof");
361-
g.loadable(
362-
"heap/BoyerMoore/BM(BM__count((I,_bigint,_bigint)).JML accessible clause.0.proof");
363-
g.loadable(
364-
"heap/BoyerMoore/BM(BM__count((I,_bigint,_bigint)).JML model_behavior operation contract.0.proof");
365-
g.loadable(
366-
"heap/BoyerMoore/BM(BM__monoLemma((I,int,int)).JML normal_behavior operation contract.0.proof");
358+
// DONE: Make BoyerMoore run automatically, not only loading proofs. Need proofs scripts for
359+
// that. YESSS, it runs with scripts now ...
360+
g.provable("heap/BoyerMoore/BM.bm.key");
361+
g.provable("heap/BoyerMoore/BM.count.accessible.key");
362+
g.provable("heap/BoyerMoore/BM.count.key");
363+
g.provable("heap/BoyerMoore/BM.monoLemma.key");
367364

368365
g = c.group("quicksort");
369366
g.setLocalSettings("[Choice]DefaultChoices=moreSeqRules-moreSeqRules:on");

‎key.ui/examples/heap/BoyerMoore/BM.bm.key‎

Lines changed: 86 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,86 @@
1+
\profile "Java Profile";
2+
3+
\settings // Proof-Settings-Config-File
4+
{
5+
"Choice" : {
6+
"JavaCard" : "JavaCard:on",
7+
"Strings" : "Strings:on",
8+
"assertions" : "assertions:on",
9+
"bigint" : "bigint:on",
10+
"floatRules" : "floatRules:strictfpOnly",
11+
"initialisation" : "initialisation:disableStaticInitialisation",
12+
"intRules" : "intRules:arithmeticSemanticsIgnoringOF",
13+
"integerSimplificationRules" : "integerSimplificationRules:full",
14+
"javaLoopTreatment" : "javaLoopTreatment:efficient",
15+
"mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off",
16+
"methodExpansion" : "methodExpansion:modularOnly",
17+
"modelFields" : "modelFields:treatAsAxiom",
18+
"moreSeqRules" : "moreSeqRules:off",
19+
"permissions" : "permissions:off",
20+
"programRules" : "programRules:Java",
21+
"reach" : "reach:on",
22+
"runtimeExceptions" : "runtimeExceptions:ban",
23+
"sequences" : "sequences:on",
24+
"wdChecks" : "wdChecks:off",
25+
"wdOperator" : "wdOperator:L"
26+
},
27+
"Labels" : {
28+
"UseOriginLabels" : true
29+
},
30+
"NewSMT" : {
31+
32+
},
33+
"SMTSettings" : {
34+
"SelectedTaclets" : [
35+
36+
],
37+
"UseBuiltUniqueness" : false,
38+
"explicitTypeHierarchy" : false,
39+
"instantiateHierarchyAssumptions" : true,
40+
"integersMaximum" : 2147483645,
41+
"integersMinimum" : -2147483645,
42+
"invariantForall" : false,
43+
"maxGenericSorts" : 2,
44+
"useConstantsForBigOrSmallIntegers" : true,
45+
"useUninterpretedMultiplication" : true
46+
},
47+
"Strategy" : {
48+
"ActiveStrategy" : "JavaCardDLStrategy",
49+
"MaximumNumberOfAutomaticApplications" : 10000,
50+
"Timeout" : -1,
51+
"options" : {
52+
"AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
53+
"BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
54+
"CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_DELAYED",
55+
"DEP_OPTIONS_KEY" : "DEP_ON",
56+
"INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE",
57+
"LOOP_OPTIONS_KEY" : "LOOP_INVARIANT",
58+
"METHOD_OPTIONS_KEY" : "METHOD_CONTRACT",
59+
"MPS_OPTIONS_KEY" : "MPS_MERGE",
60+
"NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS",
61+
"OSS_OPTIONS_KEY" : "OSS_ON",
62+
"QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
63+
"QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON",
64+
"QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF",
65+
"SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
66+
"STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
67+
"SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER",
68+
"SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF",
69+
"USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
70+
"USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
71+
"USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
72+
"VBT_PHASE" : "VBT_SYM_EX"
73+
}
74+
}
75+
}
76+
77+
78+
\javaSource "src";
79+
80+
\proofObligation {
81+
"class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO",
82+
"contract" : "BoyerMoore[BoyerMoore::bm([I)].JML normal_behavior operation contract.0",
83+
"name" : "BoyerMoore[BoyerMoore::bm([I)].JML normal_behavior operation contract.0"
84+
}
85+
86+
\proofScript { macro "script-auto"; }

‎key.ui/examples/heap/BoyerMoore/BM.count.accessible.key‎

Lines changed: 85 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,85 @@
1+
\profile "Java Profile";
2+
3+
\settings // Proof-Settings-Config-File
4+
{
5+
"Choice" : {
6+
"JavaCard" : "JavaCard:on",
7+
"Strings" : "Strings:on",
8+
"assertions" : "assertions:on",
9+
"bigint" : "bigint:on",
10+
"floatRules" : "floatRules:strictfpOnly",
11+
"initialisation" : "initialisation:disableStaticInitialisation",
12+
"intRules" : "intRules:arithmeticSemanticsIgnoringOF",
13+
"integerSimplificationRules" : "integerSimplificationRules:full",
14+
"javaLoopTreatment" : "javaLoopTreatment:efficient",
15+
"mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off",
16+
"methodExpansion" : "methodExpansion:modularOnly",
17+
"modelFields" : "modelFields:treatAsAxiom",
18+
"moreSeqRules" : "moreSeqRules:off",
19+
"permissions" : "permissions:off",
20+
"programRules" : "programRules:Java",
21+
"reach" : "reach:on",
22+
"runtimeExceptions" : "runtimeExceptions:ban",
23+
"sequences" : "sequences:on",
24+
"wdChecks" : "wdChecks:off",
25+
"wdOperator" : "wdOperator:L"
26+
},
27+
"Labels" : {
28+
"UseOriginLabels" : true
29+
},
30+
"NewSMT" : {
31+
32+
},
33+
"SMTSettings" : {
34+
"SelectedTaclets" : [
35+
36+
],
37+
"UseBuiltUniqueness" : false,
38+
"explicitTypeHierarchy" : false,
39+
"instantiateHierarchyAssumptions" : true,
40+
"integersMaximum" : 2147483645,
41+
"integersMinimum" : -2147483645,
42+
"invariantForall" : false,
43+
"maxGenericSorts" : 2,
44+
"useConstantsForBigOrSmallIntegers" : true,
45+
"useUninterpretedMultiplication" : true
46+
},
47+
"Strategy" : {
48+
"ActiveStrategy" : "JavaCardDLStrategy",
49+
"MaximumNumberOfAutomaticApplications" : 10000,
50+
"Timeout" : -1,
51+
"options" : {
52+
"AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
53+
"BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
54+
"CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_DELAYED",
55+
"DEP_OPTIONS_KEY" : "DEP_ON",
56+
"INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE",
57+
"LOOP_OPTIONS_KEY" : "LOOP_INVARIANT",
58+
"METHOD_OPTIONS_KEY" : "METHOD_CONTRACT",
59+
"MPS_OPTIONS_KEY" : "MPS_MERGE",
60+
"NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS",
61+
"OSS_OPTIONS_KEY" : "OSS_ON",
62+
"QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
63+
"QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON",
64+
"QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF",
65+
"SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
66+
"STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
67+
"SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER",
68+
"SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF",
69+
"USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
70+
"USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
71+
"USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
72+
"VBT_PHASE" : "VBT_SYM_EX"
73+
}
74+
}
75+
}
76+
77+
78+
\javaSource "src";
79+
80+
\proofObligation {
81+
"class" : "de.uka.ilkd.key.proof.init.DependencyContractPO",
82+
"contract" : "BoyerMoore[BoyerMoore::count([I,\bigint,\bigint)].JML accessible clause.0",
83+
"name" : "BoyerMoore[BoyerMoore::count([I,\bigint,\bigint)].JML accessible clause.0"
84+
}
85+

‎key.ui/examples/heap/BoyerMoore/BM.count.key‎

Lines changed: 84 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,84 @@
1+
\profile "Java Profile";
2+
3+
\settings // Proof-Settings-Config-File
4+
{
5+
"Choice" : {
6+
"JavaCard" : "JavaCard:on",
7+
"Strings" : "Strings:on",
8+
"assertions" : "assertions:on",
9+
"bigint" : "bigint:on",
10+
"floatRules" : "floatRules:strictfpOnly",
11+
"initialisation" : "initialisation:disableStaticInitialisation",
12+
"intRules" : "intRules:arithmeticSemanticsIgnoringOF",
13+
"integerSimplificationRules" : "integerSimplificationRules:full",
14+
"javaLoopTreatment" : "javaLoopTreatment:efficient",
15+
"mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off",
16+
"methodExpansion" : "methodExpansion:modularOnly",
17+
"modelFields" : "modelFields:treatAsAxiom",
18+
"moreSeqRules" : "moreSeqRules:off",
19+
"permissions" : "permissions:off",
20+
"programRules" : "programRules:Java",
21+
"reach" : "reach:on",
22+
"runtimeExceptions" : "runtimeExceptions:ban",
23+
"sequences" : "sequences:on",
24+
"wdChecks" : "wdChecks:off",
25+
"wdOperator" : "wdOperator:L"
26+
},
27+
"Labels" : {
28+
"UseOriginLabels" : true
29+
},
30+
"NewSMT" : {
31+
32+
},
33+
"SMTSettings" : {
34+
"SelectedTaclets" : [
35+
36+
],
37+
"UseBuiltUniqueness" : false,
38+
"explicitTypeHierarchy" : false,
39+
"instantiateHierarchyAssumptions" : true,
40+
"integersMaximum" : 2147483645,
41+
"integersMinimum" : -2147483645,
42+
"invariantForall" : false,
43+
"maxGenericSorts" : 2,
44+
"useConstantsForBigOrSmallIntegers" : true,
45+
"useUninterpretedMultiplication" : true
46+
},
47+
"Strategy" : {
48+
"ActiveStrategy" : "JavaCardDLStrategy",
49+
"MaximumNumberOfAutomaticApplications" : 10000,
50+
"Timeout" : -1,
51+
"options" : {
52+
"AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
53+
"BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
54+
"CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_DELAYED",
55+
"DEP_OPTIONS_KEY" : "DEP_ON",
56+
"INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE",
57+
"LOOP_OPTIONS_KEY" : "LOOP_INVARIANT",
58+
"METHOD_OPTIONS_KEY" : "METHOD_CONTRACT",
59+
"MPS_OPTIONS_KEY" : "MPS_MERGE",
60+
"NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS",
61+
"OSS_OPTIONS_KEY" : "OSS_ON",
62+
"QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
63+
"QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON",
64+
"QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF",
65+
"SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
66+
"STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
67+
"SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER",
68+
"SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF",
69+
"USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
70+
"USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
71+
"USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
72+
"VBT_PHASE" : "VBT_SYM_EX"
73+
}
74+
}
75+
}
76+
77+
78+
\javaSource "src";
79+
80+
\proofObligation {
81+
"class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO",
82+
"contract" : "BoyerMoore[BoyerMoore::count([I,\bigint,\bigint)].JML model_behavior operation contract.0",
83+
"name" : "BoyerMoore[BoyerMoore::count([I,\bigint,\bigint)].JML model_behavior operation contract.0"
84+
}

‎key.ui/examples/heap/BoyerMoore/BM.monoLemma.key‎

Lines changed: 83 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
1+
\profile "Java Profile";
2+
3+
\settings // Proof-Settings-Config-File
4+
{
5+
"Choice" : {
6+
"JavaCard" : "JavaCard:on",
7+
"Strings" : "Strings:on",
8+
"assertions" : "assertions:on",
9+
"bigint" : "bigint:on",
10+
"floatRules" : "floatRules:strictfpOnly",
11+
"initialisation" : "initialisation:disableStaticInitialisation",
12+
"intRules" : "intRules:arithmeticSemanticsIgnoringOF",
13+
"integerSimplificationRules" : "integerSimplificationRules:full",
14+
"javaLoopTreatment" : "javaLoopTreatment:efficient",
15+
"mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off",
16+
"methodExpansion" : "methodExpansion:modularOnly",
17+
"modelFields" : "modelFields:treatAsAxiom",
18+
"moreSeqRules" : "moreSeqRules:off",
19+
"permissions" : "permissions:off",
20+
"programRules" : "programRules:Java",
21+
"reach" : "reach:on",
22+
"runtimeExceptions" : "runtimeExceptions:ban",
23+
"sequences" : "sequences:on",
24+
"wdChecks" : "wdChecks:off",
25+
"wdOperator" : "wdOperator:L"
26+
},
27+
"Labels" : {
28+
"UseOriginLabels" : true
29+
},
30+
"NewSMT" : {
31+
32+
},
33+
"SMTSettings" : {
34+
"SelectedTaclets" : [
35+
36+
],
37+
"UseBuiltUniqueness" : false,
38+
"explicitTypeHierarchy" : false,
39+
"instantiateHierarchyAssumptions" : true,
40+
"integersMaximum" : 2147483645,
41+
"integersMinimum" : -2147483645,
42+
"invariantForall" : false,
43+
"maxGenericSorts" : 2,
44+
"useConstantsForBigOrSmallIntegers" : true,
45+
"useUninterpretedMultiplication" : true
46+
},
47+
"Strategy" : {
48+
"ActiveStrategy" : "JavaCardDLStrategy",
49+
"MaximumNumberOfAutomaticApplications" : 10000,
50+
"Timeout" : -1,
51+
"options" : {
52+
"AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
53+
"BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
54+
"CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_DELAYED",
55+
"DEP_OPTIONS_KEY" : "DEP_ON",
56+
"INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE",
57+
"LOOP_OPTIONS_KEY" : "LOOP_INVARIANT",
58+
"METHOD_OPTIONS_KEY" : "METHOD_CONTRACT",
59+
"MPS_OPTIONS_KEY" : "MPS_MERGE",
60+
"NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS",
61+
"OSS_OPTIONS_KEY" : "OSS_ON",
62+
"QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
63+
"QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON",
64+
"QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF",
65+
"SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
66+
"STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
67+
"SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER",
68+
"SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF",
69+
"USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
70+
"USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
71+
"USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
72+
"VBT_PHASE" : "VBT_SYM_EX"
73+
}
74+
}
75+
}
76+
77+
\javaSource "src";
78+
79+
\proofObligation {
80+
"class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO",
81+
"contract" : "BoyerMoore[BoyerMoore::monoLemma([I,int,int)].JML normal_behavior operation contract.0",
82+
"name" : "BoyerMoore[BoyerMoore::monoLemma([I,int,int)].JML normal_behavior operation contract.0"
83+
}

‎key.ui/examples/heap/BoyerMoore/BoyerMoore.key‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,7 @@
5151
"options" : {
5252
"AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
5353
"BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
54-
"CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_OFF",
54+
"CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_DELAYED",
5555
"DEP_OPTIONS_KEY" : "DEP_ON",
5656
"INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE",
5757
"LOOP_OPTIONS_KEY" : "LOOP_INVARIANT",

‎key.ui/examples/heap/BoyerMoore/README.txt‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,9 @@ entries in the array hold m.
1515

1616
Suggested by J.C. Filliâtre as an example during VerifyThis 24.
1717

18-
Currently the proofs do not go through automatically, the proof
19-
files are checked in with the example.
18+
Originally, the proofs did not go through automatically, with JML
19+
proof scripts they now succeed.
20+
2021

2122
@see https://en.wikipedia.org/wiki/Boyer-Moore_majority_vote_algorithm
2223
@author Mattias Ulbrich

0 commit comments

Comments
 (0)