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

Re: [PVS-Help] Recursive, Measure



On Mon, 2006-03-13 at 11:25 -0300, galdino@mat.unb.br wrote:
> 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?

You probably want an inductive definition rather than a recursive one,
maybe something like this:

My_relations [T: TYPE]: THEORY
 BEGIN

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

  transitive_closure(R)(x, y): INDUCTIVE bool =
      R(x, y) OR (EXISTS z: (R(x, z) AND transitive_closure(R)(z, y)))

END My_relations

Also, take a look at the closure_ops theory in the orders part of the
NASA Langley PVS collection:

http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html

where the transitive closure is defined like this:

transitive_closure(R): (transitive?) = IUnion(LAMBDA p: iterate(R, p))

Regards,
-- 
Jerry James, Assistant Professor    Email: Jerry.James@usu.edu
Computer Science Dept.              Web: http://www.cs.usu.edu/~jerry/
Utah State University

This is a digitally signed message part