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

PVS Bug 1010


Synopsis:        Wrong variable binding with Cases in 4.0
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Fri Nov  9 11:45:00 2007
Originator:      Marcus Voelp
Organization:    os.inf.tu-dresden.de
Release:         PVS 4.0
Environment: 
 System:          
 Architecture: 

Description: 
  The parameters of a constructor in a cases statements affect variables
  which are bound in a nested cases statement.
  
  Expanding the ## operator in the below lemma replaces both f_res and
  g_res with data(f(s)) although g_res should be data(g(state(f(s)))).
  
  PVS / Emacs Versions:
  ======================
  
  PVS Version 4.0 - Allegro CL Enterprise Edition 8.0 [Linux (x86)] (Nov
  28, 2006 16:50) - Allegro CL Enterprise Edition 8.0 [Linux (x86)] (Nov
  28, 2006 16:50)
  
  GNU Emacs 21.4.1 (i486-pc-linux-gnu, X toolkit, Xaw3d scroll bars) of
  2007-06-19 on ninsei, modified by Debian
  
  Linux 2.6.17.8 #1 SMP Tue Aug 15 16:46:18 CEST 2006 i686 GNU/Linux
  
  Example code:
  ==============
  
  err_result[State, Data : Type] : Datatype
  Begin
  
    ok(state : State, data : Data) : ok?
  
  End err_result
  
  error:  THEORY
   
    BEGIN
  
      State : Type
   
      Importing err_result
  
      f, g : VAR [State -> err_result[State, nat]]
  
      s : VAR State
  
      d_g : VAR [nat -> [State -> err_result[State, nat]]]
  
      ##(f,d_g) : [State -> err_result[State, nat]] =
        Lambda (s : State) :
          Cases f(s) Of
            ok(s, d) : d_g(d)(s)
          EndCases
  
      ok_result(data : nat) : [State -> err_result[State, nat]] =
        Lambda (s : State) : ok(s, data)
  
      wrong_variable_binding: LEMMA
        data((f ## Lambda (f_res : nat) : (g ## Lambda (g_res : nat) :
  ok_result(f_res + g_res)))(s)) =
          data(f(s)) + data(g(s))
   
    END error
  
  -- 
  Marcus Völp
  
  Technische Universität Dresden
  Department of Computer Science
  Institute for System Architecture 
  
  Tel: +49 (351) 463 38350
  Fax: +49 (351) 463 38284
  
  Email: voelp@os.inf.tu-dresden.de
  Web: http://os.inf.tu-dresden.de/~voelp

How-To-Repeat: 

Fix: 

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