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

PVS Bug 491


Synopsis:        Invalid type cast breaks
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Thu Sep 28 10:40:04 2000
Originator:      Holger PFEIFER
Organization:    ares.informatik.uni-ulm.de
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Sam/Dave,
  
  admittedly, the following theory is nonsense, however, when developing
  specifications things like this do occur. The typechecker breaks into
  lisp and reports the error "No methods applicable for generic function". 
  
  Regards,
  
  	- Holger
  
  
  typecast : THEORY
  
  BEGIN
  
    A : TYPE
    B : TYPE
  
    a2b(a:A) : B = a::B
  
  END typecast
  
  -- 
  --------------------------------------------------------------------
  Holger Pfeifer                           Tel.: +49 (0)731 / 50-24124
  Universität Ulm                           Fax: +49 (0)731 / 50-24119
  Abt. Künstliche Intelligenz         pfeifer@ki.informatik.uni-ulm.de
  D-89069 Ulm         http://www.informatik.uni-ulm.de/ki/pfeifer.html   
  --------------------------------------------------------------------

How-To-Repeat: 

Fix: 

 [davesc]
 Fixed in 2.3.1

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