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

PVS Bug 459


Synopsis:        dependent types in datatype declaration
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Tue Apr 25 04:40:02 2000
Originator:      Steven Shapiro 
Organization:    cs.toronto.edu
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  
  I want to be able to have 
  a dependent type within a datatype declaration.  The error I get in both
  2.2 and 2.3 is:  Could not determine the predicate for this type: (st)
  I'm not sure if this is a bug or not.  Any help would be appreciated.
  
  cg_test  : THEORY
  
    BEGIN
  
    Program: datatype
      begin
        pick(st: pred[nat], prog: [(st) -> Program]): Pick?
      end Program
  
    END cg_test
  
  Thanks,
  
  Steven.
  
  -------
  -------

How-To-Repeat: 

Fix: 
Fixed the handling of dependent types in generating the induction
hypotheses for datatypes.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools