ϵ">]>
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. Merge Sort.
[CL] Remark. Below we will use the discrimination on whether or not L (x) ≦1 . As we have
we may suppose that the test L (x) ≦1 takes constant time.
Splitting the list into two halves.
Exercise. Prove
##
Merging two ordered lists into one.
Merge sort.
Exercise. Prove the condition of regularity for the function Msort (x) :