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

[PVS-Help] Another rookie question



Hi,

  I got another rookie question: give a bool expression, how can I do
variable restriction using PVS?
  e.g. FORALL (x: int), (y: int): x > 10 & z = x+y
How to find out the constraints on z using PVS? And how to do it in Batch
mode?

yours,
Sun Jun