Embedding instructive assertions in program design

Reviewer: Anany Levitin

This paper advocates the systematic use of an "assertion perspective" in algorithm/program design. This means the embedding of informal, but mathematically rigorous assertions that pinpoint important properties of the problem at hand, and lead to an efficient algorithmic solution. According to the paper, this use of assertions (less formal than the one advocated by formal program verification proponents) should complement an "operational perspective" commonly practiced by students and programmers. The paper provides examples of assertions for four specific problems. In addition, it contains six-stage guidelines for embedding assertions in various stages of algorithm and program design. These guidelines are quite general. The goal of the first stage, for example, is to search for "core assertion patterns that concisely encapsulate relationships between the task elements. These relationships should yield the concept underlying the algorithmic solution." The usefulness of the assertion perspective for specifying algorithms, proving their correctness and investigating efficiency, is well known. Therefore, any effort encouraging assertion utilization should be welcomed. It is less clear, however, how helpful the assertion perspective is for algorithm design. This is well illustrated by the last example in the paper: checking the possibility of converting one given permutation to another, given permutation by repeated repositioning of adjacent element pairs. The problem is solved by checking the parities of the number of inversions in the permutations given. It is difficult to argue that the assertion perspective is particularly helpful for discovering this crucial insight. Online Computing Reviews Service