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

PVS Bug 1076


Synopsis:        Generic datatype, bag, wrong argument to map
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Tue Sep 20 11:20:01 -0700 2011
Originator:      Jean-Claude Royer
Release:         PVS 5.0
Organization:    mines-nantes.fr
Environment: 
 System:          
 Architecture: 

Description: 
  
  
  Hi all
  
  I try isolate one problem I don't understand.
  It seems  linked to the use of the bags.pvs from the NASA lib.
  However, it involves type parameters and as explain in my previous post (1074
 )
  I have a problem with that.
  
  The message I get when I type-checked World.pvs:
  
  first argument to map[I3, S3, I3, S31] has the wrong type
       Found: [S3 -> S31]
    Expected: [[I3 -> I3], [S3 -> S31], union_adt[I3, S3].union]
  
  I suspect a problem in the parameter ordering, but with
  	world(monitors:Monitor[S3,I3]) : world?
  the error is there with argument inversion 
  
  % World.pvs
  %--------------------------
  %  I=Information S=State
  World[I3, S3: TYPE] : DATATYPE 
  BEGIN
  	IMPORTING Monitor
  	world(monitors:Monitor[I3,S3]) : world?
  END World
  
  %Monitor.pvs
  %--------------------------
  % I=Information, S=State 
  Monitor [I2,S2:TYPE] : DATATYPE 
  BEGIN
  	IMPORTING bags
  	monitor(mailbox:bag[I2], state:S2) : monitor?
  END Monitor
  
  %sytem information
  
  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)
  ad-Orig-error: Minibuffer window is not active
  
  GNU Emacs 23.3.50.1 (i386-apple-darwin9.8.0, NS apple-appkit-949.54) of 2011-
 07-29 on braeburn.aquamacs.org - Aquamacs Distribution 2.3a
  
  Darwin ***** 10.8.0 Darwin Kernel Version 10.8.0: Tue Jun  7 16:33:36 PDT 201
 1; root:xnu-1504.15.3~1/RELEASE_I386 i386
  %----
  
  Where is my mistake ?
  
  %---------
  regards
  
  
  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