Developing loop invariants of algorithms containing nonlinear data structure is generally regarded as a difficult problem. In this paper, new strategies for developing loop invariant are introduced, and an exact and simple loop invariant of the nonrecursive postorder binarytree traversal algorithm is worked out by adopting the recursive definition technique of loop invariants and ideas of partitionandrecur. The approach considerably simplifies the process of derivation and proof of the nonrecursive algorithm and avoids the blindness of developing the loop invariant. Using datatype abstraction of Apla language, which is a part of PAR, the result algorithmic program is pretty concise and easy to be proved. Finally, the core algorithm (just 4 lines in Apla) is successfully proved by DijkstraGries standard proving technique, and the abstract program is transformed into C++ program by PAR platform. It is demonstrated that the recursive definition technique of loop invariant is feasible and effective for deriving and proving nonlinear data structure algorithms.