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

PVS Bug 813

Synopsis:        Incorrect PVS proof status information, perhaps related to incremental typechecking
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Mon Oct  6 11:25:00 2003
Originator:      "Paul S. Miner"
Organization:    larc.nasa.gov
Release:         PVS 3.1

  We have experienced several occurences of PVS reporting incorrect proof 
  status information.  This seems to be related to bug # 766.  We have several 
  people working on  a reasonably large collection of PVS theories.  On more 
  than one occasion, we have had PVS report that all items were proven and 
  complete.  However, if we typecheck and prove the theories in a completely 
  clean context, some results are no longer proven (or in some cases, fail to 
  typecheck).  It seems that PVS is keeping around some invalid state in either
  the .pvscontext or *.bin files that is causing results invalidited by changes
  to *.pvs files to not be caught by a M-x pri.
  Unfortunately, we have not been able to identify a sequence of operations 
  that will recreate this behavior.  It is not something that can be captured 
  in a dump file.  
  It seems to me that there is some bug in how pvs is checking depencies for 
  typechecking and proof status.
  It is frustrating to be unable to trust the pvs status information.  It is 
  annoying to have to repeatedly remove .pvscontext and *.bin files to assess 
  the impact of a change on a theory within a hierarchy.
  -- Paul S. Miner                | phone: (757) 864-6201
  -- 1 South Wright St. / MS 130  | fax:   (757) 864-4234
  -- NASA Langley Research Center | mailto:p.s.miner@larc.nasa.gov
  -- Hampton, Virginia 23681-2199 | http://shemesh.larc.nasa.gov/~psm/


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