Wiki Agenda Contact Version française

A Formally Verified Interpreter for the Shell-like Language CoLiS

The shell-like language CoLiS is described with abstract syntax trees and a formal semantics defined by inductive predicates. An interpreter is written in Why3 and proved correct and complete with respect to the semantics.


Authors: Nicolas Jeannerod

Topics: Inductive predicates / Ghost code

Tools: Why3

References: CoLiS project

see also the index (by topic, by tool, by reference, by year)


download ZIP archive
The source code of this example is split into several files.

Why3 Proof Results for Project "interpreter"

Theory "interpreter.CorrectTermInterpreter": fully verified in 138.96 s

ObligationsAlt-Ergo (1.30)Eprover (1.9.1-001)Z3 (4.5.0)
VC for interp_builtin0.06------
VC for interp_term---------
split_goal_wp
  1. postcondition---0.24---
2. postcondition---0.24---
3. exceptional postcondition---0.27---
4. exceptional postcondition0.32------
5. exceptional postcondition0.08------
6. exceptional postcondition0.08------
7. exceptional postcondition0.07------
8. exceptional postcondition0.17------
9. exceptional postcondition0.07------
10. exceptional postcondition0.08------
11. exceptional postcondition0.08------
12. postcondition---43.18---
13. exceptional postcondition---0.60---
14. postcondition---44.14---
15. exceptional postcondition---0.65---
16. postcondition1.81------
17. exceptional postcondition1.89------
18. exceptional postcondition1.80------
19. exceptional postcondition1.81------
20. exceptional postcondition0.12------
21. exceptional postcondition0.33------
22. exceptional postcondition0.32------
23. postcondition------0.49
24. exceptional postcondition------0.46
25. exceptional postcondition------0.44
26. exceptional postcondition------0.48
27. postcondition1.88------
28. exceptional postcondition1.43------
29. exceptional postcondition1.90------
30. exceptional postcondition1.85------
31. exceptional postcondition0.32------
32. exceptional postcondition0.33------
33. postcondition0.06------
34. exceptional postcondition0.06------
35. exceptional postcondition0.06------
36. exceptional postcondition0.05------
37. postcondition------0.06
38. exceptional postcondition------0.06
39. exceptional postcondition------0.06
40. exceptional postcondition------0.07
41. postcondition2.01------
42. postcondition1.69------
43. exceptional postcondition------0.07
44. exceptional postcondition------0.07
45. exceptional postcondition0.11------
46. exceptional postcondition0.35------
47. exceptional postcondition0.32------
48. postcondition0.06------
49. exceptional postcondition0.07------
50. postcondition0.06------
51. exceptional postcondition0.06------
52. exceptional postcondition0.05------
53. postcondition0.07------
54. postcondition0.06------
55. postcondition0.47------
56. exceptional postcondition0.49------
57. exceptional postcondition0.51------
58. exceptional postcondition0.53------
59. postcondition0.55------
60. exceptional postcondition0.48------
61. exceptional postcondition0.50------
62. exceptional postcondition0.47------
63. postcondition0.53------
64. exceptional postcondition0.48------
65. exceptional postcondition0.55------
66. exceptional postcondition0.50------
67. postcondition0.52------
68. exceptional postcondition0.49------
69. exceptional postcondition0.50------
70. exceptional postcondition0.51------
VC for interp_for---------
split_goal_wp
  1. postcondition---0.28---
2. postcondition0.18------
3. exceptional postcondition0.12------
4. exceptional postcondition0.14------
5. exceptional postcondition0.14------
6. postcondition------0.12
7. exceptional postcondition------0.12
8. exceptional postcondition------0.12
9. exceptional postcondition------0.11
10. exceptional postcondition0.15------
11. exceptional postcondition------0.11
12. exceptional postcondition2.05------
VC for interp_call---------
split_goal_wp
  1. postcondition---0.31---
2. postcondition0.07------
3. exceptional postcondition0.07------
4. exceptional postcondition0.07------
5. postcondition0.08------
6. exceptional postcondition0.07------
7. exceptional postcondition0.08------
8. postcondition0.40------
9. exceptional postcondition0.39------
10. exceptional postcondition0.24------
11. postcondition0.32------
12. exceptional postcondition0.42------
13. exceptional postcondition0.26------
VC for interp_sexpr0.09------
VC for interp_sexpr_aux---------
split_goal_wp
  1. postcondition0.04------
