Teaching

For some reason, since the weekend I'm pretty down and yesterday's events did improve anything. I had an exercise session in Software Verification and the exercises were to be done with pen and paper which suited me fine since I don't know much about separation logic and I am curious to see how convenient it is to use it to solve day to day programming problems. First disappointment: instead of presenting a collection of usable manipulation rules and theorems, he gave us an intuitive notions of what the logic is about and expected that it would be enough to solve the problem. This defeats the whole purpose of using formal logic and I equate with no less than giving up the teaching of the topic. To my liking, something good enough for the exam but unusable afterwards is a total failure of teaching Second disappointment: we had to write a program with a loop and prove its partial correctness. He mentioned techniques of weakening the postcondition to obtain a loop invariant but he said that he would not teach it since they were not likely to have to find an invariant at the exam. Instead, he suggested to (with no alternative, we could say imposed on) the students to execute their loop on paper and, through guesswork, to find the relation that is preserved throughout the iterations. This is at best a very clumsy way of finding a loop invariant and I am sure that, for many students, it has driven home the message that formal methods is no more than an academic exercise instead of something useful that they can use when dealing with hard problems. And it is not like he did not know that they are very useful for the direct derivation of programs or that he thinks that it is inefficient problem solving. The only conclusion left is that he thinks students are not up to it. That's sad to have such a poor esteem of the people that came all that way to learn something. And I don't mean that I'm the only one victim of that practice (actually, I don't consider myself a victim at all since I think lectures are only for administrative purposes; my true learning is done on my own time with books and smart people) but I think of the people that worked all through their bachelors to end up with some farce of a lecture. Even though I am aware that not everybody is as motivated as me for learning new material, I would think that the time spent there could be better spent doing something else. I feel better already, having said that! Simon

The LaTeX Syndrom

Reading a certain paper for my seminar of software engineering, I had nausea when seeing the appalling notation they chose to talk about the soundness of their system. My supervisor told me it was of no importance but still I can't help but think that the notation could be improved a lot. They seem to have chosen to use a formalism in order to pack as much information as possible in one page and I am convinced that they must not have used it much with pen and paper because it would have been much to heavy. This leads me to the hypothetical LaTeX syndrome. I think they needed LaTeX to typeset such a notation and would not be able to do it without LaTeX. I think in the design of a notation, it should be taken as a yardstick that the notation is usable with pen and paper and it must not be a torture to use it for any length of time. I would go one step further and state that I would like those that do not follow this principle to be condemned to use their formalism on paper for as long as necessary for them to repent. I could also ask for a reward for the people that do abide to the principle: they could have the joy of using their formalism and see their problems nicely stated and elegantly solved with it. I am not making a statement against LaTeX here, at least not yet. What I am complaining about is the people that use it without the application of good judgement. As a reader, I think the bad formalism was an important difficulty in seeing the point they used it for. Fortunately for me, they did not use it too much. I must admit that I now avoid LaTeX altogether since most of my efforts are spent on LaTeX itself rather than on the problem at hand. I have started using rich text editors which don't pretend to be smart. The big drawback is that they are harder to use with version control. For that reason, I'm thinking of using plain text but, for some reason, Mac OS does not make that easy. Simon Hudon Written after a bad day on October 19th 2009 Meilen

"For someone whose only tool is a hammer, every problem looks like a nail" (EWD 690)

This note is about paradigms. In short, I would define a paradigm as being the belief that a particular abstraction or theory fits a certain context. We can see, for example, in programming, the paradigm of object oriented programming as being the belief that focusing one's analysis and design efforts on the relations between different pieces of data is an efficient way to cope with the variation in requirements. Also, we can see that applying game theory to economic behavior gives rise to the paradigm that we might call "the rational choice". I think a paradigm is a very useful belief to have because it allows one to deal in simple terms with problems that might get complicated. In my opinion, a healthy use of a paradigm is like controlled schizophrenia: when you deal with a problem within the realm of applicability of the paradigm, it is useful and often necessary to assume its postulate without questions. This is very efficient when dealing with related problems. However, one should be able to defend the use of the paradigm and more specifically, should consciously stop believing in the postulates while doing so. I find it frustrating when discussing with somebody when I realize that, not only can I identify the paradigm he adopts (which is not bad) but I realize that he is unable to step out of it even after several direct attacks at his assumptions. This happens both in technical discussions about computing and in humanities. On the other hand, it is also fruitless to discuss hard problems with somebody who can't assume the postulates once they have been defended. In technical terms, this might be seen as somebody that keeps reasoning about a method call in terms of the instructions that gets executed as a substitute instead of reasoning in terms of an abstract specification. In the first case, the person is hardly schizophrenic at all (what a fraud!) and in the second case the schizophrenia is uncontrolled so the person's reasoning is all over the place: he can't focus on one aspect of his problems at a time because he can't see a clear separation between the two. As a second example of uncontrolled schizophrenia, I see some people rely strongly on set theory and have to understand everything in terms of set. Some of them for example, can't bear to use sequences for their reasoning because the proofs with sequences are so complicated and messy. This is a recent conviction of mine but I keep seeing examples where having a clear and simple abstraction would be much more effective. In the case of sequences, we need a set of postulates that describe sequences as objects of their own right and don't drag sets or anything else into the picture unless a useful relationship can be defined. And even then, the relationship is not central to understanding the abstraction. For soundness purposes, it might be useful to translate postulates of sequence theory in set theory. This becomes metamathematics though. It does not affect the use of sequences.

What is Abstraction?

I've been talking about the sin of confusing vagueness for abstraction for a while but I haven't stopped to define more precisely what it means. So far, the best I have done to give an understanding of what abstraction is is to say that it is a simplification of an object and that being abstract does not preclude being absolutely precise. Let's try to be more precise on what constitutes an abstraction and what does not. First, an abstraction is a simplification but a simplification does not qualify automatically to be called an abstraction. So, what is missing? If we wanted a completely precise expression, we would say that A is an abstraction for B with respect to a set of properties. The set of properties is usually universal in the context in which abstraction is used. For example, for software engineers, it will be interesting to see a specification as an abstraction for a set of implementations with respect to functional properties. It means that seeing the effects of a particular implementation, if we can always follow them by reading a specification and not get any surprise, the implementation is correct with respect to that specification. For somebody working with algorithms, the performances will be more important so it may be useful to have an abstraction with respect to running time but one that does not preserve functional properties. It is in this respect that I got convinced that having a small theoretical kernel for a modeling language (in Abrial's sense) is not appropriate useful or abstract. For instance, in Event-B, everything is understood in the context of set theory and I was opposed that using sequences was too difficult because of the complications of the underlying set-theoretic model. The key here is that the objection denotes a failure to create a level of abstraction where sequences are understood for what they provide. Providing a set-theoretic model for them is not useful for their use; it is useful to convince someone that the set of axioms describing sequences is sound. After that, we must understand sequences on their own. This is why, I believe, abstract data types are very important for the use of formal methods. Simon Hudon October 11th Meilen

