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