THE PURPOSE OF THE WORKSHOP is to discuss the introduction of formal methods in the early computer science courses. Broad areas to be covered are: desiderata and approaches for the early introduction of rigor and mathematics, experiences with such approaches, and the overall appropriateness of formal methods for the foundation curriculum.

The workshop itself is devoted to presentation and discussion of position papers; it is hoped that one outcome of the workshop will be formation of a regional formal methods computer science curriculum working group.
 
 

The number of different approaches to introductory computing courses continues to increase, both in terms of the content of the courses and the teaching/learning paradigms that are used. Variations on traditional programming-oriented courses include survey courses, integrating some concepts from advanced courses into the introductory courses, teaching fundamental concepts without using a programming language, and emphasizing theory and formal methods. More recently there has been increasing interest in teaching/learning paradigms such as peer learning, student-driven course content, and just-in-time learning.

This talk will provide some perspectives on various approaches to the introductory courses, both content and teaching/learning paradigms, that are currently being used or discussed. Some considerations for those who are proposing new approaches will also be included.
 
 

The role of formal methods in the early CS curriculum is closely tied to the goals of the first courses. This talk begins by considering some of these goals. Also, since the term ``Formal Methods'' may mean different things to different people, the talk presents a working definition of that term. The talk then examines the relationship between curricular goals and formal methods, concluding that the two areas complement each other well. With this background, the talk identifies several approaches for including formal methods in the first few years of the undergraduate CS curriculum, giving examples of each approach and considering appropriate support requirements.
 
 

The first course in computer science at CCNY (CSc 102) has been restructured with NSF support as an introduction to problem solving and programming, based on well-known principles of program verification. The main goals of the new course are to develop students' skill in designing programs, and to equip students with logical tools enabling them to explain how and why their programs work. The course seeks to empower students to reliably design, refine, and certify their programs by drawing their attention to the details of the logic underlying the programming process.

Our experience has been (i) that beginning students can master a formal problem-solving methodology which is at once powerful and practical; (ii) that although the coverage of the syntax of the course language (Pascal) has been reduced, students' ability to use what they were taught to design programs dramatically exceeds that achieved by our students when exposed to more standard approaches; (iii) that students who learn the style of program development presented in the course are able to explain how and why their programs work.

In this talk, we describe CSc 102, discuss what we have learned about teaching such material to beginning students, and hint at the as of yet unrealized potential the course represents for improving the subsequent CS curriculum at City College. We also describe our work to export the course to the community colleges of CUNY, with support from the FIPSE program of the U.S. Department of Education.

We discuss our participation in the City College/FIPSE program to include formal methods in the introductory programming classes.
 
 

Computer Science needs mathematical concepts for the correctness of algorithms, the properties of data structures, and the efficiency of programs. On the other hand, many high school graduates are inadequately prepared in mathematics, and college mathematics does not emphasize logic, graph theory and probability. We hope to initiate a discussion of how to meet this challenge.
 

For historical reasons, introductory Computer Science courses typically come in two flavors: CS1 and CS2. Together these courses serve as the introduction to the field for potential majors. The first course, CS1, often attracts a much broader audience. In this talk, I take the view that the entire first year, as opposed to the first course, is the proper forum for discussing the integration of formal methods. I will also address the scope of formal methods in the first year: what do we mean when we use the phrase ``formal methods''?

Is predicate or propositional calculus necessary? Are formal methods a discipline, a way of thinking, or a technique? What is compelling about these methods and how do we use them to engage students? I maintain that engagement is critical. We find ourselves with a full plate in the first year. We are expected to introduce students to (among other things): programming, data structures, software-engineering, algorithm analysis, complexity, ethics, design, specification, documentation, object-oriented methods, and human-computer interaction. Somewhere in this crowded curriculum we want to find space for formal methods.

To engage students and to do a service to our discipline we cannot view the full plate as a smorgasbord. The problem with smorgasbords (and full plates) is that it is too easy to dismiss a food as unpalatable or claim a full stomach. As in some schools of food preparation, I take the view that presentation is paramount. Formal methods, like good spices, enhance the curriculum rather than adding to it. I hope to raise some questions (and get some answers) so that as we leave this workshop we can all say ``now we're cooking.''
 

