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

PVS Bug 819

Synopsis:        min and max name overload conflict
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Wed Jan  7 23:25:00 2004
Originator:      "Paul S. Miner"
Organization:    nasa.gov
Release:         PVS 3.1

  Library theory finite_sets@finite_sets_minmax includes definitions of 
  min(x,y:T):T and max(x,y:T): T
  These functions  are only used in the definitions of minrec(SS) and 
  maxrec(SS), which are then used to discharge the existence TCCs for min(SS) 
  and max(SS) respectively.
  Unfortunately, when you import this library theory with reals for T, PVS 
  now seems to prefer the finite_sets_minmax definitions of min(x,y) and 
  max(x,y) to the definition of min and max in prelude theory 
  real_defs.  This has the effect of breaking several proofs, because now all 
  the useful properties of the prelude  version  of min and max are no longer 
  I propose that the supporting functions min and max (with signature [T, T 
  -> T]) in theory finite_sets@finite_sets_minmax be renamed to something 
  less likely to confuse PVS.
  More generally, it would be nice to be able to tag certain declarations as 
  local only (e.g. never exported).  This would be particularly useful for 
  those declarations that only exist to provide a witness for existence TCCs
  | Paul S. Miner, Ph.D.                  | phone: (757) 864-6201
  | Senior Research Engineer              | fax:   (757) 864-4234
  | Mail Stop 130                         | mailto:paul.s.miner@nasa.gov
  | NASA Langley Research Center  | http://shemesh.larc.nasa.gov/people/psm/
  | Hampton, Virginia 23681-2199 


Modified the names of these to fsmin and fsmax in finite_sets_minmax.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools