A central goal of computer science education is to teach students how to reason about the correctness of the code they write. Typically, students use a trial and error process and check that their logic "works" by running it on test inputs. Typically, instructors encour-age them towards logical reasoning through manual tracing of the code. Rarely reasoning tools are used in the process, at least partly because few instructors are familiar with them and fewer have the time to investigate and experiment. The purpose of this panel is to introduce the attendees to a variety of reasoning tools the presenters have used in their classrooms. In some cases, the tools have been used in only one or two classes of a course to illustrate specific points. In other cases, entire projects have been done using the tools. The courses range from the introductory sequence and dis-crete structures to software engineering and graduate-level courses. The tools are freely available on the web and attendees will be encouraged to experiment with the reasoning tools on their own laptops to solve simple reasoning problems.

Program correctness is central to computing, with instructors striving to convey the importance of getting it right starting in CS1. Teaching this material carefully demands a uniform framework to specify, implement, and reason about software correctness. To make these ideas accessible to educators and students, the tutorial will use RESOLVE, an integrated specification and programming language with a toolset especially designed for building verified components. The tutorial will also discuss how to get students involved through hands-on activities with software construction and modular verification using a web-integrated environment that requires no software installation and that features a prototype 'push-button' verifying compiler. The proposers have taught the ideas contained here using engaging pedagogical methods in introductory and advanced CS courses to thousands of students and dozens of educators over the past 20 years, and this SIGCSE tutorial will leverage that experience.

Syrus is courseware designed with the goal of helping students better understand logical sentences involving quantifiers. Syrus uses template-guided mutation of "seed" formulas to generate candidate practice problems, and third-party theorem-provers to automatically determine the truth value of each. It provides students with a virtually unlimited supply of unique and relevant practice problems and provides immediate feedback on each problem. Results of an empirical study of its efficacy are reported.

No abstract available.

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.

The ultimate objective of a verifying compiler is to prove that proposed code implements a full behavioral specification. Experience reveals this to be especially difficult for programs that involve pointers or references and linked data structures. In some situations, pointers are unavoidable; in some others, verification can be simplified through suitable abstractions. Regardless, a verifying compiler should be able to handle both cases, preferably using the same set of rules. To illustrate how this can be done, we examine two approaches to full verification. One replaces language- supplied indirection with software components whose specifications abstract pointers and pointer- manipulation operations. Another approach uses abstract specifications to encapsulate data structures that pointers and references are often used to implement, limiting verification complications to inside the implementations of these components. Using a modular, specification-based tool we have developed for verification condition generation, we show that full verification of programs with and without the direct use of pointers can be handled similarly. There is neither a need to focus on selected pointer properties, such as the absence of null references or cycles, nor a need for special rules to handle pointers.

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.

Among the many ways to focus CS1/CS2 content, two have been published that emphasize concepts of component-based software engineering. Courses based on these two instances of a "components-first" approach are remarkably similar in several crucial respects--which is surprising because they were developed independently and with very different objectives. Indeed, the two versions are based on virtually the same principles for content organization, and they share many common features that are unusual for CS1/CS2. Yet, they are notably different in other ways. Detailed analysis of similarities and differences suggests that it might be possible to transfer some of their claimed and documented advantages to other approaches within the programming-first paradigm for CS1/CS2, by rearranging the content of such courses in accord with the underlying principles of the components-first approach.

Rarely are the three pillars of academia---research, teaching, and service---addressed together, within one intellectually cohesive context in the graduate curriculum. Such a context is important for exposing students to the inter-relationships among these facets.This paper presents our experience with structuring graduate research seminar courses around the model of a "miniconference". Throughout the quarter, students pursue original research projects in the discipline of the seminar course. At the end of the quarter, students write their findings as technical conference papers, then act as the miniconference program committee in reviewing each other's submissions. Finally, the selected papers are presented at the miniconference. In addition to the model itself, we describe some variations in instantiation and an assessment of the benefits of this general approach.

