THE PURPOSES OF THE WORKSHOP are twofold:
 

(1) to discuss the use of formal methods in the undergraduate computer science curriculum, and

(2) to conduct tutorials on the use of formal methods in undergraduate courses

Broad areas to be covered are: desiderata and approaches for the early introduction of rigor and the use of mathematics, experiences teaching with formal methods, and the overall appropriateness of formal methods for the undergraduate curriculum.

The workshop will be devoted to the presentation and discussion of position papers and tutorials.
 
 

A number of fundamental issues that have to be addressed to substantiate claims about the benefits and drawbacks of formal methods will be presented. Requirements for effective and useful formal methods will be discussed. Additionally, the audience will be introduced to a number of public-domain tools for Z including LaTeX style-files, a partial list of textbooks and introductory articles on Z and formal methods, and references to the WWW home page, ftp and gopher sites, usenet newsgroups, and e-mail distribution lists on formal methods and Z.
 

Rice's introductory computing courses focus on teaching students a rigorous approach to program design. The design process is driven by the program's relationship with the outside world. Based on information about program's input and output data, a programmer can derive the program text using a simple three-step recipe.

The first step is to describe the input data in the form of an inductive definition. In the second step the programmer translates the data description into a program template. Finally, the third step is to fill the gaps in the program template. To this end, the programmer must study the nature of the output data and how the program can compute the answer from the given input.

The first course introduces the design recipe using mostly functional programming in Scheme; the second course shows how to apply these design principles to design imperative, object-oriented programs. The courses rely on Scheme and Java because both languages provide safe primitives and garbage-collection, which permit the beginning programmer to think about data in mathematical terms. Near the end of the second course, students are also introduced to C++ programming so that they learn to appreciate the present state of industrial programming.
 

One trend in computer science education is the introduction of object oriented technology into Computer Science I and II courses. This is very natural since object oriented technology helps to narrow the gap between real world problems and their abstract solution in software. This approach seems to make it easier for students to appreciate the abstract design of software and the software development process. We have also found that it makes it easier to introduce and motivate formal methods.

In our Computer Science I course (CSE-114) objects are introduced the first day using numerous examples from the real world (watch, timer, TV, calculator, car, etc.). All objects have a 'behavior' which can be informally or formally modeled. The object model we use is the standard one consisting of data/information and operations. The behavior of an object can be specified in terms of its operations. These operations can be described formally using pre and post conditions. Accordingly, the abstract behavior of an object can be formally specified, and students are introduced to representative formal specifications early in CS-I. Indeed, in the first few laboratory exercises students are given the interfaces for several objects and are required to understand the behavior of these objects and to then use them to solve simple problems. For example, students are given three shape objects: circle, rectangle and triangle and asked to create various figures (eg, Olympic rings). In our CS-I course we use Modula-3. Modula-3 makes it easy to separate the object interface (formal specification) from its implementation.

In a traditional CS-I course it would be very difficult to introduce all of the formal requisite mathematics (propositional and predicate logic, induction, recursion, etc.) required for formal methods, in addition to programming, object oriented techniques and an overview of the computer science discipline. At Stony Brook we recognized and solved this dilemma 10 years ago through the introduction of a Foundations of Computer Science (CSE-113) for computer science majors. Foundations of Computer Science is the first course for majors. Its primary goal is to build strong mathematical foundations and problem solving skills. For example, looking for patterns in problems and using mathematics to formally specify these patterns. Such thinking is fundamental for algorithmic and recursive problem solving. In CSE-113 students use logic, and learn inductive and recursive thinking. Subsequently, in CS-I formal methods are much easier for students to understand. The concept of a loop invariant is simply a specification of a pattern. Predicate logic can be used to formally specify the pre and postconditions of the operations of an object.
 

Since 1992, SUNY Geneseo has been teaching an introductory computer science sequence that combines algorithm design, formal (mathematics) analysis of algorithms, and scientific experimentation. Experience teaching this introduction has convinces me and my colleagues that formal methods are most accessible to students when closely integrated with algorithm design, programming, and experiments. In such a setting, students begin to appreciate formal methods as tools that can make real programs easier to write and more reliable, and that allow the visible behavior of programs to be understood and predicted.

