[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] loop in PVS
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?