Where have I been?

It has been a while since my last blog post. I have a collection of posts that I have been meaning to posts but that were somehow never good enough. I'm going to try harder to publish them. In the mean time, here is a snapshot of what has been going on with me in the last two years... at least scientifically.

I underwent a peculiar transformation since I moved from Zürich to Toronto. I used to think that you can study a software system purely from a logical point of view and, when you proved all you needed to prove, all is left to do is run the software. I have done it for some non-trivial software system but I realize that, for a bigger piece of software, the amount of work to cover the whole thing would be excessive both in the sense of "exceeding necessity" and "exceeding ability to do so". I'm reworking my vision of software design as an activity that includes proving theorem but which also comprises other techniques of validation. For example, random testing as done by QuickCheck in Haskell is often a good compromise. The key is to choose which technique applies best.

For instance, I started developing a program one year ago and it has now become relatively big (considering that I'm the only person developing it) and, to my surprise, it works well even though I didn't prove a single property about it. In the back of my mind however, I keep pulling some parts of the design aside and figuring out the logic that would make it possible to prove that it is correct. One of these days, I'll prove the correctness of some crucial parts of my programs and I think that will be both really interesting and really useful -- especially considering that the program is a formal verifier.

On the other hand, I am also discovering the interplay between mastering the theory and having good software tools for designing software. I used to think that if you know the theory well, you have no need for tools. I'm realizing that this is a pretty silly point of view: the program that I mentioned above is specialized in writing proofs for simple conjectures. It very incredibly fast. In one of the small systems that I use that tool for, there are around 500 conjectures that need to be proved. Most of them are incredibly easy to prove but they still need to be proved. My tool takes about 30s to prove 499 of them leaving me with the truly difficult theorem. That's incredibly helpful because now, I can focus my attention on the hardest of the hard design problems. The best part is, compared to an interactive prover, I do not need to manually invoke the prover on each proof obligation. They will all be attempted automatically except for those with a proof provided by the user.

The tool is designed to allow me to verify Unit-B models. I don't think I would be able to use Unit-B as confidently as I do and as efficiently as I do without it. Even better, when using Unit-B to develop the very first examples, every time I was faced with a problem, I could improvise a solution and think really hard and figure out that it was valid. This is very inconvenient to teach the method because I hardly have a list of all the tricks that I use. By implementing a verifier, I need to identify the truly useful techniques and make sure that they can be used with confidence and have a clear explanation to disallow whatever I choose to exclude. In other words, I'm now forced to formulate the rules of the method independently of any one example.

So much for simplistic views of the world.

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

Algorithms in Object Oriented Programming

Approximately two years ago, I was writing a set of classes for dealing with graphs. At one point, I had to provide facilities for depth-first and breadth-first traversal. At first, I thought of doing it as a higher order function: it would be a regular encoding of a graph traversal that would use an agent --in Eiffel talk, in C# talk, it would be called a delegate-- to process every node encountered. This seemed a lot of work to set up and use and I decided to create particular kinds of cursors that would enumerate the nodes in preorder, postorder or in breath-first order. It was a very interesting exercise because I transposed the state of the computation of the algorithm to make it the state of a class. At the time, it seemed like a very nice reinterpretation of an algorithm to have it fit a more object oriented context. I did not push that investigation further. At the moment, I am working on the development of a parsing algorithm and its correctness proof. One of the decision I took was to have a token reading primitive instead of passing a complete sequence of tokens. With respect to the formulation of the algorithm, there is very little differences but with respect to its interface, the difference is big enough to allow me to do an interesting observation. The reading can be interpreted as a routine called by the program implementing the parsing algorithm, but it could also be interpreted as a method of a class whose state is described by the local variables of the algorithm. This would allow, for example, to interpret keystrokes as tokens and feed them to the parser as they come. What if we just considered it as an input without regard to whether it is ordered by a client or by the module. With that view, we could have a scanner which outputs one token at a time and inputs one character at a time. We could plug the input of the parser on the output of the scanner for which the input could either be plugged on a streamed string or on the keyboard input without significant changes. Furthermore, if we wanted to decouple further the lexical analysis and the syntactic analysis, we could put a buffer between the two (still without changing the algorithms) and we could even put each machine on its own process. Some theoretical framework which is very useful to conceive that is that of action systems. With just a few exception, an action system could be understood as a canonical view of (not necessarily terminating) programs where we have one loop over a set of one line guarded commands. For example, for the following statement: a := 32 if b > c then b, c := c, b [] b <= c then skip fi We could get the following loop which we will consider as an action system: line := 0 ;do line = 0 then a, line := 32, 1 [] line = 1 /\ b > c then b, c, line := c, b, 2 [] line = 1 /\ b <= c then line := 2 od The advantage of using an action system instead of the corresponding program (when there is a nice one) is that the action system can compose for various purposes. If you want to simulate the concurrent execution of two programs, taking the union of the actions (the lines in the loop) of their action system will give you a model of how the two programs will execute. The assertion that you put in both programs must become invariants in the loop attached to line numbers. It is similar to the methods described in the Gries-Owiki theory and in A Method of Multiprogramming by Netty van Gasteren and Wim Feijen. The other use of the action system is that it can model objects. Each action can be understood as a method or as a method call and it allow one to model "concurrent" access to objects much better than what we have with structured programming geared with type bound procedures (what we see all the time in OO languages). Simon Hudon Finished on August 26th Zürich