|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.)|
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
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
On 04/22/2015 04:15 PM, Ben Hocking
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).
I really like the idea of using
uninterpreted positive real constants. This is far
simpler than the approach I’ve been using.
can also do something like:
cm: posreal = m / 100
m_to_cm: lemma 2.5 * m = 250 * cm
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.