August 2026
Intermediate
138 pages
2h 57m
English

Recall that we usually obtain algorithms by weakening the postconditions. The objective of this chapter is to illustrate the wide variety of postcondition-weakening approaches. We’ll use sorting as the vehicle for this purpose, and we’ll see how classical sorting algorithms (e.g., insert sort, radix sort) arise from a selected postcondition weakening. We often rely on the ability to sort, such as when sorting products for sale or files in a directory by name or by date. We will concentrate on sorting integers.
We will weaken “ordered” in the postcondition for sorting to “somewhat ordered,” but we must define what that means. ...
Read now
Unlock full access