a C function to traverse a list.

[Mauro Gargano <mauro@wjpserver.cs.uni-sb.de>]

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