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

Re: [PVS-Help] Unit composition in PVS



Hi Sam,

I’m also attempting an alternative approach (based somewhat on your "Automatic Dimensional Analysis of Cyber-Physical Systems" paper), but I was wondering if it’s possible to define “+” for arbitrary types. For example, in the following theory:

measurements: THEORY
BEGIN

  IMPORTING reals@sqrt

  % Will eventually include charge, etc.                                                                                                                                                                  
  measurement: TYPE =
    [#
      value:      real,
      length_dim: real,
      time_dim:   real,
      mass_dim:   real
     #]

  dimension_match(x: measurement, y: measurement): bool =
    (x`length_dim = y`length_dim) AND
    (x`time_dim = y`time_dim) AND
    (x`mass_dim = y`mass_dim)

  plus(x: measurement, y: {m: measurement | dimension_match(x, m)}): measurement =
    x WITH [`value := x`value + y`value]

END measurements

If I try to change “plus” to “+”, I get the message "Found ':' when expecting ‘)’”, which is not completely surprising, but when I look in the prelude, I see that “+” is defined for numfield like this:
  +, -, *: [numfield, numfield -> numfield]

I also experimented with simply:
  +: [measurement, measurement -> measurement]
but that results in a similar message - "Found ':' when expecting 'unaryop, `, etc."

Best Regards,
Ben Hocking
ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx

> On Apr 30, 2015, at 6:53 PM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
> 
> Hi all,
> 
> While I have had much success since Sam helped me to understand what I was doing wrong previously, I’m now running into two issues in the attached code:
> <units.tgz>
> 
> First, and easiest to reproduce, is what appears to be some sort of non-ending loop. In the attached example, the theory siso_test as-is can be proven with 15 TCCs. However, if you restore the first line in valve parameters:
>  valve_max_flow_rate: posvolume_per_time = 0.1 * m^3 / s
> it apparently takes forever to finish. (Possibly not forever, but I’ve seen no evidence that it’s doing anything but garbage collecting.) I’ve tried this in a variety of settings, and the result is fairly consistent. Let me know if you’re unable to recreate.
> 
> Secondly, it seems that I’m needing to use “::real” in many places where it should not be necessary, and where adding it in similar places breaks the specification. For example, consider the following line from lengths.pvs:
>  length_pred_ax: AXIOM length_pred(0::real) AND length_pred(0 * m) AND length_pred(m)
> 
> If I remove the ::real, I get the message:
>  Expecting an expression
>  No resolution for length_pred with arguments of possible types:
>    0 : reals.real
> 
> However, if I now add the following line above it:
>  f, g:      VAR real
> the ::real is not needed in the length_pred_ax line.
> 
> In fact, if I add it back, I now get the message:
>  Expecting an expression
>  No resolution for length_pred with arguments of possible types:
>    0:: real : reals.real
> 
> Note that these results seem to have a bit of Heisenberg uncertainty involved, so you might have to try some variations on this to see it.
> 
> Thank you,
> Ben Hocking
> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
> 
> 
>> On Apr 28, 2015, at 3:55 PM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
>> 
>> Excellent, thank you very much.
>> 
>> I had originally attempted to allow complex lengths, but decided to back away from that for now, so just changing number to real works for me.
>> 
>> Best Regards,
>> Ben Hocking
>> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
>> 
>> 
>> 
>> 
>>> On Apr 28, 2015, at 3:52 PM, Sam Owre <owre@xxxxxxxxxxx> wrote:
>>> 
>>> Hi Ben,
>>> 
>>> It turns out there are two definitions for length_pred.  One is
>>> automatically generated from the declaration
>>> 
>>> length: NONEMPTY_TYPE FROM real
>>> 
>>> which generates (run "M-x ppe" to see this)
>>> 
>>> length_pred: [real -> boolean]
>>> 
>>> Then you define another one over numbers.  Removing your definition causes
>>> problems with the definition
>>> 
>>> length?(n: number): bool =
>>>  number_field_pred(n) and real_pred(n) AND length_pred(n)
>>> 
>>> but this can be fixed using coercions, i.e., "length_pred(n::real)"
>>> 
>>> With these changes I had no problem discharging the TCCs.
>>> 
>>> An alternative may be to define your length_pred over number to be equal
>>> to the other length_pred when restricted to real, but you can still see
>>> sequents that look like they should be trivial, but require a definition
>>> expansion.
>>> 
>>> I'm going to look into improving show-expanded-sequent so it makes this
>>> clearer.
>>> 
>>> Regards,
>>> Sam
>>> 
>>> Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
>>> 
>>>> Hi Sam,
>>>> 
>>>> Got back to this after working on something else for a while, when I used the ‘C-u M-x show-expanded-sequent’ command, I got the following:
>>>> ===================================
>>>> length_plus_length_is_length :
>>>> 
>>>> {-1}  length_pred((number_fields.+)(x, y))
>>>> |-------
>>>> {1}   length_pred((number_fields.+)(x, y))
>>>> ===================================
>>>> 
>>>> As far as I can tell, {-1} should imply {1} fairly cleanly. Neither ‘(assert)’ nor even ‘(grind)’ resolve this, but possibly the output from ‘(grind)’ is useful:
>>>> ===================================
>>>> The following errors occurred within the strategy:
>>>> 
>>>> Couldn't find a suitable quantified formula.
>>>> 
>>>> No suitable (+ve FORALL/-ve EXISTS) quantified expression found.
>>>> 
>>>> No change on: (grind)
>>>> length_plus_length_is_length :
>>>> 
>>>> [-1]  length_pred(x + y)
>>>> |-------
>>>> [1]   length_pred(x + y)
>>>> ===================================
>>>> 
>>>> The proof (from show-proof) is simply:
>>>> ("" (skeep) (lemma "closed_plus" ("x" "x" "y" "y")) (postpone))
>>>> 
>>>> Where the judgment being proven is:
>>>> length_plus_length_is_length:  JUDGEMENT +(x, y)   HAS_TYPE length
>>>> 
>>>> And the axiom closed_plus is:
>>>> closed_plus:    AXIOM length_pred(x + y) 
>>>> 
>>>> And the definition for x, y is:
>>>> x, y: VAR length
>>>> 
>>>> Best Regards,
>>>> Ben Hocking
>>>> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
>>>> 
>>>> 
>>>> 
>>>> 
>>>>> On Apr 23, 2015, at 6:05 PM, Sam Owre <owre@xxxxxxxxxxx> wrote:
>>>>> 
>>>>> 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
>>>>>> 
>>> 
>> 
>