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

Re: [PVS-Help] Type checking issue: selections with incompatible types.



Jackie,

It looks like the problem is in your datatype declaration:

 EFFECT[st: TYPE] : DATATYPE
  BEGIN
   rel1(r: ND_EFFECT[st]) : rel1?
   fun1(f:  D_EFFECT[st]) : fun1?
  END EFFECT

Normally, the arguments to the datatype constructors have as type one of
the type parameters or the datatype you're declaring.  In your case, PVS
would expect to see rel1 and fun1 have argument types that are either
EFFECT or st.  Supplying ND_EFFECT and D_EFFECT as types seems to be
triggering the error.

Without knowing where you're heading with this specification, it's hard to
say how to restructure it.  Maybe something other datatypes would serve
your needs.

Regards,
Ben

-----

Ben Di Vito
1 South Wright Street, MS 130
NASA Langley Research Center
Hampton, VA 23681   USA

tel: +1-757-864-4883     fax: +1-757-864-4234
b.divito@xxxxxxxx






On 5/13/14 1:44 PM, "Jackie Wang" <jackie@xxxxxxxxxxxx> wrote:

>Dear Madam or Sir,
>
>We tried to type check the attached PVS theory, but there was an error
>message saying "selections have incompatible types". Could you please
>help us resolve this issue?
>
>Many thanks.
>Jackie