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

PVS Bug 623


Synopsis:        ground flawed
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Wed Nov 28 14:41:32 2001
Originator:      John Rushby
Organization:    csl.sri.com
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  The proof of before3 used in PVS 2.3 was
  (SKOSIMP) (EXPAND "before") (INST - 0) (GROUND)
  
  This no longer works in 2.4.   What does work is replacing the
  (GROUND) by (ASSERT).   But I thought (GROUND) subsumed (ASSERT).
  
  Furthermore, doing (ASSERT) after the (GROUND) doesn't work, so
  something fishy is going on.
  
  This is extracted from Holger Pfeifer's ttp proof.  There are several
  proofs in that (massive) verification that no longer work in 2.4 but
  this is the simplest.
  
  John
  
  
  bug [n:upfrom(3)] : THEORY
  
  BEGIN
  
  
  % Following should point to the dorectory containing the NASA mod library
  
    mod : LIBRARY = "./NASA-mod/"
  
    IMPORTING mod@mod
  
  
  
    time    : TYPE+ = nat
    postime : TYPE+ = posnat
    proc    : TYPE+ = below(n)        % -- processors numbered 0 .. n-1
    memvec  : TYPE+ = [proc -> bool]  % -- membership vector
  
    p,q,r,a,b,
    x,y,z,xs   : VAR proc
    S          : VAR set[proc]
    j          : VAR postime
    i,s,t      : VAR time
    v,w        : VAR memvec
    
    broadcaster(t) : proc = mod(t,n) % -- broadcaster at time t
  
    % -- x will broadcast before y, at time t or later
  
    before(t,x,y) : bool = 
      FORALL i: 
        y = broadcaster(t+i) => EXISTS s: s<i AND x=broadcaster(t+s)
  
    before3 : LEMMA 
      before(t,x,y) => y /= broadcaster(t)
  
  END bug
  

How-To-Repeat: 

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