(see below for some papers on theorem proving)
The development, specification, and use of a loop invariant are useful and underutilized tools in writing code to solve a problem or implement an algorithm. Invariants are especially useful in introductory courses (CS1 and CS2) but are usually avoided because of the mathematical notation associated with them and because most textbooks have brief, if any, coverage of them. Our intent in this paper is provide several motivating examples of the use of pictures as loop invariants and to provide pointers to literature that more fully explores and develops the ideas of using loop invariants in specifying and developing programs.
The use of real-world problems as the basis for assignments in Computer Science courses is attractive for many reasons. At the same time it is difficult to find such a problem that offers the same richness that is found, for example, in sorting or searching. In this paper a problem is presented that has many real-world instances and which is pedagogically attractive at all levels of Computer Science from the level of a non-major's course to that of an advanced algorithms course.
Programming contests can provide a high-profile method for attracting interest in computer science. We describe our philosophy as it pertains to the purpose and merits of programming contests as well as their implementation. We believe that we have successfully combined the theoretical and practical aspects of computer science in an enjoyable contest in which many people can participate.
The contests we describe have distinct advantages over contests such as the ACM scholastic programming contest. The primary advantage is that there is no travel required---the whole contest is held in cyberspace. All interaction between participants and judges is via electronic mail.
Of course all contests build on and learn from others, and ours is no exception. This paper is intended to provide a description and philosophy of programming contests that will foster discussion, that will provide a model, and that will increase interest in programming as an essential aspect of computer science.
This abstract refers to the contents of the paper in which it appears. Most readers will not be troubled by this example of self-referential writing. Why then is self-reference, usually in the form of recursive subprograms, thought to be so onerous as to be placed in its own left-until-the-end-and-often-uncovered chapter in most introductory texts? Self-reference is one of the cornerstones of computer science from the unsolvability of the halting problem, to writing a Pascal compiler in Pascal, to reveling in the beauty of Quicksort. We argue that the notion of self-reference should permeate first courses in computer science. If this is to be the case such courses should take a view far broader than ``Wow, I can average 10 numbers with the skills I learned in my first programming course!''
Our philosophy is that CS1/CS2 students learn best as apprentices, by studying the work of more experienced program designers and writers and by extending and modifying programs provided by these experienced programmers. object oriented programming supports this philosophy well and permits our students to explore a realm of programs not possible using a more traditional ``structured'' approach. Our approach emphasizes using objects before creating them, reading and modifying programs before designing them. Although our philosophy transcends a particular \oo\ language, we have chosen C++ for our courses; our approach facilitates its use by novices. In this paper we discuss our approach, and suggest simulation as a rich area for case studies, labs, and assignments when employing this objects early approach. We provide details of two simulations we have used in our courses: a simulation of the card game war and a queueing simulation.
We have developed an application-based approach to introductory courses in computer science. This approach follows an apprenticeship model of learning, where students begin by reading, studying, and extending programs written by experienced and expert programmers. Applications play a central role since programming constructs are motivated and introduced in the context of applications, not the other way around as is the tradition in most texts and courses. Under our applied approach, (1) students are able to learn from interesting real-world examples, (2) the synthesis of different programming constructs is supported using incremental examples, and (3) good design is stressed via code and concept reuse. In this paper, we provide several examples of our method as well as pointers to all the material we have developed which is freely available electronically. The philosophy underlying this method transcends a particular programming language, but we present our examples using C++ since that is the language used in the CS1 and CS2 courses at Duke. This method has been used with equal success using ISETL at Dickinson.
Object-oriented methods and programming are increasingly being used in the second (CS 2) data structures course in Computer Science. As this course migrates to an object-oriented approach, students and instructors must be given materials to support a unified and application-oriented course. In this paper we report on modules developed for what we term an Applied Apprenticeship Approach to the CS 2 course using an object-oriented framework.
A typical Data Structures CS2 course covers a wide variety of topics: elementary algorithm analysis; data structures including dynamic structures, trees, tables, graphs, etc.; large programming projects; and more advanced object-oriented concepts. Integrating these topics into assignments is a challenging task; educators often duplicate work done by others in re-inventing such assignments. At the same time, these assignments and large programs take time to develop and are often changed from semester to semester to preclude cheating. We report on a project that provides modules containing many kinds of programming and lab assignments which can be re-used across semesters with accessible and exciting application-oriented materials. Our project is a collaboration between a research and teaching oriented private university, a teaching oriented public university, and a teaching oriented historically black university. This helps ensure that the modules will be accessible to nearly all student populations. The modules developed are available electronically as hyper-text documents.
The field of software patterns has seen an explosion in interest in the last three years. Work to date has been on the recognition, cataloging, and finding of patterns with little attention to the use of patterns, especially by students and practitioners not well-versed in object-oriented technologies. This project addresses pattern use through the development of several programming and pedagogical frameworks that supply support for using patterns throughout a computer science curriculum. Although we do not claim that patterns are Brooks' silver bullet [Brooks], their use can help cope with the accidental complexity of software development and, we argue, their use is essential for a successful adoption of object-oriented techniques in academic computer science programs. This project addresses practical concerns of the computer science and software engineering communities in using, teaching, and learning patterns. In this paper we argue that patterns are an essential programming and pedagogical tool and report on our work in making them accessible to the educational community.
power-point from presentation, pdf of powerpoint, html-ized version of powerpoint
Object oriented design patterns as popularized in [Gamma, Helms, Johnson, Vlissides] are intended to solve common programming problems and to assist the programmer in designing and developing robust systems. As first year courses increasingly emphasize object orientation, knowledge of design patterns and when to use them becomes an important component of the first year curriculum. Recent literature has focused on introducing the patterns to computer science educators, but not on the situations and contexts in which the patterns are appropriate. Design patterns and object orientation are parts of a methodology that scales to large systems. In this paper we show that these concepts do not always scale down. We analyze examples from current literature that would be simpler without patterns, and provide examples of when the same design patterns do make design and programs simpler.
Text books, including books for general audiences, invariably mention bubble sort in discussions of elementary sorting algorithms. We trace the history of bubble sort, its popularity, and its endurance in the face of pedagogical assertions that code and algorithmic examples used in early courses should be of high quality and adhere to established best practices. This paper is more an historical analysis than a philosophical treatise for the exclusion of bubble sort from books and courses. However, sentiments for exclusion are supported by Knuth [The Art of Computer Programming: Sorting and Searching] "In short, the bubble sort seems to have nothing to recommend it, except a catchy name and the fact that it leads to some interesting theoretical problems." Although bubble sort may not be a best practice sort, perhaps the weight of history is more than enough to compensate and provide for its longevity.
See The Bubble Sort Presentation
When the Model Elimination (ME) procedure was first proposed, a notion of lemma was put forth as a promising augmentation to the basic complete proof procedure. Here the lemmas that are used are also discovered by the procedure in the same proof run. Several implementations of ME now exist but only a 1970's implementation explicitly examined this lemma mechanism, with indifferent results. We report on the successful use of lemmas using the METEOR implementation of ME. Not only does the lemma device permit METEOR to obtain proofs not otherwise obtainable by METEOR, or any other ME prover not using lemmas, but some well-known challenge problems are solved. We discuss several of these more difficult problems, including two challenge problems for uniform general-purpose provers, where METEOR was first in obtaining the proof. The problems are not selected simply to show off the lemma device, but rather to understand it better. Thus, we choose problems with widely different characteristics, including one where very few lemmas are created automatically, the opposite of normal behavior. This selection points out the potential of, and the problems with, lemma use. The biggest problem normally is the selection of appropriate lemmas to retain from the large number generated.
Theorem provers based on model elimination have exhibited extremely high inference rates but have lacked a redundancy control mechanism such as subsumption. In this paper we report on work done to modify a model elimination theorem prover using two techniques, caching and lemmaizing, that have reduced by more than an order of magnitude the time required to find proofs of several problems and that have enabled the prover to prove theorems previously unobtainable by top-down model elimination theorem provers.