Beaten out upon
The anvil of the sky
Brings burnished morning
To Earth's cold iron
|
|
Seering bronze sunlight Beaten out upon The anvil of the sky Brings burnished morning To Earth's cold iron |
| date | 2001-001-10:08:12 |
| Software |
I've been meaning to write something bad about Z for a long time, and if I don't do it now I won't ever, so here goes. Z is ordinary predicate logic with an enriched syntax designed for software specification. It is probably the most popular software specification language today, and even I think it has some use. Just not nearly so much as it's acolytes advocate, to the extent that I'm pretty sure it'll never be useful. There are a number of things that a technology has to have going for it to live and grow: 1) It has to solve a problem that its potential users have 2) It has to be possible to learn the basics in a fairly short time 3) It has to be possible for most people to get an adequate working knowledge of it eventually, after enough exposure 4) Ideally, it should be generalizable to other areas, or somehow tie into the users matrix of other skills. 5) The problem it solves has to be common enough that a user community can grow up around it that is big enough and dense enough to be self-supporting There may be other criteria, but those are the ones I can think of off the top of my head. I don't think Z satisifies most of them. My experience with Z is limited--a study group I belong to recently spent a couple of months going through Jacky's Z book, The Way of Z : Practical Programming With Formal Methods. We also did some readings from Anthony Diller's book, Z: An Introduction to Formal Methods and a few others. In some limited but important contexts, I think the problem Z sets out to solve is very real. Having a clear specification of the behavior of a nuclear reactor control system, or a radiotherapy machine, is a good idea. It isn't at all clear that Z is a good way to specify this, however. A couple of examples illustrate why. The first is the calender example. This is apparently a favorite in the Z community, who seem to like to repeat the same few examples over and over again in more and more detail--this was a notable feature of the books I reviewed while we were looking for a suitable candidate for the study group. One of the supposed strengths of Z is that you can run automated checkers over your Z to enusre that "all cases are dealt with". This sounds good: if all cases aren't dealt with, then your system is going to engage in unspecified behavior at some point, which is likely to be bad. But the problem is that what constitutes "all cases" is determined by the specifier's knowledge of the domain. I found it very easy to write a calander specification that was formally complete, but quite wrong. I had specified something, just not the calender as we know it. And this is the real problem: not showing that the code you have covers all the cases you've thought of, but showing that you've thought of all the cases that matter. The formal checking made possible by Z creetes a risk of producing a false sense of security by solving the first problem, not the second. To solve the second, specification, design and code reviews are the appropriate tool: getting as many human minds engaged in the problem as possible. This, by the way, is why Howard Roark was a bad architect: he didn't play nicely with others, and invite them in to comment on and critique his work. The next example is a word processor specification. Jacky's description of this violates one of the fundamental tennants of good design, which is to leave the implementation details as late in the process as possible. He points out, correclty, how clunky the the specification would be if you created your word processor spec based on a single buffer with an index for the cursor position. Instead, he specifies it in terms of two buffers, one ahead of the cursor and one behind it. Very clever, but do we really want to be talking about buffers at this stage in the process? I'd like a specification that can capture the user experience, not the internal layout of the machine's memory. Z advocates will argue that this isn't fair: Z specifies only behavior, and the details of how that behavior are specified should not affect either the design or implmentation. This is, unfortunately, not the way things happen. Having two (or three) different representations of the same behavior (specification, design and code) is asking programmers to square or cube the amount of mental work they have to do. Not only do they have to remember the different representations, they have to intertranslate them routinely. Software developement is hard enough without this kind of added burden. So I think Z solves what is mostly the wrong problem (and one that is fairly easily solved by other means, such as more formal code checking by hand) and that it does so in a way that will either lead to the specification invading the design and implemetation in inappropriate ways, or vastly multiply the burden on the development team. This is not to say that Z doesn't offer some value, but the question is: does the value it offers make the effort to learn it worthwhile? The answer to this question is: almost always No. Z is not an easy language to learn. I'm usually reckoned to be fairly clever, and I found it difficult. This suggests that the average designer will find it hard and the average developer will find it very hard. Z isn't the hardest thing I've ever learned--it's fairly simple compared to angular momentum algebra for nuclei--but it's easily one of the most difficult software related things I've encountered. And in evaluating its difficulty, you have to remember that it's estimated that 15% of developers will never "get it" with regard to object-oriented programing, which is vastly simpler in concept and execution than Z. So I think Z fails to meet my second and third criteria pretty completely, and it isn't so hot on the fourth or fifth, either. There aren't a lot of areas where the skills you gain learning Z have applicability, and all these problems add up to meaning that not many people are likely to learn Z well enough to create a viable user community. Sure, there are Z conferences, but the language has been around in one form or another for over a decade, and its following is still largely academic. This means that while I think Z has the potential to be useful in some areas--notably in documentation of complex routines--it is unlikely to ever be widely enough understood to be actually useful. There's no point in using a language that other people can't read, as APL programmers found long ago. Z is an interesting foray into one extreme of solutions to specifying software. I expect that some aspects of its design will be picked up in future attempts to address the same problem. But I am generally not hopeful about the utility of formal methods to specify informal systems, and most of the applications out there are informal systems. They don't have a formal specification because the jobs user's do with them aren't formally specifiable. The fact that the software runs on a universal Turing machine does mean that there is some interesting formal structure underlying the application's behavior, but user's represent that structure to themselves, in their minds, in highly informal ways, and that is what formal methods necessarily fail to capture. One of the great difficulties in maintaining legacy systems is that bug fixes almost always break something--users come to depend on side effects and nominally buggy behavior to perform some jobs. Bug fixes, particularly in libraries, often include backward compatibility flags to reactivate the buggy behavior for users who have come to depend on it. So long as this kind of thing happens--where some users indentify a particular behavior as a bug and others as a feature, or the same users identify the functionality as one or the other in different contexts--formal specification will fail to solve the core problem of software reliability and robustness. Rather than throw up our hands and say, "Well, I guess that means the problem can't be solved!" we should take this to mean, "Well, I guess that means formal specification doesn't solve (most of) the problem." Other means, particularly specification, design and code reviews, are powerful tools for making software more reliable and robust. Implementing them requires a culture of openness and team-work that isn't found in all software development organizations, but it can be nurtured there if the the leaders set the right example with their own behavior. |