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

PVS Bug 517


Synopsis:        Parameter instanciation error
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Mon Jan 15 11:20:10 2001
Originator:      Hendrik Tews
Organization:    inf.tu-dresden.de
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  consider 
  
      A[A : Type] : Theory
      begin
        a : type = [A -> bool]
      end A
  
      B[B : Type] : Theory
      begin
        IMPORTING A[[B,B]]
      End B
  
      C[C : Type] : Theory
      begin
        IMPORTING B
        x : Var a[[C,C]]
      end C
  
  This yields an error 
  
      Expecting a type
      No resolution for a[[C, C]]
       Check the actual parameters; the following instances are visible,
       but don't match the given actuals:
         A[[B, B]].a
  
  But B not even a valid type in C! Besides the example shouldn't
  yield an error at all.
  
  Bye,
  
  Hendrik
  

How-To-Repeat: 

Fix: 

 [davesc]
 Fixed in 2.3.1 

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