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

*To*: kolano@cs.ucsb.edu*Subject*: Re: pvs question/suggestion...*From*: John Rushby <RUSHBY@csl.sri.com>*Date*: Fri 12 Dec 97 11:40:00-PST*Cc*: pvs-help@csl.sri.com*In-Reply-To*: <199712090238.SAA16119@petrel.cs.ucsb.edu>*Mail-System-Version*: <SUN-MM(229)+TOPSLIB(128)@csl.sri.com>

Paul Kolano has asked a number of good questions lately. Here are some partial answers. > One thing I've noticed is that some of the TCCs that are not finished > off by the tcc strategy could have been if it only had access to a few > rewrite rules of the encoding. Each of the TCC strategies (SUBTYPE-TCC, TERMINATION-TCC, EXISTENCE-TCC, ASSUMING-TCC, CASES-TCC, WELL-FOUNDED-TCC, SAME-NAME-TCC, COND-DISJOINT-TCC, COND-COVERAGE-TCC) is defined as some variation of the strategy TCC, which in turn is defined as (grind$ :defs defs). The way to change a tcc strategy is to redefine it in your pvs-strategies file. For the effect Paul wants, we'd suggest defining it using GRIND and supplying the REWRITES and THEORIES arguments. > ... I will have a theory that just consists of a bunch of > theorems that are not necessarily true and want to use a single > command to attempt the proofs of all of them using the same predefined > strategy. If we understand you correctly, you want a variant of M-x tcp that automatically applies a single proof strategy to each formula in a theory and quits the proof if the strategy fails to prove the formula. This can be done, but we (Sam) would have to write it. > ...so what I'd like to know is whether there's any way to use one subgoal > as a lemma in the proof of another subgoal (other than going back to > the spec and explicity writing a lemma, that is). There is a command M-x add-declaration that lets you augment a PVS specification on the fly (there's also a M-x modify-declaration that lets you change an existing declaration). When you discover a subgoal that looks like it embodies a lemma that ought to be generally useful, type M-x add-decl at the point in the spec where you'd like the lemma to appear (in order for it to be visible in the current proof, the cursor obviously needs to somewhere above the formula you're proving), formulate the lemma in the buffer that comes up (cutting and pasting formulas from the subgoal), terminate with C-c C-c, and continue your proof (presumably citing the lemma). PVS lets you you complete the proof, but notes that the specification was modified mid-proof and asks if you'd like to rerun the proof "clean" to check that it replays correctly. This is mainly a concern with modify-declaration because an obsolete version of the declaration might have been used in some early parts of the proof. Proofs may fail to rerun after add-declaration because proof commands like auto-rewrite-theory on the current theory might cause different behavior with and without the declaration. To find out whether a particular formula would be useful as a lemma, you can use the command (case "...type the formula here..") and see if that helps you finish the proof; abandon the proof when it starts on the branch that entails proving the formula and modify the specification to include the formula if it was, indeed useful. Please ask again if you need more information, John, Sam, Shankar -------

- Prev by Date:
**Re: cannot ftp to ftp.csl.sri.com as anonymous** - Next by Date:
**cannot ftp to ftp.csl.sri.com as anonymous** - Prev by thread:
**Re: cannot ftp to ftp.csl.sri.com as anonymous** - Next by thread:
**Re: pvs question/suggestion...** - Index(es):