Two kinds of interface contract violations can occur in component-based software: A client component can fail to satisfy a requirement of a component it is using, or a component implementation can fail to fulfill its obligations to the client. The traditional approach to detecting and reporting such violations is to embed assertion checks into component source code, with compile-time control over whether they are enabled. This works well for the original component developers, but it fails to meet the needs of component clients who do not have access to source code for such components. A wrapper-based approach, in which contract checking is not hard-coded into the underlying component but is "layered" on top of it, offers several relative advantages. It is practical and effective for C++ classes. Checking code can be distributed in binary form along with the underlying component, it can be installed or removed without requiring recompilation of either the underlying component or the client code, it can be selectively enabled or disabled by the component client on a per-component basis, and it does not require the client to have access to any special tools (which might have been used by the component developer) to support wrapper installation and control. Experimental evidence indicates that wrappers in C++ impose-modest additional overhead compared to inlining assertion checks.

Dynamic module replacement - the ability to hot swap a component's implementation at runtime - is fundamental to supporting evolutionary change in long-lived and highly-available systems. Most existing solutions require special-purpose middleware or depend on research languages with limited support for mainstream software development. We present a language-neutral technique for dynamic module replacement using Service Facilities (Serfs) - a pattern-based design strategy for decoupling runtime dependencies. We demonstrate the sufficiency of Serfs with respect to a litmus test of criteria for module replacement. Next, we extend the traditional scope of module replacement to encompass the domain of modules for distributed protocols. We conclude by applying the Serf strategy to illustrate dynamic replacement of mutual exclusion protocols in modules for distributed resource allocation.

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.

Summarizes an approach for introducing component-based software engineering (CBSE) early in the undergraduate computer science curriculum, and an evaluation of the impact of the approach at two institutions. Principles taught include a modular style of software development, an emphasis on human understanding of component behavior even while using formal specifications, and the importance of maintainability, as well as classical issues such as efficiency analysis and reasoning. Qualitative and quantitative evaluations of student outcomes and end-to-end changes in student attitudes show mostly positive results that are statistically significant, confirming that: (1) it is possible to teach CBSE principles without displacing "classical" principles usually taught in introductory courses, (2) students can understand and reuse formally specified components without knowing their implementations, and (3) student attitudes towards software engineering can be altered in directions heretofore often assumed to be difficult to achieve.

Abstraction is one of the cornerstones of software development and is recognized as a fundamental and essential principle to be taught as early as CS1/CS2. Abstraction supposedly can enhance students' ability to reason and think. Yet we often hear complaints about the inability of CS undergraduates to do that. Do we supply students with the tools they need to reach their potential to think carefully and to reason rigorously about software behavior? Typically we do not, but as educators there are techniques we can use to help our students develop such skills starting in CS1/CS2.

Software components have existed in one form or another for a number of years. Work in this area can be classified into two broad categories. On the one hand, a number of researchers have approached the concept of software components from a first principles perspective, advancing ideas regarding what constitutes the ideal component paradigm from perspectives of efficiency, verifiability and reusability. On the other hand, recent commercial advances in a number of popular technologies have elevated the software component concept into widespread use within the software practitioner community. Such technologies include a number of technologies made popular by Microsoft (such as Active-X, COM, DCOM and Visual Basic), as well as CORBA and Java Beans.Neither of these perspectives on software components has become a standard cornerstone of software development pedagogy. Yet both perspectives may have an important role in preparing software developers to build high-quality software in the context of modern software development technologies. In particular, teaching students how to design and construct software components from first principles provides students with important guidance as to the "right way" to structure correct and efficient software systems (i.e., with emphasis on "what" component-based systems should contain). On the other hand, teaching students about current commercial component technologies exposes students to the important dimension of best commercial practice (i.e., with emphasis on "how" component-based systems could be built).The participants of this panel are all actively involved in the development of courses and curricula that provide various perspectives on component-based systems. They represent both the first principles and commercial perspectives discussed above. Position statements for each of the panelists appear below.

Pointer errors are stumbling blocks for student and veteran programmers alike. Although languages such as Java use references to protect programmers from pointer pitfalls, the use of garbage collection dictates that languages like C++ will still be used for real-time mission-critical applications. Pointers will stay in the classroom as long as they're used in industry, so as educators, we must find better ways to teach them. This paper presents checked pointers, a simple wrapper for C++ pointers that prevents pointer arithmetic and other common sources of pointer errors, and detects all dereferencing and deallocation errors, including memory leaks. The syntax of checked pointers is highly faithful to raw C++ pointers, but provides run-time error detection and debugging information. After debugging, changing one #include is all that is required to substitute a non-checking implementation that is as fast as raw C++.

