Re: [PVS-Help] R_pred

[Cesar Munoz <munoz@xxxxxxxxxx>]

Why should it work ? What is the definition of R?  For an arbitrary R,
the fact that R(x) and R(y) hold doesn't imply that R(x+y) holds. Take
R=odd? for example.


Jerome wrote:
> I have the following:
> 
>    [-1]  W(root, j!1) >= 0
>    [-2]  R_pred(W(root, j!1))
>    [-3]  distance(s!1)(root) >= 0
>    [-4]  R_pred(distance(s!1)(root))
>      |-------
>    [1]   R_pred(distance(s!1)(root) + W(root, j!1))
> 
> Why is "assert" not an adequate means of discharging? What am I
> missing? Thanks
> 
> jerome
> 
> 

-- 
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@xxxxxxxxxx
National Institute of Aerospace         mailto:Cesar.A.Munoz@xxxxxxxx
100 Exploration Way  Room 214       http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988
GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6  1A18 6000 89F5 C114 E6C4