[SystemSafety] Logic

[Dewi Daniels]

Peter,

I graduated with a degree in Computing Science from Imperial College, London
in 1981. I don't think I could have wished for a better foundation for my
career in computing. The teaching emphasised general principles that have
stood me in good stead throughout my career instead of specific technologies
(which have long since been rendered obsolete -- we used IBM 029 card
punches in my first year).

Yes, we were taught logic, computing theory and formal methods. I remember
being taught set theory, predicate logic, Turing machines, the theory of
algorithms, logic programming (Imperial was big on Prolog in those days) and
program proof (the text book used was Dijkstra's seminal "A Discipline of
Programming"). I was delighted to be able to put these skills into practice
when I joined Program Validation Limited in 1990 to conduct program proof of
a family of Full Authority Digital Engine Controllers and to help develop
the SPARK Examiner. While I agree with other posters that formal methods
deserve much wider application, the main point I want to make is that I have
found my education in formal methods to be invaluable even on projects that
make no use of formal methods. Throughout my career, I have been surprised
by the exceedingly poor quality of requirements produced by many
organisations. In particular, I have come across many very smart and
experienced programmers who seem totally unable to write detailed and
precise requirements without resorting to writing pseudo-code. I believe
that my experience of writing pre- and post-conditions has greatly improved
my ability to write clear and concise English-language requirements that do
not constrain the implementation. Furthermore, I believe the main benefit of
my undergraduate education was the ability to approach problem-solving in an
analytical and methodical manner and to express my ideas clearly and
concisely, which are skills that I believe would have benefited me greatly
in any career I had chosen to follow.

The course at Imperial also emphasised the principles of good software
design and the importance of abstraction. I owe a great debt to my
programming tutor, Iain Stinson, whose ideas on software design have
influenced me throughout my career. He taught the principles expounded by
Dijkstra, Wirth and Parnas. I find the main difference between average
programmers and great programmers (not that I consider myself one of the
latter) is the latter's ability to find the right abstraction, eliminating
unnecessary complexity. The best programs look so simple that they give the
misleading impression of looking as if they were easy to write.

The course at Imperial was very much a software engineering course rather
than a computer science course. Imperial was rather unusual at that time in
teaching project management as part of the undergraduate curriculum. The
teaching included practical programming projects where we were given the
opportunity to lead a project team. The main textbook used was Brooks' "The
Mythical Man-month". I'm quite depressed how many managers still think you
just divide effort by team size to get project duration.

Unfortunately, statistics was taught at Imperial by the mathematics
department, whose lecturers considered us mere engineers to be inferior to
their mathematics students, and who had an excessively theoretical approach
to the subject. Fortunately, I had studied 'A' level statistics at grammar
school under an excellent teacher called Mr Roberts, who instilled in me an
understanding of both the power and the limitations of statistical methods.
I am always amazed by the way that statistics are misused by people who
should know better.

The tutors at Imperial were right to emphasise general principles over
specific technologies. We were taught to program in Pascal (mostly),
Fortran, Cobol and Simula 67, none of which are in common use today, yet the
principles I was taught are as valid today as they were in 1981. Which leads
me to a story: many years ago, my wife insisted we switch from On Digital
(an early terrestrial digital television provider, long since defunct) to
Sky (a satellite digital television provider that now dominates the UK
market) because our video cassette recorder (yes, it was that long ago)
regularly used to record a blue screen because our Nokia set top box had
crashed. I happened to notice a recruitment advert for Nokia. I
half-seriously submitted my CV, recounting our poor experience with the
Nokia set top box, explaining that I had no idea what any of the buzzwords
or acronyms in their advert meant, but that I could introduce software
engineering techniques into their organisation that would cost very little
to implement, but which would greatly improve the reliability of their set
top boxes. They didn’t even bother to reply. Given Nokia's current woes, I
most definitely feel it was their loss and not mine.

On a final note, like Martyn, I am pleased to see the late Peter Amey's name
mentioned in this thread!

Yours,
 
Dewi Daniels | Managing Director | Verocel Limited
Direct Dial +44 1225 718912 | Mobile +44 7968 837742 |
Email ddaniels at verocel.com
 
Verocel Limited is a company registered in England and Wales. Company
number: 7407595. Registered office: Grangeside Business Support Centre, 129
Devizes Road, Hilperton, Trowbridge, United Kingdom BA14 7SZ

-----Original Message-----
From: systemsafety-bounces at lists.techfak.uni-bielefeld.de
[mailto:systemsafety-bounces at lists.techfak.uni-bielefeld.de] On Behalf Of
Peter Bernard Ladkin
Sent: 15 February 2014 10:53
To: systemsafety at techfak.uni-bielefeld.de
Subject: [SystemSafety] Logic

Folks,

we have a local issue in our faculty which I think is of more general
importance and would like to solicit views, evidence and so forth. This is
about curricula; I don't know how many people here are interested in that at
the undergrad level, and crave indulgence from those who don't.

To put the last paragraph first, I would like to gather opinions on the
necessity of some skills. I would argue that programming dependable systems,
and dependable-software engineering in general, requires some facility with
formal description languages (FDLs). FDLs are necessary for requirements
specification and analysis, and they are also necessary for the refinement
steps that occur between requirements and code, as well as for any kind of
static analysis of code. They are necessary for validating compilers.
Classical proposition and predicate logics count amongst the most common and
basic FDLs; a skill in expressing some kinds of assertions in predicate
logic has often been regarded as necessary for a basic informatics
education. I would think some understanding of how FDLs work is essential
for any work in dependable engineering of SW. Do people agree? If so, could
you please give me some evidence?

The context is this.

I am on various mailing lists for announcements of conferences and academic
research jobs (PhDs and Post-docs). Almost all of the stuff I see requires
some to considerable expertise in formal methods (FM). Indeed, I would say
that support for FM-related research has exploded in the last ten years.
But our students don't have enough experience of FM in their degree courses
to stand much of a chance applying for such jobs. Even if they take all I
regularly offer, it is barely enough.

We have four undergraduate degree programs, all "hyphen-informatics" in
which informatics is studied along with an application domain: informatics
in natural sciences (NWI); bioinformatics and genomics (BG); "cognitive
informatics" (KOI); and media informatics (MI). (The last one of these is
aimed primarily at new-media artists - selection is through an artistic
portfolio.)

