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

[PVS-Help] regarding properties of floor and ceiling


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