Academic research sometimes suffers from the “ivory tower” problem: ideas that sound good in theory do not necessarily work well in practice. An example of research that potentially could impact practice over the next few years is a novel set of component-based software engineering design principles, known as the RESOLVE discipline. This discipline has been taught to students for several years [23], and previous papers (e.g., [24]) have reported on student-sized software projects constructed using it. Here, we report on a substantial commercial product family that was engineered using the same principles — an application that we designed, built, and continue to maintain for profit, not as part of a research project. We discuss the impact of adhering to a very prescriptive set of design principles and explain our experience with the resulting applications. Lessons learned should benefit others who might be considering adopting such a component-based software engineering discipline in the future.

When teaching certain CS topics (e.g., abstract data types, operating systems), the instructor tries to make clear the distinction between the "client" perspective and the "implementer" perspective. But when teaching some programming language features and related programming techniques, this dichotomy often is not respected as strongly as it should be. We illustrate this with a discussion of how to teach recursion, comparing a traditional approach with one that is careful not to blur the distinctions between client view and implementer view. The latter better supports new learners in the creation of a sound and consistent mental model for developing and reasoning about programs that involve recursion.

Two kinds of interface contract violations can occur in component based software: a client component may fail to satisfy a requirement of a component it is using, or a component implementation may fail to fulfil its obligations to the client. The paper proposes a systematic approach for detecting both kinds of violations, so that violation detection is not hard coded into base level components, but is "layered" on top of them, and so that it can be turned "on" or "off" selectively for one or more components, with practically no change to executable code (limiting changes to a few declarations). Among the salient features of this approach are its use of formal specifications, the ability to handle parameterized (i.e., generic, or template) components, and the automatic generation of routine aspects of violation detection. We have designed, built, and experimented with a generator of checking components for C++ templates.

First-year computer science students need to see clearly that computer science as a discipline has an important intellectual role to play and that it offers deep philosophical questions, much like the other hard sciences and mathematics; that CS is not "just programming". An appropriate intellectual focus for CS1/CS2 can be built on the foundations of systems thinking and mathematical modeling, as these principles are manifested in a component-based software paradigm. We outline some of the main technical features of this approach to CS1/CS2 and report preliminary observations from our experience with it.

The typical correspondence between a concrete representation and an abstract conceptual value of an abstract data type (ADT) variable (object) is a many-to-one function. For example, many different pointer aggregates give rise to exactly the same binary tree. The theoretical possibility that this correspondence generally should be relational has long been recognized. By using a nontrivial ADT for handling an optimization problem, the authors show why the need for generalizing from functions to relations arises naturally in practice. Making this generalization is among the steps essential for enhancing the practical applicability of formal reasoning methods to industrial-strength software systems.

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.

Software engineers often espouse the importance of using abstraction and encapsulation in developing software components. They advocate the "layering" of new components on top of existing components, using only information about the functionality and interfaces provided by the existing components. This layering approach is in contrast to a "direct implementation" of new components, utilizing unencapsulated access to the representation data structures and code present in the existing components. By increasing the reuse of existing components, the layering approach intuitively should result in reduced development costs, and in increased quality for the new components. However, there is no empirical evidence that indicates whether the layering approach improves developer productivity or component quality. We discuss three controlled experiments designed to gather such empirical evidence. The results support the contention that layering significantly reduces the effort required to build new components. Furthermore, the quality of the components, in terms of the number of defects introduced during their development, is at least as good using the layered approach. Experiments such as these illustrate a number of interesting and important issues in statistical analysis. We discuss these issues because, in our experience, they are not well known to software engineers.>

How should iterators be abstracted and encapsulated in modern imperative languages? We consider the combined impact of several factors on this question: the need for a common interface model for user defined iterator abstractions, the importance of formal methods in specifying such a model, and problems involved in modular correctness proofs of iterator implementations and clients. A series of iterator designs illustrates the advantages of the swapping paradigm over the traditional copying paradigm. Specifically, swapping based designs admit more efficient implementations while offering relatively straightforward formal specifications and the potential for modular reasoning about program behavior. The final proposed design schema is a common interface model for an iterator for any generic collection.>

Summary—Software engineering processes must be understood to be managed effectively. It is important to go beyond purely metaphorical and descriptive methods to achieve such understanding. This paper proposes a framework, based on dynamic feedback control systems, for building potentially quantitative models of software engineering processes. It then uses this framework to explore some important characteristics of quantifiable outputs of such processes, including observability, measurability, independence, (near) continuity, and (near) monotonicity. General Terms—Software engineering, process modeling.

