Simon's blog prime

On Function Purity and Simple Framing

2011-07-05T09:56:00.003+02:00

Here is the latest blog post by Bertrand Meyer.

http://bertrandmeyer.com/2011/07/04/if-im-not-pure-at-least-my-functions-are/

It talks about the problem of function purity and broaches the subject of framing. In short, the frame of the specification of a routine is the set of variables (in the broad meaning of the term) that the execution of the routine can modify. In object oriented programming, it is especially tricky because of the sets of dynamically allocated objects of which it might be necessary to alter the state in a given routine. Indeed such set can be taken to be the set of objects reachable from a given root. In a limited solution, such as shown by Meyer in his latest post, you only name variables and expressions that can change. In more elaborate solutions, such as the dynamic frames of Kassios (as quoted by Meyer), it is possible to provide a set of objects and the attributes that can be expected to change. It is especially handy for specifying dynamic data structures like linked lists.

Such a solution seems to present the disadvantage of disallowing the extension of frames through inheritance, which Meyer preserves. I think a compromise can be reached between the two but it is a bit too involved for a post only intended for sharing another blog post.

Why I Prefer Predicates to Sets

2011-06-21T13:55:00.006+02:00

Various recent comments by others have made me realize that it is about time I write a comparison between sets and predicates.

One comment that springs to mind is a response I got when I said that I almost never use sets, that I prefer predicates. I was asked what was the point to choose since predicates can be represented as sets: a predicate can be seen as a boolean function which in turn can be seen as a functional relation which is basically a set of tuples. More directly, for every predicate you can associate a set which contains exactly the objects which satisfy the predicate. To which I have to add that for each set, there exist the characteristic predicate which is satisfied exactly by the object contained by the set.

What we just established is the semantic equivalence between the two. Such equivalence is less important than it might seem. From a logician's point of view, the equivalence tells us that for each theorem of predicate logic, there should be an equivalent theorem in set theory.

From an engineering and scientific point of view, that is from the point of view of someone who wants to use either of these tools, there is an important difference, one of methodological importance, which, understandably, is irrelevant for logicians.

The difference lies in the flexibility of the related notation. It is hence of syntactic nature. If we want to let the symbols do the work --and I do--, we have to make sure that we can find solutions in the simplest possible way.

One way of doing this is to avoid spurious distinction, i.e. to preserve symmetry as much as we can. This is where predicate calculus [0] is superior to set theory. If we start by encoding set theory into predicate calculus, we will see, little by little, a fundamental difference emerge. In the following, capital letters will stand for sets and their corresponding predicates will be the same letter in lower case. As an example:

	(0)  x ∈ P  ≡  p.x
		for all x

with the dot standing for function application and ≡ for logical equivalence [1]. It relates a set to its characteristic predicate.

Note:
Please notice that the convention of upper cases and lower cases is nicely symmetric. We could have defined characteristic predicates of a set as cp.S or the set of a predicate as set.p but we chose not to in order to preserve the symmetry between the two. Instead of saying that one is the characteristic predicate of the other, we say that they correspond to each other and it does not have to appear everywhere in the formulae where they appear.
(end note)

Notation

Here is a little bit more of syntax before I start the comparison. I take it mostly from [DS90].

If we want to say that a predicate p holds exactly when q holds we can express it as follows:

		〈∀ x:: p.x ≡ q.x〉

It is a bit too verbose for something that is supposed to relate p and q very simply and, for that reason, we introduce a shorthand. Instead of quantifying over x and using x everywhere in the formula, we will have an operator that will say: this predicate holds everywhere:

	 	[p ≡ q]

It is more concise and it is an improvement. It might seem like cheating though unless we know of the notion of pointwise extension of operators. For instance, ≡ applies to boolean operands but we allow ourselves to apply it to compare boolean valued functions too. This is how it then behaves:

	(1)  (p ≡ q).x  ≡  p.x  ≡  q.x
		for all x

We implicitly postulate that all logical connectors apply to boolean-valued functions. If we add one more definition, the previous universal quantification can be calculated to a form with an everywhere operator.

	(2)  [p]  ≡ 〈∀ x:: p.x〉

		 〈∀ x:: p.x ≡ q.x〉
		=   { pointwise extension }
		 〈∀ x:: (p ≡ q).x〉 
		=   { (2) with p := (p ≡ q) }
		  [p ≡ q]

Translating Sets

We can start our comparison by translating sets into predicate formulations. We will concentrate on set equality, subset, intersection, union, subtraction and symmetric difference.

	(3)  P = Q  ≡  [p ≡ q]
	(4)  P ⊆ Q  ≡  [p ⇒ q]
	(5)  x ∈ P ∩ Q  ≡  (p ∧ q).x
	(6)  x ∈ P ∪ Q  ≡  (p ∨ q).x
	(7)  x ∈ P \ Q  ≡  (p ∧ ¬q).x
	(8)  x ∈ P △ Q  ≡  (p ≢ q).x

with △ being the symmetric difference, the set of elements that are present in one set and ≢ being the discrepancy, the negation of ≡. We see that the first operators are translated into a form with one logical connector and the everywhere operator. Also, no operator is built uniquely around either of the implication or the equivalence. Therefore, there is not a unique translations of expressions like the following:

	[p ≡ q ≡ r ≡ s]

To allow us to manipulate the above, we introduce a definition for set equality. It can be calculated from our previous postulates.

	(9)  P = Q  ≡ 〈∀ x:: x ∈ P  ≡  x ∈ Q〉

		  [p ≡ q ≡ r ≡ s]
		=   { double negation }
		  [¬¬(p ≡ q ≡ r ≡ s)]
		=   { ¬ over ≡ twice, see (10) below }
		  [¬(p ≡ q) ≡ ¬(r ≡ s)]
		=   { (11) }
		  [p ≢ q ≡ r ≢ s]
		=   { everywhere expansion (2) }
		 〈∀ x:: (p ≢ q ≡ r ≢ s).x〉
		=   { pointwise extension of ≡ }
		 〈∀ x:: (p ≢ q).x ≡ (r ≢ s).x〉
		=   { (8) twice }
		 〈∀ x:: x ∈ P △ Q ≡ x ∈ R △ S〉
		=   { (9) }
		  P △ Q  =  R △ S

	(10)  [¬(p ≡ q) ≡ ¬p ≡ q]
	(11)  [¬(p ≡ q) ≡ p ≢ q]

Of course, for someone used to it, this is a simple conversion and there would be no need to be this explicit but I include it nonetheless for the sake of those who are not used to it.

Our formula is therefore proven to be equivalent to the one below.

	P △ Q  =  R △ S

we could also introduce the negations elsewhere and get:

	P  =  Q △ R △ S

Since equivalence is associative -- that is: ( (p ≡ q) ≡ r ) ≡ ( p ≡ (q ≡ r) )-- and symmetric --that is: (p ≡ q) ≡ (q ≡ p)--, there are a whole lot of other formulae from set theory that are equivalent to the predicate calculus formulae we showed. All those results create many theorems which basically "mean" the same thing but that one may have to remember anyway. As a comparison, our one predicate can be parsed in various ways and we can use it to substitute p ≡ q for r ≡ s or r for p ≡ q ≡ s to name just two usages of a simple formulae.

One could suggest that the problem lies with the usual reluctance of logicians to talk about sets complement, that if we had an operator, say ⊙, to stand for the complement of △ --which can be seen as problematic because it creates a set with elements taken from neither of its operands--, we wouldn't need to introduce spurious negations. The above formula could then be translated in:

	P ⊙ Q  =  R ⊙ S

It remains to choose which equivalence becomes an equality and which ones become the complement of a symmetric difference. I believe the biggest problem to be that set equality mangles two orthogonal notions together: boolean equality and (implicit) universal quantification. The same goes for implication.

In short, this is one example where set theory destroys a beautiful symmetry and introduces spurious distinctions that pollute one's reasoning rather than help it. Whenever I have problems to solve and that calculations can help me, in the vast majority of cases, I use predicate calculus rather than set theory.

Simon Hudon
April 10th, 2011
Meilen

Notes

[0] I use the calculus, not the logic. The difference is that the logic deduces theorems from other theorems whereas the calculus simply helps us create relations between formulae and find new formulae from old ones whether they are theorems or not.

[1] Like many others, I have forsaken the double arrow for that purpose. The choice can be traced back to [DS90] and [AvG90].

References

[AvG90] Antonetta J. M. Gasteren. 1990. On the Shape of
Mathematical Arguments. Springer-Verlag
New York, Inc., New York, NY, USA.

[DS90] Edsger W. Dijkstra and Carel S. Scholten. 1990. Predicate
Calculus and Program Semantics. Springer-Verlag New
York, Inc., New York, NY, USA.

"Lifting weights with your brain"

2011-06-14T14:40:00.003+02:00

I am posting the following just for the sake of sharing a quote I liked in an essay I'm reading:

In workouts a football player may bench press 300 pounds, even though he may never have to exert anything like that much force in the course of a game. Likewise, if your professors try to make you learn stuff that's more advanced than you'll need in a job, it may not just be because they're academics, detached from the real world. They may be trying to make you lift weights with your brain.

By Paul Graham, Undergraduation. I don't suppose it will completely eradicate the comment "What good does it do me to learn [put a beautiful piece of theory, technology, etc here]? People don't use it." Another reply of course might be to point out that "maybe they should".

Simon Hudon
June 14th, 2011
Meilen

Decidability

2011-06-06T12:49:00.002+02:00

The proof of the undecidability of the halting problem has always fascinated me. It is a formidable result to behold, at least the first time around. It relies on the construction of a program that cannot exist because of a contradiction drawn through self-reference. Here is an interesting rendering of the argument by Christopher Strachey: An Impossible Program.

However, an interesting paper written by Eric Hehner (Problems with the Halting Problem) sheds doubt on the correctness of the usual proof. He proposes that the contradiction in the proof is due to self reference rather than because of the structure of the halting problem. It is a good read and I strongly recommend it.

Simon Hudon
Meilen
June 6th 2011

A Lecture Supported by an Automated Theorem Prover

2011-05-09T17:29:00.013+02:00

UPDATED: added note [1] on mutual implication

Last week on monday, I attended the guest lecture that Prof. Topias Nipkow from the Technical University of Munich (TUM) gave at ETH. I had heard of him before because of his work on the Isabelle theorem prover. An interesting thing before I start: he refers to it as a proof assistant.

I didn't expect much of this talk because of my reluctance to rely on automatic provers to do my job and because I expected a very technical talk about proof strategies implemented or to be implemented in Isabelle. Since such issues need concern only people involved in the construction of theorem provers and that I'm not, I didn't think it would appeal to me.

I was pleasantly surprised that he had chosen to talk about a course he had recently started to give on the topic of semantics. Said course was noteworthy because formal methods and an automated prover were used as teaching vehicles. I am pleased to see that he decided to use formal methods as a tool for understanding the topic and that he would opt for spending more time on semantics, the subject matter, and less on logic and formal methods.

It is my considered opinion, however, that a prerequisite course on the design of formal proofs would be most useful, even necessary. I draw this conclusion because I believe that acquiring effective techniques for designing elegant proofs can help tremendously in making hard problems easier. But, since he didn't want to teach logic, he gave very little attention to the design of proofs and adopted "validity of the proofs" as the goal the students' had to reach in their assignments. It was asked --by someone else before I could ask it-- what importance he gave to the style of the submitted proofs. He said none because some (in his opinion) very good students had an awful style and he didn't want to penalize them for it. He considered that, having submitted a correct proof, the student had shown that he understood. I would say that, in doing so, he was doing his students a disservice. However, I can now better understand his position because the underlying assumption is very popular: since words like style and elegance have a very strong esthetic connotation, it becomes automatically whimsical to judge them or to encourage the students to improve upon them. After all, we're here to do science, not to make dresses!

* *
*

Even when it has been successfully argued just how useful mathematical elegance can be, people keep opposing its use as a yardstick on the ground that it is too subjective and enforcing one standard would be arbitrary.

It turns out that, not only are elegance and style very useful, but they can be very objectively analyzed and criticized. It has been the preferred subject of Dijkstra in the second part of his career and it appears almost everywhere in his writing --see EWD619 Essays on the nature and role of mathematical elegance for such an exposition [0]--.

