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

Re: [PVS-Help] Unit composition in PVS



Alas, it appears that the simplicity comes with a price. I cannot figure out a way to prevent meters and seconds from being added together, or more importantly of determining whether a particular measurement is of time, length, or is unitless (as examples).

Best Regards,
Ben Hocking




On Apr 22, 2015, at 8:01 AM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:

Viorel,

I really like the idea of using uninterpreted positive real constants. This is far simpler than the approach I’ve been using.

Best Regards,
Ben Hocking




On Apr 22, 2015, at 4:51 AM, Viorel Preoteasa <viorel.preoteasa@xxxxxxxx> wrote:

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