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

# Re: [PVS-Help] Unit composition in PVS

```Hi Ben,

We tried to capture dimensions and units using the PVS type system, and
failed.  Since then we have started adding it to PVS, then worked on
adding it to Simulink, and wrote a paper laying out the theory:

Automatic Dimensional Analysis of Cyber-Physical Systems,
by Sam Owre, Indranil Saha, and Natarajan Shankar,
in FM 2012: Formal Methods Lecture Notes in Computer Science pages 356-371.

We will continue adding it to PVS when there is time available.

As for your proof, you should try 'C-u M-x show-expanded-sequent'; this
often shows where mismatches occur.  My guess is you have two different
'+' operators.

If you still have problems, please send your specs to me so I can debug
this.

Thanks,
Sam

Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:

> 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
> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
>
>     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
>     ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
>
>         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
>         ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
>
>             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
>                 ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
>

```