[PVS-Help] Defining PVS Recursive Function

[chanyen hui <chanyen.hui@xxxxxxxxx>]

Dear all,
             I have part of code as below: 
int P(int S, int N) {
	          int sum=0;
	          if ( (S==1) || (N==0) ) return 1;
	         else {
		                for (int i=0; i<=N; ++i) {
			                     sum = sum + P(S-1,i);
            } 
		      }
	       return sum;
	}

I need help in translating this into PVS recursive function? 

Thanks,

Chanyen