Hello all,
I want to prove termination of a partial recursive function that insert an
element in a linked list, which is modeled using a finite mapping to represent
the heap, which can contain element of type list or nodes of the list.
I use Hol_defn to define the recursive function
val listInsertRec_def = Hol_defn "listInsertRec" `
(listInsertRec h elemIndex pIndex laddr =
let nextElemIndex = (getField next (h ' pIndex)) in
if (getField index (h ' nextElemIndex)) <= (getField index (h '
elemIndex)) then
listInsertRec h elemIndex nextElemIndex laddr
else
listInsertAfter h pIndex elemIndex laddr )
`;
This generates the function definition, induction, and the following
termination conditions:
0. ∀laddr elemIndex pIndex h nextElemIndex.
(nextElemIndex = getField next (h ' pIndex)) ∧
getField index (h ' nextElemIndex) ≤
getField index (h ' elemIndex) ⇒
R (h,elemIndex,nextElemIndex,laddr) (h,elemIndex,pIndex,laddr)
1. WF R:
R should be related to the length of the sublist starting at pIndex and ending
at a fixed last element, so at each step the length of this sublist decreases,
so I can use the measure relation. However, I am struggling to see how can I
add assumptions related to the heap and to that fixed element, which belong to
a global invariant.
Is this possible or should I add these constrains to the definition of
listInsert in order to restrict the domain of the function?
Thanks!
Cheers,
David.
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