The difficult-to-achieve goal of a software project manager's access control policy is to help coordinate the work of the team members — to maximize cooperative access to project artifacts such as source code while preventing interfering and destructive forms of access. Solutions to two problems that arise from current approaches to access control are discussed: • How much information about the software being built is needed to develop and support effective access control strategies? • How can access control strategies be applied not just to the work of programmers and designers, but to all members of the software project team? A key element in answering these questions is a model of software in which each component has separate specification and implementation. This model further distinguishes structural from behavioral aspects of a specification. An access control framework which exploits these distinctions and relies on the structural (but not the behavioral) facet of specification is explored. The framework supports a number of different access control policies. The specific policy selected depends upon management's objectives in coordinating programmers and other members of the team such as technical writers. The combination of the software model, a developments environment that is based on it, and a flexible access control tool that supports many feasible policies can result in a greater degree of team members' concurrent access to components without the problems often associated with such access.

The authors argue that a simple alternative to copying as a data movement primitive-swapping (exchanging) the values of two variables-has potentially significant advantages in the context of the design of generic reusable software components. Specifically, the authors claim that generic module designs based on a swapping style are superior to designs based on copying, both in terms of execution-time efficiency and with respect to the likelihood of correctness of client programs and module implementations. Furthermore, designs based on swapping are more reusable than traditional designs. Specific arguments and examples to support these positions are presented.>

To increase speed and reliability of operation, multiple computers are replacing uniprocessors and wired-logic controllers in modern robots and industrial control systems. However, performance increases are not attained by such hardware alone. The operating software controlling the robots or control systems must exploit the possible parallelism of various control tasks in order to perform the necessary computations within given real-time and reliability constraints. Such software consists of both control programs written by application programmers and operating system software offering means of task scheduling, intertask communication, and device control. The Generalized Executive for real-time Multiprocessor applications (GEM) is an operating system that addresses several requirements of operating software. First, when using GEM, programmers can select one of two different types of tasks differing in size, called processes and microprocesses. Second, the scheduling calls offered by GEM permit the implementation of several models of task interaction. Third, GEM supports multiple models of communication with a parameterized communication mechanism. Fourth, GEM is closely coupled to prototype real-time programming environments that provide programming support for the models of computation offered by the operating system. GEM is being used on a multiprocessor with robotics application software of substantial size and complexity.

To increase the speed and reliability of robots and of industrial control systems, multiple processing elements are used in their computing hardware. However, performance increases are not attained by hardware, alone. It is the hardware's operating software that must exploit the possible parallelism to gain the increases desired. Such software consists of control programs written by application programmers and operating system software offering means of task scheduling, inter-task communication, and hardware configuration control. The Generalized Executive for real-time Multiprocessor applications (GEM) is an operating system that addresses several problems arising due to the unique requirements of operating software, including: (1) GEM supports two different sizes of tasks and task scheduling, called processes and micro-processes, and offers a variety of real-time scheduling calls, and (2) GEM supports multiple models of communication.

A probabilistic model of a class of parallel programs is used to investigate the counterintuitive behavior observed for some parallel algorithms. Two main points are made: 1) it may, in general, be beneficial to consider using more logical processes than physical processors in a parallel algorithm; and 2) results from order statistics are useful tools in analyzing parallel systems.

One major difficulty in analyzing algorithms for graph optimization problems is that the probabilistic behavior of the optimum solutions to most of the important problems is generally unknown. We present a general method for relating some well-known results regarding the probability of existence of certain subgraphs in random graphs to the probabilistic behavior of solutions to graph optimization problems, where the problem graphs have edge weights independently chosen from an arbitrary distribution. Application of the technique to well-studied problems such as the traveling salesman problem shows that stronger statements can be made about the optimum solutions than have previously been proved, and that the analysis is straightforward.

Geometric closest potnt problems deal with the proxLmity relationships in k-dimensional point sets.Examples of closest point problems include building minimum spanning trees, nearest neighbor searching, and triangulation constructmn Shamos and Hoey [17] have shown how the Voronoi dtagram can be used to solve a number of planar closest point problems in optimal worst case tune.In this paper we extend thmr work by giving optimal expected.trinealgorithms for solving a number of closest point problems in k-space, including nearest neighbor searching, finding all nearest neighbors, and computing planar minimum spanning trees.In addition to establishing theoretical bounds, the algorithms in this paper can be implemented to solve practical problems very efficiently.