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

Re: [PVS-Help] cases - incompatible



Qinguo,

I(T1) and I(T2) have both the type [[V->V]->V], but the binary operators
+,-,*,/ expect terms of type V. I guess that you want:

I(T1)(sgm)+I(T2)(sgm)

instead of 

I(T1) + I (T2)


Cesar

-- 
Cesar A. Munoz                             NASA Langley Research Center
Cesar.A.Munoz@xxxxxxxx                     Bldg. 1220  Room 115 MS. 130
http://shemesh.larc.nasa.gov/people/cam    Hampton, VA 23681-2199, USA
Office: +1 (757) 864 1446                  Fax: +1 (757) 864 4234




On 5/2/12 2:23 AM, "许庆国" <qgxu@xxxxxxxxxxxxxxx> wrote:

>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.
> 
> 
>Terms[V: TYPE+]: THEORY
> BEGIN
>  term: DATATYPE
>   BEGIN
>    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 =
>    CASES T
>      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)
>      ENDCASES
>     MEASURE T BY <<
> END Terms
> 
>Best Regards
> 
>
>Qingguo XU
>2012-05-02 
>
>________________________________________
> 
>
>
>