For several years, the introductory programming courses at Southwestern University have centered on derivation of programs from formal specifications. From the beginning, students study predicate calculus and the calculus of weakest preconditions. From given pre/post specifications, they derive programs in Dijkstra's guarded-command notation and then translate these programs to Pascal (or the Pascal subset of Oberon). As one might expect, we have had significant difficulties in motivating student and in developing other skills typically taught in the first-year courses (e.g. testing, debugging, top-down design). On the other hand, we have found that students are able to master material at this level of difficulty, and there are significant benefits in later courses. I propose to give introductory tutorial on program derivation, and in that context to discuss implications of our experience at Southwestern.
 
 

There are various approaches to introducing categories into undergraduate computer science instruction. These include the introduction of specific categorical methods and ideas used directly in examples or group of examples in different courses; the introduction of a specific category theory module utilized in a particular course; or the introduction of an actual undergraduate category theory course drawing examples and motivation from computer science. We briefly discuss some of these approaches and illustrate them with some examples.
 

It can be argued that one of the central goals of a computer science curriculum should be to guide students toward a level of understanding which allows them to deal with the programming process at an intuitive level as well as a theoretical level. The problem facing computer science educators is to bring formal semantics into the introductory programming sequence in such a way that this goal can be met. Rather than the more formal axiomatic approach, we advocate a longer term and less formal approach which blends operational and axiomatic semantics.

I will first motivate and discuss our proposed assertion-based programming methodology. In particular, I will discuss how the methodology could be incorporated in the existing curriculum for CS1/CS2 without much change in the coverage of topics (both order and extent).

Then I will discuss our implementation of the methodology with examples used during lectures and examples of lab assignments.

In the remaining time, I hope to stimulate a discussion amongst the tutorial participants to understand their reactions to our methodology and hear about their experiences at using assertions in introductory CS courses.
 
 

I believe that Formal Methods must make their way into the standard required curriculum if there is ever to be progress toward making them part of the standard practice of software engineering. In most programs that I've seen, formal methods are taught in a nicely encapsulated, advanced, elective course whose subject is the study of formal methods. It is not surprising that students come away with the belief that formal methods represent an isolated (esoteric) topic that hasn't much to do with real software engineering.

I've designed a course that incorporates an introduction to formal specification with the study of data structures. The ``Advanced'' in the title is used to distinguish the course from the typical second programming course that is often called ``Data Structures.'' Rather than focusing on programs that implement and/or use standard data structures (such as stacks, queues, binary trees), we focus on data structures as abstractions, the formal specification of what they are, and the implications of design choices that are made in order to represent and implement these abstractions.

Data Structures is a topic that all students of Computer Science and/or Engineering study. The specification, representation, and implementation of abstract data structure present an ideal opportunity to introduce students to formal methods of specification, and the practical use of those specifications to guide design and testing of programs.
 

The general problem that I would like to solve is how to incorporate formal methods of specification and verification into an object oriented method of software development. The specific question I will address here is an instance of that general problem: how to incorporate formal methods of specification and verification into an undergraduate course in an effective and efficient manner.

The application of formal methods to object oriented systems is complex and multifaceted. This intersection is a subject of on-going research that will produce usable methods in the future. In the present absence of such established results, we proceed by application of more conventional formal methods. We consider both formal specification and formal verification of object-oriented software systems. We do not assert here that we have the ultimate solution to this problem. We will not argue or defend the merits of one object-oriented programming language over another, or one formal method over another. We are operating in a particular context that allows us to experiment with some curricular changes, but constrains us in other ways. For example, we are constrained to use C++ as the basis language for our curriculum. We do not assert that this language is optimal, but we find ways of using it.
 

Formal methods, and in particular, the language Z, have become important ingredients of many software engineering programs, and quite a few software engineering textbooks nowadays include a chapter or two to emphasize the role of formal methods during modeling and analysis and use Z as a means to illustrate the concepts. Z is a software specification language based on the systematic application of simple mathematics and has become quite popular in recent years.

This presentation is designed for software engineering instructors who are considering to introduce formal methods into an existing software engineering (or data structures course). It will provide a thorough introduction to the language Z, and will teach the audience how to construct and read Z specifications. The important components of Z will be described, including:

* Z schemas,

* Z calculus (i.e., schema linking, schema inclusion, and Delta and Xi convention). The role of Z calculus as a means of combining smaller schemas to construct more complex systems will be emphasized.

* The most important set theoretic types used in Z specifications, such as sets, relations, functions, and sequences, as well as operators for manipulating these types.

* Calculations of preconditions for simple analysis and reasoning.
 
 

Despite over a quarter of a century of research and application, formal methods still remain one of the most contentious areas of current software engineering practice. It is really only in recent years that the uptake of formal methods in the industrial sector has become obvious. Even then, their usage is far from commonplace despite the increasing prominence of formal methods in various standards, and the accepted benefits of formalization.

