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

Re: [PVS-Help] Unit composition in PVS



You can also do something like:

  m: posreal
  cm: posreal = m / 100
  m_to_cm: lemma 2.5 * m = 250 * cm

Best regards,

Viorel Preoteasa

On 04/22/2015 01:16 AM, Ben Hocking wrote:
Is anyone familiar with work that has been done on unit composition in formal specifications within PVS? E.g., verifying that when you multiply meters by meters you get square meters?

I have some ideas on what I want to do (and have actually started down that path), but I don’t want to reinvent the wheel if this has already been done.

Best Regards,
Ben Hocking