|
1
|
Result of the analysis by WP
|
|
2
|
----------------------------------------------------------
|
|
3
|
Axiomatics Proved Total Success
|
|
4
|
Lemma 5 5 100%
|
|
5
|
lemma_inv_init_1_top 1
|
|
6
|
lemma_inv_init_2_top 1
|
|
7
|
lemma_inv_inv_top 1
|
|
8
|
lemma_inv_spec_top 1
|
|
9
|
lemma_missing 1
|
|
10
|
----------------------------------------------------------
|
|
11
|
Functions Proved Total Success
|
|
12
|
Sofar_reset 4 4 100%
|
|
13
|
Sofar_reset_post 1
|
|
14
|
Sofar_reset_stmt_post 1
|
|
15
|
Sofar_reset_stmt_assign 1
|
|
16
|
Sofar_reset_assign 1
|
|
17
|
Sofar_step 14 14 100%
|
|
18
|
Sofar_step_post 1
|
|
19
|
Sofar_step_stmt_post 1
|
|
20
|
Sofar_step_stmt_post_2 1
|
|
21
|
Sofar_step_stmt_post_3 1
|
|
22
|
Sofar_step_stmt_post_4 1
|
|
23
|
Sofar_step_stmt_post_5 1
|
|
24
|
Sofar_step_stmt_post_6 1
|
|
25
|
Sofar_step_stmt_assign 1
|
|
26
|
Sofar_step_stmt_assign_2 1
|
|
27
|
Sofar_step_stmt_assign_3 3
|
|
28
|
Sofar_step_stmt_assign_4 2
|
|
29
|
Sofar_step_stmt_assign_5 5
|
|
30
|
Sofar_step_stmt_assign_6 1
|
|
31
|
Sofar_step_assign 1
|
|
32
|
Age_reset 4 4 100%
|
|
33
|
Age_reset_post 1
|
|
34
|
Age_reset_stmt_post 1
|
|
35
|
Age_reset_stmt_assign 1
|
|
36
|
Age_reset_assign 1
|
|
37
|
Age_step 16 16 100%
|
|
38
|
Age_step_post 1
|
|
39
|
Age_step_stmt_post 1
|
|
40
|
Age_step_stmt_post_2 1
|
|
41
|
Age_step_stmt_post_3 1
|
|
42
|
Age_step_stmt_post_4 1
|
|
43
|
Age_step_stmt_post_5 1
|
|
44
|
Age_step_stmt_post_6 1
|
|
45
|
Age_step_stmt_post_7 1
|
|
46
|
Age_step_stmt_assign 1
|
|
47
|
Age_step_stmt_assign_2 1
|
|
48
|
Age_step_stmt_assign_3 4
|
|
49
|
Age_step_stmt_assign_4 2
|
|
50
|
Age_step_stmt_assign_5 4
|
|
51
|
Age_step_stmt_assign_6 1
|
|
52
|
Age_step_stmt_assign_7 1
|
|
53
|
Age_step_assign 1
|
|
54
|
top_reset 14 14 100%
|
|
55
|
top_reset_post 1
|
|
56
|
top_reset_post_2 1
|
|
57
|
top_reset_stmt_post 1
|
|
58
|
top_reset_stmt_post_2 1
|
|
59
|
top_reset_stmt_post_3 1
|
|
60
|
top_reset_stmt_post_4 1
|
|
61
|
top_reset_stmt_assign 1
|
|
62
|
top_reset_stmt_assign_2 1
|
|
63
|
top_reset_stmt_assign_3 1
|
|
64
|
top_reset_stmt_assign_4 1
|
|
65
|
top_reset_assign 10
|
|
66
|
specialization_Age_reset_pre_at_top_reset_stmt_8 1
|
|
67
|
specialization_Age_reset_pre_at_top_reset_stmt_11 1
|
|
68
|
specialization_Sofar_reset_pre_at_top_reset_stmt_14 1
|
|
69
|
top_step 45 47 95.7%
|
|
70
|
top_step_post 1
|
|
71
|
top_step_post_2 1
|
|
72
|
top_step_post_3 1
|
|
73
|
top_step_stmt_post 1
|
|
74
|
top_step_stmt_post_2 1
|
|
75
|
top_step_stmt_post_3 1
|
|
76
|
top_step_stmt_post_4 1
|
|
77
|
top_step_stmt_post_5 1
|
|
78
|
top_step_stmt_post_6 1
|
|
79
|
top_step_stmt_post_7 1
|
|
80
|
top_step_stmt_post_8 0
|
|
81
|
top_step_stmt_post_9 1
|
|
82
|
top_step_stmt_post_10 1
|
|
83
|
top_step_stmt_post_11 1
|
|
84
|
top_step_stmt_post_12 1
|
|
85
|
top_step_stmt_post_13 1
|
|
86
|
top_step_stmt_post_14 0
|
|
87
|
top_step_stmt_post_15 1
|
|
88
|
top_step_stmt_post_16 1
|
|
89
|
top_step_stmt_post_17 1
|
|
90
|
top_step_stmt_assign 1
|
|
91
|
top_step_stmt_assign_2 1
|
|
92
|
top_step_stmt_assign_3 1
|
|
93
|
top_step_stmt_assign_4 1
|
|
94
|
top_step_stmt_assign_5 1
|
|
95
|
top_step_stmt_assign_6 1
|
|
96
|
top_step_stmt_assign_7 1
|
|
97
|
top_step_stmt_assign_8 8
|
|
98
|
top_step_stmt_assign_9 2
|
|
99
|
top_step_stmt_assign_10 1
|
|
100
|
top_step_stmt_assign_11 1
|
|
101
|
top_step_stmt_assign_12 1
|
|
102
|
top_step_stmt_assign_13 1
|
|
103
|
top_step_stmt_assign_14 6
|
|
104
|
top_step_stmt_assign_15 1
|
|
105
|
top_step_stmt_assign_16 1
|
|
106
|
top_step_stmt_assign_17 4
|
|
107
|
top_step_assign 14
|
|
108
|
specialization_Age_step_pre_at_top_step_stmt_56 1
|
|
109
|
specialization_Age_step_pre_at_top_step_stmt_56_2 1
|
|
110
|
specialization_Age_step_pre_at_top_step_stmt_56_3 1
|
|
111
|
specialization_Age_step_pre_at_top_step_stmt_59 1
|
|
112
|
specialization_Age_step_pre_at_top_step_stmt_59_2 1
|
|
113
|
specialization_Age_step_pre_at_top_step_stmt_59_3 1
|
|
114
|
specialization_Sofar_step_pre_at_top_step_stmt_81 1
|
|
115
|
specialization_Sofar_step_pre_at_top_step_stmt_81_2 1
|
|
116
|
specialization_Sofar_step_pre_at_top_step_stmt_81_3 1
|
|
117
|
----------------------------------------------------------
|