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

Proofing problem

Dear PVS-experts!

Sorry to bother you with a maybe trivial question.
My problem is, PVS wants me to proof:

{-1}  interval > 0
{-2}  interval <= max_interval
[-3]  number_intervals > 0
[-4]  p!1 >= 0
[-5]  p!1 < number_intervals
[1]   interval * number_intervals > p!1 * interval - interval

where interval and number_intervals are of type nat.
The (grind) command wont work, so my question is, do I have problems
whith my specification, or is it that I just don't know the right proofing

Thanks a lot for your attention, maybe you can help a rookie.

Best Regards,
wilfried steiner