(In-)Formal Methods: The Lost Art --- A Users’ Manual

Link to article: InformalMethods-Morgan.pdf

Abstract

This article describes an experimental course in “(In-)Formal Methods”, taught for three years at the University of New South Wales to fourth-year undergraduate Computer-Science students. An adapted version was then taught (disguised as “Software Engineering”) to second year undergraduate students.

Fourth-year CS students at UNSW are typically very-good-to-excellent programmers. Second-year students are on their way to the same standard: but many of them have not yet realised how hard it will be actually to get there.

Either way, whether good or on the way to good, few of these students have even heard of static reasoning, assertions, invariants, variants, let alone have learned how to use them. . . None of the simple, yet profoundly important intellectual programming tools first identified and brought to prominence (more than 40 years ago) has become part of their program- ming toolkit.

Why did this happen? How can it be changed?

What will happen if we do change it?

Below we address some of those questions, using as examples actual material from the two related courses mentioned above; they were given in the years 2010–4. As an appendix, we present feedback from some of the students who took one course or the other.

At the same time, some suggestions are made about whether, when and how courses like this one could possibly be taught elsewhere.