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

[PVS-Help] cases - incompatible

Dear user:
when I typechech the following pvs specification file
PVS give me the error message "Selections have incompatible types"  for the defintion "I", that is to say variabe T   is not compatible with the +(T1,T2) or  /(T1,T2),...
 what kind of error I make. thank you!
p.s. PVS version is 5.0.
  term: DATATYPE
    atom(x: V): atom?
    +(T1, T2: term): add?
    -(T1, T2: term): sub?
    *(T1, T2: term): mul?
    /(T1, T2: term): div?
   END term
  VarS(T: term)(x: V): RECURSIVE bool =
    IF atom?(T) THEN x(T) = x ELSE VarS(T1(T))(x) OR VarS(T2(T))(x) ENDIF
     MEASURE T BY <<
  size(T: term): RECURSIVE nat =
    IF atom?(T) THEN 1 ELSE size(T1(T)) + size(T2(T)) ENDIF
     MEASURE T BY <<;
  +, -, *, /: [V, V -> V]
  sgm: VAR [V -> V]
  I(T: term)(sgm): RECURSIVE V =
      OF atom(x): sgm(x),
         +(T1, T2): I(T1) + I(T2),
         -(T1, T2): I(T1) - I(T2),
         *(T1, T2): I(T1) * I(T2),
         /(T1, T2): I(T1) / I(T2)
     MEASURE T BY <<
 END Terms
Best Regards
Qingguo XU