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

PVS Bug 529


Synopsis:        PVS wishes
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Wed Mar  7 12:20:01 2001
Originator:      Christoph Berg
Organization:    cs.uni-sb.de
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Hello,
  
  using PVS over the last year, I've discovered several small bugs and
  improvements that could be made:
  
  
  * starting proofs
  
  - M-x xsp should invoke xpr when no proof exists.
  
  - .pvscontext is always generated, even if answering "no" to "no context foun
 d
    - create one?"
  
  - M-x prove-pvs-file should list a summary of incomplete lemmas/lemmas that t
 he
    theories depend on.
  
  - A command M-x prove-pvs-context would be nice. (see next paragraph)
  
  - I have not yet found a way to 'import' all PVS files in the current directo
 ry
    into .pvscontext so that PVS knows where to find a theory (e.g. after
    unpacking a tar archive). Otherwise, M-x pri will not work. M-x parsing eac
 h
    file is tedious; M-x undump-pvs-files creates .pvscontext, but appears not 
 to
    import the files into it.
  
  
  * TCL windows:
  
  - Closing tcl windows using the window manager does not reset the counter, e.
 g.
    sequents/commands get a ever higher number.
  
  - The (violett) circle marking the current sequent is not always on the right
    sequent, especially when many proof steps are performed (re-run) in a short
    time.
  
  - It would be nice, if the postscript output of Tcl windows were black for
    readability (and not blue).
  
  - The highlight color in the x-theory-hierarchy windows is white by default,
    which is not a good idea on white background.
    Hot-fix: put the line
      pvs.activedisplayforeground: red
    into .Xdefaults
  
  - Some contexts do not have a single 'top level' theory. It would be nice if
    x-theory-hierarchy could show all theories from a context.
  
  - When clicking on a theory name in x-theory-hierarchy, the cursor is placed 
 on
    the beginning of the theory. M-x show-tccs the displays preceding theory's
    TCCs, if there are several theories in the file.
  
  - As neighboring proof branches are often similar, it would be nice if the tc
 l
    window could leave one row empty below the current sequent, so that the
    'next' sequent from the other branch is visible. (Now I have to scroll down
    to see what command to apply next.)
  
  - The maximum tcl command window width is 1264, which is to little, wrapping
    long lines would improve readablity.
  
  
  * the prover (handling proofs)
  
  - When using Tab-U to undo proof steps, it is annoying that '(undo)y' is
    inserted into the history (M-p).
  
  - When cut-and-pasting formulae, PVS saves the linebreaks (\n) that occur
    within "" in the proof file. The proof succeeds, but re-running these proof
    fails.
  
  - It would be nice if a currently running proof could be saved to the proof
    file without having to (exit) and restart.
  
  - (postpone :dir left) would be convenient.
  
  - (case-replace) is missing a :hide? argument.
  
  - M-x show-expanded-sequent should show the fully parenthesized sequent, as t
 he
    binding range of quantors and let is sometimes not obvious.
  
  - (show-expanded-sequent should show actuals for o ^ etc. -- see bug #512)
  
  
  * the prover / decision procedures
  
  - The decision proedures often need a (name-replace "N" "2^n") for (assert) t
 o
    succeed.
  
  - integer_pred(x) is defined only on rationals:
  
  integ: THEORY
   BEGIN
  
    x: VAR real
  
    integ: LEMMA integer_pred(x) IMPLIES rational_pred(x)
   END integ
  
  leads to the unprovable TCC
  
   integ_TCC1: OBLIGATION FORALL (x: real): rational_pred(x);
  
  
  (Unfortunately, I've lost the examples for the following two bugs.)
  - In one case, (decompose-equality) removed a formula instead of splitting it
 .
    A workaround was to use an appropriate (case) expression.
  
  - One proof generated lots of TCC subgoals that vanished when doing M-x tcp i
 n
    advance. The TCCs would reappear when rerunning the proof without checking
    the TCCs first. (again M-x tcp)
  
  Christoph Berg
  -- 
  Lehrstuhl für Rechnerarchitektur
  Universität des Saarlandes, Saarbrücken, Germany
  http://www-wjp.cs.uni-sb.de/~cb/ , +49/681/302-4490, -4290 (Fax)
  

How-To-Repeat: 

Fix: 

[davesc]

Most of these will be transferred to the pvs-suggestions list.
This one is real tricky though:

  - The decision proedures often need a (name-replace "N" "2^n") for
    (assert) to succeed.

The decision procedures aren't very good at non-linear arithmetic.
It's a fine trade-off between deciding such examples, and the great
potential for looping.  This will be enhanced with the next set of
decision procedures for PVS, known as ICS.

  - integer_pred(x) is defined only on rationals:
   leads to the unprovable TCC
  
   integ_TCC1: OBLIGATION FORALL (x: real): rational_pred(x);

This is a known issue.  If you find yourself writing "integer_pred"
consider writing "integer?" instead (see the prelude) as "integer?"  is
defined over number (the supertype of real) instead of rational (the
supertype of integer).

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