2. postcondition---------
eliminate_let
  1. VC for interp_sexpr_aux---------
split_all_full
  1. VC for interp_sexpr_aux0.10------
2. VC for interp_sexpr_aux0.04------
3. VC for interp_sexpr_aux0.42------
4. VC for interp_sexpr_aux0.16------
5. VC for interp_sexpr_aux0.48------
6. VC for interp_sexpr_aux0.51------
7. VC for interp_sexpr_aux0.14------
8. VC for interp_sexpr_aux0.54------
VC for interp_sfrag_aux---------
split_goal_wp
  1. postcondition0.05------
2. postcondition0.04------
3. postcondition------0.06
4. postcondition------0.06
5. postcondition---------
inversion_pr
  1. postcondition0.06------
2. postcondition0.05------
3. postcondition0.05------
4. postcondition0.06------
5. postcondition0.06------
6. postcondition0.05------
7. postcondition0.05------
8. postcondition0.05------
9. postcondition0.06------
10. postcondition0.06------
11. postcondition0.06------
12. postcondition0.06------
13. postcondition0.05------
14. postcondition0.06------
15. postcondition0.06------
16. postcondition0.06------
17. postcondition0.06------
18. postcondition------2.39
19. postcondition0.06------
20. postcondition0.05------
21. postcondition0.05------
22. postcondition0.05------
VC for interp_lexpr0.07------
VC for interp_lexpr_aux3.70------
VC for interp_lfrag_aux0.08------
VC for interp_process0.80------

Theory "interpreter.TerminatingTermInterpreter": fully verified in 278.04 s

ObligationsAlt-Ergo (1.30)CVC4 (1.5-prerelease)Z3 (4.5.0)
VC for interp_builtin0.04------
VC for interp_term---------
split_goal_wp
  1. postcondition1.66------
2. postcondition1.12------
3. exceptional postcondition1.74------
4. precondition2.54------
5. variant decrease0.09------
6. precondition1.94------
7. exceptional postcondition0.71------
8. exceptional postcondition0.14------
9. exceptional postcondition0.13------
10. exceptional postcondition0.13------
11. precondition2.44------
12. variant decrease0.09------
13. precondition1.95------
14. exceptional postcondition0.69------
15. exceptional postcondition0.12------
16. exceptional postcondition0.13------
17. exceptional postcondition0.11------
18. precondition2.49------
19. variant decrease0.10------
20. precondition1.82------
21. postcondition------1.86
22. exceptional postcondition------1.02
23. precondition2.69------
24. variant decrease0.08------
25. precondition1.86------
26. postcondition------1.31
27. exceptional postcondition------1.23
28. precondition1.75------
29. variant decrease0.05------
30. precondition3.31------
31. precondition------0.74
32. variant decrease0.15------
33. precondition------3.16
34. postcondition------0.52
35. exceptional postcondition------0.55
36. exceptional postcondition------0.52
37. exceptional postcondition------0.55
38. exceptional postcondition------0.64
39. exceptional postcondition------1.69
40. exceptional postcondition------1.88
41. precondition1.91------
42. variant decrease0.07------
43. precondition------0.44
44. precondition------1.24
45. variant decrease0.06------
46. precondition------2.39
47. postcondition------0.51
48. exceptional postcondition------0.49
49. exceptional postcondition------0.48
50. exceptional postcondition------0.45
51. precondition------1.52
52. variant decrease0.07------
53. precondition------1.18
54. postcondition------0.44
55. exceptional postcondition------0.41
56. exceptional postcondition------0.48
57. exceptional postcondition------0.48
58. exceptional postcondition------1.97
59. exceptional postcondition------1.97
60. precondition2.70------
61. variant decrease0.09------
62. precondition1.87------
63. variant decrease0.09------
64. precondition------3.20
65. postcondition0.08------
66. exceptional postcondition0.07------
67. exceptional postcondition0.05------
68. exceptional postcondition0.05------
69. precondition0.91------
70. variant decrease0.20------
71. precondition------0.46
72. precondition------0.90
73. variant decrease0.25------
74. precondition------1.54
75. precondition------2.58
76. variant decrease0.23------
77. precondition------2.86
78. postcondition------0.48
79. exceptional postcondition------0.51
80. exceptional postcondition------0.56
81. exceptional postcondition------0.57
82. postcondition------4.23
83. postcondition------4.14
84. exceptional postcondition------2.03
85. exceptional postcondition------2.15
86. exceptional postcondition------0.63
87. exceptional postcondition------1.97
88. exceptional postcondition------1.93
89. precondition2.76------
90. variant decrease0.06------
91. precondition1.69------
92. postcondition0.11------
93. exceptional postcondition0.14------
94. exceptional postcondition0.09------
95. postcondition0.15------
96. exceptional postcondition0.14------
97. postcondition0.09------
98. exceptional postcondition0.14------
99. precondition2.52------
100. variant decrease0.08------
101. precondition2.18------
102. variant decrease0.09------
103. precondition------2.50
104. postcondition0.06------
105. exceptional postcondition0.05------
106. exceptional postcondition0.06------
107. postcondition1.45------
108. postcondition2.15------
109. precondition2.70------
110. variant decrease0.10------
111. precondition2.60------
112. variant decrease0.16------
113. precondition------2.45
114. postcondition1.75------
115. exceptional postcondition1.87------
116. exceptional postcondition1.95------
117. exceptional postcondition1.82------
118. variant decrease0.14------
119. precondition------1.06
120. postcondition1.86------
121. exceptional postcondition2.03------
122. exceptional postcondition1.94------
123. exceptional postcondition1.85------
124. variant decrease0.16------
125. precondition------2.47
126. postcondition1.90------
127. exceptional postcondition2.04------
128. exceptional postcondition2.02------
129. exceptional postcondition1.95------
130. variant decrease0.14------
131. precondition------2.69
132. postcondition1.75------
133. exceptional postcondition1.89------
134. exceptional postcondition1.84------
135. exceptional postcondition1.84------
VC for interp_for---------
split_goal_wp
  1. postcondition0.15------
