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

[PVS-Help] Measure Induction



Hi--

I would be grateful if measure-induction is the proper way to prove certain 
things below .If not if there is an alternate way.

say that i have two bitvectors, each of length 32. call them r1 and r2. Let 
r1 hold some data which I need to left shift. However the shifting is done 
as following

if r1 has the data that is to be shifted and r2 holds some sort of counter, 
the repeated addition of r1 with itself produces its shifted version, like 
this

while(bv2nat(r2) != 0) {
  r1 = r1+r1
  r2 = r2 - 1

}

if i put this in PVS the thing above would appear

self_add(rs1:bvec[32],rs2:bvec[32]): RECURSIVE bvec[32] =
    IF  rs2 = fill[32](FALSE) THEN   %if shift amount is zero
        rs1
    ELSE
        self_add(rs1+rs1,rs2-1)
    ENDIF
    MEASURE bv2nat(rs2)

add_is_left_shift:LEMMA
  FORALL(rs1:bvec[32],rs2:bvec[32]):
       self_add(rs1,rs2) = left_shift(bv2nat(rs2),rs1)


for the above lemma is measure-induct the proper way to proceed.since i am 
kind of clueless about measure-induct can someone give me a rough 
"paper-and-pencil" idea about what needs to be done?

Thanks

rgds
-NDK

---
http://engr.smu.edu/~nikhil

_________________________________________________________________
Reach out to over a million NRIs. 
http://www.sulekha.com/classifieds/cllist.aspx?nma=IN&ref=msn Get great 
responses for your ads.