We used to have degree programs based on the German Diplom system
(equivalent to a Master's with thesis, but as a first degree) but have
switched in the last decade to (Germany's idea of) Bachelor's/Master's
combination.

The course in Theoretical Informatics (TheoInf) used to be compulsory (for
all except media informatics), and comprised the usual automata theory,
Chomsky-hierarchy languages and logic. We agreed a few years ago to separate
logic from the other two subjects and have two courses. This decision was
based partly on the fact that I had developed an applied-logic module (= two
courses in two semesters) which did rather more than the somewhat cursory
nod (from my point of view) it got in the combined course.

But something odd happened that nobody I asked has been able to explain.
TheoInf is compulsory for NWI and KOI, as it should be. But Applied Logic
did not become compulsory for anyone. So, essentially, logic became an
elective.

Boolean logic is taught in the Technical Informatics module, which is
compulsory for NWI and KOI (the other two get a brief survey of TechInf),
which does the usual Karnaugh-diagram and Quine-McCluskey minimisation
stuff. But there is the question whether people who study Boolean logic for
TechInf can apply what they learn to Propositional Logic in the form of
language rather than algebra.

Logic is also briefly, very cursorily, mentioned in the Mathematics modules
required for NWI and KOI, which are taught by the Maths Department, but not
to the extent that any student feels they can use it.

My indications from a decade ago were that our students couldn't, very well
(I didn't teach TheoInf, but I used to examine for it. I would give an exam
question - "what does (A AND B OR C) mean, where A,B and C are
propositions". The answer is twofold: that the meaning of a statement in
propositional logic is given by its truth table; and further that there are
two possible truth tables corresponding to this statement. Less than half
could give the first answer, and only about one in five would notice the
ambiguity. This despite asking the *same question* for years and years).
This is why I developed my Applied Logic course, to get people familiar with
the basics of inference
(syntax) and meaning (semantics). The first semester is coextensive with,
say, Huth and Ryan Section 1.2.

One of my Bachelor's students (that is, a student who has done a number of
electives which my group offers, and has subsequently tutored the courses)
applied to do a Master's at another German university (the Technical
University of Braunschweig) and was told he didn't appear to have enough
logic. He told them he was currently taking my Applied Logic course, as well
as another course in logic in the Philosophy department, and he was then
provisionally admitted (he did end up staying with us, though).

I suggested to my colleagues that we didn't appear to be teaching all of the
basic material which other informatics people would expect from people with
a degree in Informatics, and that it would be a good idea at least to inform
students of what electives they might need in addition to compulsory
material in order pursue a Master's in Informatics elsewhere. We had some
discussion of that.

At least some colleagues seem to think that we offer broadly what the
professional society (GI) recommends in curricula. That may formally be so,
but I would say only formally. It also doesn't address the issue of what
kind of skill with FDLs people with a university degree in informatics could
be expected to have.

I looked at the curricula of three top-20 universities in the UK: Oxford,
Cambridge and Imperial College London. All of them have substantial logic in
their curricula for any of the degree courses.
(Oxford seems to have logic in about half its electives as well!).

I have started to contact people who are likely to feel similarly about the
importance of skills with FDLs and in particular with applied logic in
informatics as I do. I'd be grateful for any material - stories, opinions,
observations about curricula, about software engineering practice, and so
forth - which you may be able to convey.

PBL


Prof. Peter Bernard Ladkin, Faculty of Technology, University of Bielefeld,
33594 Bielefeld, Germany
Tel+msg +49 (0)521 880 7319 www.rvs.uni-bielefeld.de




_______________________________________________
The System Safety Mailing List
systemsafety at TechFak.Uni-Bielefeld.DE