Reversing: An Essential Heuristic in Program and Proof Design

摘要

Program and proof designs are fundamental in computer science (CS). The designs involve the employment of various heuristics that may be considered rather inherent and natural, such as decomposition. Yet, not all heuristics are natural. One less natural, and rather unintuitive heuristic is that of reversing, in which a task is approached by reasoning backwards or viewing entities through "inverse lenses". One primary form of this heuristic is recursion. But, there are additional forms throughout the CS curriculum that are essential yet not underlined. In this paper we display these forms, underline their important role, and illustrate them in five core courses. In addition, we describe our experience with student difficulties due to unawareness and lack of competence with this heuristic, and offer preliminary guidelines for elaborating it during CS studies.