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

PVS Bug 1009


Synopsis:        PVS 4.1 M-x tc --> Error: No methods applicable for generic function
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Thu Nov  8 14:50:00 2007
Originator:      Rick Butler
Organization:    larc.nasa.gov
Release:         PVS 4.0
Environment: 
 System:          
 Architecture: 

Description: 
  The following theory:
  
  vect_trig_2D: THEORY
  BEGIN
  
    IMPORTING vectors2D
  
    u,v,w     : VAR Vector
    a,b,c     : VAR real
  
    cross(u,v): real = u`x*v`y - v`x*u`y
  
    sin(u: Vector,v:{vv: Vector | norm(u) * norm(vv) /= 0}): real = cross(u,v)/
 (norm(u)*norm(v))
  
    cos(u: Vector,v:{vv: Vector | norm(u) * norm(vv) /= 0}): real = u*v/(norm(u
 )*norm(v))
  
    trig_range  : TYPE = {a | -1 <= a AND a <= 1}
  
    sin_range   : JUDGEMENT sin(u,v) HAS_TYPE trig_range
    cos_range   : JUDGEMENT cos(u,v) HAS_TYPE trig_range
  
    sin2_cos2: THEOREM sq(sin(u,v)) + sq(cos(u,v)) = 1
   
  END vect_trig_2D
  
  produces 
  
     Error: No methods applicable for generic function
  
  when given
  
      M-x tc

How-To-Repeat: 

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