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

PVS Bug 830


Synopsis:        CODATATYPE: some is INDUCTIVE
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Wed Mar 31 10:25:00 2004
Originator:      Jerry James
Organization:    eecs.ku.edu
Release:         PVS 3.1
Environment: 
 System:          
 Architecture: 

Description: 
  With PVS 3.1, in the expansion of a CODATATYPE, the "every" predicate is
  COINDUCTIVE as expected, but the "some" predicate is INDUCTIVE.
  -- 
  Jerry James
  Email: james@eecs.ku.edu -or- jamesj@acm.org
  WWW:   http://people.eecs.ku.edu/~james/

How-To-Repeat: 

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