ϵ">]>
Literature.
[1] J. Komara. Specification and Verification of Programs. Online.
[2] Ján Kľuka. Úvod do deklaratívneho programovania. Online.
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.
Exercise. (2 points) Prove
Subsection. Merge Sort.
Exercise. Implement merge sort; that is, define the function Msort (x) such that
with the help of the function Msplit (x) :
and the function Merge (x,y) :