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

*To*: pvs-help@xxxxxxxxxxx*Subject*: Re: [PVS-Help] How to define a step for splitting withoutgenerating redundant TCCs*From*: Johannes Eriksson <joheriks@xxxxxx>*Date*: Mon, 30 Nov 2009 11:57:14 +0200*In-Reply-To*: <C73566AC.2828%cesar.a.munoz@nasa.gov>*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*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <20091126091942.GA1919@jweeriks.sby.abo.fi><C73566AC.2828%cesar.a.munoz@nasa.gov>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*User-Agent*: Mutt/1.5.18 (2008-05-17)

Hi Cesar, thank you for your long informative reply, that clarified a great deal to me. Though I use the NASA libs, I had not looked at the strategies, and so ended up re-implementing SPLASH. I was originally thinking along lines that since PVS already identifies subsumption of TCCs in formula substructure, e.g. if I have declared l1: formula a(very_long_and_complex_expression) then no addditional TCCs are generated for formulas involving a(very_long_and_complex_expression), it would be possible to use the same mechanism to discharge TCCs in proofs when a(very_long_and_complex_expression) is used. But perhaps this is not so, or not easily done. Johannes * Munoz, Cesar Augusto (LARC-D320) [Fri, Nov 27, 2009 at 10:21:16AM -0600]: > Hi Johannes, > > I also write strategies and I'm constantly frustrated by the problem you > mention. I have a solution, but it's a hack that uses some low level PVS > manipulations I'm not proud of. > > Let me tell you what I know about this problem. > > First, let me decouple your problem in two problems. One is easy to solve, > the other one is not. > > In PVS, when you use (split) you loose information. As you have certainly > noticed, when you have a consequent > > |------- > {1} a AND b > > Rule? (split 1) > Splitting conjunctions, > this yields 2 subgoals: > foo0.1 : > > |------- > {1} a > > foo0.2 : > > |------- > {1} b > > The fact that you can use "a" to prove "b" is gone. For that reason, I > created the strategy SPLASH, which is available as part of the NASA PVS > libraries. > > Rule? (splash 1) > > Splashing formula 1, > this yields 2 subgoals: > foo0.1 : > > {-1} a > |------- > {1} b > > foo0.2 : > > |------- > {1} a > > > Now, the second problem. Let's say that you have the following definition > > a(x:posreal) : bool > > and then a sequent with a "top level" expression: > > a(very_long_and_complex_expression) > > any occurrence of "a(very_long_and_complex_expression)" as an explicit > parameter of a strategy, e.g., name, name-replace, case, etc, will generate > a TCC sub-goal "very_long_and_complex_expression > 0". > > I believe that this TCC is not needed as, by construction, it can be checked > that the TCC was already generated when the expression appeared for the > first time in the sequent. > > When doing proofs interactively, this is not a big deal because in every > case, it is possible to use a "case" with the TCC before any manipulation > and thus the TCCs become trivial. But it's a nightmare for writing > strategies since TCCs are not easily to preview beforehand. > > As consequence of this behavior in the PVS typechecker, my SPLASH strategy, > which is based on CASE, will generate the unwanted TCC > "very_long_and_complex_expression > 0". > > TOWARDS A SOLUTION > ------------------ > In PVS 3.2 (see Release Notes > http://pvs.csl.sri.com/pvs-release-notes/pvs-release-notes_4.html#SEC35) > two new strategies were implemented: typepred! rule and all-typepreds > strategy. These strategies are supposed to add as hypothesis all > type-information that is available for an expression or a sequent at a given > time. > > However, for some reason, they don't work in this case: > > foo : > > |------- > {1} a(very_long_and_complex_expression) AND b > > Rule? (all-typepreds 1) > Generating typepreds for expressions: > No change on: (all-typepreds 1) > foo : > > |------- > {1} a(very_long_and_complex_expression) AND b > > (typepred! "a(very_long_and_complex_expression)" :implicit? t) > No top-level occurrences of any of the terms in > ("a(very_long_and_complex_expression)") > yielded type constraints > No change on: (typepred! "a(very_long_and_complex_expression)" > :implicit? t) > foo : > > |------- > {1} a(very_long_and_complex_expression) AND b > > In both cases, I would have expected the following formula to be added as > hypothesis: "very_long_and_complex_expression > 0" > > > Cesar -- Johannes W. E. Eriksson, M.Sc. Ph.D. Student / Turku Centre For Computer Science (TUCS) Åbo Akademi University / Department of Information Technologies e-mail: joheriks@abo.fi www: http://www.abo.fi/~joheriks

**References**:**Re: [PVS-Help] How to define a step for splitting withoutgenerating redundant TCCs***From:*Johannes Eriksson

**Re: [PVS-Help] How to define a step for splitting withoutgenerating redundant TCCs***From:*Munoz, Cesar Augusto (LARC-D320)

- Prev by Date:
**Re: [PVS-Help] How to define a step for splitting withoutgenerating redundant TCCs** - Next by Date:
**[PVS-Help] arrays** - Prev by thread:
**Re: [PVS-Help] How to define a step for splitting withoutgenerating redundant TCCs** - Next by thread:
**[PVS-Help] how to induct?** - Index(es):