18.4 Function call
Still following the syntax of ML, the function application is written
(f a1 ... an), where f is a function and the ai's
its arguments. Notice that f and the ai's may be annotated
programs themselves.
In the general case, f is a function already specified (either with
Global Variable or with a proof of correctness) and has a
pre-condition Pf and a post-condition Qf.
As expected, a proof obligation is generated, which correspond to
Pf applied to the values of the arguments, once they are evaluated.
Regarding the post-condition of f, there are different possible cases:
-
either you did not annotate the function call, writing directly
(f a1 ... an)
and then the post-condition of f is added automatically
if possible: indeed, if some arguments of f make side-effects
this is not always possible. In that case, you have to put a
post-condition to the function call by yourself;
- or you annotated it with a post-condition, say Q:
(f a1 ... an) { Q }
then you will have to prove that Q holds under the hypothesis that
the post-condition Qf holds (where both are
instantiated by the results of the evaluation of the ai).
Of course, if Q is exactly the post-condition of f then
the corresponding proof obligation will be automatically
discharged.