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

Re: [PVS-Help] measure about finity



Xu,

You can use a lexicographic order:
  MEASURE lex2(N-length(vis),length(l))

where N is the number of graph nodes (6 in your case). 

Note that the correctness proof of this algorithm may be a little bit
tricky. You probably have to add some information to the type of the
parameters.  

BTW, I have proven the correctness of a similar algorithm (although mine
is a breadth first algorithm):

http://research.nianet.org/~munoz/Besc/

The strategy "grind" performs symbolic computations and, therefore, it
can be very inefficient. Instead you could use "eval-formula", which is
defined in PVSio:

http://research.nianet.org/~munoz/PVSio

In contrast to "grind", "eval-formula" directly uses the PVS Lisp engine
to evaluate ground terms.

Hope that this helps,
Cesar

On Mon, 2006-04-03 at 21:42, 庆国 许 wrote:
> hello everybody: 
>  
>   I want to implement an algorithm for depth first searching(DFS) to a
> graph. so I give  the following "toy" theory (from a book written by
> Lawrence C. Paulson).
>  
>    I don't know how to give the measure function for the function
> "depthf" despite  the lemma "dfb" can be proved by (grind) simply,
> that is to say, this function to this test is terminated.
>  I think the recursive fucntion "depthf" should be terminated because
> of the finity of the graph represented by list[[T,T]].
>  
>  And another question, if the graph is very large,  how about DFS's
> efficiency?
>  
>  who can help me?  thank you very much.
>  
>  
> t: THEORY
>  BEGIN
>  
>   T: TYPE = {a, b, c, d, e, f, g}
>  
>   TL : TYPE = list[T]
>  
>   G: TYPE = list[[T,T]]
>  
>  graph1:  G = 
>      (: (a, b), (a, c), (a, d), (b, e), (c, f), (d, e), (e, f), (e, g)
> :)
>  
> %   /----->b--------\
> %  |                      |
> %  |                     \/ 
> %  a -> c -> f <-- e --> g        
> %  |                     /\
> %  |                     |
> %  \- ---->d-------/
>  
> %      graph1 
>  
>  nexts(a: T, l: G): RECURSIVE TL =   CASES l
>      OF null: (: :),
>         cons(hd, tl):
>           IF a = hd`1 THEN cons(hd`2, nexts(a, tl)) ELSE nexts(a, tl)
> ENDIF
>      ENDCASES
>     MEASURE  length(l);
>  
>   depthf(l: TL, g: G, vis: TL): RECURSIVE TL =
>    CASES l
>      OF null: reverse(vis),
>         cons(hd, tl):
>           IF member(hd, vis) THEN depthf(tl, g, vis)
>           ELSE depthf(append(nexts(hd, g), tl), g, cons(hd, vis))
>           ENDIF
>      ENDCASES
>     MEASURE ......; 
>  
>   dfb: LEMMA
>     depthf((: b :), cons((f, d), graph1), (: :)) = (: b, e, f, d, g :)
>  
>    END t
>  
>  Q.G.,  XU
>               
>   qgxu@mail.shu.edu.cn
>            2006-04-04
> 
> 
> ______________________________________________________________________
> 想成为冯小刚、陈凯歌、张纪中三大导演的主角吗?
-- 
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
GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6  1A18 6000 89F5 C114 E6C4