equal
deleted
inserted
replaced
60 |
60 |
61 IMPORTANT: |
61 IMPORTANT: |
62 This is a logic of partial correctness. You can only prove that your program |
62 This is a logic of partial correctness. You can only prove that your program |
63 does the right thing <i>if</i> it terminates, but not <i>that</i> it |
63 does the right thing <i>if</i> it terminates, but not <i>that</i> it |
64 terminates. |
64 terminates. |
|
65 A logic of total correctness is also provided and described below. |
|
66 |
|
67 <H3>Total correctness</H3> |
|
68 |
|
69 To prove termination, each WHILE-loop must be annotated with a variant: |
|
70 <UL> |
|
71 <LI> <kbd>WHILE _ INV {_} VAR {_} DO _ OD</kbd> |
|
72 </UL> |
|
73 A variant is an expression with type <kbd>nat</kbd>, which may use program |
|
74 variables and normal variables. |
|
75 <P> |
|
76 |
|
77 A total-correctness goal has the form |
|
78 <PRE> |
|
79 VARS x y ... [P] prog [Q] |
|
80 </PRE> |
|
81 enclosing the pre- and postcondition in square brackets. |
|
82 <P> |
|
83 |
|
84 Methods <kbd>vcg_tc</kbd> and <kbd>vcg_tc_simp</kbd> can be used to derive |
|
85 verification conditions. |
|
86 <P> |
|
87 |
|
88 From a total-correctness proof, a function can be extracted which |
|
89 for every input satisfying the precondition returns an output |
|
90 satisfying the postcondition. |
65 |
91 |
66 <H3>Notes on the implementation</H3> |
92 <H3>Notes on the implementation</H3> |
67 |
93 |
68 The implementation loosely follows |
94 The implementation loosely follows |
69 <P> |
95 <P> |