Vladimir I. Shelekhov (vshel@iis.nsk.su)

A.P. Ershov Institute of Informatics Systems Siberian Branch of the Russian Academy of Sciences

The simple predicate program of reversing a list as datatype object is presented. Deductive verification of this program is simple. The imperative program of reversing a linked list is obtained by the set of program transformations for the predicate program.

program transformation, data type, linked list