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

PVS Bug 471


Synopsis:        Bug in prettyprinter
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Mon Jul 10 13:40:04 2000
Originator:      Sam Owre
Organization:    csl.sri.com
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Typecheck the following theories, prettyprint them, and typecheck again
  and a type error is generated.
  
  th[T: TYPE, <=: PRED[[T, T]]]: THEORY
   BEGIN
  
   END th
  
  ppbug: THEORY
   BEGIN
  
    IMPORTING th[nat, <=]
   END ppbug
  
  This is distilled from a spec from Ian Mason.
  
  Sam Owre

How-To-Repeat: 

Fix: 

 [davesc]
 Fixed in 2.3.1

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