Blame testing/035_invariant.c
|
Packit Service |
50c9f2 |
// objective: test \invariant, \pre and \post commands
|
|
Packit Service |
50c9f2 |
// check: 035__invariant_8c.xml
|
|
Packit Service |
50c9f2 |
|
|
Packit Service |
50c9f2 |
/** \file */
|
|
Packit Service |
50c9f2 |
|
|
Packit Service |
50c9f2 |
/** \invariant i+j=p
|
|
Packit Service |
50c9f2 |
* \pre p\>=0
|
|
Packit Service |
50c9f2 |
* \post *q=2^(p+1)
|
|
Packit Service |
50c9f2 |
*/
|
|
Packit Service |
50c9f2 |
void func(int p,int *q)
|
|
Packit Service |
50c9f2 |
{
|
|
Packit Service |
50c9f2 |
int j = p, k=1, i;
|
|
Packit Service |
50c9f2 |
for (i=0; i<=p; i++) j--,k=k*2;
|
|
Packit Service |
50c9f2 |
*q = k;
|
|
Packit Service |
50c9f2 |
}
|