[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*: Thu, 30 Apr 2015 18:53:21 -0400*Cc*: pvs-help@xxxxxxxxxxx*In-reply-to*: <E90E0311-D7E5-4DBC-9627-0DD5CF749DDD@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> <12394.1430250723@ubi> <E90E0311-D7E5-4DBC-9627-0DD5CF749DDD@dependablecomputing.com>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

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:

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

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

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