Obligations | Alt-Ergo (1.01) |
VC for mult_naive | --- |
split_goal_wp | |
| 1. precondition | 0.01 |
2. postcondition | 0.01 |
3. postcondition | 0.01 |
4. loop invariant init | 0.01 |
5. loop invariant init | 0.01 |
6. loop invariant preservation | 0.01 |
7. loop invariant preservation | 0.01 |
8. loop invariant init | 0.01 |
9. loop invariant preservation | 0.01 |
10. loop invariant preservation | 0.01 |
11. loop invariant init | 0.01 |
12. index in array bounds | 0.01 |
13. index in array bounds | 0.01 |
14. type invariant | 0.01 |
15. index in array bounds | 0.01 |
16. index in array bounds | 0.01 |
17. loop invariant preservation | 0.03 |
18. loop invariant preservation | 0.19 |
19. loop invariant preservation | 0.02 |
20. loop invariant preservation | 0.01 |
21. loop invariant preservation | 0.01 |
22. loop invariant preservation | 0.03 |
23. type invariant | 0.01 |
24. postcondition | 0.00 |
25. postcondition | 0.01 |