[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Type checking issue: selections with incompatible types.
It looks like the problem is in your datatype declaration:
EFFECT[st: TYPE] : DATATYPE
rel1(r: ND_EFFECT[st]) : rel1?
fun1(f: D_EFFECT[st]) : fun1?
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
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
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?