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

*To*: pvs-help@csl.sri.com*Subject*: [PVS-Help] regarding properties of floor and ceiling*From*: Nikhil Kikkeri <nikhil.kikkeri@gmail.com>*Date*: Mon, 27 Feb 2006 15:51:06 -0600*DomainKey-Signature*: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com;h=received:message-id:date:from:reply-to:organization:user-agent:x-accept-language:mime-version:to:subject:content-type:content-transfer-encoding;b=iS+JiFZUsoOpYEM7k597GyfL8KkXffdpJMaJdqPcer6Wkmh5aZga7CAUNrZumC+ODqeKLxdUU4vrQ+FtJk684f7LEpYnNdUVkS6CZ0dC33qh/J/PhLy+7cgbkS9mwq0/3hN1LEVwt2vJUxCkFF9Bfff+ZtUXciFg2d270ga6m3s=*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>*Organization*: SMU*Reply-To*: nikhil.kikkeri@gmail.com*Sender*: pvs-help-bounces+archive=csl.sri.com@csl.sri.com*User-Agent*: Mozilla Thunderbird 1.0.2 (Windows/20050317)

Hi-- This is a long e-mail. I am dealing with the following problem consider the following bitvector of length 6 101011 -> x If i divide this bitvector by 2^5 = 32 I have a real number equal to 1.34375 Assume that I chop of the bitvector as shown 1010 -> the head 11 -> the tail this chopping off is nothing but taking the floor of the real number above. If the leftmost bit has weight 2^0 then the rightmost bit has weight 2^-k (here k = 5) so if I want a bitvector of precision 3 then I simply say 2^-3*floor(x*2^-5*2^3) where x is the original bitvector which is nothing but the head and its value works out to 1.25. the tail works out to be 0.9375 which is nothing but 2^-P*fractional(x*2^-k*2^P) . so what I have is x*2^-k = 2^-P*floor(x*2^-k+P) + 2^-P*fractional(x*2^-k+P) Also at all times P is strictly lesser than k Now if I move away from bitvectors to a general case for any real number of the type y*2^-k where y is of type natural then I face a problem in proving some essential properties that can be easily shown with bitvectors. For example I should be able to prove 2^-P*fractional(x*2^-k+P) <= 2^-P - 2^-k which in terms of bv is the maximum value of a bitvector it can be easily shown that 2^-P*fractional(x*2^-k+P) < 2^-P by the properties of floor in the prelude but the above property is more strict and relates fractionals with bitvectors. Also it would be nice to show that if 2^-P*fractional(x*2^-k+P) /=0 Then 2^-P*fractional(x*2^-k+P) >= 2^-k the only thing I have done so far is used the floor and ceiling definitions and floor_within_1 and floor_0 lemmas to see how far I can go, but it just keeps me going through circles. Any clues to solve this would be of great help. Thank you rgds -nikhil

- Prev by Date:
**[PVS-Help] Regular expressions** - Next by Date:
**[PVS-Help] PVS Hangs** - Prev by thread:
**Re: [PVS-Help] PVS Hangs** - Next by thread:
**[PVS-Help] Regular expressions** - Index(es):