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

[PVS-Help] measure about finity



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


想成为冯小刚、陈凯歌、张纪中三大导演的主角吗?