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

Re: [PVS-Help] Unit composition in PVS



Hi Ben,

Overloading '+' is not a problem, here the problem is that the PVS parser
gets confused, as '+' is an infix operator, and it thinks it's still in
the preceding declaration.  To fix this, you need to put a semi-colon
(';') operator between the end of the 'dimension_match' definition and the
beginning of the '+' declaration.

Regards,
Sam

Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:

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