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

*To*: pvs-help@csl.sri.com*Subject*: [PVS-Help] Measure Induction*From*: "Nikhil D. Kikkeri" <nikhil23@hotmail.com>*Date*: Tue, 26 Jul 2005 03:20:59 +0530*List-Help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-Id*: PVS-Help <pvs-help.csl.sri.com>*List-Post*: <mailto:pvs-help@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*Reply-To*: nikhil.kikkeri@gmail.com*Sender*: pvs-help-bounces+archive=csl.sri.com@csl.sri.com

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.

- Prev by Date:
**Re: [PVS-Help] prop simplification of COND** - Next by Date:
**[PVS-Help] Turning let declarations into name equalities** - Prev by thread:
**Re: [PVS-Help] Turning let declarations into name equalities** - Next by thread:
**[PVS-Help] measure induction** - Index(es):