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

[PVS-Help] Help for a recursion TCC



I am having difficulty proving the below TCC:
 
 
set_Node_TCC2: OBLIGATION
FORALL (v: finite_set[Entity]):
NOT empty?(v) IMPLIES
(FORALL (a: (v)):
a = choose(v) IMPLIES
card[Entity](remove[Entity](a, v)) < card[Entity](v));
 
_________________________________________________________
 
 
My PVS code looks like:
%initializes all nodes
set_Node(c: L_Graph, v: finite_set[Entity], n: n_db): recursive L_Graph =
if empty?(v)then c
else let a = choose(v) in set_Node(c, remove(a,v), Node_ops(c`Node,c,a, outgoing_edges(a, c`g)))
endif measure card(v)
 
 
 
As far as I can tell my recursion function should work, so maybe I'm just not using the right proving commands.
Any help would be greatly appreciated
 
Thanks
Kelly
 
 


Peek-a-boo FREE Tricks & Treats for You! Get 'em!