Home | • | Intro | • | Announce | • | FAQ | • | Docs | • | Download | • | • | Status | • | Bugs | • | Users | • | Related | • | FM Tools |
---|

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 | • | • | Status | • | Bugs | • | Users | • | Related | • | FM Tools |
---|