1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
CORE dfcc-only
main.c
--dfcc main --apply-loop-contracts --replace-call-with-contract ackermann
^\[ackermann.precondition\.\d+\] line \d+ Check requires clause of contract contract\:\:ackermann for function ackermann: SUCCESS$
^\[ackermann.assigns.\d+\] line \d+ Check that the assigns clause of contract\:\:ackermann is included in the caller\'s assigns clause: SUCCESS$
^VERIFICATION SUCCESSFUL$
^EXIT=0$
^SIGNAL=0$
--
--
It tests whether we can prove (only partially) the termination of the Ackermann
function using a multidimensional decreases clause.
Note that this particular implementation of the Ackermann function contains
both a while-loop and recursion. Therefore, to fully prove the termination of
the Ackermann function, we must prove both
(i) the termination of the while-loop and
(ii) the termination of the recursion.
Because CBMC does not support termination proofs of recursions (yet), we cannot
prove the latter, but the former. Hence, the termination proof in the code is
only "partial."
Furthermore, the Ackermann function has a function contract that the result
is always non-negative. This post-condition is necessary for establishing
the loop invariant. However, in this test, we do not enforce the function
contract. Instead, we assume that the function contract is correct and use it
(i.e. replace a recursive call of the Ackermann function with its contract).
We cannot verify/enforce the function contract of the Ackermann function, since
CBMC does not support function contracts for recursively defined functions.
As of now, CBMC only supports function contracts for non-recursive functions.
|
