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

PVS Bug 1036


Synopsis:        PVS Bug ?
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Sun May 11 13:45:01 -0700 2008
Originator:      Cesar Munoz
Release:         PVS 4.1
Organization:    nianet.org
Environment: 
 System:          
 Architecture: 

Description: 
  Hi Sam,
  I'm trying to finish some PVS work today, but I'm having some problems  
  with the typechecker (It may be that I'm not thinking clearly today).
  
  This is a simple incarnation of the problem: I have defined the  
  theories composable and composition.
  
  composable[Local  : TYPE,
              Global : TYPE] : THEORY
  BEGIN
  
     SharedState : TYPE = [#
       local  : Local,
       global : Global
     #]
  
  END composable
  
  composition[Local1:TYPE,
               Local2:TYPE,
               Global:TYPE,
               (IMPORTING composable[Local1,Global] as A,
                          composable[Local2,Global] as B)
               initial1:PRED[A.SharedState],
               transition1:PRED[[A.SharedState,A.SharedState]],
               initial2:PRED[B.SharedState],
               transition2:PRED[[B.SharedState,B.SharedState]]
              ] : THEORY
  BEGIN
  ...
  END composition
  
  PVS complains "Wrong number of actuals in composition" when type  
  checking:
  
  test : THEORY
  BEGIN
  
     IMPORTING composable[nat,nat] as A,
               composable[nat,nat] as B,
               composition[nat,nat,nat,
                           LAMBDA(x:A.SharedState):true,
                           LAMBDA(x,y:A.SharedState):true,
                           LAMBDA(x:B.SharedState):true,
                           LAMBDA(x,y:B.SharedState):true]
  
  
  END test
  
  Any help will be appreciated,
  
  Cesar Munoz (NIA)
  munoz@nianet.org
  
  
  
  
  

How-To-Repeat: 

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