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

PVS Bug 1074


Synopsis:        "no method applicable to generic function"
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Mon Jun 13 10:10:00 -0700 2011
Originator:      Jean-Claude Royer
Release:         PVS 5.0
Organization:    mines-nantes.fr
Environment: 
 System:          
 Architecture: 

Description: 
  Hi all
  I have also the "no method applicable to generic function" when I
  type-checked the World.pvs specification.
  I saw no solution on the bug list.
  
  Hint: Writing my email I saw two many [I:TYPE] formal parameters,
  renaming them seems to allow type-checking ...
  
  sorry for the noise but I expect it may help.
  regards
  
  %------------
  
  PVS Version 5.0 - Allegro CL Enterprise Edition 8.2 [64-bit Mac OS X (Intel)]
  (Apr 14, 2011 1:42) - Allegro CL Enterprise Edition 8.2 [64-bit Mac OS X (Int
 el)] (Apr 14, 2011 1:42)
  
  GNU Emacs 23.3.1 (i386-apple-darwin9.8.0, NS apple-appkit-949.54) of
  2011-03-19 on braeburn.aquamacs.org - Aquamacs Distribution 2.2
  
  Darwin portinfo27.local 10.7.0 Darwin Kernel Version 10.7.0: Sat Jan 29 15:17
 :16 PST 2011; root:xnu-1504.9.37~1/RELEASE_I386 i386
  
  %--------------------------
  % %%% 13/6/2011
  % World.pvs
  %--------------------------
  % I=Information Type
  World[I:TYPE] : DATATYPE
  BEGIN
  	IMPORTING Controlled
  
  	new(procs:list[Controlled[I]]) :new?
  	com(pred:World) : com?
  
  END World
  
  %%%%---------------
  %%% 13/6/2011
  %%% Controlled.pvs
  %%%%%--------------
  % I=Information Type
  Controlled[I:TYPE] : THEORY
  BEGIN
  	IMPORTING TheoryParticipant, Message
  
  	Controlled : TYPE =  Participant[Message[I]]
  
  END Controlled
  
  %--------------------------
  % %%% 13/6/2011
  % participant with its in/out list boxes
  % and location with parametric messages
  % Participant.pvs
  %--------------------------
  % M=messages
  Participant[M:TYPE] : DATATYPE 
  	BEGIN
  	part(location:int, msg_in, msg_out:list[M]) : part?
  END Participant
  
  %--------------------------
  % %%% 13/6/2011
  % message with  location receiver
  % Message.pvs
  %--------------------------
  % I=information type
  Message[I:TYPE] : DATATYPE 
  BEGIN
  	% emitter, receiver, information 
  	msg(rec:int, info:I) : msg?
  END Message
  
  %--------------------------------------------
  
  Jean-Claude.Royer@mines-nantes.fr
  ASCOLA, Mines de Nantes - INRIA
  + 33 2 51 85 82 05
  
  
  
  
  
  

How-To-Repeat: 

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