26.

Benefits of Specifications

Although no formal specification (akin to that of ML) exists for Java, a good deal of care was put into development of a precise informal specification. Many smaller, toy versions of Java have been formalized from this specification, and correctness properties have been proven about them. Furthermore, Java is typically compiled to bytecode for the Java Virtual Machine, which itself is well specified (although, at the time of this writing, the process of bytecode verification is not). The result is an unprecedented level of portability for programs written in this language.

Tip 

Java programs have a higher degree of portability because of the language's precise, albeit informal, specification.

The conclusion we can draw from this is that there really are advantages to having as precise a specification as possible. The costs of an ambiguity or inconsistency can be quite high, leading to decreased portability, reliability, or even to a security hole.

But even in the world of programming languages, where problems in a specification are most costly, formal specifications are rare. Some of the reasons for this are:

  • Few language properties are checked automatically. The process of proving properties about a programming language specification hasn't been automated, as of yet, to the same degree that proving properties about hardware design has. As a result, there's not quite as much advantage to formalizing them.

  • Many language users prefer the informal. Informal specifications are preferred by most of the people who will actually read them, like compiler writers. (In fact, compiler writers often revel in less formal specifications because it gives them more room to optimize a program.) The other, occasional, users of a language specification are the programmers, and most of them greatly appreciate an informal specification that they can easily understand.

  • It costs money to produce a formal specification. Producing a formal specification up front is expensive. Companies have found it more cost effective to ship early and flesh out the details of a specification later (or, more often, never). Admittedly, if a development team commits to producing a specification, it may not finish formally specifying its system before its competitors have already shipped! If Sun had waited to produce formal language semantics for Java before releasing it, the language may not have come out in time to ride to fame as the preferred language for Internet programming.

But if up-front and formal specification is too costly, what approach should a development team take in specifying software? Many development teams have been so turned off by the cost of up-front specification that they've renounced specification entirely. But that's never a good idea.



Bug Patterns in Java
Bug Patterns In Java
ISBN: 1590590619
EAN: 2147483647
Year: N/A
Pages: 95
Authors: Eric Allen

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net