Dear DDJ,
The article "Plug-In Components for MFC" by Stefan Hoenig (DDJ, August 1998) describes the best GUI architecture using MFC I have seen. Ironically, Stefan has used MFC to bend Windows event handling into something that resembles the Java 1.1 event model. I applaud him. However, the claim that he presents "...a completely new approach for encapsulating window functionality into different objects." is false. In addition to paralleling Java 1.1 event listeners, Stefan's approach is similar to the Taskmaster pattern presented by Robert Martin in the March 1997 issue of C++ Report. I do not doubt that Stefan developed his method independently, since MFC programmers usually refer strictly to Microsoft publications, which emphasize "tips and tricks" and have less to say about architecture and engineering. This may also explain "...why the MFC team had never considered such a solution."
Joshua Lynch
joshualynch@yahoo.com
Dear DDJ,
"Embedded Development Compilers," by Don Hair and Cesar Quiroz (DDJ, August 1998), presents a nice overview of what an embedded-systems programmer requires of a compiler. I would like to add one comment about the use of C language bitfields: Avoid them!
Reason 1: So much of the implementation is left to the choice of the compiler writer so that you cannot rely on repeatable memory alignment/allocation should you need to change compilers (or if you elect to change to a later version of the same compiler). One compiler may heed the unsigned char type applied to a bitfield, the next may ignore it and treat the field as an int (and still be in accordance with standard C).
Reason 2: A compiler's optimization pass may compress several sequential bit accesses into a single read/modify/write operation, which manipulates all the bits in the same cycle. This is all right for creating bit patterns, but if (as is often the case) the bitfield is memory mapped to hardware registers, the order of bit operations as originally programmed might be crucial to proper hardware operation, and that information is lost. Standard C provides the keyword volatile to help the embedded programmer deal with this, but I advocate masking and other logical operations to make such bit manipulations more reliable and portable.
Russ Heeschen
Russ.Heeschen@respironics.com
Dear DDJ,
I just finished reading "Embedded Development Compilers," by Don Hair and Cesar Quiroz (DDJ, August 1998), and found it one of the best articles I ever read. It is simply excellent and well worthy of appearing in a prestigious magazine like DDJ. It is written in a clear and professional way. It describes its subject in just the right amount of detail. It is even written in beautiful English (the "ostensible locals" is a gem). And most of all, it doesn't beat Microtec's drum. Yet at the end the reader must conclude that to get a good embedded compiler one has to go to your kind of professionals (though there is no URL for Microtec/Mentor Graphics). Bravo! !que lindo!
Antonio Bigazzi
AntonioB@Microsoft.com
Dear DDJ,
I found Sergei Savchenko's article "Theorem Proving and Database Querying" (DDJ, August 1998) interesting and informative. I do, however, think a couple of points should be clarified.
On page 112 Sergei states that existentially quantified variables are eliminated by replacing them with constants. Actually, the process is more complicated than that, and the complications are relevant to other parts of the article. Briefly, after quantifiers have been moved to the front of a logical statement, each existentially quantified variable is replaced by a new function symbol that takes as arguments all the universally quantified variables whose quantifiers occur to the left of the existential quantifier being replaced, and the existential quantifier is removed; these functions are known as "Skolem functions." For example, the statement (A x) (E y) P(x,y) is changed to P(x,f1(x)); I use (A x) for for all x and (E y) for there exists a y such that. This sheds light on the comment in the middle of the first column of the same page about predicate logic using functions with no arguments instead of constants: Since a constant is logically equivalent to an existentially quantified variable whose scope is the entire statement, replacing it with a function of no arguments is just part of quantifier elimination. A more important effect of Skolem functions is that when an interpretation of a logical statement is being built, they can act like pumps blowing up the size of the domain of interpretation: Each time a universal quantifier is instantiated to a new object, the Skolem functions to its right denote yet more new objects. In some cases this can result in an interpretation with an infinite number of objects.
The second point that needs clarification concerns the discussion on page 112, including the Tim Kientzle's introductory note. I think Sergei's text is more accurate than the note. The reasons require delving into the proof process. Most automated proof procedures, including the resolution process sketched by Sergei, are based on a result proven by Jacques Herbrand in 1930. A logical statement is said to be satisfiable if a consistent interpretation of its variables, constants, predicate symbols, and function symbols can be found with respect to which the statement is true. Herbrand invented a procedure for checking the satisfiability of a sentence that had the following three properties:
Given a hypothesis H (which may be the conjunction of several hypotheses) and a conclusion C, the theorem H-C (using Sergei's notation of "-" for implication) may be proven by applying Herbrand's procedure to the negation of H-C, which is H&~C. There are three possibilities:
If, as I believe, Sergei was referring to the third possibility when he said "the search space can be infinite," then he was exactly right. Tim is mistaken in saying that interleaving an attempted proof of P with an attempted proof of ~P would result in one of the two halting. The reason is that it is possible for both ~P and P to have only infinite interpretations. For example, consider the statement (A x) (E y) (A z) P(x, y, z) with its negation (E x) (A y) (E z) ~P(x, y, z): Using the manual refutation procedure described in Formal Logic: It's Scope and Limits by Robert C. Jeffrey (McGraw-Hill, 1991, ISBN 0-070-32357-7), pp. 113-114, on each it soon became clear that the procedure was in a loop generating more and more objects. By the way, did you notice that both the above statement and its negation have an existential quantifier to the right of a universal quantifier? Remember those existential quantifier pumps?
Finally, in 1936 Alonzo Church proved that there was no mechanical proof procedure for predicate logic. As Tim indicated, Gödel's Incompleteness Theorem establishes a similar result for "any reasonable system of mathematics," but pure predicate logic is not such a system (and yes, logic students everywhere are eternally grateful to Kurt Gödel for proving both the Completeness Theorem for first-order predicate logic and the Incompleteness Theorem for first-order arithmetic).
Bill Wood
wtwjek@winternet.com
Dear DDJ,
The article "Theorem Proving and Database Querying," by Sergei Savchenko ("Algorithm Alley," DDJ, August 1998) confuses logical OR with logical IMPLIES in the description of example clauses on page 111. The clauses a|~b, b|c and a|c are described as if b follows from a and c follows from b, you can conclude that c follows from a. The relationship between OR and IMPLIES is that x->y is equivalent to ~x|y. The correct logical clauses for the English description in the article are ~a|b, ~b|c, ~a|c. The correct English description of the clauses in the article is if ~b follows from ~a, and c follows from ~b, then c follows from ~a.
Andy Thomas-CramerSergei responds: Thanks Andy. It indeed must be ~a|b, ~b|c, ~a|c to correspond to the description. Resolution: a|~b with b|c producing a|c is ok, but it rather means not a implies not b and not b implies c producing not a implies c. I cannot believe I missed it.
Dear DDJ,
I thoroughly agree with Al Stevens in his conclusions about Windows CE (DDJ, July 1998). I am no expert on the handheld or auto-PC market, but I have been programming embedded systems for years, and regularly write for Embedded Systems Programming magazine. I attended a WinCE class at the Embedded Systems Conference last April, where MS turned up in force (and were still surprised that there were so many embedded systems programmers there!).
The level of misunderstanding between the class and the speaker was amazing. The speaker assumed that all WinCE applications could be tested on the PC in CE emulation mode. It never occurred to him that the embedded target might have a motor hanging off of it, and correct control of the motor might be an important part of testing and debugging. There were many similar misunderstandings, and most embedded programmers left very confused. Someone needs to shout very loud that CE is not an alternative to conventional RTOSs (though it may have something to offer to people who want a stripped down Win95).
Niall Murphy
nmurphy@iol.ie
DDJ