a C function to traverse a list.

```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
---------------------------------------------------------------------------

```