[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Question: LINUX installation & Type Check



Hi,

I try to install PVS under RED-HAT LINUX.

I have downloaded 3 files from PVS2.1/linux directory.
My sequence of untar : pvs-system-2, pvs-linux,pvs-linux-patches.
When I run PVS I got this following message : 
 warning lisp directory `/usr/share/emacs/site-lisp' does not exist.
Do you think I will have any problem with it ?

I try to typecheck this codes:

tryout  : THEORY
  BEGIN
    type0 : type = [# name1: string, name2: string #] 
    type1 : type = list[type0]
    type2 : type = [# group: string, member: type1 #]
    type3 : type = list[type2] 
  n1 : type0 = (# name1:= "1-1", name2:= "1-2" #)
  n2 : type0 = (# name1:= "2-1", name2:= "2-2" #) 
  l1 : type1 = (: n1,n2 :)
  l2 : type1 = (: (# name1:= "1-1", name2:= "1-2" #),
                  (# name1:= "2-1", name2:= "2-2" #) :)
  g1 : type2 = (# group:= "G1", member:= l1 #)
  g2 : type2 = (# group:= "G1", 
                  member:= (: (# name1:= "1-1", name2:= "1-2" #),
                              (# name1:= "2-1", name2:= "2-2" #) :) #)
  gl1: type3 = (: g1,g2 :)
  gl2: type3 = (: (# group:= "G1", member:= l1 #),
                  (# group:= "G1", 
                     member:= (: (# name1:= "1-1", name2:= "1-2" #),
                                 (# name1:= "2-1", name2:= "2-2" #) :) #) :)
  END tryout

I got an ERROR message for g12 :
No methods applicable for generic function #<STANDARD-GENERIC-FUNCTION
FIND-SUPERTYPE> with args ([# group: finseq[(char?)], member: (cons?
[[# name1: finseq[(char?)], name2: finseq[(char?)] #]]) #]) of classes
(ACTUAL)

If I eliminate g12, it succesfully terminated.
I wonder is it because a nested list concrete declarations ?
(I produced the above codes to simualte my problems)

I also have tried to type-check the code under solaris.
Type-check did not complain for 'g12'.

Why this happen ?
Is it because the previous warning that I got when starting PVS ?
Do you have any suggestion what should I do ?

------------------------------------------------------------
Kong Woei Susanto
Department of Computing Science - University of Glasgow
17 LilyBank Gardens, Glasgow G12 8RZ. 
Phone: +44-141-3304454  Fax: +44-141-3304913
e-mail: susanto@dcs.gla.ac.uk
------------------------------------------------------------