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

*To*: Sam Owre <owre@xxxxxxxxxxx>*Subject*: Re: [PVS-Help] Unit composition in PVS*From*: Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx>*Date*: Tue, 28 Apr 2015 14:13:43 -0400*Cc*: pvs-help@xxxxxxxxxxx*In-reply-to*: <23921.1429826758@ubi>*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>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

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:*Sam Owre

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

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

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