The usefulness of an elegant style come from the fact that it yields simple and clear proofs requiring very little mental work from the reader (which is not something to be underestimated) but, more importantly, it allows the writer of a proof to be economical in the use of his reasoning abilities. This can make the difference between a problem which is impossible to solve and one which is easily solved. On the other hand, in such a course as what Nipkow has designed, the most interesting things for students to learn are not the individual theorems that they proved but the techniques that they used to find a proof. If the techniques are not taught, it can be expected that the skills the students acquire will be of much less use when confronted to different problems.

What an elegant style boils down to is, to put it in Dijkstra's words, the avoidance complexity generators and the separation of one's concerns. He also argued that concision is an effective yardstick to evaluate the application of those techniques. Indeed, concision is effectively achieved by both separating one's concerns and avoiding complexity generators. The most well known complexity generators are case analyses, proofs of logical equivalence by mutual implication and inappropriate naming. The first two are legitimate proof techniques but their application double the burden of the proof. It doesn't mean that they should never be used but rather that they should be avoided unless the proofs of the many required lemmata differ significantly. [1] I say significantly to stress that, in some cases, they can differ in small ways and, upon closer scrutiny, the differences can be abstracted from.

The issue of naming is also closely related to the separation of one's concerns but, being a tricky issue, I would rather point the reader in the direction of van Gasteren's book "On the Shape of Mathematical Arguments" to the chapter 15 "On Naming" which covers the subject very nicely. Since Dijkstra was van Gasteren's supervisor, he wrote the chapter with her and it has earned it an EWD number: 958 [0]. This allows me to skip directly to the matter of separation of concerns.

* *
*

While debating about concision and about Nipkow's lecture with my supervisor, something kept coming up in his arguments. I was favoring short formal proofs and he kept asking: "What if a student doesn't want to call 'auto' [the function of Isabelle which can take care of the details of a proof step] but wants to go into the details to understand them?" First of all, I have to point out that being the input for an automated tool doesn't relieve a proof from the obligation of being clear. [2] Unlike Nipkow, I see that the proof must include intermediate formulae accompanied with a hint of how one proceeds to find them. This would correspond to the combination of what he calls a proof script --a series of hint without intermediate formulae-- and a structured proof --a series of intermediate formulae with little to no hints; this is what he prefers to use--. In that respect, 'auto' is no better than the hint "trivially, one sees ...". The choice of how early one uses 'auto' is basically related to decomposition. It is unrelated to the peculiarities of the prover but relies on how clear (to a human reader) and concise the proof is without the details. What my supervisor and Nipkow name "using auto later in the proof" would be, in a language independent of the use of an automated prover, including more details. If the proof is clear and concise without those details, they don't belong in the body of the proof. It is that simple. One could, however, include them in the proof of a lemma invoked in one (or many) proof steps of the main proof.

By Including a lemma, one doesn't destroy concision because the proof of said lemma can be included beside that of the main theorem rather than intertwined with it. The difference is that, while one reads a proof, each step must clearly take him closer to the goal. Any digression should be postponed so as not to distract the attention from the goal. One good indication that a lemma is needed is when many steps of a proof are concerned with a different subject than the goal. For instance, when proving a theorem in parsing theory, if many successive steps are concerned with predicate calculus, the attention is taken away from parsing. Instead, making the whole predicate calculation in one step and labeling it "predicate calculus" is very judicious. Nothing prevents the proof that pertains to predicate calculus to be presented later on, especially if it is not an easy proof.

The important point here is that, sticking to the subject at hand doesn't mean forgetting that there are other problems that need one's attention. It means dealing with one problem at a time each time forgetting momentarily what the other problems are. This is exactly what modularity is about.

Furthermore, with an automatic prover, nothing prevent someone to use 'auto' to commit the sin of omission; details that would make a step clear are then missing. It is then a matter of style to judge how much should be added. This reinforces my point that good style should be taught because clarity is the primary goal with proofs [3].

With respect to such a tool, I would welcome the sight of one where keywords like 'auto' are replaced by catchwords like 'predicate calculus' to hint at the existence of a simple proof --at most five steps-- in predicate calculus --in this case-- that supports the designated step. More often, we could use invocations like 'theorem 7' (or '(7)' for short) or 'persistence rule' as a way of invoking a very straightforward application of a referenced theorem. It is clear to the reader what is going on then and to the prover, the problem is very simple: it looks for a simple proof. If no proofs of at most five steps exist, the search fails. More importantly: the user should have foreseen it. The prover should never be used to sweep problems under the carpet.

Like with the type system of a programming language, it should be easy for the human reader to see that a given proof step is going to be accepted. It is by being predictable that automatic tools are useful, not by working magic.

* *
*

By way of conclusion, I go on to another aspects of Nipkow's talk. He said that applying formal proofs to the teaching of computer science is especially useful in those subjects where the formalization is close to people's "intuition". In the rest of the subjects, it is a bad idea. I say this is a drawback of his approach, not one of formal proofs. If you take formal proofs as a proper input format for the mechanized treatment of intuitive arguments, it seems inevitable to run into that problem. However, formalism can be used for purposes which have nothing to do with mechanization: the purposes of expressing and understanding precise and general statements. If it is used in this capacity, formalism allows a (human) reasoner to take shortcuts which have no counterpart in intuitive arguments. It is one of the strengths of the properly designed formalisms that you can use them to attain results which is beyond intuitive reasoning.

Case in point, the topics where Nipkow says formal proofs are not an appropriate vehicle for teaching are those where it would be crucial to rely on formalisms that are not merely the translation of intuitive reasoning. To use those, we would have to stop relying on our intuition and acquire the techniques of effective formal reasoning. This leads me back to my first point. 'Effective' means that we're not interested in finding just about any proof: we are looking for a simple and elegant one so that problems for which the solution would be beyond our abilities could admit a simple solution.

In other words, striving for simplicity is not a purist's concern as much as a pragmatic preoccupation that allows us to solve with as little efforts as possible problems that are beyond the unaided minds.

Simon Hudon
ETH Zurich
Mai 11th 2011

[0] For the EWD texts, see http://www.cs.utexas.edu/users/EWD/

[1] For those who are used to using deductive systems for formal reasoning, the question "what alternative do we have to mutual implication?" might have come up. The answer is that equivalence is a special case of equality and should be treated as such. That is to say that its most straightforward use is by "substituting equals for equals" also known as "Leibniz's rule". It is also the most straightforward way to prove an equivalence. The naming of equivalence by "bidirectional implication" is a horrible deformation. It is analogous to calling equality in numbers "bidirectional inequality": it hints at a way of proving it using implication but does not distinguishes between this shape of one possible proof and the theorem and, indeed, I realize that some people immediately think of mutual implication when they see an equivalence. It's a shame.

[2] In this respect, theorem provers seem to be more primitive than our modern programming languages. Whereas they become more and more independent of their implementation to embody abstractions (for instance, in Java, there no longer is a "register" keyword for variables), the proof languages of automated provers shamelessly include a lot of specific command for what I shall call "sweeping the rest of the problem under the rug". In proofs explicitly constructed for human readers, those would be replaced by vague expressions like "well you know..." followed, if presented in a talk, by a waving of the hands intended to say "anyone but idiots will get this".

[3] This goes against what seems like a school of thought that views formal proofs as the input of tools like theorem provers. It is easy for people of that school to draw the fallacious analogy with assembler programming. The important difference is that a proof designed with style can be the vehicle of one's understanding. Since mechanisms like abstraction are routinely applied to make proofs as simple as they can be, if one wants to understand an obscure and counter intuitive theorem, an elegant formal proof is very likely to be the best way to do it. On the other hand, assembler is not a language which helps one understand an algorithm. It is clearly an input format of a microprocessor and people should treat it as such.

Special thanks to my brother Francois for applying his surgical intellect to the dissection of the objections made against the notions of elegance and style and to Olivier who also help me improve this text.

Done in One Step

2011-03-23T18:19:00.005+01:00

This is a short note to relate an anecdote that just happened to me. I'm learning Rutger M. Dijkstra's computation calculus by reading his paper with the same name and I come across a very short proof.

The objects of the calculus are computations taken as predicates over state traces. The result looks like a relational calculus in that in never names the computations it is dealing with. It adds • ; ~ to the usual predicate calculus. • takes a state predicate `p', this is a predicate over traces that is satisfied only by traces of one state, and makes it a predicate satisfied by traces starting with a state satisfying `p'. It is captured by definition (13).

(13)	•p = p;true

where ; is the sequential composition of computation. `a;b' can be interpreted as constructing a computation satisfied by traces produced by executing `a' first then `b'. For the proof, all we need is the state restriction property. It applies to state predicate `p' and arbitrary computation `s'.

(8)	p;s  =  p;true  ∧  s

Finally, ~ is a negation of a state predicate that also yields a state predicates. That is to say that computations form a predicate algebra and so do state predicates, using ~ instead of ¬. And now, here is the proof. Don't spend to much time reading it, the second step is far from obvious.

	  [ •~p ⇒ ¬•p ]
	=   { Shunting, definition (13) (see below) }
	  [ p;true ∧ ~p;true  ⇒  false ]
	=   { state restriction (8) thrice }
	  [ (p ∧ ~p);true  ⇒  false ]
	=   { Predicate calculus }
	  [ false;true  ⇒  false ]
	=   { false is left zero of ; }
	  true

I decided to see for myself how the second step works and my calculation took five steps instead of one. After struggling with it for a minute or so in my head, I decided to make appeals to associativity explicit in order to consider it as a manipulation opportunity. One last thing: the weaker state predicate is 1, it plays the role of true in the related predicate algebra and we can express that any predicate `p' is a state predicate by making it stronger than 1: [ p ⇒ 1 ]. In my calculation, ~ doesn't pay a role so I replace `~p' by `q'. Therefore, we are trying to transform p;true ∧ q;true into (p ∧ q);true using equality preserving steps.

	  p;true ∧ q;true
	=   { (8) using p is a state predicate }
	  p;(q;true)
	=   { At this point, all other application 
	      of (8) would take us back a step or
	      would lead nowhere, let's use 
	      associativity }
	  (p;q);true
	=   { Now we can recognize the left hand 
	      side of (8) so we apply it using that p
	      is a state predicate again }
	  (p;true ∧ q);true
	=   { We can now take advantage of the
	      fact that q is a state predicate for the
	      first time with [ q ⇒ 1 ] or, rather
	      [ q  ≡  q ∧ 1 ] }
	  (p;true ∧ 1 ∧ q);true
	=   { Now p;true ∧ 1 matches the right
	      hand side of (8) and we can use it
	      to eliminate true and we can 
	      eliminate 1 because it is the identity
	      of ; }
	  (p ∧ q);true

There are mostly two things that helped design the above computation.

We kept track of the properties of that were left unused through the calculation. It especially help to move forward
Realizing that some intermediate formulae would contain a series of consecutive ; and that we might get to manipulate different groupings lead us to make the appeals to associativity explicit and made apparent the best way to use (8) for the second time.

Although I'm happy to use the opportunity to practice various techniques for designing formal proofs, the writing of the above was prompted by a (mild) dissatisfaction at Dijkstra's proof for leaving out most of the helpful and relevant bits.

Simon Hudon
March 23rd, 2011
ETH Zurich

Calculating with Partitions

2011-03-09T14:58:00.004+01:00

In the book of Chandy & Misra [CM88], I found an interesting consequence of three variables of which exactly one is true. To begin with, such a relation can be formalized as follows:

(0)	[ x ∨ y ∨ z ]
(1)	[ ¬(x ∧ y) ]
(2)	[ ¬(x ∧ z) ]
(3)	[ ¬(y ∧ z) ]

Note

Before proceeding with the interesting fact, let's have a closer look at the square brackets. They come from the book of Dijkstra & Scholten and they constitute a form of implicit universal quantification. If x, y and z are normal boolean variables, it can be omitted. However if they are predicates ([DS90] introduces them as boolean structures), you can leave out their arguments and it is considered that they are universally quantified over. In such a case,

	[ x ∨ y ∨ z ]

would be equivalent to

	〈∀ i:: (x ∨ y ∨ z).i〉

and predicate application is considered to distribute over the logical connectives so it is, in turn equivalent to

	〈∀ i:: x.i ∨ y.i ∨ z.i〉

