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

Re: [PVS-Help] Unit composition in PVS



For lengths, I’ve tried creating a “lengths” theory similar to the reals theory in the PVS prelude, but I’m stuck here:
length_plus_length_is_length :

  |-------
{1}   FORALL (x, y): length_pred(x + y)

Rule? (skeep)
Skolemizing and keeping names of the universal formula in (+ -),
this simplifies to:
length_plus_length_is_length :

  |-------
{1}   length_pred(x + y)

Rule? (lemma "lengths.closed_plus" ("x" "x" "y" "y"))
Applying lengths.closed_plus where
  x gets x,
  y gets y,
this simplifies to:
length_plus_length_is_length :

{-1}  length_pred(x + y)
  |-------
[1]   length_pred(x + y)

Rule?

I’ve tried “assert”, “smash”, “grind”, etc., but nothing seems to resolve this seemingly simple statement…

(Note that length_pred is an undefined function that I’ve attempted to “define” via axioms, such as closed_plus, etc.)

Best Regards,
Ben Hocking




On Apr 22, 2015, at 9:15 AM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> 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