At least part of the reluctance for the uptake of formal methods by industry must be attributed to the lack of appropriately trained and educated personnel. Moves in both the US and Europe to integrate formal methods into university curricula indicate positive efforts to ameliorate this situation.

The question remains, however, as to how much emphasis should be placed on formality, exactly what mathematics, notations and techniques should we be teaching to our students, and precisely, ``How formal is `formal?.

Techniques proposed by Chen, Gane and Sarson, Yourdon, and others, throughout the 70s and 80s were claimed at that time to be formal. At best these techniques were semi-formalized, in that, in fairness, they were more prescribed than other techniques in existence at that time --- they set out rules for layout of design notations, rules for how entities could be linked, and prescribed sequences for the development process.

Nowadays, however, we refer to these techniques as structured methods, in that they describe the structure of the system under consideration, and move towards an implementation of that structure. Formal, therefore, has become synonymous with mathematical in the software engineering community. While to an extent the two are inextricably linked, the mistaken conception that formal methods require great mathematical ability has served to restrict the growth of the formal methods community.

While proof, refinement, and indeed the development of new methods and techniques are likely to require significant mathematical ability, formal methods can be taught to those with only basic mathematical ability, and certainly any competent programmer should at least be able to read formal specifications after some basic instruction in the notation used.

This presentation will discuss the role of formality and the level to which development and education should be formalized in the areas of:

1) Prescribed (essential) mathematical foundations;
2) Formal methods as core to the curriculum;
3) Constructivism vs. decomposition;
4) Methods integration;
5) The role of realistic case studies;
6) Hands-on practical experience;
7) Tool support;
8) Testing and quality.

Each of the above areas will be discussed in relation to both industrial training and academic education, and will provide references and overviews of various viewpoints, success stories and failures with regard to teaching formal methods.

The presentation will also draw on the work reported upon in a new book, Teaching and Learning Formal Methods, edited by C. Neville Dean and Michael G. Hinchey, and to be published in August 1996 as the first book in a new formal methods book series.
 

The objective of the advanced software engineering course is to familiarize the student with the software engineering process model: requirements analysis, specification, design, implementation, verification, and validation. In this talk we describe how we accomplished this objective, overcoming the limitations of time and students' lack of recent exposure to formal logic. We will also discuss student reactions to the course, and their observation that in their experience with job interviews, not one interviewer knew what formal methods were.
 
 

As industries become increasingly concerned with the quality of their software products, it is imperative that academia adequately prepare potential software engineers with the knowledge and skills needed to tackle the quality problem. In spite of the documented quality-related benefits of using formal methods in the software engineering process, formal methods are seldom part of the skill set of software engineers in industry. In the United States, some graduate software engineering programs with significant formal methods content are starting to appear (the graduate software engineering program at Carnegie Mellon University is a notable case), but very few institutions have undergraduate software engineering course tracks that include significant formal method content. We feel that formal methods, in particular, formal specification techniques (FSTs), is an integral part of a software engineer's skill set, and should be introduced at the undergraduate level. here, a FST consists of a precise specification language and mechanisms for analyzing specifications expressed in the language. The early introduction of FSTs allows a student to adequately develop the skills needed to rigorously model and analyze software systems, and thus attain a depth of knowledge and experience that facilitates the transfer of the technology to industry.

In this talk we describe our approach to incorporating FSTs into the undergraduate software engineering course offerings at Florida Atlantic University (FAU). We introduce FSTs not as a set of single development approaches (as is often done for most development techniques), rather, we emphasize how they can be used in conjunction with less formal, but structured, software development methods (e.g., object-oriented (OO) and structured analysis/design (SA)/D) methods). This approach provides students with a multi-method view of software development, and helps them understand how FSTs can be used in conjunction with graphical structured techniques. Our course materials are based on work on integrating FSTs with structured and OO methods). We have recently developed a CASE tool supporting a particular integrated FST/OO approach that we plan to use in an undergraduate software engineering project course in Fall 1996. A description of our planned use of the tool will be included in the talk.
 
 

In recent years, both the application of formal methods and the reuse of existing software components have been increasingly advocated as appropriate mechanisms to diminish the problems associated with constructing reliable software. During this same time period, functional programming languages have emerged as a viable medium for real-world applications. Since these trends are likely to continue, students should benefit from a software engineering course that integrates formal methods, software reuse, and functional programming. This paper proposes such a course using the intermediate specification language FunZ and its associated methodology.

The FunZ methodology is a new approach for translating existing Z specifications into functional implementations. An integral part of this methodology is the intermediate specification language FunZ which combines features from the model-oriented specification language Z and the purely functional programming language Haskell. FunZ itself is best described as an extension of Haskell, yet the language also retains a Z-like flavor in that it contains notational conventions similar to those of standard Z or many of its object-oriented variants.

Because FunZ blends features from both Z and the functional programming paradigm, the language can be used to introduce several software engineering concepts. In particular, for those students who are knowledgeable in functional programming but unfamiliar with formal specification languages, FunZ affords a gentle introduction to Z. Similarly, for students versed in Z but less familiar with Haskell, FunZ provides a bridge between Z specifications and Haskell implementations. In addition, both groups can benefit form the systematic guidelines of the FunZ methodology which explain how to translate an abstract Z specification to a concrete FunZ design and how to construct a prototype form the resulting design.
 

Instead of teaching logic as one more isolated topic of discrete math, logic can be used as the fundamental tool underlying all other topics of the course. In such a course, six to seven weeks are spent learning logic and how to develop formal proofs. The other topics of discrete math are then taught in a more rigorous fashion than usual, using logic as the foundation.

In this tutorial, I will lead the participants through the inference rules, axioms, and selected theorems of propositional logic. The theorems will be selected to illustrate the heuristics presented in the text, the goal directed nature of the proofs and the opportunities to engage in problem solving. After extending the theory to quantification and predicate logic, I will present examples from set theory, relation theory, integer theory and math induction.

At the 1995 SIGCSE Technical Symposium in Nashville, David Gries and Fred Schneider moderated a panel on Teaching Logic as a Tool. As a panelist, I discussed my experience using their textbook for a two semester discrete math sequence at the freshman level. Joan Krone from Denison University, Stan Warford from Pepperdine University and I countered the perception that this approach works only with Cornell type students. We all found that formality actually helps the weaker students more than the stronger students, mainly because the approach explains everything clearly and gives them strategies and principles for constructing proofs.

Software Engineers in general do not embrace mathematics as part of their professional tool set. Few take the time to verify correctness or to even apply formal reasoning of any kind in their endeavors. This is in sharp contrast with other engineering disciplines where the distinguishing factor between an "engineer" and a "technician" is the math based analytic skills of the engineer.

As part of the Master's Program in Software Engineering, MUSE requires a course in math followed by a course in formal methods. The math course, as with most math for computer science courses, builds upon set theory as a basis. We have found that the students "take the course", "get the grade", "find it interesting" but rarely apply its content.

In 1993, Gries and Schneider attempted a paradigm shift with their new text, "A Logical Approach to Discrete Math" and have successfully used this in an undergraduate setting. In contrast with set theory, the Gries-Schneider basis in logic appears to have great appeal to software engineers who do embrace logic as part of their tool kit. Several other aspects of their approach have similar appeal. MUSE is currently revising the required math graduate course to use the Gries-Schneider material and to be in place this September.

In this paper we will discuss the aspects of the Gries-Schneider approach that hold appeal to the practicing software engineer and why we are projecting success with this approach.
 
 

The computer algebra system Mathematica lends itself naturally to the development of computer-held courses in discrete Mathematics. Lectures, laboratories, homeworks, quizzes and exams can all be organized in the form of so-called notebooks, a versatile form of electronic document that combines text, code and graphics.

Mathematica contains a high-level programming language, thus emphasis is placed naturally on algorithmic concepts (e.g., Euclidian algorithm, loop invariants, correctness). Since programming requires a high degree of precision, precise formal arguments appear automatically when one tries to argue about programs. Induction and recursion stand side by side, and it becomes possible to illuminate induction arguments on interesting structures such as lists and trees.

We report on our experience with ModMath, an introductory course in discrete mathematics developed by D. Scott at CMU, automata theory, and a new experimental course that combines discrete mathematics and programming.
 

The growing demands for assurance of properties like correctness, safety, and security have led to the development of design methods using mathematical logic. These methods have broad application to hardware, software, and system design. Design based on mathematical logic offers a capability to relate structural descriptions with behavioral descriptions and properties. The challenge is to move these methods into mainstream engineering. This requires teaching mathematical logic in engineering courses which are directly applicable to engineering design. This paper describes how formal logic is included in the computer engineering curriculum at Syracuse University, our experience teaching formal logic to engineers, and how VLSI circuits have been fabricated by students using formal development process.