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

*To*: pvs-help@csl.sri.com*Subject*: a C function to traverse a list.*From*: Mauro Gargano <mauro@wjpserver.cs.uni-sb.de>*Date*: Fri, 24 Jan 2003 17:10:33 +0100*Sender*: pvs-help-owner@csl.sri.com*User-Agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.0.1) Gecko/20021003

Hi to everybody, I'm really in trouble ... I cannot get rid of a proof. So I decided to extract some code from my pvs project and to sent it to you ... asking for hits and suggestions. The original pvs project aim to verify some pieces of C code, so I cut-and-pasted some functions, predicates and lemmas and I presented to you a THEORY that contains a LEMMA that I'd like to prove. The lemma says that the function "FIND_NODE" acts like it's specification (aka. "FIND_NODE_SPEC"). The function "FIND_NODE" is just a function that traverse a linked list of elements starting from "m". The linked list has the element starting to the memory location 1 ending to the memory location list_l`max, the memory is represented by the function list_t`list. The path predicate says that the element "n" is after the element "m" in the list. The is_searchable? predicate says that the element in the list are unique (aka. the result of the search is the empty_set or a set that has only one element) Hoping to gets some help from you, I thank you in advance, Mauro Gargano. ------------------------------------------------------------------------------------------ mylist : THEORY BEGIN % I'm trying to proof an algorithm to traverse and to find elements in a list, % the memory is simulated by the list_t`list array and the list_t`max integer is the % number of inserted elements. % Each element has a value field and a pointer to the index of the next element. % % the element in position 0 of the list is defined to be empty (it's contents are ignored) % the last element of the list points to 0. list_t: TYPE = [# max: posnat, list: [ below(max) -> [# next:nat, value:nat#] ] #] % % There is a path between two elements A and B (path(A,B)=TRUE) if traversing % the list starting from A, I find B. % % path is recursive -> I need to measure the recursion! % the maximum recursion is obtained starting from the first element and arriving % to the last, so the maximum recursion is the number of elements (= to LIST_T`MAX). % path ( tree : list_t, m : nat, n : nat, recurse_step: nat) : RECURSIVE bool = ( IF (recurse_step>0) AND (m < tree`max) AND (n < tree`max) THEN path(tree,tree`list(m)`next,n,recurse_step-1) OR m=n ELSE FALSE ENDIF ) MEASURE recurse_step % Some Predicates % an elementh is found if it contains the right value and it follows the elemement that rappresent the starting point (aka. m). found?( tree : list_t, m : nat, %from k : nat, %to val : nat) : bool = IF ( k < tree`max AND m < tree`max AND path(tree, m, k, tree`max) AND tree`list(k)`value=val ) THEN true ELSE false ENDIF % % is_searchable? is a predicate on the list. % it is true if there are no duplicate elements. % m,val: VAR nat is_searchable?(tree:list_t) : bool= (FORALL m,val: LET set=LAMBDA(k: below(tree`max)): found?(tree,m,k,val) IN (nonempty?(set) AND singleton?(set)) OR empty?(set)) % % specification of the function find_node % % It finds the (unique, if present) element that follows m and has a value of val. % IT returns the number (aka. address) of the element that has a given value and follows m % OR returns 0. % find_node_spec( tree : (is_searchable?), m : nat, % starting point val : nat ) : nat = LET set=LAMBDA(k: below(tree`max)): found?(tree,m,k,val) IN IF nonempty?(set) THEN the(set) ELSE 0 ENDIF % % implementation of the function find_node % % a typical list iterator. % find_node( tree : (is_searchable?), m : nat, % starting point val : nat, recurse_step: nat) : RECURSIVE nat = ( IF (recurse_step>0) AND (m < tree`max) THEN IF tree`list(m)`value=val THEN m ELSE IF tree`list(m)`next/=0 THEN find_node(tree,tree`list(m)`next,val,recurse_step-1) ELSE 0 ENDIF ENDIF ELSE 0 ENDIF ) MEASURE recurse_step % % % the correctness lemma % % tree: var (is_searchable?) find_works: LEMMA (FORALL tree, m, val : find_node(tree, m, val, tree`max) = find_node_spec(tree, m, val)) END mylist -- --------------------------------------------------------------------------- Mauro Gargano University of Saarland, Saarbruecken, DE Computer Architecture and Parallel Computing building 45, room 320 mauro@wjp.cs.uni-sb.de ---------------------------------------------------------------------------

- Prev by Date:
**Re: Please Help Me** - Next by Date:
**Semantics of operators** - Prev by thread:
**Semantics of operators** - Next by thread:
**"Trouble loading ICS, so it is not available."** - Index(es):