[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: 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
    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))
    MEASURE ......;
  dfb: LEMMA
    depthf((: b :), cons((f, d), graph1), (: :)) = (: b, e, f, d, g :)
   END t
 Q.G.,  XU