Modeling vs Programming vs Coding

I usually adhere to Dijkstra's and Morgan's view of programming: it's the action of passing from a precise specification to an executable program. I've had some contacts recently with the Chair of Programming Methodology recently and I was expecting them to have a similar view to mine on what constitutes programming. I was a little disappointed to see that their view was more closely related to "writing down executable code" than "reflecting on the design of a suitable implementation for a given specification". What they call programming, I would rather call coding. Before that, I had a short talk with Dr. Jean-Raymond Abrial, founder of the B and Event-B formal methods where I saw that he shunned programming. However, I came to realize that what he called programming was also coding. On the other hand, he called the activity of central importance to software engineers "modeling" which is a term I have been trying to avoid for some time, now, because of its central role in methods like UML, which I find eminently ignorable for software engineers; it simply seems to stem from confusing vagueness with abstraction and I think there's no reasons to accept vague documentation for a design. I still prefer the word programming for the formal derivation of implementations but I feel more and more like I will have to find a substitute because of the lexicon associated with programming. It is associated with programs which is related to routines and sequential execution whereas I believe that sequential vs parallel execution is an implementation choice that should not receive half of the importance that it is usually given in the development process. To be absolutely unambiguous, I could rename the activity "designing a software system" taking the liberty of changing software with discrete if necessary but it might be a bit too long. However, design is an activity so widespread that it does not feel appropriate to use it on its own when talking about programming. For this purpose, I could resort to "modeling" but I run the risk of having to precise all the time that I have nothing to do with UML or their bubbles and arrows techniques. Ah, well! I'll keep thinking about it. In the mean time, I'll keep programming for short and design of software system to be unambiguous. Simon Hudon October 11th, 2009 Meilen

Hehner's Program Calculus

Preamble This post, although involving unusual notions for most, is meant to be very basic and I expect most computer scientists, computer science students to be able to understand it. If you don't please let me know, I'll arrange to put enough background in it.

End of preamble

For some time, Prof. Jonathan Ostroff has been trying to convince me of the elegance of Hehner's method of refinement. Recently, I was giving examples of Dijkstra's program calculus. Among these was the derivation of the program for computing the maximum of two numbers and its proof. I eventually came around to consider this example terms of Hehner's method and I was struck with at how simple his formulation is. For example, the semantics of the following conditional statement is given in Hehner's formulation and in Dijkstra's (and Morgan's, for that matter).

if b -> x := E [] c -> x := F fi

