Commit e40b8781 authored by MARCHE Claude's avatar MARCHE Claude

doc cosmetics

parent c4b5b91b
......@@ -11,16 +11,14 @@ VC generation for program functions
For each program function of the form
`let` :math:`f (x_1:t_1) (x_n:t_n) : t`
`requires` { :math:`Pre` }
`ensures` { :math:`Post` }
`=` :math:`body`
| let :math:`f (x_1:t_1) (x_n:t_n) : t`
| requires { :math:`Pre` }
| ensures { :math:`Post` }
| `=` :math:`body`
a new logic goal called `f'VC` is generated. Its shape is
.. math:: \forall x_1,..,x_n. Pre \rightarrow WP(body,Post)
| :math:`\forall x_1,..,x_n. Pre \rightarrow WP(body,Post)`
where :math:`WP(e,Q)` is a formula computed automatically using rules defined recursively on :math:`e`.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment