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

PVS Bug 1022


Synopsis:        [Fwd: errTh]
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Wed Jan  2 03:10:00 2008
Originator:      Hesselink
Organization:    rug.nl
Release:         PVS 4.1
Environment: 
 System:          
 Architecture: 

Description: 
  This is a multi-part message in MIME format.
  --------------040609000002070606080902
  Content-Type: text/plain; charset=ISO-8859-1; format=flowed
  Content-Transfer-Encoding: 7bit
  
  Dear Sam,
  
  In PVS 4.0, the second definition in the attached file creates 5 TCCs, 
  the last two of which are unprovable and unnecessary.
  
  Best regards,
  Wim
  
  -- 
  Wim H. Hesselink  
  
  Dept. of Computing Science       /   phone +31 50 3633933
     University of Groningen      /       or +31 50 3633939
                 P.O.Box 407     /     fax   +31 50 3633800
           9700 AK Groningen    /      email: w.h.hesselink@rug.nl
             The Netherlands   /       http://www.cs.rug.nl/~wim
  
  
  --------------040609000002070606080902
  Content-Type: text/plain;
   name="errTh.pvs"
  Content-Transfer-Encoding: 7bit
  Content-Disposition: inline;
   filename="errTh.pvs"
  
  errTh[T: TYPE]: THEORY
  BEGIN
  
    find(x: T, f: finseq[T]): nat
  
    delete(f: finseq[T], x: T): finseq[T] =
      LET n = find(x, f) IN 
      IF n < f`length THEN 
        (# `length := f`length - 1 ,
           `seq := (LAMBDA (i:below[f`length - 1]): 
                      IF i < n THEN f`seq(i) ELSE f`seq(i+1) ENDIF) #)
      ELSE f ENDIF
  
  END errTh
  
  
  --------------040609000002070606080902--

How-To-Repeat: 

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