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

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



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
specification: THEORY
  BEGIN
  % effect record of operation specification (which includes infeasible specifications)
  EFFECT_REC[s: TYPE] : TYPE = [# pre : [s    -> bool], 
                                  post: [s, s -> bool]
                               #]

  % non-deterministic effect
  ND_EFFECT[st: TYPE] : TYPE = 
    {e: EFFECT_REC[st] | 
       (FORALL (s_ : st) : e`pre(s_) IMPLIES 
          (EXISTS (s : st) : e`post(s_, s)))}

  % deterministic effect
  D_EFFECT[st: TYPE] : TYPE =
    [# pre : [    st           -> bool],
       post: [{s: st | pre(s)} -> st  ]
    #]

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