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

PVS Bug 597


Synopsis:        [2.3] Prelude bug fix
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Tue Aug  7 14:30:00 2001
Originator:      Jerry James
Organization:    eecs.ku.edu
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 

  In theory orders, the following appears:
  
        strict_total_is_strict: JUDGEMENT
           (strict_total_order?) SUBTYPE_OF (strict_total_order?)
  
  It should, of course, be:
  
        strict_total_is_strict: JUDGEMENT
          (strict_total_order?) SUBTYPE_OF (strict_order?)
  

How-To-Repeat: 

Fix: 

 [davesc]
 Fixed in 2.3.1.  

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