Since i doesn't play a role in our manipulations, it simplifies the formula and our work to leave it out.

This means that, if x, y and z are the characteristic predicate of sets X, Y, Z, our set of constraint states that they partition the type over which they range.

(end of note)

Now the interesting consequence is this one:

(4)	[ ¬x  ≡  y ∨ z ]

Its proof is nice and simple. The usual heuristics to design a proof of such a theorem is either to manipulate the whole formula or to transform one side into the other. Since we don't have rules to relate either of y or z to ¬x, we choose to manipulate the whole formula. Also, we need to join ¬x and y ∨ z with either a disjunction or a conjunction because of the shape of the rules that we have. The golden rule, stated below, is a good candidate to achieve just that.

(5)	[ x ∨ y ≡ x ≡ y ≡ x ∧ y ]	("Golden rule")

For those unfamiliar with the rule, they can convince themselves of the validity or the rule by seeing that x ⇒ y can be equivalently formulated as follows:

	x  ≡  x ∧ y
	x ∨ y  ≡  y

By transitivity, they are equivalent. Hence, the golden rule. Now for the proof of (4):

	  ¬x  ≡  y ∨ z
	=   { ¬ over ≡ to get ¬ out of the way }
	  ¬(x  ≡  y ∨ z)
	=   { Golden rule }
	  ¬(x ∧ (y ∨ z)  ≡  x ∨ y ∨ z)
	=   { (0) }
	  ¬(x ∧ (y ∨ z))
	=   { ∧ over ∨.  It acheives the
	      grouping of (1) to (3) }
	  ¬( (x ∧ y) ∨ (x ∧ z) )
	=   { ¬ over ∨ }
	  ¬(x ∧ y) ∧ ¬(x ∧ z)
	=   { (1) and (2) }
	  true

This simple proof is six step and it carries an inactive negation around needlessly. We could remove one step and the noise of the negation if we simply realize that

	¬(x  ≡  y)  ≡  x  ≢  y

Also, we can use the golden rule over ≢ if we realize that replacing an even number of ≡ by ≢ in a sequence of equivalences leaves the truth value unchanged.

	  x  ≢  y ∨ z
	=   { Golden rule }
	  x ∧ (y ∨ z)  ≢  x ∨ y ∨ z
	=   { (0) }
	  ¬(x ∧ (y ∨ z))
	=   { ∧ over ∨ }
	  ¬((x ∧ y) ∨ (x ∧ z))
	=   { ¬ over ∨ }
	  ¬(x ∧ y) ∧ ¬(x ∧ z)
	=   { (1) and (2) }
	  true

It is nicer this way: the proof is shorter and ¬ is inactive only for one step. We can suppose that it can be generalized to more variables. Indeed, (0) to (3) can be generalized by (6) and (7) and we can replace x, y, z by x.i for any appropriate i.

(6) [〈∃ i:: x.i〉 ]
(7) [〈∀ i,j: i ≠ j: ¬(x.i ∧ x.j)〉 ]

A first attempt at generalizing (4) might yield

