[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.

```