# 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