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

Re: [PVS-Help] Recursive, Measure



Andre,

Define transitive_closure using an INDUCTIVE predicate, instead of a
recursive function:

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

Cesar
On Mon, 2006-03-13 at 09:25, 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?
-- 
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace        mailto:C.A.Munoz@larc.nasa.gov
100 Exploration Way                 http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988