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

*To*: Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx>*Subject*: Re: [PVS-Help] Unit composition in PVS*From*: Sam Owre <owre@xxxxxxxxxxx>*Date*: Tue, 28 Apr 2015 12:52:03 -0700*Cc*: Sam Owre <owre@xxxxxxxxxxx>, pvs-help@xxxxxxxxxxx*Comments*: In-reply-to Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> message dated "Tue, 28 Apr 2015 14:13:43 -0400."*In-reply-to*: <EDAA7EF5-2915-4F2D-BF18-47C77128B8B6@dependablecomputing.com>*List-archive*: <http://mls.csl.sri.com/pipermail/pvs-help>*List-help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-id*: PVS-Help <pvs-help.csl.sri.com>*List-post*: <mailto:pvs-help@csl.sri.com>*List-subscribe*: <https://mls.csl.sri.com/cgi-bin/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-unsubscribe*: <https://mls.csl.sri.com/cgi-bin/mailman/options/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <11131_1429656958_5536D57D_11131_7796_1_6C39E08D-CB62-45E7-B5FC-033EFB34BDCD@dependablecomputing.com> <553760FD.3060703@aalto.fi> <999AA24A-88DA-44CB-8978-EEC2AF1DC478@dependablecomputing.com> <D044D911-511E-4D84-8D4B-21511B1B86A9@dependablecomputing.com> <74403C29-F83B-426F-9788-B67B729A3476@dependablecomputing.com> <23921.1429826758@ubi> <EDAA7EF5-2915-4F2D-BF18-47C77128B8B6@dependablecomputing.com>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

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

**Follow-Ups**:**Re: [PVS-Help] Unit composition in PVS***From:*Ben Hocking

**References**:**Re: [PVS-Help] Unit composition in PVS***From:*Viorel Preoteasa

**Re: [PVS-Help] Unit composition in PVS***From:*Ben Hocking

**Re: [PVS-Help] Unit composition in PVS***From:*Ben Hocking

**Re: [PVS-Help] Unit composition in PVS***From:*Ben Hocking

**Re: [PVS-Help] Unit composition in PVS***From:*Sam Owre

**Re: [PVS-Help] Unit composition in PVS***From:*Ben Hocking

- Prev by Date:
**Re: [PVS-Help] Unit composition in PVS** - Next by Date:
**Re: [PVS-Help] Unit composition in PVS** - Previous by thread:
**Re: [PVS-Help] Unit composition in PVS** - Next by thread:
**Re: [PVS-Help] Unit composition in PVS** - Index(es):