Eidola Examples
Examples
Comparisons and Metaphors
Growin' Code
Trial by Eidola
Tag Team Coding
Why Eidola Wants to Evolve
About Eidola
Project Status
FAQ
Contact
Eidola Home
 
  Trial by Eidola
Having the structure of a program formally specified, easily accessible and cleanly separated from its representation opens up all sorts of useful possibilities in testing and formal verification. Software reliability is a universal problem -- the few people who do have to build absolutely reliable software work very, very hard to do it. (And no, most allegedly "mission critical" business applications do not count.)

One of these people, Nick Weininger, who helped build a real-time avionics operating system, wrote a really marvelous paper on what kind of work this involved, and how a language like Eidola could help make such work faster and cheaper. On this page, he helps briefly restate of some of his thoughts on how a mission-critical developer might use Eidola.

  Review Your Code? I'd Rather Wrestle Marmots!
Conceptual clarity in code writing is always a good thing, but in mission-critical software development it is absolutely essential. When writing mission-critical code, the developer must not only carefully think through the correctness of the code they are writing; they must also present it in a form suitable for careful review, by an independent reviewer. An independent reviewer means, at least, someone who did not write the particular piece of code they are reviewing. Ideally, the reviewer should never have seen the program before, and thus have no hidden preconceptions about its correctness. Naturally, this gives the reviewer a horrendously difficult task, making truly independent reviews difficult to achieve in practice.

This is a problem Eidola can address, and not only because of the potential of better notation to make code more understandable. Because an Eidola program is interactive at edit time, a reviewer can interrogate it to understand the program's structure, and check this structure against the specification. The more independent the reviewer is, the more important this capability becomes.

Suppose you are assigned to review part of a program that you've never seen before. For example, you might be asked to ensure that the Foobar class performs, and is used by other classes, in a manner matching its specification. If you've ever actually had to do something like this, you know that it can be close to an impossible task. You might end up with a nicely filled-out review checklist with all the i's dotted and t's crossed, but it is unlikely you will be able to do a real and thorough examination of the class's correctness.

Why? Well, consider what you have to do to perform such an examination. If you're reviewing good code on a well-organized project, the header file for the Foobar class will contain a well-written, clear explanation of what the requirements on the class are; the headers for each function will explain what the function does, what the conditions are on its arguments, etc. So far, so good. (I can hear most of you snickering already).

But this is only the beginning. One requirement might say that the Foobar class fits into the GiantEventQueue in a certain way. What's the GiantEventQueue? Call up another file, read another explanation, try to grok all the author's references to six other classes. Another requirement might say that the Foobar::SelfDestruct() method must only be called after the global initialization of the Frammitz class. Now you have to search through all the places where the SelfDestruct() is called, look for the Frammitz initializations before those calls, worry about whether you missed one because of some subtlety of program flow....

At this point, you Emacs studs out there are probably still unconcerned. "What's the problem?" you say. "I can write an elisp macro in five seconds that will automate all that searching for me." OK, sure, a good programmer's editor could keep you sane so far. But now suppose you come across the requirement:

WARNING: Instances of Foobar may only be added to or removed from other Foobars or FrammitzFinders, and then only if they really like each other. Under no circumstances may a Foobar be added to a WrestlingMarmot or one of its subclasses, as a FatalGiggleException may result.
How do you check that? You can't search for all instances of "add" and "subtract". You could search for every time anything of type Foobar, WrestlingMarmot, etc. was instantiated, and look in the code below those instantiations for "add" and "remove" functions. But if there are 990 instantiations of Foobar and only three times where a Foobar gets added to anything, you're in for a serious case of eyes-glazed-over.

The essential problem here is the tediousness of understanding the complex semantic structure in which program components are embedded, and the difficulty of searching for constructs based not on their syntax, but on their semantics. Text editors cannot really remedy this problem because they don't understand (or at best, understand only superficially) the semantics of what they're editing.

But an Eidola notation does understand that semantics, so constructing semantically-based search-and-display constructs would be a snap. Want to search for calls to the "add" function where one argument is a Foobar and the other argument has a WrestlingMarmot as its ancestor? No problem. Want to display all of the places where a Foobar is passed to a GiantEventQueue method? Piece of cake. With these sorts of capabilities, a good Eidola notation could alleviate the pain of one of the most thankless, and necessary, tasks in software development.

  Very Literate Programming
Mission-critical code usually involves carefully written requirements specifications, which have a very direct bearing on the code -- each requirement must be implemented in the code, and every piece of code must tie to a requirement. At least in theory. In practice, enforcing this is very difficult and time-consuming. There are various means of automating the checking for formal compliance, but checking for substantive compliance is difficult, for the reasons outlined in the previous section.

Although Eidola focuses on semantic structures in a program, it will also allow a notation to attach hints to pieces of code. They might be display hints -- for example, a sequential ordering or a two-dimensional arrangement of the members of a class.

Hints need not be all sugar, however. Structured documentation stored as hints are a way of realizing Donald Knuth's idea of "literate programming", or self-documenting code. In a mission-critical context, hints could carry not only English, but computer-parsable cross-references to a set of specifications. Given a notation that knows how to handle these specification hints, it would be possible to ask "show me the specs that this code implements", or "show me all the code related to this spec", without any tedious human effort. There would, of course, still be tremendous human effort involved in keeping code tied with the appropriate specs, but such work would carry a greater reward in Eidola. Once again, the software can't think for the programmers; it can only help them when they're willing.

  Formal Modeling and Automated Testing
Many tools exist to help developers model their code in some useful problem space other than the language itself. It is very common to make mathematical assertions about the behavior of a piece of code, and then include runtime checks of these conditions. The problem with this approach is that it catches the failure only when it happens. "What's that blue thing...doing here? Abort! Abort!" Testers simply try to drive the software into as many states as possible, hoping to flush out the illegal ones.

A more powerful method is to determine which parts of the code could affect these assertions, then use software which can model the behavior of these parts and check the assertions against the space of all possible software states. When the assertion fails, a good formal modeling tool can graphically display the circumstances leading to the assertion failure, allowing the developer to figure out where the bug came from easily. The problem with currently available formal modeling tools is that the good ones can't work directly on the code itself; they need it to be translated to a modeling language which has an easily manipulable formal semantics.

In a language like Eidola, this translation would be easier, since the fundamental form of programs is already expressed by a formal semantics. Furthermore, the process of "program slicing", extracting the slice of a program related to a particular assertion and boiling that slice down to a form more suitable for modeling, could be at least partially automated. This would save time and dramatically reduce the potential for mistranslation. And such a translation would be much easier to write for Eidola, with APIs already available for dealing with the code's structure, than for a traditional language, which would require writing or adapting a partial compiler for the source code.

Also, a good notation might integrate modeling with the development process, allowing testing to be done more often in the course of development. If you wanted to know whether your nifty new class would work correctly with two existing classes, and you had a rigorous expression of what "correctly" means, the notation could let you select the classes to model, run the modeling tool, and display any errors found in the context of the program code itself-- not in the context of the sliced model.

Next: Tag Team Coding >>
 
Copyright 2000-2001 Nicholas Weininger, Paul Cantrell