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

Re: [PVS-Help] Unit composition in PVS



How does one syntactically check that the result does not contain any of the unit constants? I tried something like this, but every approach I used failed. If I could define “unitless?”, I could pretty much get everything else to work out.  E.g., “length?(x)” would be “unitless?(x/m)”. (I couldn’t prevent one from adding meters and seconds, but I could at least verify that certain inputs have the desired dimensions.)

Best Regards,
Ben Hocking




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

You are right. You cannot prevent adding or testing for measurements of different physical properties.
However if you start with an _expression_ which is correct from this point of view, then you preserve
its correctness.

You can test for unitless, by sintactically checking that the result does not contain any of the unit
constants. If you also manage to group mechanically all unit constants together, without any other
constant, then again, syntactically you should get some _expression_ that uses only * and / and the
unit constants.


Best regards,

Viorel Preoteasa

On 04/22/2015 04:15 PM, Ben Hocking wrote:
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