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

Re: [PVS-Help] Unit composition in PVS



Probably you could just add an uninterpreted positive real constant m, and then work with
in the following way:


test: theory
begin
  m: posreal
  s: posreal
  some_property: lemma 4 * m * 2 * m = 8 * m^2
  some_other: lemma 4 * m / (2 * s) = 2 * (m / s)
end test

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