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

Re: [PVS-Help] Unit composition in PVS



Attached:

Attachment: lengths.prf
Description: Binary data

Attachment: lengths.pvs
Description: Binary data

Best Regards,
Ben Hocking
ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx




> On Apr 28, 2015, at 2:26 PM, Sam Owre <owre@xxxxxxxxxxx> wrote:
> 
> Hi Ben,
> 
> It does look like a bug - could you send me your PVS theory?
> 
> Thanks,
> 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
>>>>