(4')	[ x.j  ≢ 〈∃ i: i ≠ j: x.i〉 ]

but we can do better. We don't need to only have on variable on the left hand side of ≢, we could have many, like on the right hand side. The important thing is that variables appear on exactly one side. To formalize this, we can use an arbitrary separating predicate P. The x.i such that P.i holds will be on the left and the others will be on the right.

(4'')	[〈∃ i: P.i: x.i〉 ≢〈∃ i: ¬P.i: x.i〉 ]

Notice how nicely symmetric (4'') is. The same technique can be used to prove it as what we used for (4).

	 〈∃ i: P.i: x.i〉 ≢〈∃ i: ¬P.i: x.i〉 
	=   { Golden rule }
	   〈∃ i: P.i: x.i〉 ∧〈∃ i: ¬P.i: x.i〉 
	  ≢〈∃ i: P.i: x.i〉 ∨〈∃ i: ¬P.i: x.i〉 
	=   { ∧ over ∃ and nesting; merge ranges }
	 〈∃ i,j: P.i ∧ ¬P.j: x.i ∧ x.j〉 ≢〈∃ i:: x.i〉 
	=   { (6) }
	  ¬〈∃ i,j: P.i ∧ ¬P.j: x.i ∧ x.j〉 
	=   { ¬ over ∃ }
	 〈∀ i,j: P.i ∧ ¬P.j: ¬(x.i ∧ x.j)〉 
	⇐  { P.i ∧ ¬P.j ⇒ P.i ≠ P.j and the 
	      contrapositive of Leibniz's
	      principle applies }
	 〈∀ i,j: i ≠ j: ¬(x.i ∧ x.j)〉 
	=   { (7) }
	  true

Our next investigation is whether or not (4'') is sufficient to characterize the kind of partition defined by (6) and (7). To do so, we prove that (4'') ≡ (6) ∧ (7). Mutual implication is an intesting choice of strategy since half of the work is already done and we only have a weaker proof obligation to take care of. We can prove (6) and (7) separately under the assumption of (4'')

Proof of (6)

	 〈∃ i:: x.i〉 
	≠   { (4'') with P.i ≡ true }
	 〈∃ i: false: x.i〉 
	=   { Empty range }
	  false

For the proof of (7), we have to notice the formal differences between (7) and one of the sides of (4''). First of all, (7) has more dummies and has a universal quantification instead of an existential one. Second, the term of the quantification has two (negated) occurrences of x rather than just one positive one. What we must do is split the dummies between two quantifications --nesting should do nicely--, then move the second x term out of the inner quantification and use one of the negations to change the ∀ into ∃. The formula should then be amenable to an application of (4'').

Proof of (7)

	 〈∀ i,j: i ≠ j: ¬(x.i ∧ x.j)〉 
	=   { Nesting to separate the dummies }
	 〈∀ i::〈∀ j: i ≠ j: ¬(x.i ∧ x.j)〉 〉 
	=   { ¬ over ∧ then ∨ over ∀ to keep only one
	      x term inside the inner quantification }
	 〈∀ i::〈∀ j: i ≠ j: ¬x.j〉  ∨ ¬x.i〉  
	=   { ¬ over ∃ }
	 〈∀ i:: ¬〈∃ j: i ≠ j: x.j〉  ∨ ¬x.i〉  
	=   { Now we have the shape we were looking for
	      we can use (4'') with P.i  ≡  i = j }
	 〈∀ i::〈∃ j: i = j: x.j〉  ∨ ¬x.i〉  
	=   { One point rule }
	 〈∀ i:: x.i ∨ ¬x.i〉  
	=   { Excluded middle and identity of ∀ }
	  true

Luckily enough, after the application of (4''), the steps are of the kind "there is only one thing to do". Without context, the rest of the proof could look like a giant rabbit but, since (4'') is the main part of the rules that we can apply, it is reasonable to expect that we should create an opportunity to apply it and each step before its application bridges the formal difference between the two.

The above proof has been presented as a nice example that an elegant proof can be designed using only the properties of the formulae rather than their interpretation and to present some more advanced heuristics to do so.

The investigation has been prompted by my delight at seeing how nicely the first parts of the problem were solved using the golden rule but the decision to show the proof was taken because of my surprise at how easily the last proof came to me with a simple analysis of the formal differences between the two main formulae although I had expected it to keep me busy for a long time.

Simon Hudon
March 8th, 2011
Meilen

References

[CM88] K. Mani Chandy and Jayadev Misra, Parallel Program Design:
A Foundation, Addison-Wesley, 1988

[DS90] Edsger W. Dijkstra and Carel S. Scholten, Predicate Calculus
and Program Semantics, Texts and Monograph in Computer
Science, Springer Verlag New York Inc., 1990

On the Notion of Ghost Variables

2010-11-09T11:29:00.007+01:00

When one reads the literature of formal methods, especially that of formal verification, one encounters the notion of ghost variable also called model variable. In short, they are variables added to a program for the sake of verification to express simply and concisely what is the data abstraction a certain module is supposed to be implemented. They reflect very well the a posteriori nature of verification because they add the variables to a presumably existing program. They are characteristically absent from the regular data flow and control flow and, as such, their values need not be stored during the execution of the program. They are mere abstractions.

The naming seems to come from the fact that the predominant role the verification community gives to a program variable is to be an abstraction for the storage of a category of important values. A variable for which the values need not be stored then feels kind of odd: it looks like a variable but it's not really one. Hence the special attribute is added to warn anyone reading the program that this is a strange sort of variables.

We can take a different view with respect to variables though. If we try to understand a problem to then create a program to solve it and a compelling argument for trusting the results of the latter, we need a way to speak of the problem. Namely, it is important to identify the central abstractions, the objects of central importance and give them a name so that their properties of interest can be spelled out using that name rather than mainly in terms of their relation to other objects. One such example is given by:

Jim and Julia's brother play football together. During one match, Jim tackled Julia's brother and hurt him badly.

Compare it to:

Jack and Julia are siblings. Jim and Jack play football together. During one match, Jim tackled Jack and hurt him badly.

Notice how disentangled the second version of the story is. Every sentence states a fact and, if we are interested in the accident, we realize that Julia has very little role to play in it and the first sentence can be ignored altogether without missing any information. In the first version of the story, Julia and her relationship to one of the players is dragged all through the story although, as far as we can see, she plays no role in it herself. More about the issue of naming in mathematical arguments (which is relevant in software design) can be found in [0], in chapter 15 which is dedicated to the subject.

The point I am coming at with all this rambling on naming is that, during the analysis of a programming problem and the design of a solution, the introduction of variables should be seen as the introduction of names for the relevant quantities. The fact that the binary representation of the exact set of variables introduced should not be of immediate concern. A confidence that an efficient representation can be found later on is healthy but anymore thoughts about them should be postponed. What Dijkstra calls a change of coordinates in [1] can be applied later to improve efficiency. In the mean time, the prime concern is to establish sufficient conditions for an implementation to be correct. It is also possible that the set of variables chosen during the design process don't have to be transformed in order to get an efficient implementation and, again, it is of no concern while we come up with them.

When I say those problems are of no concern, it means we should concentrate on them but also, we should not let the vocabulary that we use reflect a distinction that we are not ready to make. For that purpose, I would abandon the notion of model or ghost variables or, at least, downplay there role considerably and introduce the notion of stored variables. Those are the variables of the final implementation for which the value has an impact over the control flow and the data flow directed to the output variables. By symmetry, we can call the others model or ghost variables but, since we reduce their importance to the final implementation stage and that, even there, they are the ones to be left out rather than kept, omitting to name them would not be a big methodological impediment.

Regards, Simon Hudon ETH Zürich Tuesday the 9th of November 2010

References

[0] On the Shape of Mathematical Arguments, A.J.M. van Gasteren [1] EWD1032 - Decomposing an Integer in a Sum of two Squares, E.W. Dijkstra, available at here

The Segment of Maximum Sum

2010-10-18T00:02:00.012+02:00

This is the recording of a solution found together with Bernhard Brodowsky where he did most of the work in one of the first lectures where I explained the techniques to him. The problem is to find a segment of an array for which the sum of the elements is maximal. We stopped when we had a simple specification of the body of the loop for fear that actually calculating the assignments would be too much tedium. In this recording, I will calculate them to see exactly how tedious it is. Also, we did not pay any mind to calculating too many auxiliary values --that is using them before updating the variable holding it in the loop body so that one is always thrown away--. In this recording, the solution will be changed slightly to avoid that.

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

 P0: r = 〈↑ p, q: 0 ≤ p ≤ q ≤ N: 〈∑ i: p ≤ i < q: X.i〉〉

where ↑ denotes the maximum of two operands. Like the conjunction and the disjunction, it is idempotent, associative and symmetric so we can use it in the same was as the universal and existential quantification. The first thing to do is to introduce a name for the summation part so that we can manipulate it independently of the overall specification.

 (0) S.p.q = 〈∑ i: p ≤ i < q: X.i〉

And the specification becomes:

 P1: r = 〈↑ p, q: 0 ≤ p ≤ q ≤ N: S.p.q〉

The traditional way to get an invariant from this is to replace N by a variable, let's call it n, and use n = N as an exit condition:

 J0: r = 〈↑ p, q: 0 ≤ p ≤ q ≤ n: S.p.q〉 
 C0: n = N

By symmetry, we can assume that 0 is a proper initial value for n which makes S.0.0 a good one for r.

 I0: n = 0
 I1: r = 0

Last formality: having n increase by one at each iteration will guarantee termination provided 0 ≤ N.

 S0: n' = n + 1

Let's now start calculating with J0 to see what adjustments we have to make to r to preserve it. Two distinct heuristics get us to start calculating with the right-hand side of the equality: it is much more complicated than the left-hand side so we can assume that most of our moves will be eliminations and all the program variable involved in the right-hand side don't have a matching assignment so we would basically be stuck right at the start. For a given loop with invariant J and body S, the invariance of J is assured by:

 J'  ⇐  J ∧ S

where J' is J with all its program variables primed. It means we can use whatever is part of the body or the invariant to prove J's invariance, to do so, we can invent new statements for the body as we go.

    〈↑ p, q: 0 ≤ p ≤ q ≤ n': S.p.q〉 
  =   { S0 }
    〈↑ p, q: 0 ≤ p ≤ q ≤ n+1: S.p.q〉 
  =   { Split range }
      〈↑ p, q: 0 ≤ p ≤ q ≤ n: S.p.q〉
    ↑ 〈↑ p: 0 ≤ p ≤ n+1: S.p.(n+1)〉 
  =   { Use final value of a new variable using
         Q0: s' = 〈↑ p: 0 ≤ p ≤ n+1: S.p.(n+1)〉 and J0 }
    r ↑ s'
  =   { New statement: S1: r' = r ↑ s' to conclude
         the proof of J0's invariance }
    r'

 Q0: s' = 〈↑ p: 0 ≤ p ≤ n+1: S.p.(n+1)〉
 S1: r' = r ↑ s'

Q0 links unprimed variables with primed variables in a way that cannot be evaluated. Let's turn it into an invariant to fix this.

    〈↑ p: 0 ≤ p ≤ n+1: S.p.(n+1)〉
  =   { S0 }
    〈↑ p: 0 ≤ p ≤ n': S.p.n'〉
  =   { J1' }
    s'

where

 J1: s = 〈↑ p: 0 ≤ p ≤ n: S.p.n〉

We now have to make sure that J1 is also invariant and use the same heuristic as for J0 to do so.

    〈↑ p: 0 ≤ p ≤ n': S.p.n'〉
  =   { S0 and split }
    〈↑ p: 0 ≤ p ≤ n: S.p.(n+1)〉↑ S.(n+1).(n+1)
  =   { (1), see below ; S.n.n = 0 }
    〈↑ p: 0 ≤ p ≤ n: S.p.n + X.n〉↑ 0
  =   { + over ↑ }
    (〈↑ p: 0 ≤ p ≤ n: S.p.n〉+  X.n) ↑ 0
  =   { J1 }
    (s + X.n) ↑ 0
  =   { New statement: S2: s' = (s + X.n) ↑ 0 }
    s'

 S2: s' = (s + X.n) ↑ 0

 (1) S.p.(n+1) = S.p.n + X.n   ⇐   p ≤ n

(1) is a theorem that we calculated because we had a term S.p.(n+1) that we needed to replace by one formulated in terms of S.p.n to make it possible to use J1 to eliminate the quantified maximum. Proof of (1):

    S.p.(n+1)
  =   { (0) }
    〈∑ i: p ≤ i < n+1: X.i〉
  =   { Split range using p ≤ n }
    〈∑ i: p ≤ i < n: X.i〉+  X.n
  =   { (0) }
    S.p.n + X.n

end of proof All that is missing now to have a complete program is to add an initialization for s. An examination of J1 tells us that for n = 0, S.0.0 is an appropriate value for s. We now get:

   n = 0 ∧ r = 0 ∧ s = 0
 ; while n ≠ N do
    n' = n+1  ∧  r' = r↑s'  ∧  s' = (s + X.n) ↑ 0
   od

This would be a simple enough program to execute except for S1 which has primed variables on both side of the equality. Let's see if we can find a sequence of assignments (rather than a conjunction of equalities) that will do the same as S0 ∧ S1 ∧ S2. The main law that we use for calculating assignments is

 (2) s := E ; P  ≡  P [s \ E]

where P [s \ E] is the same as P except for the occurrences of s which are replaced by E. The way in which we will make assignments appear is by replacing terms of the initial specification by specifications of the form x' = x so that we can eventually replace the whole boolean specification by a skip and keep only the assignments.

    n' = n+1  ∧  r' = r↑s'  ∧  s' = (s + X.n) ↑ 0
  =   { Let's deal with s' to introduce s' = s 
         and solve the assignment to r }
      s := (s + X.n) ↑ 0  
    ; (n' = n+1 ∧ r' = r↑s' ∧ s' = s)
  =   { Leibniz }
      s := (s + X.n) ↑ 0
    ; (n' = n+1 ∧ r' = r↑s ∧ s' = s)
  =   { Assignment (either of r or n will do.  Let's pick
         them in inverse order of introduction }
      s := (s + X.n) ↑ 0  
    ; r := r↑s  
    ; (n' = n+1 ∧ r' = r ∧ s' = s)
  =   { One last time, assignment }
      s := (s + X.n) ↑ 0  
    ; r := r↑s  
    ; n := n+1  
    ; (n' = n ∧ r' = r ∧ s' = s)
  ⇐   { Introduce skip }
      s := (s + X.n) ↑ 0  
    ; r := r↑s  
    ; n := n+1  
    ; skip
  =   { Identity of ; }
      s := (s + X.n) ↑ 0  
    ; r := r↑s  
    ; n := n+1

It is a bit disappointing to see that the order between the assignment to r and that to n is irrelevant and we could have used a multiple simultaneous assignment for them but, then, we would have noticed that the choice of grouping n with r or grouping it with s is also irrelevant. One way or another, an irrelevant choice has to be made. By interpreting the initialization in a similar way, we get the following program:

   n, r, s := 0, 0, 0
   { invariant J0 ∧ J1 }
 ; while n ≠ N do
      s := (s + X.n) ↑ 0
    ; r := r ↑ s
    ; n := n + 1
   od

Modularity in Design versus Modularity in Code

2010-08-30T11:17:00.013+02:00

At the moment, the widespread use of libraries is characterized by the reuse of code in various contexts outside the one which gave it birth. It has been made much easier by the development of .NET --which I salute as being a great technical achievement-- because .NET allows the combination of code written in different languages. I believe it is a stepping stone with respect to exposing programming languages as reasoning aids rather than execution models and it is only hampered by Microsoft's lack of commitment towards portability.

However, I suggest that, although it is an important step, it is not satisfactory as far as the concern for reuse goes. I propose that we start thinking of the reuse of the thoughts behind the code and that they are the things of foremost importance. It does not mean that reusing code is not important -- assuming we preserve the documentation of its interfaces-- but it does not go far enough. Indeed, in code, all the different ideas justifying the design choices are mangled together and one can hardly look at each aspect in isolation. In the community of programming languages, several attempts have been made to provide better modules but, so far, we still see a lot of code where different concerns end up intertwined with one another and I expect it will remain the case.

I think that a good modularity cannot be achieved in (what is understood today as) a programming language because of the universal assumption that the code a programmer types has to be directly (through compilation) executable.

My favorite example comes from parallel programming. In the field of programming language design, many mechanisms have been proposed to make the task of parallel programming easier. It includes semaphores, monitors and message passing. They make it easier to avoid low level design errors like race conditions but they still don't address design issues. In each case, the code is still organized in processes; since the behavior of a parallel program is really a property of the combination of the processes, a change to said behavior requires a change of many modules when the modular boundaries are drawn around processes.

Aside: I consider threads to be a special kind of processes and I don't think that, at the design level, differentiating between the two is of any help at all. I will therefore not mention threads again. (end of aside)

As a comparison, UNITY ([CM88]) uses action systems as the basic unit of composition. An action system has some local variables and can share variables with its environment. It also has a set of atomic actions that can modify the variables. The important thing is that it is possible to make assumptions about how the data is going to be manipulated, to enforce the assumptions and to use them to prove some safety and progress properties. When someone wants to change the functionality of a program, either he can add a new module built around the new properties or he can add the properties to an existing module, if it is close enough to what the module was built for. The key here is to see that programs properties (specifically safety and progress properties) are closely mapped to modules so we have a very good encapsulation.

At the end of a development, a UNITY system consists of a set of actions and a set of variables both partitioned between modules. If someone wants to execute the system, he needs first to choose the platform on which he wants to execute it (e.g. it could be a network of computers or a network of processes residing on one computer) and then partition the various variables and actions of the system between the components of the platform without consideration for the modular boundaries. Some variables might become channels between processes or between computers, others may be stored in the memory of a computer, private to one process or shared and possibly protected by locks.

In sequential programming, the control flow is something that can be closely tied to program properties and it can therefore be safely attributed to a modular unit --such as a procedure-- because the properties of interest --preconditions, postconditions and termination-- closely apply to syntactic structures describing the control flow. That is to say that pre- and postconditions are paired and, between them lies a sequence of statement which are structured in a proper fashion for proving correctness. Similarly, loops are associated with invariants and variants and nothing outside of the loop is relevant for reasoning about said loop.

In contrast, [FvG99] shows the kind of proof obligation one has to contend with when working with processes in parallel programming. In their theory, each assertion has local correctness, which is analogous to partial correctness in sequential programming, and a global correctness which relies on the structure of the other processes. At this point, it is unthinkable to take one process away and to expect that the properties one has proven about it will hold in a different environment. In short, the interface between processes, when made explicit, is too far from a thin interface to allow processes to properly encapsulate anything.

In UNITY, the fact that it is based on action systems rather than processes makes it possible to attribute a precise and small set of properties to a module and work in isolation on it. The usual process is called refinement and it makes all the intermediate design decisions explicit. It makes the effort spent on the development easier to transpose to different situation even when none of the code produced is actually useful.

The UNITY method has proof rules and formal semantics and the most rigorous approaches will take advantage of them. However, it is not necessary to use the whole battery to reap the benefits of the method. Since modularity is something they did well with UNITY, using it and its temporal logic as a guideline for design can already be beneficial in pointing out what we must be careful about.

In short, I believe that it is a property of paramount importance for modular boundaries to confine each programming task to the construction or modification of only one module. The best possible way to achieve that is to choose a unit of modularity for which the proofs of correctness need only rely on very few, simple and chosen a priori --that is, chosen as much as possible independently of any implementation-- assumptions of the surrounding environment. Some might say that it is an obvious goal but as far as I can see, very few modular decomposition mechanisms are satisfactory in that respect and I think that most language designers are still confined by "how the program is going to be executed" so are unable to meet my criteria.

* *
*

I know of another effort directed at the reuse of design: the so-called design patterns. The idea is a good one but its realization is much too weak. They are basically pattens of modular decomposition which have proved useful in many situations. However, there is no basis to state precisely what properties make them useful or how they meet those properties. In short, they cannot have an existence of their own because no notion of correctness apply to them. I do recognize it as a step in the right direction but it seems over-hyped for what it provides. I would welcome the publication of such books where designs are proven correct, where it is (formally) precise where the modules fit in a larger design and how one should proceed to code them correctly.

Next, I would have like to address some of the objections to formal methods that I have heard again and again and that used to unsettle me. However, this post is already pretty long and, by now, it is long overdue. I will, therefore, leave it for a post which, hopefully, will be coming soon.

Simon Hudon
April 10th, 2011
Meilen

References

[CM88] K.M. Chandy and J. Misra, Parallel Program Design:
A Foundation, Addison-Wesley, 1988

[FvG99] W.H.J. Feijen, A.J.M. van Gasteren, On a Method of
Multiprogramming, Springer-Verlag New York, Inc.,
1999

The Development of a Solution to the Problem of the Cubes

2010-08-05T15:11:00.002+02:00

Note:
Before I begin, let me point out that the publication of this blog entry is made possible because I haven't used Blogger's interface to edit it (or at least, I used it as little as possible). Instead, I wrote it in a plain text editor using a markup language I am developping. Since I don't have developed an HTML generator yet, I had to convert it myself to HTML. Blogger did not make it easy but I think the result is much better than what I got previously by just fighting with the web interface. I would certainly appreciate any feedback concerning the resulting layout.
(end of note)

The first statement of this problem that I have seen is in Wim Feijen's note WF114 [0]. I really like the structure of his presentation but, whenever I have reproduced it, either for myself of to present the problem and a method to find a solution to somebody else, I have made on slight change: instead of using predicate transformers semantics, I use a relational semantics and I believe the switch to be quite significant from a practical standpoint. I still use the invariant based loop development techniques developped by Dijkstra & cie instead of the recursion / precondition technique of Hehner and I think it is very characteristic for my style. It shows that I prefer to manipulate one small part of the program at a time.

DEVELOPMENT ===========

The problem at hand consists in producing an array with the N first cubes without resorting to multiplication operations. Formally, the postcondition we are trying to satisfy is:

 P0:   (A i: 0 ≤ i < N: f.i = i^3)

with f the output variable (a function). About notation '.' is the function application operator and (A i: R: T) is a universal quantification over the range R and with the term T. Here, we use the property that ≤ and < are mutually conjunctional which means that their combined application can be unfolded into

 a ≤ b < c  ≡  a ≤ b ∧ b < c

They are also mutually conjunctional with equality (=) whereas logical equivalence (≡) is not conjunctinal at all because it is associative and the two features of the operator would interfere. (end of note) We can now proceed to find a suitable invariant for our loop. A good technique to do so is to replace some constants in the postcondition by variables. Since it is a quantification, it seems reasonable to focus our search in the range. We find 0 and N. We could choose either or both but if we use 0 as our initial value and N as the final one, we get the first cube for free. We will therefore opt for replacing only N with a variable:

 E0:   k = N
 J0:   (A i: 0 ≤ i < k: f.i = i^3)

If we start k off at 0, the range of J0 is becomes false and the invariant is therefore trivially true. From there, it is not a big step to say that increasing k regularly will lead us to E0 (our variant is then N-k).

 I0:   k = 0
 S0:   k' = k + 1

It is now time to see how we will maintain J0 (in the loop) while applying S0 to converge. Note on proof obligations If we use the technique of the invariant to build our loop, we have to fulfill a certain certain proof obligation. Assuming that J is the invariant, B is the body of the loop, E is the exit condition, IN is the initialization of the loop and P is the postcondition:

 (0)   J'  ⇐  J ∧ B ∧ ¬ E    "B (and E) preserve(¬s) J"
 (1)   J  ⇐  IN              "IN establishes J"
 (2)   P  ⇐  J ∧ E           "J and E lead to P"

In the preceding definitions, primed predicates are predicates for which all unprimed program variables are replaced with their primed version. Unprimed variables designate their initial values (before the execution of a given statement or program) and the primed variables designate their final values.

 (3)     (B and E preserve J) 
       ∧ (IN establishes J) 
       ∧ (J and E lead to P)
    ≡ 
       { IN } until E do B od { P }

The last line is to be interpreted as a Hoare triple with assertions between brackets. It reads "started in a state satisficing IN, the program [here the while loop], finishes in a state satisficing P." (end of note)

   (A i: 0 ≤ i < k': f'.i = i^3)
 =   { S0 }
   (A i: 0 ≤ i < k + 1: f'.i = i^3)
 =   { Split off one term }
   (A i: 0 ≤ i < k: f'.i = i^3) ∧ f'.k = k^3
 =   { Modify only f.k; S1: (A i: 0 ≤ i < k: f'.i = f.i) }
   J0 ∧ f'.k = k^3

 S1:   (A i: 0 ≤ i < k: f'.i = f.i)

The last line of the provious proof makes a nice assignment. The only problem is that it requires some multiplications, we will continue out calculations rather than adopt it as our next assignment.

   f'.k = k^3
 =   { Let's introduce a new variable to hold k^3 }
     { at all time.  J1: a = k^3                  }
   f'.k = a

 S2:   f'.k = a
 J1:   a = k^3

If we added the symmetric complement of S1, that is that everything beyond k in the values of f stays unchanged but it is not required yet. We add it afterwards to complement S1 and S2 as array assignments but it is not urgent.

 (4)   (J0'  ≡  J0 ∧ S2)  ⇐  J1 ∧ S0 ∧ S1

Since the left argument of ⇐ is monotonic, we can weaken (4) by weakening its left-hand side and replacing the equivalence by a consequence (⇐). After applying the shunting rule (see (A) in the appendix), we have exactly the shape of the proof obligation for maintaining an invariant... except that invariant used to maintain J0 (i.e. J0 ∧ J1) is much stronger than J0. We can prove that we can maintain it too, though.

 (5)   J0'  ⇐  J0 ∧ J1 ∧ S0 ∧ S1 ∧ S2

To maintain J1, we will split it in two, manipulate the left-hand side of the equality since we know a lot about k and hope it will lead to operations on a.

   k'^3
 =   { S0 }
   (k + 1)^3
 =   { Unfold _ ^3; ∙ over + }
   k^3 + 3∙k^2 + 3∙k + 1
 =   { J1 }
   a + 3∙k^2 + 3∙k + 1
 =   { We need a new variable to hold the term          }
     { which contains a product J2: b = 3∙k^2 + 3∙k + 1 }
   a + b
 =   { We want to fall back on J1'.  S3: a' = a + b is  }
     { good candidate.                                  }
   a'

 J2:   b = 3∙k^2 + 3∙k + 1
 S3:   a' = a + b

 (6)   J1'  ⇐  J1 ∧ J2 ∧ S0 ∧ S3

It seems like we have just created some more work for ourselves but we could be reasured by the sight of the decreasing order of the equations in our new invariants.

   3∙k'^2 + 3∙k' + 1
 =   { S0 }
   3∙(k + 1)^2 + 3∙(k + 1) + 1
 =   { ∙ over + }
   3∙k^2 + 6∙k + 3 + 3∙k + 3 + 1
 =   { J2 }
   b + 6∙k + 6
 =   { You know the drill! J3: c = 6∙k + 6 }
   b + c
 =   { S4: b' = b + c }
   b'

 J3:   c = 6∙k + 6
 S4:   b' = b + c

 (7)   J2' ⇐  J2 ∧ J3 ∧ S0 ∧ S4

Now for the last touch on the invariant:

   6∙k' + 6
 =   { S0 }
   6∙k + 6 + 6
 =   { J3 }
   c + 6
 =   { S5: c' = c + 6 }
   c'

 S5:   c' = c + 6

 (8)   J3'  ⇐  J3 ∧ S0 ∧ S5

We can now happily conclude

 (9)   S6 preserves J4

with

 S6:   S0 ∧ S1 ∧ S2 ∧ S3 ∧ S4 ∧ S5
 J4:   J0 ∧ J1 ∧ J2 ∧ J3

We started off knowing that J0 ∧ E0 ⇒ P0 so all that is left for a correct loop is to find the initialization. We already have I0 and, from there, we can easily calculate the initial values of the auxiliary variables. Let's ignore the calculations and see the initial values right away.

 I1:   a = 0
 I2:   b = 1
 I3:   c = 6

We can see that there is no value specified for f and, as a matter of fact, any value will do. We now have the final lemma for the correctness of this loop.

 (10)  I0 ∧ I1 ∧ I2 ∧ I3 establishes J0 ∧ J1 ∧ J2 ∧ J3

CONCLUSION ========== Looking at the end result, we can see that we ended up with a series of assignments (SX) but we haven't specified an order in which they have to be executed. It is because it is both simple and tedious to come up with an order and the order so arbitrary that it is all noise. For that reason, we can trust a compiler to do it for us. When we have to deal with a programming languages that doesn't support multiple simultanous assignments, we have to take the time to introduce the noise that is the order ourselves. The key here is that we must not overwrite a variable before we are done with its initial value. We have a bit of a problem when we run into an assignment where the use and the writing of variables are cyclicly dependant like in the following:

 S6:   x' = y ∧ y' = x

To solve the problem, we can add an auxiliary variable (say, t) and initialize it so that it can be substituted for every use of a certain variable.

 I4:   t = x

   x' = y ∧ y' = x
 =   { I4 }
   x' = y ∧ y' = t
 =   { Assignment law (B) }
   (x := y) ; (x' = x ∧ y' = t)
 =   { Assignment law (B) }
   (x := y) ; (y := t) ; (x' = x ∧ y' = y)
 ⇐    { Skip introduction (C) }
   (x := y) ; (y := t) ; skip
 =    { Identity of ; (D) }
   (x := y) ; (y := t)

And, of course, it is also simple to implement I4 and prepend it to the program we just derived. Note: Since we are interested in a program that ends up with I4, we are going to use primed variables. (end of note)

   t' = x ∧ x' = x ∧ y' = y
 =   { Assignment law (B) }
   (t := x) ; (t' = t ∧ x' = x ∧ y' = y)
 ⇐   { Skip introduction (C) }
   (t := x) ; skip
 =   { Identity of ; (D) }
   t := x

In short, this is why I don't bother to do it with the body of my loop. Finally, the main interest of this programming exercise does not lie in the resulting program. Quite frankly, it accomplishes quite a banal task. However, the technique which led us to it is quite systematic. We used very little knowledge to find it and, unlike Feijen's version, we did not introduce assignments of '?' to mark the necessity to create a new assignments to then 'guess' what should be the expression. To be honest, it is not a very hard guess but it is still outside of the scope of a calculation. The fact that I integrated that choice in a calculation makes it easier to justify. Regards, Simon Hudon ETH Zürich APPENDIX ======== Unusual laws of propositional calculus

(A)   A ∧ B ⇒ C  ≡  A ⇒ (B ⇒ C)    { "shunting" }

Hehner's programming laws [1]

(B)   (x := E) ; P  ≡  P [x \ E]     
              { "assignment law" P [x \ E] is the }
              { variable substitution notation,   }
              { P is a predicate, x a program     }
              { variable and E an expression      }
(C)   x' = x  ⇐   skip              
              { For any program variable x }
(D)   P ; skip  ≡   P                
              { For any program predicate P }

REFERENCES ========== [0] Wim Feijen, WF114 - The problem of the table of cubes, http://www.mathmeth.com/wf/files/wf1xx/wf114.pdf [1] Eric Hehner, A Practical Theory of Programming, http://www.cs.toronto.edu/~hehner/aPToP/

A Prehistoric Qualification of Languages: Succinctness

2010-08-01T13:46:00.001+02:00

I read this morning the essay Succinctness = Power [0] by Paul Graham which, so far, I find (note the present tense) to be quite smart. I can't believe he would use such a metric as lines of code or number of symbols as a meaningful metric to compare implementations with. He says that one of the goal of high level programming languages is to be more succinct for expressing a given amount of machine code. Of all people, I would expect that somebody who spent so much time with LISP would see the the fallacy. The idea and benefit of a high level language is that it allows you to think in higher level IDEAS. Those ideas can be implemented using half a machine code instruction or a thousand, it is of no relevance for its use. What IS relevant is whether the properties of that particular abstraction are good enough to fit in the context of the solutions but include very little (I am tempted to say none at all) information which does not pertain to the context it will be used in. And, finally, this is something LISP is interesting for because it drives home the message that those particular abstractions can be encapsulated in functions or data types but you can also build up the language to cover it too and It is not too say I prefer long solutions but I see succinctness as a consequence --and not the main one at that-- of a language's "power" (which I find to be a poor choice of adjective especially since he does not define how he uses it right away). Its real power lies in the variety of abstractions that one can define and use. If you exaggerate the aim for succinctness, you end up with APL or PERL which are notoriously bad. Their goal is not abstraction but packing as many operations in tiny expressions. As a consequence, those solutions are unreadable and they just seem like dignified way of writing short machine code. It gives no more flexibility and no more readability. This comment was mostly about the beginning the essay. I don't have much to say about the rest except that, at some points, he can expose some really nice insights but it really started off on the foot and I didn't expect the rest of the essay to compensate for that and, in my view, it didn't. [0] Paul Graham, Succinctness = Power, http://www.paulgraham.com/power.html Regards, Simon Hudon ETH Zürich August 6th 2010

I hate powerpoint slides

2010-07-28T16:22:00.000+02:00

I am taking a break in my study session to write about powerpoint slides as they are used by lecturers. Actually, it is such a general phenomenon that powerpoint is more the name of one of the most popular product to produce those atrocities than the only one to do so. Since this is a general post for ranting, even if I try to rationalize what is going on, I will focus on how much I hate them. It seems that most of them are produced as a combination of cue cards for the lecturer and of visual entertainment for the childish students. It means that, although they can be effective at entertaining those with short attention span (and I mention that I am of those with a short attention span but not of those who are entertained) they are quite ineffective as basic material for any lectures. This is caused by their cue card structure. Those cards are used to give directions for a speaker and they need not contain complete sentences since the material should be in the speaker's head. As a consequence, bad English, ambiguous statements and inaccurate vocabulary plague them and it would be alright if the cue cards were to be either discarded after use or kept privately for future repetitions of the lecture by the same person. I don't know if it is possible to design proper slide to act both as visual aid and supporting material for a course but, as I am about to start an academic career, I am completely opposed to their use in my lectures. I would rather use a combination of reading assignments and blackboard presentation with some possible rare exception. That being said, I can now resume my study of the most empty (in academic content) course in my school experience. Best regards, Simon Hudon ETH Zürich July 28th 2010 Post Scriptum: I am still studying for the same exam and I realize that the slides are really full of motherhood statements [1] like "Repeat the experiments until you get a reasonable standard deviation". I'm not sure how usual this is though but I realize this is something that always annoys me when I see it anywhere. [1] "motherhood statements" is an expression I borrowed from Dijkstra, it designates a set of argumentative positions and advices to which it does not make sense to be opposed to. In the case of the analogy, if you don't qualify your statement, you cannot just say that you support motherhood because the opposite does not make sense. Meyer also calls them argumentative platitudes. end of post scriptum

About the Analogy between Verification and Compilation

2010-07-07T17:42:00.001+02:00

Some people in the verification community have started responding to the complaint that formal proofs of program correctness are too long by making an analogy between verifiers and compilers:

Formal proofs of correctness are tedious in the same way coding in assembler is tedius. The use of tools, namely high level programming languages, solved the latter, and it can also solve the former.

I've seen it many times and I don't really know whom to credit for it. I think the analogy is fundamentally flawed. For one thing, the translation of high level programming language into assembler is a computable problem and its use is rather straightforward if the language is well designed and its semantics is as simple and systematic as it can be. We don't have any such luck with automated theorem provers. Since their job is to solve an uncomputable problem, they have to use lots of heuristics which make the interface with the user fuzzy. When submitting formula to the theorem prover, there is no way of saying if it will be found to be a theorem or not because the class of recognized theorems is not precisely defined. On the other hand, given a theorem (in our case the conformance of a given program to a given specification) the problem of generating a proof is well know to be uncomputable. But this should not deter us in seeking a formal backing for our design because, contrary to the folklore, writing a formal proof is not a tedious activity. It is hard but it is a very inventive process. It can become tedious though if one uses an inappropriate logic like, say Gentzen's Natural Deduction or like the sequent calculus. Although they are popular formal logic system, they are hardly the only ones available. It is not too say that they are useless formal systems, just like Turing Machines are not useless. They are not meant to be used but meant as a simplification for logicians and theoreticians to understand what tasks can be accomplished with the formal system. It is not proper for understanding how best to accomplish the tasks. Just like programming directly with Turing machines is a waste of effort, proving with Natural Deduction is also a waste of effort. It forces the user of making irrelevant distinctions, for example, with its rule for the proof of logical equivalence. The only way to prove it or even to use it is as a shorthand for two implications. Very often, you can exploit properties of logical equivalence in the calculations of theorems (like it is done in [0] and [1]) in at most half of the effort (and some times one fourth or less) that would be expended for the same proof in Natural Deduction. Contrarily to Natural Deduction, the use of calculational proofs allows one to focus on the subject matter and use the activity of proving as an improvement of his understanding rather than as a necessary evil for being certain of one's guesses. As a consequence, automating the construction of the significant proofs of correctness does not improve the productivity but decreases it because it removes any useful hints that the (human) prover could use to orient his efforts in the right direction. In short, in all important respect, the analogy is invalid and cannot be used to the defend the necessity of automating theorem proving. It is so first because, of the two compared activities, only one solves a computable problem, and, second, one of them is tedious and repetitive whereas the other involves a lot creativity. The fallacy comes from talking some properties of inappropriate formal systems as being valid for all of them. To be effective at proving, we don't only need a logic which is sound and theoretically powerful enough, we need a formalism suited as a carrier for reasoning. References [0] On the Shape of Mathematical Arguments, A.J.M. van Gasteren [1] Predicate Calculus and Program Semantics, E.W. Dijkstra and C.S. Scholten

Quality Criteria for Writing

2010-07-05T12:04:00.000+02:00

I have been less active in writing lately, and lots of explanations are possible. I possibly have ranted to my heart's content about my situation in Zürich and the sins of the industrial and academic communities but that's probably overly exaggerated. As I discuss with people, try to be more nuanced in my opinions, I find new and interesting faults to describe, some of which I have started an entry about and never finished.

I stumbled upon EWD 1068 today which I had never read and which makes me presume that I might have mispostulated (please accept the offering of that verb) my audience as not being curious or sympathetic. In any case, I should know better than to think that people interested in my fabulation are not curious; this is very rarely a step by step tutorial to do anything in particular.

I find that, mostly, I feel myself shackled by Blogger. Whenever I find a very beautiful proof that I would like to share on my blog, half an hour to an hour of struggling with the layout dissuade me of sharing that kind of logical poetry. That is really a shame and I am yet unsure about what I'm going to do about it.

In any case, enjoy the reading of EWD 1068, I found it quite interesting.

Simon Hudon

ETH Zürich

July 5th, 2010

Some Light Technical Reading

2010-06-02T13:08:00.000+02:00

I realize that I haven't posted anything in a while and as an apology I will explain to my readers (all four of them!) that I have several post in a state of a draft which I cannot bring to a satisfactory state. To show that I am still alive and interested in writing I offer you a reference to a proof I read today. I wanted to do the same thing but the solution is really delightful and I didn't think I could top it. So without further ado, here is an essay from Dijkstra's EWD series:

http://userweb.cs.utexas.edu/users/EWD/ewd11xx/EWD1162.PDF

(for the interested, all or most of his essays can be obtained here:

http://userweb.cs.utexas.edu/users/EWD/welcome.html

)

Enjoy!

Simon Hudon

Wednesday, June 2, 2010

ETH Zürich

Back in the 60s

2009-11-28T15:38:00.000+01:00

Since the beginning of Computing Science and computer programming, there has been an important evolution in the methods used to design software. We're now much better than we used to be to produce software. When I turn around and look at the Internet trend though, I have the impression of looking at a software seen of at least 40 years ago. Whereas people are now capable of choosing a programming language on account of the abstractions it allows them to formulate and use for desktop applications, it seems that web programming is still tightly tied with the individual idiosyncrasies of the browser that will be used to run them. Whenever I complain about the hazards of using Javascript, I get the answer that this is what gets executed in the browsers! Since I'm very enthusiastic about the research that I do, I don't usually refrain to mention the sorry state of affair of software and the thought that formal methods can be of great use for that. One year ago, I met a friend of a friend who is enthusiastic about web programming. When I suggested that we should be very careful about the properties that we select for our programs and the assumptions that their validity rely on, he pointed out that would be of very little help for web programming because of the important differences that exist between the browsers. Continuing in that direction, I got the strong feeling that he considered the variety of platforms to be one of the most important and most interesting challenges of web programming. I could not help but be remembered the accounts of the software scene of the 60s that I have read. The accidental complexity is so important that people mistake it for the core of the problem. In that respect, I guess this is no surprise that web applications are of such a poor quality. What triggered the present note is my suffering from the poor quality and and random behavior of Facebook, Google Wave and, while I type, I am reminded that Blogger is not much better. A final word, lest I am mistakenly assumed to be satisfied with the state of the art in non-browser based application: they appear much better in comparison to web application but there are important shortcomings also and I think that they are part of the problem of the web scene. Simon Hudon November 28th Meilen

More of the Same

2009-11-18T17:45:00.000+01:00

I just submitted a post on language design and I feel that this one is closely related. I just attended a talk in the context of my software verification course. We are now studying techniques related to data flow analysis and we had a speaker present us how he used such techniques to measure the quality of a test suite. A priori, I am not very much into testing but still, I think there is something to be done with the topic. As far as I know, the only research done in that respect that treats testing in a decent way consider the specifications even though it also uses the program's structure as a guide for testing. Now that I think of it, this is the shortcoming that ticked me off the most. It was based on Java code and there was no hint of suggestion that considering an invariant or any other statement of abstract properties of the data or of the program would enhance the assessment of the tests suites. The code was taken as it stands, assuming that the mind of the programmers is impenetrable. To avoid repeating myself, I will simply say that the overwhelming feeling I got while listening was: "this advanced computing theory of obsolete programming techniques".

I have no difficulty explaining its survival though: it does not suggest the need for education for anybody and produces a tool which can be used without thoughts. In other words, it's a fancy way of patting on back the industrial managers and the programmers alike. Nothing is more welcomed than being told that you're doing a good job by an automated tool. In my eye, this is just more of the same.

Simon Hudon

Zürich

November 20th, 2009

Bad Separation of Concerns

2009-11-04T15:28:00.000+01:00

In the course of my master's, I have to attend a seminar and prepare one talk. Last week, the talk I listened to was about using pattern matching in object oriented programming languages. I thought, as the talk went on, that all the yardstick they took to evaluate the design of their language construct was all wrong. It struggled, in my opinion in vain, to improve the expressiveness while retaining the best possible performances and remaining "concrete". In that respect, I tend to take for granted the necessity of expressing precise specifications with every piece of code. This means that, for me, the most important is that my specification language be expressive enough, but still very simple, to allow me to reason about my problems and my implementation language be as simple as possible and allow me to express any algorithm I wish. In my experience, the specification language should involve as little operational elements as possible for simplicity. As for the implementation language, it should be possible to implement it on any reasonable architecture. Before I'm objected that it is not customary in industry to use precise specification notations or to keep multiple representations, at different degrees of abstraction, of a single solution, I have to point out that this is an academic result and it does not have to follow industrial customs. Actually, I would go one step further and state that, if, in academia, we wait for techniques to become widely adopted before using them, we are lagging behind and risk doing no more than producing more of the same. Academia being more remote from the market place than industry are supposed to be less affected by the political issues that keep industry behind the state of the art. And this is not badmouthing the industry: it is understandable that they have more concerns than only technological ones. Let's get back to the paper. In their design, they seemed to tackle both problems of expressiveness and implementation at once and the result was not pretty. For example, in their pattern matching, they had to take into consideration that the evaluation of the expression (which, in their case, is an absolute necessity) they were dealing with could very well have side effects and this was an important concern of theirs. I think that this possibility was popularized by C and I think this is an important set back with respect to allowing programmers to think about their programs. I think, already, the discipline of separating queries from commands, which is part of Eiffel's style, is much better in this respect. They also had to deal with constructors in order to match objects like you would in Haskell. This is very ugly. Pattern matching is a very elegant way of writing expressive specifications but object creations do not fit in it. This is because an expression creating an object has an implicit reference to memory allocation and it can't be dissociated to it. People can't forget that the object has a memory representation and that a comparison in the context of pattern matching will have a given cost. I prefer to use mathematical expressions to express the value contained by the object and allocate the object only if necessary.

Aside In a recent programming experiment where I derived my code from its proof of correctness, I was parsing a string and, since all the properties of a language can so elegantly be formulated in terms of strings of character, I used strings to represent the state of the computation. I had my input string S, the processed string x and the left over string z and they were linked by the invariant:

S = x ++ z

with ++ the string concatenation operator. At each iteration, I split z in two parts such that

z = [ y ] ++ w

and scanning one character was encoded as:

x, z := x ++ [ y ], w

If you can't help yourself and have to imagine the memory footprint and performances of this algorithm, you might be scandalized that this is really inefficient. This is not meant to be executed as such; it is only a very simple way of understanding defining what the algorithm does. With one data refinement, I went to a representation where the use of memory is limited to the array representing the input, an integer index indicating which character y is and two booleans to represent the acceptance state of the algorithm. There is no efficiency problem with that, and my proof of correctness and my proof of data refinement are very simple and I consider them the clearest documentation for the algorithm.

end of aside

In summary, I think the right way of seeing that problem is:

Pattern Matching is a power way of associating properties or code with the shape of the data and we need to be able to express it. Since we can use it with code, it would be important to have programming techniques to make the executable, that is, techniques usable by a programmer to transform a specification using pattern matching into executable code implementing it. If the methods are especially effective and simple, we could have it implemented in our compiler but this is far from being a design consideration for the construct.

* * *

More recently, in my compiler design class, we were presented a research programming language which is said to be "relationship-based". I think the idea is a good one: they factor the inter-class relationship out of classes to treat them as separate modules. The question whether each such relationship deserve its own module is worthy of debate but, for now, what bothers me is that they treat it as a programming language construct, that is to say they keep an "implementability anchor" in their heads while they design the notation. One of the consequence is that they will refrain from adding anything for which they aren't sure they can compile it automatically. I would rather see this emerge as a specification structuring artifact and see some programming techniques emerge in connection to it so that the most common one can be implemented quite straightforwardly. For the rest, it's open to experimentation and, in all cases, a case by case implementation would allow optimization that systematic compilation wouldn't be able to do.

I think the big problem here is still the taking of current practices as a guideline for academic research: "since programmers don't write specifications, we won't provide a means to write good specifications even though progress would require it". I put it in my "more of the same" bin, look at the original ideas and forget about the language. Actually, I will do so when my semester is over.

Simon Hudon

ETH Zürich

finished on November 18th

Teaching

2009-10-20T16:35:00.000+02:00

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

2009-10-19T21:28:00.000+02:00

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)

2009-10-13T18:44:00.000+02:00

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?

2009-10-11T19:57:00.000+02:00

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

2009-10-11T17:46:00.000+02:00

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

2009-09-18T07:27:00.000+02:00

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

2009-09-14T14:04:00.000+02:00

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

Collective Knowledge

2009-09-05T14:36:00.000+02:00

At the moment, I have a few drafts I am writing but they are not progressing very fast and I am offering this short reflection. Looking around and reading different kinds of research, I can't help but feel that there exists a hierarchy of collective knowledge. Science is part of that hierarchy but it is not the whole story. As somebody who is strongly mathematically inclined, I have a tendency to view formal mathematics as the only means for expressing one's understanding but this position does not hold water. Since I am also very interested in methodology, namely, how we program and how we do mathematics, I have to have considerations for human activities and those are particularly hard to formalize and one might wonder what need we have of formalizing them. It must be honestly revealed that the activity of formalization demands tremendous efforts which are not carried out merely for the beauty of formal theories (although, many don't need much more motivation for doing it). The point is that, at any time before embarking on a formalization project, it is worth it to wonder if it is worth embarking on. On one hand, there is a class of programming languages, of which C++ and PL/I are nice representative, for which the formalization is not worth the effort because they are so complex and there documentation is so ambiguous that the formalization amount to reinventing them. Also, while reinventing them for the sake of formalization, for survival's sake, one should have the reflex of questioning every design decision before deciding to adopt them and, doing so, one would not end up with C++ or PL/I but with a language à la Wirth. If we carried that judgment to a further conclusion, it can also mean that they are not worth using either. On the other hand, there are subjects which are worth studying but the gain of a formalization is not immediately obvious. We have other tools than formalization to be rigorous and precise in our discourse and should not neglect them (to name only one: we have our natural language for which an exceptional mastery can do wonders). Once the benefit of formalization is seen, though, one should not hesitate. At the moment of writing, I am thinking about the general literature about programming methodology (aka software engineering). I have the feeling that although some publications concentrate on giving examples of the use of a particular method, some succeed at being very rigorous by being modest and accepting that they are merely working with one example. Also, their rigor seem to rely on the analysis of their example, of what helped and what did not. On the hand, some very disappointing papers on the topic try to be more rigorous by building a tool, having a handful of programmers use them, measure (in some vague sense) the improvement in their productivity and publish the statistic. Without a theory to compare those numbers to, they are meaningless and I can't help but see it as another instance of the general hype around statistic which I would summarize with "a number is better than no numbers at all". Simon Hudon Zürich, September 5th 2009

On Credibility

2009-08-18T23:07:00.000+02:00

I just had a conversation on Skype with my mother and I made an interesting reflection while seemingly lecturing on our attitudes toward great authors. I was talking about the way Edsger Dijkstra was prejudiced and said that I found it too bad because he was otherwise very smart. And then I thought back on the period where I had not realized the prejudices that he had and wondered what I could do against that. I noticed, not for the first time, that, as I read, as the author gains my respect and esteem I tend to give him (or her) the benefit of the doubt. However, people that are always objective throughout their writing probably don't write much so, for the rest, we should remain prudent not to consider everything that is said by any trusted author to be true. The next question that I would expect to ask myself while reading what I wrote is: so, what difference does it make whether an author is trusted (alternatively more trusted) or not (alt. less trusted? Well, for one thing, an author that I trust is one of which I have read many text and it is a little bit less likely that I would be surprised by something he says or write. More importantly, when I hear people talking and I know the particular author is also giving his opinion, I'll give more attention to that author because I trust him. As a corollary, when I have interrogations on topics of which I suspect my author to be interested, I'll first try to find out what his opinion is on the topic. However, it shouldn't mean that I'll be satisfied once I did. As a good computing scientist, I just saw a case where the good behavior to take is ambiguous. If I stress my imagination a lot, I can imagine cases where I trust many authors. What to do? The naive extrapolation is to choose one randomly whenever I need to. It is not very satisfying so I go ahead and look at the next credible solution: to define a more subtle notion of trust for which I can trust author X on topic Z more than I trust author Y on topic Z. If I take one topic at a time for my investigations, this should be fine-grained enough. As a final note, I am not stating that this is what I usually do. It is more like the exposition of a judgment error I do more often than I would like to and a possible solution that I would like to adopt. Simon Hudon Zürich August 19th 2009

Algorithms in Object Oriented Programming

2009-08-17T14:36:00.000+02:00

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

First post

2009-08-14T23:37:00.000+02:00

After a long hesitation, I finally took the decision to start this blog. Admittedly, a lot of what I'm going to write is pretty technical but I'm going to take the liberty of switching from technical and non-technical topics as often as I feel like it. I am a big fan of Edsger W. Dijkstra and I think his EWD series is a great idea. However, I'm not sure that I'm completely in shape to make such amazing pamphlets as he did. From time to time, I plan to try it and I hope that any reader that finds it excessive will be able to tell me so to help stay as rigorous with my social (or other) commentaries as possible. I also appreciate the way in which he presented his work and his exercises but I am not sure yet that this is the right place to publish and receive comments on those. Since I see this account mostly as a trial for blogging for now, I'm going to try different things and see how it turns out. Another consequence of this is that I'm going to discover the features of the server as I go. Simon August 15th 2009 Zürich P.S. I already have some notes on my Facebook profile but I'm not sure I want to move them all over here. I'm going to think about it. P.P.S. Since I wrote and stored essays on different platform, I'm going to try and put them all or almost all in the say public place. Don't be surprised of some posts appear with a date anterior to that of this post.

On the Pervasiveness of Social Networks

2009-08-14T16:33:00.000+02:00

I was about to write something on LaTeX or on technical writing but while surfing (read: procrastinating) I observed how much the features on many social networks in a wide sense of the word overlap on many points. It feels like some of the strongest incentives -at least for me- of joining one or another of the social networks is to get in contact with people which are not present on platform I'm on and to benefit from features that others don't have. For instance, I have an account on Facebook -no, really!-, on Twitter (which I don't really use), on google mail, google reader, google talk and linkedin. I'm sure I omitted some but it does give an idea on the many account I survey on regular basis. Just to see some of the zones of overlapping, we see that all keep a list of contacts, although the Google platform seem to use a common one. They also offer the possibility, with various levels of necessity of exposing one's profile, i.e. name, interests, education, jobs, etc. There is some measures of unification but it seems limited to the consumption of links, for example for sharing with friends on facebook or adding rss feeds. What could possible make the situation simpler for users of multiple platforms? I am very reluctant to suggest imposing or pushing a standard since it seems like a nice path to technological stagnation. For now, I'm happy to leave the question open and see if my reader(s) (if any) have anything to say on that matter. Simon August 14, 2009 Zürich

To Blog or Not to Blog

2009-08-14T16:32:00.000+02:00

Having seen the recent birth of Simon Mathieu's blog and especially the motivations he evoked to do it, I started to wonder again whether it would be a good idea for me to do it as well. Since I seem to have some readership here, I think it would be a good idea for me to stick with Facebook's note for expressing various thoughts and distributing essays. I'm also considering to put technical documents here since I would like to give the opportunity to those I have intrigued with my talks of formal methods to see how I conduct it. For example, I am now conducting an experiment to implement something similar to the shunting yard algorithm to parse mathematical expressions with custom operators and precedence rules. I would like to include infix binary operators, prefix and bracketed operators (including parenthesis), quantification and substitution. The peculiarity of the experiment lies in the fact that I use the proof obligation to guide my programming efforts and it results in a program and its correctness argument growing together. Also, it allows me to stall the moment I don't know what I'm talking about so both the proof and the program are kept as simple as possible. I would like to know if anybody would like to be tagged when I upload the document. Simon August 14th, 2009 Zürich

Pondering about Reasoning Errors

2009-08-14T16:30:00.000+02:00

This note is mostly about teaching and, in general, communicating with other human beings. I have thought about writing it for a while but I was afraid not to have enough material. I'm writing it now because of new observations and I don't care too much about the length, today. In logic, we have the two important notions of soundness and of completeness. In short, a logical system is sound if you can only use it to prove statements that are true (but maybe not all of them) and complete if you can prove all statements that are true (but maybe also some false statements). I mention them because they appear more and more relevant to the way I choose to explain or with which I choose to help people. In such cases, it is necessary to make assumptions in order to explain or skip notions. Two kinds of errors are of interest for me here: either I assume that the other person does not know something and choose to explain it while he or she already know about it or I assume that he or she does and skip it while he or she does not know about it. In the first case, the reaction can be to be insulted because the attitude seems patronizing because the notion seems obvious. In the second case, the other person can miss a notion and be too afraid to appear stupid to ask about it. While I was an intern at A2M (a game developer in Montreal), my supervisor, which I regard with high respect, taught me that it is desirable to make communications as simple and concise as possible and to trust that the other person (in this situation an engineer or a scientist) will not be shy to ask about the missing parts. During the last hour, I've been thinking about this post while doing my groceries and I realized that there are a handful of people that I trust enough to be very straightforward in my communications because I've been talking to them for a long enough period to see that they are active while listening. For the others, it does not mean they are any less. It just means that I don't know if they will ask questions and, from time to time, I don't want to risk them misunderstanding me. In no case is this a sign that I mistrust someone's intelligence because I noticed recently that I was too explicit even with some people which I have in high esteem. This is pretty short but it's all I could summon before my stomach started threatening me. Simon August 14th 2009 Zürich

A Distributed Library

2009-07-12T16:34:00.000+02:00

To make sure not to mislead my readers for too long, in particular the programmers among them, I insist in specifying that the topic is a library made of shelves and books (remember those bunches of paper?). The idea of this essay is to explain, mostly for my own benefit but maybe for that of others, one of the interests of collecting books. Personally, I love books and, although appreciate wikipedia for what it is, I think no electronic medium can overcome the joy of possessing an extensive book collection. Once in a while, I go on a book buying spree and, although some of them have been sitting on my shelves unread, I think this habit of mine is very useful. For one thing, I read fairly slowly and, sometimes, I like to put a book back in the shelf without finishing it. For those reason, if the book is good enough, it is very beneficial to own it. On the other hand, I like to see myself as a node in a distributed library. Whenever I invite people over at my place, one of the things he or she will see is my collection of books and, sometimes, they get interested in one or two of them and bring them home to see if they like it or if they can learn something from it. It can be viewed as a means of propaganda but also as a means for education. Indeed, I think it is very convenient to be able to educate each other in an informal way and being part of a distributed library seems like an efficient way to do so. Simon Hudon July 12th, 2009 Zürich

Computer Aided ...

2009-07-12T09:55:00.000+02:00

I made no secret that I consider E.W. Dijkstra a very wise thinker and I take many of my ideas from him. One of the things I've been hesitant to accept from him at first is his abhorrence of the use computers. It's been at least 4 months maybe as much as six months since it dawned on me that I am indeed addicted to the use of computers. There's no other ways to talk about the excessive reliance on electronic communication (e.g. looking for emails more than once an hour), my habit of browsing meaningless content on the internet and, more importantly, my habit of relying on software tools when they ofter arguably little improvements on productivity and probably some awful deterioration also. I just started reading the book "In Praise of Slow" by Carl Honoré and went through the section where he describes how in capitalist societies we made of time a new god. In other words time is more in control of our life than we are. It makes for some very nice reflections but for now, I'll come back to my main topic. In a similar way, the computer has come to possess control over our work. I can't count anymore how many times a day I get annoyed and frustrated with how my computer is working against me. It goes from simple trivia like message boxes popping up while I am typing something and forcing me to respond immediately to the use of theorem provers that relays my job to a secondary place by taking the reins passing to the use of IDE that do not work and word processors that pretend to know better than me what I want to do. In some cases, this is plain condescending but in every cases is completely harmfu to productivityl and destroys my motivation. Recently, I bought a new tool that I am pretty satisfied with. As a word processor, it does not argue with me. As a theorem prover, it allows me to keep the reins and go where I want to go. As an language editor, it does not crash and does not ship with faulty libraries. Finally, it very rarely interrupts me in my work. I bought a fountain pen and, although I still use the computer in a pretty addicted fashion, I see a change happening and I can't see how it wouldn't be for the best. In any case, the feeling is one of pleasure and satisfaction. And now, for those who wonder when it interrupts me: it's when my cartridge of ink is empty and I store two in my pen so the replacement is a fairly short operation. I am now resolute to using computer as much as possible for communicating with my loved ones which are now very far away and to question every other necessity I feel of using a computer. This is far from done but I expect some nice results. As an aside, as a software developer I think I draw an important lesson. In the same way you should never be condescending toward your readership, you should not be either towards your users. If they use the computer, they should know what they want and you should not take the control from them. For example, when forms have to be filled, you should allow the user as much as possible to fill them in one go and possibly even in the order of his choice. A good example of a violation of this principle is the setup of Windows where installation sequences are interspersed with questions so the user has to sit through the whole process. Simon Hudon 12:55 AM on July 12th Zürich during a sleepless night

On Programming Languages

2009-07-10T16:38:00.000+02:00

Sometimes, some programming languages popularize powerful ways of thinking about a problem. It is not too rare however that a language would create popular way of obfuscating a problem. APL and C++ are an example of the former. The difference between the two is that C++ allow you to believe you actually understand the problem when you don't have a clue about it. On the other hand, I have never met anybody knowing APL that claimed to be able to read an APL program. Simon Hudon July 10th 2009 Zürich

Nice Quote and Comments about User-Friendliness

2009-07-10T16:37:00.000+02:00

"Build a system that even a fool can use, and only a fool will want to use it." I have encountered very often the notion that user-friendliness is the quality of being intuitive or, put in Dijkstra's words, the quality of "appealing to the uneducated". It seems that Microsoft can be very active in that respect. Take Word for example, it is sold with the pretense that you don't have to learn to use it but, invariably, you'll have to get accustomed to it and get an intuition of the heuristics used to justify one or another behavior. In other word, because there is the clear criteria guiding the behavior of the system that can be written down, it is believed that you don't need to understand anything to use it. If user-friendliness is to have a non condescending meaning, I would associate it with the simplicity of the design of the system and of its interface. It is acceptable to have to learn how to use a system but the description should be as short and as precise as possible. To those who believe those to be contradictory qualities, I refer to the manual of the Algol language and conclude with a quote by Dijkstra. "About the use of [natural] language: it is vain to try to sharpen a pencil with a blunt axe. It is equally vain to try to sharpen it with ten blunt axe". E.W. Dijkstra Simon Hudon July 10th 2009 Zürich

SH53 - Natural Deduction seen as the Turing Machine for Logical Reasoning

2009-06-09T16:02:00.000+02:00

Reading through the chapter of mathematical reasoning in the B Book, I couldn't help but notice how much emphasis was put in using natural deduction. I strengthening the belief that natural deduction is not appropriate as it is for practical reasoning. In fact, I think it is appropriate to compare it to Turing machines. When we are interested in the power of a system, we want to reduce it to its bare essential. In that sense, the few simple inference rules usually associated with natural deduction are very helpful. But we must keep in mind the bias that we have when delivering that judgment: we are doing the job of a logician who wants to compare different systems. It is the same for Turing machines. They are very simple and this is why it helps reasoning about their computability properties. I think nobody knowing anything about programming would suggest to use a Turing machine to build any kind of useful system unless it is sufficiently small as to be of no significance.

Similarly, I don't think that using natural deduction as a means for reasoning about systems is any wiser than programming with Turing machines. For simplifying the logic, natural deduction offers no means to exploit equivalence because it can be dealt with using implication. It is true but not helpful when carrying out an actual reasoning. Keeping equivalence intact is simply much more efficient. People don't have to go through the same proof twice. It is also true that even if case analysis can help achieve the proof, it also helps making it unmanageable.

In short, developing proof design techniques is as necessary as developing program design techniques and, similarly, it involves developing the right notation and finding powerful heuristics. Natural deduction is not a means to that end. However, it can be used to prove properties of equational logic without to need use it when carrying out the actual reasoning.

Simon Hudon Zürich June 9th, 2009

SH48 - Weakening Preconditions

2009-05-18T16:09:00.000+02:00

I remember an instant messaging conversation I had with Prof. Jonathan Ostroff (YorkU) where he said he was buying more and more the view of preconditions as waiting conditions like in Event-B and SCOOP. I objected that, obviously, unlike Event-B, we can't hold the position that preconditions must be strengthen. It was, as I thought, some kind of law of nature and common sense that only postconditions can be strengthened. Preconditions can only be weakened. But what if it does not fit the essence of object oriented programming? Certainly, it is acceptable that the precondition of routines be weakened in the process of refinement. Since features in classes are implemented as routines (whenever they use arguments), why not just carry over the rule to the implementation of class features?

The fact that they are type bound makes an important difference. Rather than understand that the target of a call is just another kind of argument to a routine that will be dynamically chosen so that it meets (in a semi-formal way) the specifications of the routine, it should be understood as an event that occurs that (might) transform the current state of an object. That event can be or not provoked by a certain client. Whenever it is, it does not matter for the correctness of that client that the precondition gets weakened in the refinement of its supplier. On the other hand, since object aliasing is an important part of object oriented programming, considering the transformation of an object by other clients makes sense as the general case. If we assume that no other clients will invoke a certain feature unless its guard (or precondition) is satisfied, weakening it might produce surprising results. On the other hand, if we allow ourselves to blur the distinction between a class and an event-B abstract machine, we might want to make sure that the deadlock condition of a module is not strengthened in its refinements. It would mean that, in any refinement, if the guard of an action is strengthened, it must only be in the context of an action split where the guard of all resulting actions complement each other in a way that their disjunction is equivalent to the guard of the refined event.

The door does not seem to be completely closed for the notion of precondition weakening but I, for one, would not dwell on it.

Simon Hudon May 18th 2009 ETH Zürich

SH16 - Sacrificing Efficiency for Some Degree of Confidence

2009-05-15T16:05:00.000+02:00

Is the concern for software correctness getting in the way of efficiency? or Sacrificing efficiency for confidence (as opposed to correctness)

Post-scriptum note: the opposition between correctness and confidence is based on the objectivity of the criterion of correctness and the subjectivity of the criterion of confidence. Confidence can be the result of obliviousness.

Also, I have not reread it since posting it on my blog and it might need some moderation. (End of note)

With modern trends like test driven development, it seems like, for the sake of having a testable system, one will always (or most of the time) take the shortest path allowing him to add just one feature. It is positive to see that he always worry about having something that works, albeit using very restrained notion of what a "working system" is. However, the fact that the modern programmer (or, to borrow a more trendy term, the average programmer) is unable to reason in any effective way about the formulation of his specifications or even those of his architecture makes him unable to postpone the implementation until such a time as his design has been validated on its own. This points out to a blatant lack of separation of concerns. A more disciplined approach would require that the programmer be able to validate his architecture using nothing but the information contained in it and the information contained in the formulation of the relevant requirements.

It is very important to make precise what is meant by validation. Like the term coined for any profound notion, it has been used to designate so many different concepts that, it cannot be understood as anything more than a buzz-term unless it is explicitly defined.

The validation of an architecture means that any implementation following its rules is bound to produce correct result for every valid input. This means that it is a validation impossible to accomplish using testing. Some might argue that model checking would be a valid choice to come to grip with that separation of concern. If we forget everything else, they could be right. The problem with model checking is that we still rely on a posteriori verification: the concern for correctness still fails to guide the programmer to his solution. Proponents of the notion of the "average programmer" might be satisfied with that since they accept that the layman has, at best, a third rate intellect and we cannot ask him reason in any formal way about his work. However, it is clearly a better approach than postponing any kind of validation until after an implementation has been provided.

What I'm coming at now is that since the implementations are rushed at, programmers don't seem to take any care for making it efficient or correct in a general way. All that is expected is that the test suite passes. If any efficiency issues arises (much later in the development) it is considered that it is the good time to address them. It seems that an efficient implementation would have been easier to produce at the very first moment that the programmer started writing it.

Simon Hudon Gatineau, December 2008 continued in Zuerich, May 2009

SH34 - Thoughts on the Use of Typed Logic and Dependent Types

2009-03-04T16:12:00.000+01:00

On one hand, it is a very bad thing (TM) to make type checking depend on undecidable conditions, therefore inducing a proof obligation to ensure syntactic and type correctness. One of the best example is the need to prove that a given function lookup is made on a member of the domain of the mentioned function. When it is generated for an axiom, lemmata cannot be reused from one to the other.

On the other hand, if we are content with the fact that every proposition (i.e. axiom or theorem) concerning functions is accompanied by the assumption that the argument is part of the function's domain, we leave open the value of lookups of functions outside their domain.

Either we decide to associate the arbitrary value of the associated type to arguments outside a function's domain or we leave it undefined and accept a different value from function to function.

In the second case, whereas the interesting property of function equality is

f = g == dom.f = dom.g /\ < x =" g.x">

However, if we don't have also

f = g == dom.f = dom.g /\ < x =" g.x">

it becomes impossible to use the principle of substitutability.

If, to the contrary, we choose to assign the arbitrary value of the associated type to arguments outside of partial functions' domain we are asking for trouble as an axiom might specify the image of a function regardless of whether or not the mentioned argument is part of the image as in the following:

axm1: f.x = 3 axm2: dom.f = { x | x mod 3 = 2 : x } axm3: g.x = 7 axm4: dom.g = { 1, 2, 3, 4 }

However, an axiom of function theory might state

fun1: ¬ x in dom.f ==> f.x = choice (H)

For an arbitrary f: G +-> H, x: G and generic types G and H. Let's now assume x is neither a member of dom.f nor a member of dom.g (as the union of both of them does not include all the natural numbers, it is a sensible assumption).

	3
=		{ axm1 }
	f.x
=		{ fun1 with f, x := f, x }
	choice (NAT)
=		{ fun1 with f, x := g, x }
	g.x
=		{ axm3 }
	7

Which is obviously nonsensical. This choice of interpretation is not the only way to introduce nonsense indirectly. Take for example the choice function. Asserting a particular type for it as an assumption is a nice way to run into trouble. The problem at hand is related to that kind of error. The goal here is to discuss several possibilities for making all the nonsense obvious and more difficult to introduce. In general, we would like to be able to build a theory in a modular way allowing different modules to reference each other in a non circular way. As is often the case in software design, it is desirable to limit the number of dependancies between modules. In that context, nonsense can be introduced when referencing two modules that have been developed independently if they postulate additional constraints on a common module. The trouble will arise when the accumulation of third-party constraints contradict each other.

In that case, axioms referencing definitions made in another module should make sure to make nothing more than put a name on an element for which it is possible to prove that it exists. In fact, it might be a good thing to require such a proof when postulating such axioms. In appearance, we are coming back at the apparent ugliness of set theory as it is used in B. To solve it, it might be sufficient to relax the constraint imposed on the order of the declaration of axioms and theorems. By allowing theorems to be defined before axioms, we retain the ability to reduce the labor of formal reasoning for every proof including those induced by the definition of axioms.

Simon Hudon ETH Zürich March 4th 2009