Hehner (x' denotes the value of the variable x after execution whereas x denotes its initial value):

(b  /\  x' = E)  \/  (c /\ x' = F)

Dijkstra (it is defined as a function of the predicate p and it represents the weakest precondition that will allow the statement to enforce the postcondition p):

(b   ==>   (x := E).p)  /\  (c   ==>   (x := F).p)  /\  (b  \/  c)

Just here, we have a factor of a little bit less than two. It is a bit of an unfair comparison, though since the two formulae are not used in the same way. It is interesting to note, however, that Dijkstra's formulation includes a term (b \/ c) which he calls "the law of excluded miracle" (as a pun referring to "the law of excluded middle"). Its purpose is to make sure that one of the branches of the conditional applies whenever we get ready to execute the statement. On the other hand, Hehner's formulation implies (b \/ c) and it does not have to be included in the term. Unfortunately, it is necessary with Hehner's method to mention every variable that do not change which, as it appears to me, an amateur when it comes to Hehner's method, can be quite inconvenient.

Here is the development of the mentioned program with both methods. We start by stating the postulates that we have.

(0)   x max y  >=  x
(1)   x max y  >=  x
(2)   x max y  =  x   \/   x max y  =  y
(3)   x max y  =  y max x
(4)   x  =  x max y   ==   x  >=  y
(5)   y  =  x max y   ==   y  >=  x
(6)   x >= y  \/  y >= x

Now, here is the postcondition that we want to implement:

P:  z =  x max y 

because of the form of (2) we could presume that the appropriate execution of either of:

Q:  z := x

and

R:  z := y

We must therefore investigate when it is appropriate to execute each. For that, we calculate the weakest precondition that allows each of them to establish the postcondition. We can do that by applying the statements Q and R as a subtitution over the postcondition P.

   Q.P
==    { Subtitution }
   x  =  x max y
==    { (4) }
   x >= y

(with == being the logical equivalence) Using a similar calculation, we get

R.P    ==    y >= x

We can conclude that the following code establishes the postcondition:

if  x >= y -> z := x 
[]  y >= x -> z := y 
fi

The only thing left to do is to apply the law of excluded miracle and make sure that there is always a branch which is executable.

   (x >= y)  \/  (y >= x)
==    { (6) }
   true

If we try the same derivation with Hehner's method, we can start by saying that the postcondition is trivially established by

P:  z := x max y

which, unfortunately, is not executable. For simplicity, we will assume that x is the only assignable variable. We have the following statement representing the semantics of P.

Q:  z'  =  x max y

We can now start calculating:

   z'  =  x max y
==    { Identity of /\ }
   z' = x max y  /\  true
==    { (2) }
   z' = x max y  /\  (x = x max y \/ y = x max y)
==    { /\ distributes over \/ }
   (z' = x max y  /\  x = x max y)  \/  (z' = x max y  /\  y = x max y)
==    { Leibniz, twice }
   (z' = x  /\  x = x max y)  \/  (z' = y  /\  y = x max y)
==    { (4) and (5) }
   (z' = x  /\  x >= y)  \/  (z' = y  /\  y >= x)

The final stage of the calculation represents the semantics of the following conditional:

if  x >= y -> z := x
[]  y >= x -> z := y
fi

What I like about the previous derivation is that it is very straight forward. There is a small invention involved which is to introduce true at the beginning and transform it into (2). It seems reasonable since it gives a simple expression for any possible value of x max y. Also, the proof contains a little too much detail. For instance, the first and the second steps could have been merged and explained simply by referring to assumption (2).

On a more personal side, I must admit that, for at least one year, I was very enthusiastic about Ralph Back's lattice theoretic interpretation of programs: it's just so elegant! In practice however, I can't help but being struck with awe at how straightforward the program derivation is with Hehner. Like Dijkstra said so often: we must not become enamored with our tools especially if they show how clever we have been. Back's interpretation introduced me to lattice theory which I still like and find pretty useful but using it for program calculus does not seem necessary and I should probably turn over to Hehner's program calculus even though it does not yell "I know lattice theory!"

Simon

September 18th 2009

Zürich

Trends in programming languages

I just saw a very insightful comment in the 2003 publication of the IFIP work group 2.3 on programming methodology about one of the paper it contains. I cannot attribute it for sure but since Annabelle McIver and Carroll Morgan are the editors, one of them must be at the origin of the comment. It says that in the field of programming languages, one can distinguish two trends. The first, by far the most popular, views a programming language as a formalism to abstract away from the specifics of the machines and the tiny optimizations that might be useful but are tedious to come up with and to maintain. It gives Fortran and Java as examples. Fortran allows the programmer to keep his concentration on other things than the evaluation of mathematical expressions which is quite useful. On the other hand, Java allows the programmer to put the implementation of classes in one place and the latter does not have to think about the specific details of the use of classes (e.g. dynamic binding and memory management). Personnally, I would call those coding languages: they make programming simpler than writing machine code. The second trend views a programming language as a formalism to help reflect on the problem at hand. I give here two of my own examples: Eiffel and B. The fact that they cover analysis, design and implementation is a telling sign that it does not support the view of a program as a sequence of instruction but as a computational solution to a problem. When trying to "sell" languages of the latter category, I often encounter objection stemming from the interlocutor's adherence to the first category and, most of the time, it ticks me off because I have the impression that they are focusing on the wrong aspect of a programming language. Having seen this description of the two trends, I'm thinking of questioning my interlocutor's yardstick instead of getting frustrated. Simon Hudon September 13th 2009 Zürich