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

Re: [PVS-Help] Array Reversal

There are several ways to specify this problem in PVS. I would do something a little bit different:

1. I would parametrize the type of the array.

2. PVS supports dependent records, I would define a type record Arr with fields lb,ub, and the array ar. Notice that the types exploit the PVS predicate sub-typing features.

3. I would defined a currifyed version of reversed?, i.e., two separate parameters. This way, you can define reverse(a) of type (reversed?(a)). PVS will generate a TCC that is automatically discharged.

4. Instead of a recursive definition of reverse, I would prefer a direct definition. Notice that an array is just a function from indices to elements. The sanity check is simply discharged by
(grind) (decompose-equality 1) (decompose-equality 1)

reverse_program[T:TYPE] : THEORY

  Arr: TYPE = [#
    lb : nat,
    ub : upfrom(lb),
    ar : ARRAY[subrange(lb,ub)->T]

a,b : VAR Arr

  reversed?(a)(b) : bool =
    a`ub-a`lb = b`ub-b`lb AND
    FORALL (i:subrange(a`lb,a`ub)) :
      a`ar(i) = b`ar(b`ub-i+a`lb)

  reverse(a) : (reversed?(a)) = a WITH [
    ar := LAMBDA(i:subrange(a`lb,a`ub)) :

  rev_prop1 : LEMMA
    FORALL (a:Arr) : reverse(reverse(a)) = a

END reverse_program

If you want to animate the specification (via PVSio, see http://research.nianet.org/~munoz/PVSio) ,

  IMPORTING reverse_program[int]

  println(a:Arr) : void =
    print("[ ") &
    (FORALL (i:subrange(a`lb,a`ub)) :
       print(a`ar(i)+" ")) &

  A : Arr = (#
    lb := 1,
    ub := 3,
    ar := LAMBDA(i:subrange(1,3)):
            IF i=1 THEN 4
            ELSIF i=2 THEN 8
            ELSE 10
END io

Once you get the PVSio prompt via M-x pvsio, type, for example:
<PVSio> println(A);
[ 4 8 10 ]

<PVSio> println(reverse(A));
[ 10 8 4 ]

<PVSio> println(reverse(reverse(A)));
[ 4 8 10 ]


On Apr 12, 2008, at 8:29 PM, cozy shack wrote:
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

Cesar Munoz (NIA) munoz@xxxxxxxxxx