[PVS-Help] loop in PVS

[lingzhao <maolzh@xxxxxxxxx>]

    Assuming  a N nodes ring,the state of each node is set to 1 or 0. I
want to calculate the sum of nodes whose state is 1,Which can be
obtained by s(0)+s(1)+...+s(N-1)+S(N). 
    It can be easily expressed in  programming language using  for or
while loop,but it seems a bit hard to express in PVS,I have to use
recursive function defined as follows:
    sum(s)(n): recursive nat=
    if(n)=0 then s(0) else sum(s)(n-1)+s(n)
   
    And then apply it to s,N  sum(s)(N)
    Is there a convenience way to do that?

    Thanks
    Lingzhao.