035_invariant.c File Reference

Go to the source code of this file.

Functions
void	func (int p, int *q)

Function Documentation

void func	(	int	p,
		int *	q
	)

Invariant

i+j=p

Precondition

p>=0

Postcondition

*q=2^(p+1)

Definition at line 10 of file 035_invariant.c.

{
  int j = p, k=1, i;
  for (i=0; i<=p; i++) j--,k=k*2;
  *q = k;
}