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

*To*: pvs-help@csl.sri.com, tamarah@narkis.wisdom.weizmann.ac.il*Subject*: Can one use comments in strategies?*From*: Tamarah Arons <tamarah@wisdom.weizmann.ac.il>*Date*: Fri, 15 Jun 2001 16:50:38 +0300 (IDT)*Sender*: pvs-help-owner@csl.sri.com

Hello, I have been adding comments to strategies and have come across a problem : if I edit a proof file with comments in it from strategies it seems to delete the commands after the comment. This happens even if I just open the file for editing and then install it unchanged. Below is a PVS dump file with a short proof exhibiting this problem. It was run on PVS2-3. Using a patch does not seem to make a difference. If you edit the proof using (M-x edit-proof), save, and then install it, with or without making changes, the commands after (CASEPROP) are replaced with NIL. Is there some prohibition on using comments in strategies? Or is there some rule regarding their use that I am violating? Thanks, Tamarah _________________________________________________________ $$$pvs-strategies (defstep caseProp () (then (spread (case "prop!1(seq!1, i!1)") ((comment "case prop!1(seq!1, i!1)") (comment "case (NOT prop!1(seq!1, i!1))") ) ) ) "Splits on the case that a!1(seq!1, i!1)" "Splits on the case that a!1(seq!1, i!1)" ) $$$myops.pvs myops[STATE : NONEMPTY_TYPE]: THEORY BEGIN STATE_SEQ: TYPE = [nat -> STATE] MY_PROP : TYPE = [STATE_SEQ, nat -> boolean] i,k : VAR nat e, f : VAR STATE seq : VAR STATE_SEQ prop, prop2 : VAR MY_PROP NOT : [MY_PROP -> MY_PROP] = (lambda prop : (lambda seq, i: not prop(seq, i))); IMPLIES : [MY_PROP, MY_PROP -> MY_PROP] = (lambda prop, prop2: (lambda seq, i: not prop(seq, i) or prop2(seq, i))); AND : [MY_PROP, MY_PROP -> MY_PROP] = (lambda prop, prop2: (lambda seq, i: prop(seq, i) and prop2(seq, i))); G : [MY_PROP -> MY_PROP] = (lambda prop : (lambda seq, i: FORALL k: k >= i IMPLIES prop(seq, k))); valid : [MY_PROP -> bool] = (lambda prop : forall seq, i : prop(seq, i)) test : lemma forall prop: valid(G(prop) implies (prop and not not prop)) END myops $$$myops.prf (|myops| (|test| "" (EXPAND "valid") (("" (EXPAND "G") (("" (EXPAND "implies") (("" (SKOSIMP*) (("" (EXPAND "and") (("" (CASEPROP) (("1" (EXPAND "not") (("1" (ASSERT) NIL NIL)) ";;;case prop!1(seq!1, i!1)") ("2" (INST? -) (("2" (ASSERT) NIL NIL)) ";;;case (NOT prop!1(seq!1, i!1))")) NIL)) NIL)) NIL)) NIL)) NIL)) NIL))

- Prev by Date:
**Re: Problem typechecking over conversions on patched version** - Next by Date:
**Can PVS run on Cygwin / Cygnus** - Prev by thread:
**Re: Can PVS run on Cygwin / Cygnus** - Next by thread:
**Re: Can one use comments in strategies?** - Index(es):