Home | • | Intro | • | Announce | • | FAQ | • | Docs | • | Download | • | • | Status | • | Bugs | • | Users | • | Related | • | FM Tools |
---|

Synopsis: Problem using comments in strategies Severity: serious Priority: medium Responsible: owre State: open Class: sw-bug Arrival-Date: Wed Jun 20 13:05:00 2001 Originator: Tamarah Arons Organization: wisdom.weizmann.ac.il Release: PVS 2.3 Environment: System: Architecture: Description: Hello, I have been adding comments to strategies and have come across a problem : editing a proof file with comments in it from strategies often deletes 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? I find it very useful to have some comments telling me where the strategy "got to", especially if there are a number of subgoals, but not being able to edit (and thus also not checkpoint) the proof files is inconvenient. Thanks, Tamarah P.S. I sent this previously to pvs-help, but did not get a response, and I suspect it may be a bug. Sorry for the duplication. _________________________________________________________ $$$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)) ----- End of forwarded message from Tamarah Arons ----- How-To-Repeat: Fix:

Home | • | Intro | • | Announce | • | FAQ | • | Docs | • | Download | • | • | Status | • | Bugs | • | Users | • | Related | • | FM Tools |
---|