We will look at techniques intended to teach C++ multiple inheritance in a first-year course in computer science. This daunting subject is reduced to a manageable set of pencil-and-paper skills---techniques derived from our recent formal model of C++-style multiple inheritance. Students learn concrete skills based on formal methods.

The formal model will be part of the OOPSLA'95 proceedings. It can be found at the following URL:
http://www.cs.indiana.edu/hyplan/jrossie/papers/oopsla95.ps.gz
 

Combinatorics and graph theory are subjects of increasing importance, and are interesting and relevant to students on a variety of different levels. In this talk, we describe our system Combinatorica, as well as other software for discrete mathematics. We then proceed to show, as an example, how some of the properties of permutations can be made to come alive with Combinatorica. We conclude by presenting a variety of other interesting problems which can be approached via Combinatorica in a non-traditional way.
 
 

Formal methods are now recognized as highly successful in controlling complexity and assuring the reliability of complex computer systems. Further, they are being recommended, and indeed mandated, in more and more international standards, so it is critical for graduate engineers (both software and hardware) to be trained and conversant in their application.

However, the standards and rationale of formal methods education are questionable. Many practicing software engineers, even after learning something about formal systems, have little skill in using a formal method. Many seem happy to take to heart both criticisms and exaggerations regarding what formal methods can and cannot do. Students are often lead to believe that formal methods are difficult to use, involve complex mathematics, and basically require the use of Greek symbols and hieroglyphics to specify trivial systems such as Birthday Books and Library Systems (which could have been hacked together in a fraction of the time).

In addition, many students lack the basic prerequisites for applying formal methods in practice -- basic ability with discrete mathematics and logic, the ability to abstract and build simple models, and the ability to derive rigorous proofs.

The potential of teaching formal methods (and discrete mathematics) as a way of developing attitudes and analytical skills that can be of immense value in all areas of computing is not understood. We argue in favor of a practical approach to the introduction of formal methods, involving case studies and hands-on experience.
 
 

Our introductory course at Rice teaches computing as an extension of grade school arithmetic and high school algebra. In analogy to algebra text books, which define functions (over numeric operations) and asks students to evaluate them, students define functions (over basic data operations) and ask computers to evaluate expressions over these definitions. Since students are used to evaluating algebraic expressions from high school, they quickly understand the execution model of computers---in terms of programs instead of bits and bytes. This understanding is a significant aid in constructing, testing, and debugging programs.

Our course also teaches the systematic construction of programs based on the input and/or output data. Since most simple programs process algebraic data, we can teach program design as the definition of homomorphisms, without discussing the background. In our experience this approach teaches students why a program must have a certain shape. We are now developing guidelines for translating such programs into C/C++ programs to facilitate the transition between our introductory courses and subsequent portions of our curriculum.
 

The roots of the distinction between program and data reviewed along with numerous trends that are weakening this distinction. The implications of the equivalence of program and data are explored for programming methodology, formal methods, and programming language pedagogy. The power of meta-linguistic abstraction is emphasized. The properties of a suitable meta-language, such as Scheme, are reviewed. This enables remarkably formal semantics to be presented in a hands-on manner. It is argued with illustrations that programming language material can and should be introduced very early in computer science education and used throughout.

(Slides available via http://www.cs.indiana.edu/hyplan/chaynes.html.)

One of the principal challenges to creating high-confidence systems, be they global-scale information infrastructures or high performance/scalable systems, is they must operate in a known and trustworthy manner. This requires the correct and timely integration of specifications and designs at all levels of detail. The needs of high-confidence systems have led to the development of mathematical tools sometimes known as ``formal/high- assurance design methods.'' These tools have broad application to hardware, software, and system design. The successful development and deployment of high-confidence design methods could have as much impact on system design as the development of very-large- scale-integrated (VLSI) circuit technology had on computer design. The purpose of this talk is to advocate for education in high-confidence design methods which lead to their industrialization and incorporation into standard engineering practice.