Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 572


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 Mail Status Bugs Users Related FM Tools