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

PVS Bug 625


Synopsis:        Bug resolving use of overloaded function
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Sat Dec  1 22:59:52 2001
Originator:      Marcelo Glusman
Organization:    csd.cs.technion.ac.il
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  I think I know how you can recreate the bug.
  Here's a stupid example:
  
  test: THEORY
  BEGIN
    IMPORTING finite_sets@finite_sets_minmax[nat,<=]
  
    under10: set[nat] = {i:nat|i<10}
    exists_max: THEOREM
      EXISTS(n: nat): FORALL(m: (under10)): m<=n
  END test
  
  Of course one can prove the theorem by instatiating n with 9.
  But if you start the proof with:
  (inst + "max[nat,<=]({i:nat|i<10})")
  
  You get a message that says that [nat->bool] should be a subtype 
  of [nat,nat].
  
  I don't remember why in my original proof I used "max[nat,<=](...)"
  I now removed this (calling max directly) and the bug doesn't happen.
  
  You can decide if this is still a bug or not - it's certainly unexpected,
  
  since PVS should realize that there are two max functions in that 
  theory.
  
  Good luck,
  Marcelo.
  
How-To-Repeat: 

Fix: 
Modified matching-actual-expr* to check for compatible types correctly.
Was using (some (lambda (x y) ...)) when it should have used
(some (lambda (x) (some (lambda (y) ...))))

The problem with the first form is that it compares the possible types as
ordered lists, rather than as sets.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools