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.
You 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
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
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.