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

Re: [PVS-Help] measure about finity



Hi Xu,

The measure function to use is: 
lex2(card(fullset[T]) - n_uniq_elems(vis), length(l))
If you are interested in the proofs, see the dump file in the
attachment.

stan

On Tue, 2006-04-04 at 09:42 +0800, 庆国 许 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
> 
> 
> ______________________________________________________________________
> 想成为冯小刚、陈凯歌、张纪中三大导演的主角吗?

dfs.dump.gz