[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Array Reversal

I'm new to PVS and software verification in general. I was able to prove simple theories using flatten, skoelm, inst, induct,.... etc. However, I wanna move to the next level and thus tried to prove an array reversal algorithm but I don't really know where to start and how to tackle this problem.
Here is the PVS code that I wrote:
And I hope you could help me first, whether I'm missing something in my code. second, how I prove this. Also, I'd really appreciate a breif on the usage of measure-induct. I coudn't totally understand it from the manual.
reverse_program: THEORY
a, b: VAR ARRAY [nat -> int]
l,u,lb,ub: VAR nat % These are always used for upper and lower array bounds
z: VAR int % Always used for some item in an array
reversed?(a,l,u,b,lb,ub):bool =
u-l = ub-lb AND (((u-l) <= 0) OR forall( j:{i:nat | 0 <= i AND i <= (u-l)}): a(j) = b(ub-j))
A_0: ARRAY [nat -> int]
N: nat
Reverse(l:nat, u:{i:nat | l <= i}, a): RECURSIVE ARRAY [nat -> int] =
IF l = u
ELSE Reverse(l+1, u-1, a WITH [(l) := a(u), (u) := a(l)])
MEASURE u-l by <
%% Sanity check:
reverse_prp_1: PROPOSITION FORALL(l:nat, u:{i:nat|l<=i}): Reverse(l, u, Reverse(l,u,a)) = a
reverse_prp_2: PROPOSITION reversed?(a, 0, N, Reverse(0,N,a), 0, N)
END reverse_program

Do You Yahoo!?
Tired of spam? Yahoo! Mail has the best spam protection around