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

*To*: "'pvs-help@csl.sri.com'" <pvs-help@csl.sri.com>*Subject*: PVS Problem*From*: TENEVA G Ms -NUCLEAR <galina.teneva@opg.com>*Date*: Fri, 27 Apr 2001 15:37:22 -0400*Sender*: pvs-help-owner@csl.sri.com

Hi I have a problem: In my current work I have to prove about 100 theorems. I used to work in an interactive way, typing the corresponding primitive rules after the prompt "rule?". After a while, I realized that all these proof strategies for the different theorems can be generalized in one. Now I want to create a generalized user-defined strategy (something like grind, but for our specific theorems) in a file, which file to be started after the first prompt "rule?" or so. I looked at the "PVS Prover Guide" (version 2.3), in section 5.5 "Defining Strategies", there is a very brief and not clear to me explanation (and no example) how to create pvs-strategies file. I have especially difficulties to understand the syntax of the content of this file. (I want to use defstep, but as I don't have required-parameters, shall I leave this field blank?) My questions are: 1) Where the name of the user-defined strategy (galina) in the pvs-strategies file should be tipped? After the first "rule?" prompt or in the command line area at the bottom, before starting the proof (before typing M-x xpr)? Could you send me an example, please how the typed command should look like? 2) Could you send me more explanation and an example of a pvs-strategies file (just a simple one), to see how it must be organized. My "success" at the moment: -I created a pvs-strategies file in the current context directory. -I put name - galina of my user-defined stratedy. For strategy expression I used a simple "try" strategy, which strategy works fine if I type it after the prompt "rule?). -When then I start the PVS proof, there is a message: "Error in loading file "/.../.../.../pvs-strategies" -When I typed the user-defined name "(galina)" of the strategy after the prompt "rule?" , a message from the PVS tool appears "GALINA is not a valid prover command" 3) Is this message because of bad syntax of the pvs-strategies or something else in the installation of PVS tool? I'll appreciate very much your help. Thanks: Galina

- Prev by Date:
**Re: Datatype-problem** - Next by Date:
**Re: PVS Problem** - Prev by thread:
**Re: Length of proof** - Next by thread:
**Re: PVS Problem** - Index(es):