Presentations do-s and don't-s

While attending SAVCBS, FroCoS, and FTP I made some notes with things I liked and things I disliked in the presentations. These are questions of personal style and the list below reflects what I want and I do not want to be as a presenter.

Do

• speak loudly, slowly, and clearly
• use questions to engage the audience and to make sure you are proceeding at the right pace
• say explicitly what are the main ideas
• present examples, details, and technical material periodically
• explain the notation
• use English properly
• present open questions
• present (slowly!) some basics
• skip the formal parts if time is pressing
• ask if the audience has questions periodically (≈ 5 minutes)
• make pauses to allow the audience to think about the consequences of what you said and to read the extra information on the slide (≈ 30 seconds)
• say everything twice, preferably once in an informal way and once in a more formal way, but with some pause in-between
• present `lessons learned'
• show the implementation in the presentation, because it gives a concrete idea of what it does if it is seen in action
• leave time for questions

Don't

• be overtime
• present only a high-level view
• say “I'm sure everyone knows”
• waste time with the outline (in the beginning)
• speak in a monotone voice (I'm skeptic I'll be able to fix this, somehow my throat hurts if I do otherwise)

Red and Blue

Red and Blue are playing a game on the infinite integer plane grid. A move consists of uniting two adjacent points. ((x1,y1) and (x2,y2) are adjacent if |x1-x2|+|y1-y2|=1) Red and Blue moves alternate with Red starting. Red tries to form a closed (red) curve. Can he force this or is Blue able to indefinitely stop him?

Reachability analysis — part 1

Compilers do reachability analysis (also known as dead code elimination) as an optimization that cuts down the size of the produced (machine/byte)-code. Mikoláš had the idea that dead-code should result in a warning because it is likely a bug and, moreover, if we use code annotations we can do a more precise analysis of what is reached and what is not. So we implemented this in the context of JML-annotated Java.

//@ requires x >= 0;
int f(int x) {
  if (x < 0) return 1 / 0;
  return 1;
}

The bytecode produced by the Sun Java compiler is the following.

int f(int);
  Code:
   0:   iload_1
   1:   ifge    8
   4:   iconst_1
   5:   iconst_0
   6:   idiv
   7:   ireturn
   8:   iconst_1
   9:   ireturn

As you can see, the bad division ends up in the bytecode and no warning is produced. But from the comments we see that the intention of the programmer is to push the obligation of providing a non-negative x to the clients of f. What a smart compiler should do is check at all call-sites that this obligation is fulfilled, detect that the condition in the if statement will always be false, and provide a warning saying so. That's basically what we do. (Note that we don't generate bytecode; that's left to the Java compiler.)

The first (boring) phase is to reduce the Java code to an intermediate representation that is much simpler. I'll handwave over this part. Suffice to say that there are many smart people working on how to do it and that current implementations (in ESC/Java and Spec^#, for example) are satisfactory.

The intermediate representation we get to work on is an acyclic control flow graph labeled with first order logic formulas. A node in this graph represents a statement in the program (roughly). The state of a program that executed a certain path in the flow graph is described by the conjunction of all formulas on that path. If we don't care about how a program gets to statement s we can take the disjunction (logical or) of all execution paths that lead to s. The result describes the state of a program about to execute s, irrespective of how the control flow got there. Such a formula is called the precondition of s. So if the graph has the edges a→ b, a→ c, b→ d, and c→ d, then we know that the statement (a∧ b)∨(a∧ c) is true about a program that is about to “execute” the statement in the node labelled d. (Of course, there are more efficient ways than looking at all paths.)

We then use a theorem prover to see if some statement precondition can never be true. (Alternatively, the set of states described by it is empty.) Theorem provers are reasonably good at answering this kind of questions. Still, they are quite slow, and asking the question for each statement results in an unusable extended static checker. We should be able to do much better. For example, if the flow graph is a chain a₁→ a₂→⋯→ a_n and we ask about a_n and the theorem prover says it is reachable, then we might as well conclude that everything is fine, solving the problem with 1 query instead of n. More generally, the answers given by the prover can be propagated in the flow graph using some simple rules. It should then be possible to use these rules to decide about which statements to ask the prover in order to minimize the expected total number of prover queries. I'll describe this in a subsequent post.

Liverpool bookshops

I have a day to spend in Liverpool. Naturally, I visited some bookshops. It turns out they are much better than the ones in Dublin. Most of them actually have a section with scientific books that go beyond the for dummies and teach yourself in 2 seconds type of books. Of course, strange things remain. For example, I have no idea how they decided to put side-by-side a textbook on Calculus and a "textbook" on plumbing. In fact, I've heard recently that plumbers and car repairers in England are called "Engineers."

I was pleasantly surprised to notice that they even have travel guides for Bucharest and Romania. So I spent about 30 minutes reading these. The one on Bucharest started by saying that it is "the most unappealing European capital." Fair enough. From what I've seen that might well be true. The main good point was that it is a "lively" city. That sounds right too. Besides, all the places recommended in there seemed OK. Of course, there were plenty of misspellings and, at some point, the "English phonetic" translation of some phrase made absolutely no sense and was probably in some other language.

Then I looked at the Lonely Planet guide to Romania. It started with a picture of icons in a monastery. Yep, Romania has lots of small monasteries, usually placed in picturesque places. The next picture was with a group of Gypsies celebrating something. Hmm, well, there are many Gypsies in Romania but their behavior, traditions, way of life, and even appearance are quite different than that of an average Romanian. I think that choice of a picture was inappropriate. Such guides should show typical people in the beginning.

Then I continued to read a bit about history and I got quite upset. There is a well-known controversy between Romanians and Hungarians concerning the history of Transylvania. But the way it was presented in this travel-guide was simply made to generate more animosity. Which is a pity. There were lots of slightly imprecise statements and small omissions that made me feel this way.

For example, they said that "Iancu de Hunedoara is claimed by both Hungaria and Romania but he is probably of Serb lineage." What I learned in school was simply that he was born in Transylvania and that he had Serb ancestors.

Another statement was that "there is simply no evidence for the theory of continuity" which is "simply" not true as you can tell by reading the Wikipedia article linked above. This theory is also presented as being fabricated by the Communists. Also, what they say there about what this theory is about does not match either what Wikipedia says or what I have been taught in school. The latter is as follows: It is unlikely that all Dacians left from Transylvania when the Roman administration left Dacia; one piece of evidence is a couple of art objects we found that date after the Roman administration left (271-275) and look like they are made by Dacians. By no means have I been taught the obnoxious version presented in that guide, which I won't even spell out.

Finally, they say that many Magyars left Transylvania after 1920 because they have been discriminated against. Fair enough. I don't actually know about 1920 but I do know that they were discriminated against during communism. And they still are but to a much lesser extent and only by uneducated people. This is a pity and I hope things will improve. This kind of discrimination determines Magyars living in areas where they are a majority to not serve Romanians in stores sometimes, for example. (This happened to my wife.) It's regrettable but entirely understandable. The guide also says that for most of the period 1000-2000 the Transylvania was under Hungarian control. Also true. But I find it a bit strange that nowhere is mentioned that during those periods there were laws that precluded Romanians to own land and in some cases even restricted their freedom of movement.

I'd wish this kind of historical studies will be made by specialists from now on without any political pressure. In particular, I think that events from 1000 years ago cannot be sensibly used in any political claim nowadays. In fact, I hope frontiers in Europe will gradually disappear. This should reduce hate among people.

Oh, yes: Please use more reliable sources than Lonely Planet from now on when traveling. Even Wikipedia is better.

SAVCBS 2007

In the beginning of September I attended SAVCBS in Cavtat, Croatia. The place is beautiful, with landscapes in the style of the Pirates of the Caribbean. The focus of the workshop is on components, but a good proportion of people who run it are from the formal methods world. The presentation I liked most was that of Ádám Darvas. One reason why I liked it is that I am familiar with the subject so I was able to understand. He talked about what model classes are good for and how to encode them in first-order logic so that theorem provers can reason about them. The first previous solution is to give an encoding using uninterpreted functions. The second previous solution is to use the built-in theories of the theorem prover. ESC/Java does neither. Model classes are specified using normal JML and that will roughly get translated by ESC/Java into uninterpreted functions for the theorem prover. That translation is probably slightly worse than a handcrafted translation. And Ádám claims that the problem with the handcrafted translation into uninterpreted functions is performance, which sounds quite probable. The reason theorem provers have built-in theories is performance, while in principle uninterpreted functions are good enough for everything.

Ádám presented a systematic way of encoding model classes using higher-order provers built-in theories. A simple and powerful idea. I forgot to ask him while I was there what he things about using his method for an automated prover.

By the way, Ádám is Hungarian and on my way back to Bucharest I stopped for a little while in Budapest, which appears to be a beautiful city. I certainly have to go there again. Now I am in Liverpool, a rather sad city, attending FroCoS and FTP.