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

PVS Bug 541


Synopsis:        Strange trap to ILISP
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Tue Mar 20 13:20:01 2001
Originator:      Steve Johnson
Organization:    cs.indiana.edu
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  This isn't an urgent problem.
  
  The appended PVS file causes anomalous behavior in PVS.  I tried briefly
  and unsuccessfully to create a smaller file with the same problem.  The
  problem is due to the occurance of a double hyphen on the penultimate
  line of the file (The student got confused about comments).  This file
  parses but typechecking puts it in ILISP error mode with the message:
  
     Error: 2 got 0 args, wanted at least 1 arg.
  
  I don't happen to know how to get the PVS system back after reaching
  this mode, and all I can do is interrupt and then close PVS.  You probably
  want to handle this error in a different fashion.
  
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  Steven D. Johnson                     net: sjohnson@cs.indiana.edu
  Indiana Univ. Computer Science Dept.  tel: +1 812-855-2567
  Lindley Hall                          fax: +1 812-855-4829
  150 W. Woodlawn Ave.                  www: www.cs.indiana.edu/~sjohnson
  Bloomington IN 47405-7104
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  
  ======================================================8<--------------------
  th_G: THEORY
  BEGIN
  
  %%%
  %%% Solve the problem below and prove your solution in PVS.  This will involv
 e
  %%% building the appropriate PVS theory.
  %%%
  % 
  % Taken from _Algebra 1_, Glencoe/McGraw-Hill, New York, New York, 1998 
  % pg. 411, Problem 56
  % 
  % There are 8 houses on McArthur St, all in a row.  These houses
  % are numbered from 1 to 8.
  % 
  % Allison, whose house number is greater than 2, lives next door
  % to her best friend, Adrienne.  Belinda, whose house number is
  % greater than 5, lives 2 doors away from her boyfriend, Benito.
  % Cheri, whose house number is greater than Benito's, lives
  % three doors away from her piano teacher, Mr. Crawford.  Daryl,
  % whose house number is less than 4, lives 4 doors from his
  % teammate, Don.  Who lives in each house?
  % 
  %%%
  %%%
  
    people: TYPE = {Allison, Adrienne, Belinda, Benito, Cheri, Crawford, Daryl,
  Don}
    house: [people -> int]
    
    p, q: VAR people
  
    Range: AXIOM house(p) = 1
            or house(p) = 2
            or house(p) = 3
            or house(p) = 4
            or house(p) = 5
  	  or house(p) = 6
  	  or house(p) = 7 
  	  or house(p) = 8
  
    Unique: AXIOM house(p) = house(q) implies p = q
  
    clue1: AXIOM house(Allison) > 2
  
    clue2: AXIOM house(Allison) - house(Adrienne) = 1 
  	       or house(Adrienne) - house(Allison) = -1
  
    clue3: AXIOM house(Belinda) > 5
  
    clue4: AXIOM house(Belinda) - house(Benito) = 2
   	       or house(Belinda) - house(Benito) = -2
  
    clue5: AXIOM house(Cheri) > house(Benito)
  
    clue6: AXIOM house(Cheri) - house(Crawford) = 3 
  	       or house(Cheri) - house(Crawford) = -3
  
    clue7: AXIOM house(Daryl) < 4
  
    clue8: AXIOM house(Daryl) - house(Don) = 4 
  	       or house(Daryl) - house(Don) = -4
  
    G_1: LEMMA house(Daryl) = 1 
  
    G_2: LEMMA house(Don) = 5
  
    G_3: LEMMA house(Adrienne) = 2
  
    G_4: LEMMA house(Allison) = 3
  
    G_5: LEMMA house(Cheri) = 7
  
    G_6: LEMMA house(Crawford) = 4
  
    G_7: LEMMA house(Belinda) = 6
  
    G_8: LEMMA house(Benito) = 8
  
  --
  END th_G
  
  
  
  

How-To-Repeat: 

Fix: 

 [davesc, 7/23/01]
 This error now reports:

  Typecheck error: second argument to - has the wrong type
     Found: [reals.real -> reals.real]
            [[reals.real, reals.real] -> reals.real]
  Expected: reals.real


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