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

Re: [PVS-Help] Unit composition in PVS



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
> >>