Analytical reasoning is central to code correctness, and every computer science curriculum aims to teach students how to achieve this objective in one form or another. With the acceptance of object-based computing and component-based software engineering, the need for analytical reasoning that is based on formal contracts to establish correctness of software across module boundaries has become ever more obvious. Yet there are few institutions that have integrated modular, analytical reasoning principles into their undergraduate curriculum. Among many reasons for this shortcoming are: the effort it takes overloaded faculty to integrate new ideas of any kind in their courses, the challenge of institutionalizing ideas within a specific context, and constraints of a particular college. This paper presents our experiences over nearly two decades at five different institutions with the hope that they will serve as useful curriculum examples for like-minded educators at other institutions.

Abstract A central objective of the verifying compiler grand challenge is to develop a push-button verifier that generates proofs of correctness in a syntax-driven fashion similar to the way an ordinary compiler generates machine code. The software developer’s role is then to provide suitable specifications and annotated code, but otherwise to have no direct involvement in the verification step. However, the general mathematical developments and results upon which software correctness is based may be established through a separate formal proof process in which proofs might be mechanically checked, but not necessarily automatically generated. While many ideas that could conceivably form the basis for software verification have been known “in principle” for decades, and several tools to support an aspect of verification have been devised, practical fully automated verification of full software behavior remains a grand challenge. This paper explains how RESOLVE takes a step towards addressing this challenge by integrating foundational and practical elements of software engineering, programming languages, and mathematical logic into a coherent framework. Current versions of the RESOLVE verifier generate verification conditions (VCs) for the correctness of component-based software in a modular fashion—one component at a time. The VCs are currently verified using automated capabilities of the Isabelle proof assistant, the SMT solver Z3, a minimalist rewrite prover, and some specialized decision procedures. Initial experiments with the tools and further analytic considerations show both the progress that has been made and the challenges that remain.

A model and a taxonomy to characterize pointer manipulations are introduced, along with an instrumentation technology that leverages them to provide students with immediate reports of pointer errors in C++ programs. Data collected from CS2 student assignments show that the vast majority of student pointer errors either would not have been noticed at all, or would have been detected only much later in execution, if this infrastructure were not used. Possible applications of the underlying technology--both to conduct long-term educational research into students' understanding of pointers, and to improve pedagogy directly--are discussed.

Currently there is a serious conceptual and technical gap between ideas emphasized in object-oriented programming and ideas as taught in algorithms courses. We suggest both a paradigm for "re-expressing" algorithms in terms of classes and objects, and a set of criteria relative to which the quality of such re-expressions can be evaluated. A detailed example is provided for re-expressing the algorithmic idea of sorting.

Two important objectives when designing a specification for a reusable software component are understandability and utility. For a typical component defining a new abstract data type, a significant common factor affecting both of these objectives is the choice of a mathematical model of the (state space of the) ADT, which is used to explain the behavior of the ADT's operations to potential clients. There are subtle connections between the expressiveness of this mathematical model and the functions computable using the operations provided with the ADT, giving rise to interesting issues involving the two complementary system theoretic principles of "observability" and "controllability". The paper discusses problems associated with formalizing intuitively stated observability and controllability principles in accordance with these tests. Although the example we use for illustration is simple, the analysis has implications for the design of reusable software components of every scale and conceptual complexity.

Reverse engineering of large legacy software systems generally cannot meet its objectives because it cannot be cost-effective.There are two main reasons for this.First, it is very costly to "understand" legacy code sufficiently well to permit changes to be made safely, because reverse engineering of legacy code is intractable in the usual computational complexity sense.Second, even if legacy code could be cost-effectively reverse engineered, the ultimate objective -re-engineering code to create a system that will not need to be reverse engineered again in the future -is presently unattainable.Not just crusty old systems, but even ones engineered today, from scratch, cannot escape the clutches of intractability until software engineers learn to design systems that support modular reasoning about their behavior.We hope these observations serve as a wake-up call to those who dream of developing high-quality software systems by transforming them from defective raw materials.