2. precondition0.29------
3. variant decrease0.07------
4. precondition0.43------
5. postcondition0.16------
6. exceptional postcondition0.15------
7. exceptional postcondition0.13------
8. exceptional postcondition0.13------
9. precondition0.17------
10. variant decrease0.07------
11. precondition0.45------
12. precondition---0.22---
13. variant decrease0.14------
14. precondition---0.20---
15. postcondition10.85------
16. exceptional postcondition---0.47---
17. exceptional postcondition12.33------
18. exceptional postcondition12.03------
19. exceptional postcondition17.01------
20. exceptional postcondition17.31------
21. exceptional postcondition16.76------
VC for interp_call---------
split_goal_wp
  1. postcondition0.43------
2. postcondition0.26------
3. exceptional postcondition0.24------
4. exceptional postcondition0.29------
5. postcondition0.25------
6. exceptional postcondition0.25------
7. exceptional postcondition0.34------
8. precondition0.70------
9. variant decrease0.07------
10. precondition2.03------
11. postcondition------0.06
12. exceptional postcondition------0.05
13. exceptional postcondition0.73------
14. postcondition------0.06
15. exceptional postcondition------0.05
16. exceptional postcondition0.75------
VC for interp_sexpr0.76------
VC for interp_sexpr_aux---------
split_goal_wp
  1. postcondition0.09------
2. precondition0.13------
3. variant decrease0.07------
4. precondition0.10------
5. variant decrease0.08------
6. precondition---0.27---
7. postcondition---0.23---
VC for interp_sfrag_aux---------
split_goal_wp
  1. postcondition0.11------
2. postcondition0.05------
3. postcondition0.26------
4. postcondition0.27------
5. precondition0.17------
6. variant decrease0.05------
7. precondition0.28------
8. postcondition1.02------
9. postcondition0.11------
10. postcondition1.08------
11. postcondition1.07------
VC for interp_lexpr0.78------
VC for interp_lexpr_aux---------
split_goal_wp
  1. postcondition0.07------
2. precondition0.10------
3. variant decrease0.06------
4. precondition0.10------
5. variant decrease0.08------
6. precondition---0.21---
7. postcondition------1.94
VC for interp_lfrag_aux1.17------
VC for interp_process---------
split_goal_wp
  1. precondition2.51------
2. variant decrease0.09------
3. precondition1.71------
4. postcondition2.40------
5. postcondition0.13------
6. postcondition1.64------
7. postcondition1.66------

Theory "interpreter.Interpreter": fully verified in 0.05 s

ObligationsAlt-Ergo (1.30)
VC for populate_penv0.05
VC for interp_program---
split_goal_wp