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

PVS Bug 933


Synopsis:        auto rewrite ignored
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Tue Jan 24 11:35:00 2006
Originator:      Hendrik Tews
Organization:    tcs.inf.tu-dresden.de
Release:         PVS 3.2
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  in the appended files in TCC
  unchanged_memory_invariant_unchanged_write_list_TCC2 (in
  memory.pvs) the auto rewrite result_pred_ok is not used, although
  it would finish the proof. Even track-rewrite does report on
  result_pred_ok and why it is ignored.
  
  My guess is that 
  
    states : Var PRED[State]
  
    result_pred_ok : Lemma Forall(res : Result[State, A]) : 
      result_pred(states)(res) And OK?(res) Implies
        states(next_state(res))
  
  does not qualify as an autorewrite, because of the quantification
  over states. If this is true the documentation about
  auto-rewrites should be more precises.
  
  Bye,
  
  Hendrik

How-To-Repeat: 

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