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

[PVS-Help] Recursive, Measure



Hi, my name is Andre and I am trying to specify:

***********************************

My_relations [T: TYPE]: THEORY
 BEGIN

  R: VAR PRED[[T, T]]
  x, y, z: VAR T

  transitive_closure(R): RECURSIVE PRED[[T, T]] = 
                        (LAMBDA x,y : R(x,y) OR (EXISTS z: (R(x,z) AND    
transitive_closure(R)(z,y)))) MEASURE ?

END My_relations

**********************************

When I typecheck I have the following problem "Wrong number of arguments in
measure". I already tried some measure, but I haven't had success. Please, can
someone help me?