ϵ">]>
Literature.
[1] J. Komara. Specification and Verification of Programs. Downloadable lecture notes available through the web page of the course.
[2] J. Komara and P. J. Voda. Metamathematics of Computer Programming. 2001.
Chapter. Programs Operating on Lists.
Section. Sorting of Lists.
[CL] Remark. See the auxiliary module Maux*.
Subsection. Insertion Sort.
Insertion function.
Exercise. Prove
##
Insertion sort.