Kuro5hin.org: technology and culture, from the trenches
create account | help/FAQ | contact | links | search | IRC | site news
[ Everything | Diaries | Technology | Science | Culture | Politics | Media | News | Internet | Op-Ed | Fiction | Meta | MLP ]
We need your support: buy an ad | premium membership

[P]
Something Every Java Programmer Should Know

By Coryoth in Technology
Wed Jan 18, 2006 at 05:47:29 AM EST
Tags: Software (all tags)
Software

Sometimes ideas don't get the attention that they deserve. The Java Modelling Language (JML) is just such an idea. JML is something every Java programmer should know about. That does not mean every project in Java should make use of JML, only that developers should be aware of it so they can use it wherever it does make sense. The fact is that JML provides so many benefits for so little extra work that it deserves far more use than it gets. If you program in Java it could definitely make your life easier.


What is JML?

In a sense JML is just a way to document your code better. JML provides simple intuitive syntax to provide concise descriptions of behaviour in a Java module, inheriting ideas from Eiffel, Larch and Refinement Calculus. JML uses annotations to document all the mundane things you would normally document. For example you might want to note which fields are allowed to ever be null, or whether a particular method requires one of its parameters to be greater than zero, or if a method is side-effect free. What JML really offers, however, is the tools to make use of these extra comments to save you time and effort later. JML simply asks you to do what you would normally do, and in return offers improved productivity when it comes to documenting, testing, and debugging your code.

So what exactly does JML look like? Here's a simple toy example that, while contrived, manages to demonstrate a lot of basic JML and will be useful later for demonstrating what tools that use JML can do.

public class Example {

    public int modifiable = 0;
    private /*@ spec_public @*/int additional_value = 5;
    private /*@ spec_public non_null @*/ String current_substring;

    //@ invariant additional_value >= 5;
    //@ invariant current_substring.length() == modifiable;

    //@ requires ((String) o).length() > modifiable;
    //@ assignable current_substring;
    public void castExample(/*@ non_null @*/ Object o) {
        additional_value = 5 + o.hashCode()%5;
        current_substring = ((String) o).substring(0, modifiable);
    }

    //@ requires x >= -5;
    //@ ensures result > 0;
    public /*@ pure @\*/ int pureFunction(int x) {
        return x + additional_value;
    }

    //@ assignable modifiable;
    //@ signals (ExampleException e) additional_value <= 4;
    public void unreachable() throws ExampleException {
        if (additional_value > 4 && modifiable > 0) {
            modifiable++;
        }
        else if (modifiable == 0)  {
            throw new ExampleException();
        }
        else {
            //@ unreachable;
        }
    }
}

Most of the JML annotations should be clear: We are simply documenting constraints on inputs (requires clauses) and outputs (ensures clauses, noting when fields or parameters cannot be null or when code is (we presume) unreachable, and what invariant properties that we expect the objects to have. A little less immediately obvious are the assignable and signals clauses. An assignable clause declares what is allowed to be written/assigned to from within the method, and a signals clause declares conditions that must be met in the case of an exception being thrown. Finally spec_public simply declares that these private fields have public visibility to the specification. You may note a few errors where the specification and the code don't agree - we'll come to those shortly.

This is, of course, only a small sample of what JML offers. JML provides a lot of useful syntactic sugar to make stating your intentions as easy and natural as possible. For a proper introduction to JML there are some presentations on basic JML and more advanced JML as well as an introductry paper on Design by Contract in JML. Full documentation can be found in the JML Reference Manual.

What do I get out of it?

JML provides an easy to use language with which you can concisely say how you intend your code to behave. More importantly it provides tools to make full use of that. For the small amount of extra effort of documenting your intentions with JML you get a lot of easy gains.

The JML tools

The JML distribution comes with a number of tools that use JML annotations. The four most useful are jmldoc, jmlc, jmlrac, and jmlunit. The first, jmldoc performs the same function as Javadoc, producing almost identical API documentation. The advantage of jmldoc is that it understands JML annotations and includes suitable extra information in the API documents based on the annotations. As long as you document requirements and guarantees for modules in JML you can be sure that the API documentation will always include those constraints. Furthermore because JML annotations become integral for testing and debugging it is far more likely that the annotations are kept up to date with the code, meaning that documentation is also more likely to be up to date.

The tools jmlc and jmlrac provide a JML aware compiler and runtime environment. The advantage of compiling and running code with such tools is that JML annotations are converted into assertions which are checked at runtime, making it easier and faster to discover and locate bugs. For the small cost of writing a few annotations you can significantly speed up the testing and debugging cycle.

You can get the similar results by liberally sprinkling assertions through your code, but JML offers several advantages over such a scheme:


  1. JML provides a lot of syntactic sugar like universal and existential quantifiers (\forall and \exists), and logical connectives like "implies" (==>) and "if and only if" (<==>).

  2. JML elegantly handles inheritance. When overriding a method you will have to rewrite all your assertions, while JML annotations are automatically inherited. If you want to add annotations to those inherited by an overridden method JML provides the also keyword.

  3. As JML annotations are comments, and only converted into runtime assertions when you use the jmlc compiler, turning off runtime checking is as easy as compiling with a standard Java compiler. Using assertions will have you jumping through hoops to arrange anything similar.

  4. JML annotations can be automatically included into your JavaDoc documentation. If you use assertions you'll have to repeat the information elsewhere to get it included in the documentation


Of course having assertions based on intended behaviour is no substitute for a decent unit testing framework. JML has an answer for this too however. The jmlunit tool can read a Java module with JML annotations and automatically generate a JUnit test class based on the annotations. For example running jmlunit over our example above creates two new files Example_JML_Test.java and Example_JML_TestData.java. The first of those files is a JUnit test suite, and the second is used to generate test data. JML attempts to come up with a reasonable test data generation strategy, but leaves space for you to enter your own set of test data instead should you prefer.

Extended Static Checking

Extended static checking is where JML annotations begin to truly come into their own. ESC/Java2 is an extended static checking tool for Java that uses JML annotations to catch errors before you even compile, let alone run, the code. You can think of it as type checking on steroids - using the information in the annotations to warn you about a wide variety of potential errors. It runs about as fast as compilation, so there's no waiting for results.

Consider what happens when we run the example above through ESC/Java2. We get a series of warnings (some not revealed until others have been corrected):


  1. We are warned that current_substring is uninitialized and could be null.
  2. We are warned that additional_value is modified when it shouldn't be (line 14).

  3. We are warned that the cast made in castExample may be invalid.

  4. We are warned that the postcondition for pureFunction may be violated (it's possible that x = -5 while the invariant only ensures that additional_value is at least 5, thus 0 could be returned).

  5. We are warned that an exception may be thrown in unreachable without the conditions being met.

  6. We are warned that the //@ unreachable portion of code is, in fact, reachable.

  7. We are warned that the invariant current_substring.length() == modifiable can be violated.


Most of the errors listed above are either errors in code, or in our expectations of what the code will do. Some of these errors can be remedied by strengthening the constraints. For example we can add //@ requires o instanceof String to castExample to fix the warning, but at the cost that any code calling that method must meet that precondition (though the API documentation will state the precondition). Other errors can only be corrected in the code itself.

While the errors are necessarily simple in this toy example, hopefully this gives you the flavour of what ESC/Java2 can do for you - it has very powerful algorithms and scales to remarkably complex code, easily finding errors that would be hard to spot by inspection. For more examples of what ESC/Java2 can do for you (and it is well worth reading) try this introduction to ESC/Java2. ESC/Java2 offers a robust and powerful tool for finding subtle errors in your code earlier when they are easier to fix.

Conclusions

JML is simple to use: it has an expressive and intuitive syntax, and you can write the annotations at the same time the code. JML is also flexible: you an use as much or as little in the way of annotations as you need. Perhaps you simply want to add some pre- and post-conditions, or just keep track of which methods can access or alter certain fields; perhaps you want to use the full power of the theorem provers in ESC/Java2. Most of all JML makes many aspects of development, from debugging and testing to documenting, easier and more efficient, all for very little extra effort. If you program in Java for a living then JML can almost certainly make your code better, and your life easier.

Sponsors

Voxel dot net
o Managed Hosting
o VoxCAST Content Delivery
o Raw Infrastructure

Login

Related Links
o Java Modelling Language (JML)
o Eiffel
o Larch
o Refinement Calculus
o basic JML
o more advanced JML
o Design by Contract in JML
o the JML Reference Manual
o ESC/Java2
o introducti on to ESC/Java2
o Also by Coryoth


Display: Sort:
Something Every Java Programmer Should Know | 107 comments (90 topical, 17 editorial, 0 hidden)
For non-Java Programmers (3.00 / 4) (#3)
by Coryoth on Tue Jan 17, 2006 at 03:04:45 AM EST

If you're not programming in Java, but still like the look of what JML has to offer, there are other options. Spec# offers very similar functionality (though I think tool support is a little earlier in the development stage) for C#, and SPARK offers similar syntax and very mature tool support for Ada. There's also EML for SML, and if you're a Haskell programmer you might consider HasCASL (If you've delved into the theory for Haskell then you'll appreciate the theory for HasCASL, if not the "intuitive" syntax).

In the C world, (none / 0) (#8)
by daani on Tue Jan 17, 2006 at 08:00:45 AM EST

we also have a highly-developed and sophisticated technology allowing the programmer to not only communicate but automatically verify arbitrary invariants at any point in a programs execution, including entry and exit of procedures. AKA assert().

[ Parent ]
dumbass (none / 0) (#14)
by tkatchevzz on Tue Jan 17, 2006 at 10:37:22 AM EST

lol u tool

[ Parent ]
well... (none / 1) (#16)
by khallow on Tue Jan 17, 2006 at 11:07:34 AM EST

And don't forget to insert those preprocessor commands so your asserts can be optionally removed from the compiled code.

Stating the obvious since 1969.
[ Parent ]

Not really (3.00 / 2) (#18)
by Coryoth on Tue Jan 17, 2006 at 12:23:08 PM EST

Java has assert statements too, and as I point out in the article they don't provide the same expressiveness, flexibility, and elegance that can be obtained with JML (let alone the extended static checking, which assertions simply cannot provide).

While C has #ifdef for conditional compilation making adding and removing runtime assertion checking a little easier, you're still lacking a lot of the features. Much more comparable for C would be the likes of DbC for C a C preprocessor written in ruby that provides similar sorts of constructs to JML, or GNU Nana which again provides more comparable capabilities.

Jedidiah.

[ Parent ]

Purey FYI (none / 1) (#36)
by daani on Wed Jan 18, 2006 at 10:04:08 AM EST

assert() statements are not included in your binary if you compile with "-DNDEBUG". Make your assert()s as expensive as you like, you don't usually include them in a deployed version.

Compile time type-checking on the other hand, even if it is on steroids, does more or less fuck-all as far as finding programming errors goes anyway. Sure it finds a bunch of them, but not the ones that are difficult to find or persist for any length of time.

But fair enough points. I was just being a twit for a while. :)

[ Parent ]

Code length not execution time (none / 1) (#42)
by Coryoth on Wed Jan 18, 2006 at 10:56:21 AM EST

assert() statements are not included in your binary if you compile with "-DNDEBUG". Make your assert()s as expensive as you like, you don't usually include them in a deployed version.

I was more referring to the amount of code you have to write to get equivalent assert statements rather than anything to do with execution speed. JML and things like GNU Nana come with a lot of syntax for expressing assertions elegantly. In the same way that you'll want to use a regular expression library if you're doing a lot of complex text parsing, having a suitably expressive syntax for making assertions can make your life much easier.

Jedidiah.

[ Parent ]

How about for C or C++? (none / 0) (#97)
by eraserewind on Mon Jan 23, 2006 at 08:57:21 AM EST

I quite like this tool as described. I think it would be useful, but frankly I am not ever going to have a chance to use Java (or C# or Ada or Haskell) in my work. Do you know of any good similar tools for C++ or C? (or ARM assembler :) After all the usefulness of a formal specification of the higher level components must be limited if the system level doesn't specify it's API contracts formally also?

[ Parent ]
There are some options (none / 0) (#98)
by Coryoth on Mon Jan 23, 2006 at 09:18:20 AM EST

I'm not exactly an expert having not actually played with these options, but at least in terms of what is documented they look useful: GNU Nana and DbC for C both provide some reasonable support for expressive contracts in C. How good the tool support is particularly with regard to static checking, I don't know. Certainly you'll get runtime assertions, but documentation and unit testing might be unavailable. DbC for C, at least, has plans for Doxygen support and some manner of unit testing, and can be used with C++ as well.

Jedidiah.
 

[ Parent ]

Splint (none / 0) (#104)
by Julian Morrison on Thu Jan 26, 2006 at 07:56:48 AM EST

http://www.splint.org/
Seems to be much the same sort of thing.

Splint is a tool for statically checking C programs for security vulnerabilities and coding mistakes. With minimal effort, Splint can be used as a better lint. If additional effort is invested adding annotations to programs, Splint can perform stronger checking than can be done by any standard lint.


[ Parent ]
Something every Java programmer should know (1.00 / 17) (#5)
by My Other Account Is A Heterosexual on Tue Jan 17, 2006 at 05:34:27 AM EST

Your life is a meaningless dribble of putrid man-juices. You fucked up at some point and you have no hope of redemption or salvation. Do the only honourable action possible at this point - kill yourself.

We are a nation that drinks blood, and we know that there is no blood better than the blood of Jews. - some random Muslim.
these java programmers sure are a touchy bunch (none / 1) (#34)
by zombie HollyHopDrive on Wed Jan 18, 2006 at 02:28:39 AM EST





[He blew]inside..m..e.. [and verily] corrected a deviated septum and cauterized my turbinates. - MichaelCrawford
[ Parent ]
I'm afraid that when you add all the other meta (2.66 / 3) (#17)
by creativedissonance on Tue Jan 17, 2006 at 11:37:52 AM EST

that people have made available for Java (javadoc, et. al) and inline comments taboot, you'll have made a hash of your code.

that, and you've added yet another layer of commenting to maintain.  I know that in my job at least I have no time alloted in my schedule for this kind of overhead.


ay yo i run linux and word on the street
is that this is where i need to be to get my butt stuffed like a turkey - br14n

It replaces, rather than adding to, commenting (none / 1) (#19)
by Coryoth on Tue Jan 17, 2006 at 12:35:39 PM EST

that people have made available for Java (javadoc, et. al) and inline comments taboot, you'll have made a hash of your code.

It depends on how much in the way of JML annotations you want to add - and remember the annotations are part of your Javadoc documentation (at least as long as you bother to use jmldoc which support and reads all the usual Javadoc syntax). If you're really that concerned because you're writing a lot of annotations then JML has an answer for that too: You can write a separate specification file with all your JML annotations and the field and method declarations, and then simply reference that as the spec from within you implementation file. Think of it as akin to .h files from C, allowing you to have a all your declarations in a separate file from your implementation.

that, and you've added yet another layer of commenting to maintain.  I know that in my job at least I have no time alloted in my schedule for this kind of overhead.

It's not really another layer of commenting because it's replacing some of the existing layers, and because it is part of your testing regime it is commenting that is worth maintaining. In general that means your commenting is far more likely to be up to date and well maintained.

As to whether you have time for this sort of overhead... is it really that much harder to write

//@ requires input >= 0 && input <= 255

instead of

/**
* ...
* This method requires the input value to be in the range 0 to 255.
* ...
*/

Or do you simply not bother to document such things, figuring that details like that are things people should have to look through the code to find out instead of just reading the API docs?

Jedidiah.

[ Parent ]

hmm (none / 0) (#28)
by binford2k on Tue Jan 17, 2006 at 10:52:30 PM EST

I just write if(input <0 || input> 255) return -1;

Looks like that's shorter than either method. ;)

[ Parent ]

btw (none / 0) (#29)
by binford2k on Tue Jan 17, 2006 at 11:09:34 PM EST

Yes, I'm being facetious.

Still, the repetition annoys me.

[ Parent ]

And that helps how? (none / 0) (#33)
by Coryoth on Wed Jan 18, 2006 at 01:57:44 AM EST

I may well have a check in the code, but I would still bother to have something documenting what exactly is going on for anyone else who wants to use the class/module/package.

I must be missing something. Are you honestly saying "Yes, I think the only way anyone else should be able to use this class/module/package is to dig through the raw code and find all the checks I make on input parameters. Documentation is for pussies!"?

Let's be honest, regardless of how you handle invalid input in your code you still need to document what the valid inputs are for anyone else who wants to use your code. Maybe you don't use Javadoc and write all your documentation separately. So be it, that just means you'll be writing "Inputs must be in the range 0 to 255" in some other document somewhere else which will quite possibly fall out of sync with your code.

All I'm suggesting is that you may as well write the documentation at the same time as you write the code. And while you're at it you might as well write that documentation in a format that can be used for runtime checking, generating unit tests, and doing extended static checking across your entire project.

Jedidiah.

[ Parent ]

A better one: (1.00 / 14) (#23)
by V on Tue Jan 17, 2006 at 02:27:01 PM EST

java sucks.

V.
---
What my fans are saying:
"That, and the fact that V is a total, utter scumbag." VZAMaZ.
"well look up little troll" cts.
"I think you're a worthless little cuntmonkey but you made me lol, so I sigged you." re
"goodness gracious you're an idiot" mariahkillschickens

programming sucks? (2.50 / 4) (#25)
by tkatchevzz on Tue Jan 17, 2006 at 03:59:48 PM EST

but don't tell anyone

[ Parent ]
Interesting article, but JML has problems (3.00 / 2) (#30)
by GreenYoda on Wed Jan 18, 2006 at 12:49:04 AM EST

Unfortunately, heaping all this extra syntax on top of the code, especially the in-line comments, makes the code significantly harder to read, and thus may cause more errors than it prevents.

Maybe what JML needs is some kind of support in an IDE, which could display the JML in a different typeface and hide the ugly and bulky /*@ @*/ junk, or optionally hide the JML completely.

Ask and you shall receive! (3.00 / 2) (#31)
by Coryoth on Wed Jan 18, 2006 at 01:35:13 AM EST

Maybe what JML needs is some kind of support in an IDE, which could display the JML in a different typeface and hide the ugly and bulky @ @ junk

As it happens there is a JML plugin for Eclipse that provides syntax coloring for JML comments, JML keywords, etc. exactly as you suggest, making it much easier to differentiate. Even better it has integrated support for the JML tools and ESC/Java2, so you can can have all of those working for you without having to leave the comfort of your IDE. It even goes one step further and support Daikon which is a tool that uses JML annotations to try and detect likely program invariants.

...or optionally hide the JML completely.

This is also an option, and doesn't require an IDE. JML supports the ability to have the specifications in a separate file, like a header file in C, and then reference that as the specification in the implementation file with your code - that removes all the annotations from cluttering up your code.

Jedidiah.

[ Parent ]

Oh, and... (3.00 / 2) (#32)
by Coryoth on Wed Jan 18, 2006 at 01:45:08 AM EST

support in an IDE, which could display the JML in a different typeface and hide the ugly and bulky /*@ @*/ junk, or optionally hide the JML completely.

I forgot to mention that, as well as providing syntax coloring for JML, the Eclipse plugin also lets you do code folding on JML if you use block comments instead of linewise as I did for the example, for instance


/*@ requires x >= 0;
  @ ensures result > old(x);
  @ signals (Exception e) result == old(x);
  @ assignable a, b, c;
  @*/

can be suitably folded up and out of the way.

Jedidiah.

[ Parent ]

Thanks! (none / 0) (#48)
by GreenYoda on Wed Jan 18, 2006 at 02:13:35 PM EST

Since I'm an Eclipse user, this makes me want to check it out.

[ Parent ]
we need more and better (none / 0) (#35)
by bunk on Wed Jan 18, 2006 at 08:35:34 AM EST

integration between IDE's and programming languages (and associated bells and whistles like markup/meta data/documentation).

The mess in java code can get to ridiculous levels with things like javadoc and hibernate mappings.

We need programming languages designed for integration with IDE's, rather than the IDE coming in as an afterthought.  Then we will see some real advances in programming productivity.


hunger strike + bong hits = super munchies -- horny smurf
[ Parent ]

You mean... (none / 0) (#52)
by creaothceann on Wed Jan 18, 2006 at 03:55:47 PM EST

... like Delphi?

[ Parent ]
What we need (none / 1) (#87)
by Masklinn on Fri Jan 20, 2006 at 10:43:08 AM EST

are languages that don't fucking require you to use an IDE in the first place.

Java should die.



[ Parent ]
Try jman.sf.net (none / 0) (#99)
by alevin on Mon Jan 23, 2006 at 09:22:33 PM EST

Written mostly in just plain emacs and jed.
--
alevin
[ Parent ]
Evil (3.00 / 6) (#37)
by tmenezes on Wed Jan 18, 2006 at 10:10:26 AM EST

I have been programming in all sorts of languages for the last 15 years so depite being 29 I think I might consider myself a veteran. I have a degree in computer sciences so I learned and used all sorts of quality control techniques. I became a sceptic. I think people waste way to much time with stuff that in the end does a worst job than:
  • good design;
  • good code style;
  • api documentation generator (doxygen, javadoc, whatever);
  • developers who are not afraid of reading code;
  • thorough testing (yes I like regression testing);
It is my opinion that most of this quality control techniques are created to hide the sympthoms when the real diseases are:
  • marketing types in charge of development / creative processes
  • buzzword-driven technological decisions
  • factory style (as oposed to talented based) development
  • language fundamental limitations (yes I don't like Java that much, and yes I developed in it a lot)
Good developers are intelligent, hard-working, talented people with a passion for creation. People who tend to climb corporate ladders are not. Big software houses don't like to give power to the former class of citizens so they dream of a software factory where development work is like a 19th century industrial nightmare and developers are fully disposable. That's why they promote this kind of drivel. It allways fails.

Academia is to blame too (none / 1) (#38)
by Hung Fu on Wed Jan 18, 2006 at 10:21:58 AM EST

Computer science professors love teaching formal methods and specification languages to students because it's easier than teaching more useful abilities like good design skills.

__
From Israel To Lebanon
[ Parent ]
Good point (none / 0) (#41)
by tmenezes on Wed Jan 18, 2006 at 10:49:00 AM EST

Some teachers can't teach real design and programming skills because they never had them themselves. It allways amused me how some of them babble about "real world" and "complex systems" when they never been in touch with any of them.

[ Parent ]
Formal/specification languages solve some problems (none / 0) (#44)
by lukme on Wed Jan 18, 2006 at 11:02:04 AM EST

Unfortunately, they are usually complex and you cannot generate code from any that I have heard of - so you wind up writing things twice. Most employer (here in the US) believe that this alone makes it worthless.




-----------------------------------
It's awfully hard to fly with eagles when you're a turkey.
[ Parent ]
Formal specification (none / 0) (#47)
by Coryoth on Wed Jan 18, 2006 at 12:36:26 PM EST

If you're programming in Java then you're already using formal specification. Every time you write a type signature for a method, or declare the type of a variable you are formally specifying your code. You are providing, with type signatures, explicitly specified constraints on the input parameters and the return value. Every time you declare a variable you are providing specification hinting so that the type checker, which is really just a theorem prover, can do its job.

JML (and other similar specification schemes) simply provides additional specification syntax letting you be more specific in your requirements. With more specificity comes far more powerful theorem provers like ESC/Java2 which can catch errors that type checking never can, and that would only show up through extensive exhaustive testing. The difference between JML and type declarations is that JML is optional. You can add as much or as little extra specification as you care to.

Jedidiah.

[ Parent ]

Meh... Type verification is low bar for success. (none / 0) (#63)
by skyknight on Wed Jan 18, 2006 at 10:53:31 PM EST

I would argue that it actually encourages sloppier code by having developers lean on the compiler to prove the correctness of their code. There's not much that strong typing gives you that isn't a subset of what you get from having good automated tests that you run regularly.

It's not much fun at the top. I envy the common people, their hearty meals and Bruce Springsteen and voting. --SIGNOR SPAGHETTI
[ Parent ]
That would be the point... (none / 0) (#65)
by Coryoth on Wed Jan 18, 2006 at 11:03:03 PM EST

Type verification is nice, but it isn't that strong. Extended static checking (which goes way beyond just type verification) catches a lot of errors that you'll be doing very exhaustive testing to find. Hell Esc/Java2 can even do space and time constraint checks statically if you provide the requirements (for which JML kindly provides suitable syntax).

Static checking, even just type checking, has another advantage too - it's available to other developers who are making use of your code libraries . It provides easy checks that they are using you code correctly without forcing them to write a whole series of new tests for themselves.

Jedidiah.

[ Parent ]

And...? (none / 0) (#43)
by Coryoth on Wed Jan 18, 2006 at 11:01:52 AM EST

Think of JML as a way to add appropriate (as in, what you would expect to be documenting anyway) extra information to your API docs, that has a whole bunch of side benefits for error checking, and testing (including automatically building your testing framework).

There's really no work here that you wouldn't already being doing, presuming you do bother to actually produce useful API documentation, and in return you get automatic testing.

I'm not sure I see your problem.

Jedidiah.

[ Parent ]

The problem (3.00 / 2) (#45)
by tmenezes on Wed Jan 18, 2006 at 11:29:24 AM EST

The problem is that it makes the code much harder to read. Despite current popular beliefs, good code is self-documenting. Intoducing another layer of syntatic sugar instead of solving the real problem is a horrible hack. The problem of producing good API documentation is long solved by tools like doxygen or javadoc with the help of non-intrusive comment headers. Too much information is not necessarily a good thing. If you are a user of the class, standard API documentation is enough. If you are a developer of the class, good code and good design documents are what you need. Granted that most software is horrible to look inside but in this case bad developers and management are usually to blame. I don't see how JML is going to solve this. If you do get automatic and sufficient testing for free you might have a point. Problem is that I don't believe it. I have yet to see one of this schemes scale to heterogeneous real world situations without creating more work than you'd need in the first place. I might be wrong, I'm just sceptic based on previous experience.

[ Parent ]
I don't see your real issue. (none / 0) (#46)
by Coryoth on Wed Jan 18, 2006 at 12:29:39 PM EST

The problem is that it makes the code much harder to read.

Is it really that much harder? Given appropriate syntax highlighting like in JMLEclipse it mostly gets out of your way visually.

The problem of producing good API documentation is long solved by tools like doxygen or javadoc with the help of non-intrusive comment headers.

And for 99% of the JML annotations you'll add they'll be non-intrusive comment headers just like Javadoc - they are Javadoc comments really, in that they are included in the Javadoc API documentation produced by jmldoc. If Javadoc comment headers are fine, how exactly is JML bad? All you're doing is changing the bit in the Javadoc header where you would have written

* the method requires that ...

to

//@ requires ...

And yes JMLEclipse supports code folding for blocks on JML annotations, so you can fold them out of the way if you don't want to look at them. You seem to be complaining about a largely imaginary problem.

If you do get automatic and sufficient testing for free you might have a point.

The sufficiency of your automatically generated testing is defined by the sufficiency of your statement of requirements. But then that's always been true - unless you define how something is supposed to behave it is impossible to know when it is not behaving correctly.

If you're writing annotations seriously with an eye to correct code and heavy use of ESC/Java2 to catch all the subtle errors then yes the generated tests will most likely be sufficient.

If you're just writing a few annotations to outline your intent for what the code should do then the generated test probably won't cover all the behaviour you want to proscribe. That just means you have to write a separate unit test to test the rest of the behaviour - which you would be doing anyway.

Whether you're writing a lot or a little in the way of annotations, the annotations, due to the expressive syntax are (1) easier (and faster) to write and (2) easier to read; than a separate test class. Even getting some of your testing generated for free is surely a good thing?

And then there's the issue of ESC/Java2, which is not testing but can catch a lot of errors that would previously have only shown up through exhaustive testing. ESC/Java2 is great for catching the odd corner cases, the subtle coding errors in complex methods, and other things that testing is often not so good at. I think it would be worth your while, if you're actually doing a lot of Java coding, to spend some time learning about what ESC/Java2 can actually do.

Jedidiah.

[ Parent ]

no, the problem is that americans are stupid (1.00 / 2) (#49)
by tkatchevzz on Wed Jan 18, 2006 at 03:19:23 PM EST

and ignorant.

most notably, the american cs culture precludes the understanding of the concept of 'layers of abstraction', so indeed you get the crap you get in the end.

look at the idiotically unfunny joke that is lisp for a slap-in-your-face example.

import some frenchman to do things properly for you, for God's sake already.

[ Parent ]

Is this a joke? (2.66 / 6) (#39)
by claes on Wed Jan 18, 2006 at 10:26:51 AM EST

Seriously, that's what I first thought.

Java syntax is on the very edge of being too verbose (some would argue way beyond the edge). You're proposing adding all this "noise" to the code. Plus it's stuff that people should maintain but don't.

Your code should be like a story that people can actually read. The meat of the story should be in the code itself, where the variable, class, and method names explain as best they can what's going on. Directory structure and file names provide the volume and chapter headings. Comments serve as guide posts to show either overall structure or point out a particularly hairy bit. If you've done a good job people will be able to sit down and read the code and figure out what the hell is going on, and if you're really good get a laugh or at least a smile out of it.

If the story is easy to follow, you've got a good architecture. If it's hard to follow you've got a bad design.

It's kind of like the saying about planes "Looks Good, Flys Good".

Anyhow, I guess it isn't a joke. Thanks for writing this up, it may be useful to some people.

-- claes

Not a joke at all. (none / 1) (#50)
by Coryoth on Wed Jan 18, 2006 at 03:33:47 PM EST

Java syntax is on the very edge of being too verbose (some would argue way beyond the edge). You're proposing adding all this "noise" to the code. Plus it's stuff that people should maintain but don't.

Well it's only "noise" in the way that Javadoc is "noise". You get to replace a lot of what you would have written as plain English text in Javadoc comments with slightly more formal JML comments - which will still get included in the final Javadoc generated API documentation when you use jmldoc. Grab a decent Java IDE like Eclipse and load up JMLEclipse and you get syntax highlighting and code folding that removes a lot of the "noise" aspect.

As to maintaining it - in some sense that's the point: by making it part of your testing (as in your tests will fail if you update the code but not the JML associated with it) it forces you to keep your documentation up to date - which is a good thing!

Your code should be like a story that people can actually read. The meat of the story should be in the code itself, where the variable, class, and method names explain as best they can what's going on.

Exactly. JML is not some cure for poor design and coding habits, it's meant to supplement and expand on good design and coding habits, helping you catch your mistakes. Instead of trying to pack the whole story into the method name you can give a brief outline of the story in a JML comment header. More importantly JML provides you with the sort of expressive syntax that makes it easy to outline the story succinctly yet concisely. The benefit you get for outlining said story in a little more detail than just the method name is not just better documentation, but better testing and debugging, and far, far better static checking. If you put in some work at the beginning in annotations you save yourself work in documentation, writing unit test classes, and debugging your code.

And please note, as I said in the introduction, I am not claiming that this is some magic cure all to be applied to all Java projects. What I am claiming is that it does a sufficiently good job of doing a lot of work for you that it's bound to be useful for some projects... and that makes it worth knowing about so you can use it when the sort of project that can benefit does come up.

Jedidiah.

[ Parent ]

obfuscation rules (none / 1) (#103)
by oki on Wed Jan 25, 2006 at 07:18:04 PM EST

as a bit of a perl evangelist I often take flac from people bagging perl because of its unreadability (regexes, html, pod all mixed together etc..)
I think this is a positive step to bring perls powers of obfuscation to java
Well done :)

However IANAJP, just a dabbler so maybe this makes more sense to other people

This sig intentionally not left blank
[ Parent ]
Good point (none / 1) (#40)
by tmenezes on Wed Jan 18, 2006 at 10:46:56 AM EST

Some teachers can't teach real design and programming skills because they never had them themselves. It allways amused me how some of them babble about "real world" and "complex systems" when they never been in touch with any of them.

Standards (3.00 / 3) (#53)
by gidds on Wed Jan 18, 2006 at 05:57:20 PM EST

Why doesn't JML use the standard @annotation format? It seems designed for exactly this sort of thing, and might remove the need for a separate copmiler, or at least let JML-instrumented code work better with standard compilers and tools.

Similarly, why doesn't it use the standard assertions system? The "hoops you have to jump through" are hardly taxing, and let you do stuff like avoiding separate developer builds and enabling assertions in the field, that JML can't support.

My other first reaction is that, while JML may indeed be about commenting stuff you'd comment anyway, given the choice you wouldn't have to put half of those comments in the middle of the code, which makes both comments and code far harder to read. (Even with syntax colouring.)

JML looks like a great idea, but I can't help thinking the implementation isn't quite there yet.


Andy/

Re: Standards (none / 1) (#57)
by Coryoth on Wed Jan 18, 2006 at 09:03:29 PM EST

Why doesn't JML use the standard @annotation format?

JML was originally developed well before any such thing was available. If there's interest I expect some sort of integrated system could be developed, but for now it is what it is.

The other point is that JML has become somewhat of a standard as it is. When it comes to specification of Java code JML seems to have become the standard language for anyone developing tools the leverage specification, and there are a lot:


  • ESC/Java2 for extended static checking.

  • Daikon an invariant detetctor.

  • SpEx a model checker, with a eye toward concurrency issues.

  • Krakatoa which connects JML with the Coq proof assitant tool.

  • KeY a verification tool and theorem prover for Java Dynamic logic.

And I believe there are others. In practice JML got standardised on first, and while taking advantage of new things in the Java language itself would be good, it will take effort to make that shift.

Similarly, why doesn't it use the standard assertions system?

The annotations are converted into assertions when compiled, the reason for having JML in general is to  provide a much more powerful, expressive and intuitive format for the sort of assertions that are common when doing Design by Contract and formal specification. JML actually comes with a assert of it's own, the only difference from standard Java asserts being that you have the full JML syntax with which to express the property that you are asserting. If it's not clear why JML is better than standard assertions then you really should read through some of the JML reference manual to see exactly what the syntax actually offers - what is demonstrated in the example in the article is only a small taste to give the general idea of what things look like.

given the choice you wouldn't have to put half of those comments in the middle of the code, which makes both comments and code far harder to read.

It is, perhaps, my fault that the example came out the way it did, I was trying to show a reasonable range of features. In practice most JML comments are going to be in headers to methods rather than than in the code. The example is, perhaps, not very representative.

JML looks like a great idea, but I can't help thinking the implementation isn't quite there yet.

I would certainly agree that there is room for improvement. Personally I think the specification language shouldn't be pushed into the state of being comments - I'd much rather see it fully integrated into the programming language (the same why type specification is). You can get that with, for instance Eiffel or D, but those languages have their own issues (mostly lack of widespread use).

Barring a new programming language we have to use what we have however, and certainly if you're using Java then JML is far and away the best thing on offer in terms of providing the sort of functionality that it does. No, it's not perfect, but it is very good given the circumstances, and regardless of lack of perfection in implementation I assure you it is quite practical to use. That is, it gets the job done, and well.

Jedidiah.

[ Parent ]

Um (2.00 / 4) (#54)
by trhurler on Wed Jan 18, 2006 at 07:48:27 PM EST

That's not a modelling language at all. That's a really poor attempt to give Java the advantages of Eiffel, and it completely fails. Just another lame comment-annotation tool that results in code that doesn't match comments in real world settings. Garbage. Bah.

--
'God dammit, your posts make me hard.' --LilDebbie

Real men don't comment their code. $ (none / 1) (#55)
by skyknight on Wed Jan 18, 2006 at 08:04:11 PM EST



It's not much fun at the top. I envy the common people, their hearty meals and Bruce Springsteen and voting. --SIGNOR SPAGHETTI
[ Parent ]
Real code comments MEN! $ (none / 1) (#56)
by trhurler on Wed Jan 18, 2006 at 08:54:56 PM EST



--
'God dammit, your posts make me hard.' --LilDebbie

[ Parent ]
I believe that you forgot... (none / 0) (#58)
by skyknight on Wed Jan 18, 2006 at 09:15:53 PM EST

"in Soviet Russia"...

More seriously, though, I personally dislike commenting code as I deem it a crutch, used in lieu of re-structuring it to be more human readable, and a Faustian bargain because, as you note, it's a fundamentally difficult problem to keep code and comments in sync. It's better to actually take the time to make your stuff human readable.



It's not much fun at the top. I envy the common people, their hearty meals and Bruce Springsteen and voting. --SIGNOR SPAGHETTI
[ Parent ]
There is a difference... (none / 0) (#60)
by Coryoth on Wed Jan 18, 2006 at 09:25:32 PM EST

There is a difference between comments to explain what overly complex or poorly written code is doing, and comments that describe the intended behaviour of code.

Readable code is, I agree, something to be aspired to. That's one of the strong points of Eiffel and Ada and Python: they try to encourage you to write clear readable code. And readable code is certainly self documenting if written well. The problem is that the code only documents what it does and completely fails to document what it is intended to do. Without ever documenting what is upposed to happen it is impossible to tell whether code is actually working or not - there is no definition of working, so whatever it does is "correct".

That is fine, of course, if you always write 100% correct bug free code that always does exactly what you intend it to do in all cases... For those of us that are human it can be helpful to document what the expected behaviour actually is - not to clarify what the code is doing, but so that we can tell when it is not actually working or being used as intended.

Jedidiah.

[ Parent ]

I disagree... (none / 0) (#61)
by skyknight on Wed Jan 18, 2006 at 10:37:07 PM EST

If you name a function well, this goes a long way toward making its intent evident. If you add parameter validation code, this illustrates expectations about arguments. If your class member variables' names are good, then side effects should be evident. Yes, you can make mistakes, but you can just as well also let your documentation drift out of sync, and that strikes me as a much more likely danger. If you can't describe what your function does clearly in a one-liner, then there's probably a problem.

Also, while we're at it, I would argue that specifying the intent of a function is best accomplished by well written regression testing suites. If done artfully, test suites are living and executable documentation of the expected behavior of your code. This is the kind of "documentation" that keeps you honest, because when it drifts you're apt to find out in a noisy way.

That being said, I do like the idea of programming by contract when it's properly integrated into the language. Alas, I find most languages' attempts to retrofit it disappointing because they drop the ball on inheritance.



It's not much fun at the top. I envy the common people, their hearty meals and Bruce Springsteen and voting. --SIGNOR SPAGHETTI
[ Parent ]
re: Disgree... (none / 0) (#66)
by Coryoth on Wed Jan 18, 2006 at 11:15:56 PM EST

If you name a function well, this goes a long way toward making its intent evident.

I would suggest there are pretty significant limits on what you can say in a function name unless you're making them huge. Giving a vague idea of intent is nice, but that hardly clearly delineates correct from incorrect behaviour.

If you add parameter validation code, this illustrates expectations about arguments.

Wow, another person in the "Everybody should have to pick through my source code by hand to use any of it" camp. Do you use API docs other people write, or do you just read through every single source file to see what's required and what a function is supposed to do? Or, more to the point I guess, do only really write code that you yourself will have to use and maintain?

Yes, you can make mistakes, but you can just as well also let your documentation drift out of sync

Given that as soon as your documentation is out of sync all your unit tests will fail... I think you'll go back and see what happened to the documentation. Besides, this is a pure argument from laziness: "I'm pretty sure I can't be assed actually writing and maintaining documentation... I mean that's not really part of the development process is it?"

Also, while we're at it, I would argue that specifying the intent of a function is best accomplished by well written regression testing suites.

Yes, because a whole lot more code in a language not designed for specification is a much better way to define behaviour than a set of clear and concise statements in a specification language. And of course the test suite will be automatially added to the documentation right? I mean you are, in essence simply documenting with a test suite of code. If you can claim my documentation (which, remember, defines the tests) can drift out of sync then surely your test suite can drift out of sync? Your trying to straddle here - either both are going to be kept in sync, or both are equally capable of falling out of sync.

This is the kind of "documentation" that keeps you honest, because when it drifts you're apt to find out in a noisy way.

Right... just as when thr JML specification drifts out of sync all your tests will fail in a noisy way. Make up your mind.

That being said, I do like the idea of programming by contract when it's properly integrated into the language. Alas, I find most languages' attempts to retrofit it disappointing because they drop the ball on inheritance.

So out of curiousity, exactly how does JML fail with regard to inheritance? Have you actually read any of the documentation on it? Perhaps you should try.

Jedidiah.

[ Parent ]

Here's the thing... (none / 0) (#67)
by skyknight on Thu Jan 19, 2006 at 06:55:08 AM EST

Documenting code for people who will be doing development work on it and documenting code for people who will be using its published API are fundamentally different tasks. If you conflate them, you're almost guaranteed to do both poorly. Information that is necessary for a developer will mire a client in needless detail, and information that is adequate for a client will leave a developer needing more. A client wants a quick snapshot with which he can get up and running or refresh his memory and in most cases doesn't give a rats ass about class invariants. One of the major purposes of OO-style coding is that implementation is hidden behind APIs, is it not?

Developers should read source code before working on a piece of code. If the code is laid out in an artfully hierarchical fashion, then you can read things at the right level of detail, drilling down as far as you need. Your characterization of this as having to pick through source code tediously is a straw man. Unless you've done something wrong, locating the code of interest ought to be like traversing down a tree structure, something that is reasonably painless.

As you may have noticed, the very best documentation provides code snippets that quickly characterize how to use the API that a module exports. If you write your tests with the same degree of professionalism that you write your application code, then you simultaneously serve two needs, putting your code through its paces to provide guarantees about its correctness, and giving the client executable code that he knows works because he saw it running in the test harness.

Also, if you had read my comment with a cooler head, you'd note that I didn't say that JML failed on inheritance.



It's not much fun at the top. I envy the common people, their hearty meals and Bruce Springsteen and voting. --SIGNOR SPAGHETTI
[ Parent ]
JML specs are better "documentation" (none / 0) (#71)
by GileadGreene on Thu Jan 19, 2006 at 03:46:15 PM EST

If you name a function well, this goes a long way toward making its intent evident.

Perhaps, but it goes nowhere towards permitting automatic verification that the actual code produces the intended behavior.

If your class member variables' names are good, then side effects should be evident.

Hopefully. But again, does the actual effect correspond to the intent?

but you can just as well also let your documentation drift out of sync, and that strikes me as a much more likely danger

Not if your documentation is automatically being checked by the JML static checking tools - that's the whole point.

Also, while we're at it, I would argue that specifying the intent of a function is best accomplished by well written regression testing suites. If done artfully, test suites are living and executable documentation of the expected behavior of your code. This is the kind of "documentation" that keeps you honest, because when it drifts you're apt to find out in a noisy way.

So in other words you favor a style of documentation that's just like a JML spec, except that it's written in a language that isn't intended for specification (and is thereby harder to read), can only cover a limited subset of cases (versus a full static check), and lacks the expressive power of JML (which has things like quantifiers). Sounds great to me. Really. Not to mention the fact that JML integrates with jUnit, so unit tests can be derived from the JML specs...

[ Parent ]

Er... (none / 0) (#74)
by trhurler on Thu Jan 19, 2006 at 08:46:55 PM EST

Seriously, you need to read up on the limitations of static checking. It is impossible in principle, let alone in reality, to statically determine the meaning of a program written in any modern programming language and/or running on any modern CPU.

--
'God dammit, your posts make me hard.' --LilDebbie

[ Parent ]
After that he can tackle the halting problem.$ (none / 0) (#75)
by skyknight on Thu Jan 19, 2006 at 09:10:27 PM EST



It's not much fun at the top. I envy the common people, their hearty meals and Bruce Springsteen and voting. --SIGNOR SPAGHETTI
[ Parent ]
I solved the halting problem (none / 1) (#79)
by trhurler on Thu Jan 19, 2006 at 09:57:46 PM EST

Someone said "I can't tell when or if my algorithm will terminate!" I said "shut up and suck my dick, bitch!" She did. Nobody thereafter actually cared when her algorithm would terminate.

--
'God dammit, your posts make me hard.' --LilDebbie

[ Parent ]
Did she halt? $ (none / 0) (#80)
by skyknight on Thu Jan 19, 2006 at 10:01:19 PM EST



It's not much fun at the top. I envy the common people, their hearty meals and Bruce Springsteen and voting. --SIGNOR SPAGHETTI
[ Parent ]
Some time later, yes (none / 0) (#82)
by trhurler on Thu Jan 19, 2006 at 10:07:32 PM EST

But then I told her what I'd do if she didn't start up again.

--
'God dammit, your posts make me hard.' --LilDebbie

[ Parent ]
She must have made you NP hard. $ (none / 0) (#85)
by skyknight on Fri Jan 20, 2006 at 06:44:18 AM EST



It's not much fun at the top. I envy the common people, their hearty meals and Bruce Springsteen and voting. --SIGNOR SPAGHETTI
[ Parent ]
Yeah (none / 0) (#90)
by trhurler on Fri Jan 20, 2006 at 08:08:12 PM EST

The rest was a story of sockets and ports and so on.

--
'God dammit, your posts make me hard.' --LilDebbie

[ Parent ]
Er... (none / 0) (#76)
by GileadGreene on Thu Jan 19, 2006 at 09:21:48 PM EST

Seriously, you need to read up on what the ESC/Java static checker can do with JML specifications. Yes, it is "impossible ... to statically determine the meaning of a program written in any modern programming language". However, that does not mean that it's impossible to statically verify that a given program will meet specifications written in JML: there is a big difference between "the meaning of a program" in general, and the specific properties that are expressible in JML.

Now, granted, the static checking provided by ESC/Java isn't perfect. But it's a helluva lot better than the complete lack of static checking provided by well-named functions and methods (which is not to say that you shouldn't have well-named functions and methods - belt and suspenders) or natural language comments. The fact that JML integrates well with jUnit, facilitating testing for those properties that are impossible to statically check, is just gravy.

[ Parent ]

Uhuh. (none / 1) (#59)
by Coryoth on Wed Jan 18, 2006 at 09:16:46 PM EST

That's not a modelling language at all. That's a really poor attempt to give Java the advantages of Eiffel, and it completely fails.

I know I'm being trolled, but I may as well make a few comments.

The real advantages of Eiffel for me are its clean syntax and design sense, and nice things like agents. Design by Contract integrated into the language is certainly a very nice thing indeed, but there are other languages that have that. Besides, the degree of language integration is actually not all that crucial. As far as having suitable DbC syntax JML is more than adequate, and the runtime assertion checking is identical to what Eiffel or D will offer. On the other hand JML has syntax for more than just pre- and post-conditions and invariants, and allows for proper extended static checking which Eiffel doesn't offer.

As to whether it is a modelling language - I hate to inform you but if you read through the JML reference manual I think you'll find that JML actually provides a full formal specification language for modelling, and you can even get model checkers for JML.

Keep up the trolling.

Jedidiah.

[ Parent ]

I disagree... (none / 0) (#62)
by skyknight on Wed Jan 18, 2006 at 10:44:51 PM EST

Besides, the degree of language integration is actually not all that crucial.

What you're missing is the benefit you get by having everyone use a standard set of mechanisms, and it's hard to guarantee that short of having it integrated into the language. For any given feature you can always argue that it can be retrofitted to an existing language, but that's never as nice as having it be integrated formally. For instance, consider exceptions in Perl versus exceptions in Java. Yes, there are ways to do exceptions in Perl, but there are tons of different ways, and everyone does them a little bit differently. Contrast this with Java which does them in one way that is built into the language.



It's not much fun at the top. I envy the common people, their hearty meals and Bruce Springsteen and voting. --SIGNOR SPAGHETTI
[ Parent ]
And JML is standard (none / 0) (#64)
by Coryoth on Wed Jan 18, 2006 at 10:56:22 PM EST

JML pretty much is the standard for specification of Java programs - at least as far as tool support goes. It would be nice if it was built into the language I agree (I don't think I ever disputed that), but I don't think it's crucial. There is a standard way to do formal specification for Java, what more do you want?

Jedidiah.

[ Parent ]

Er... (none / 0) (#73)
by trhurler on Thu Jan 19, 2006 at 08:45:43 PM EST

Eiffel was invented primarily as a vehicle for contract programming. Whatever else you may like about it is incidental.

As for modelling languages, the JML reference manual's redefinition of preexisting terms notwithstanding, JML does not consist of modelling - period.

--
'God dammit, your posts make me hard.' --LilDebbie

[ Parent ]
Static checking (none / 0) (#69)
by GileadGreene on Thu Jan 19, 2006 at 02:41:07 PM EST

Just another lame comment-annotation tool that results in code that doesn't match comments in real world settings.

Except that that static checking that is part of the JML suite will detect when code and "comments" are out of sync. Then you can take a look at the code and the "comments" that have been flagged, decide which is correct, and make the appropriate fixes. If the JML static checking is part of your development cycle in the same way that many people use unit testing, then the "code and comments out of sync" problem goes away.

[ Parent ]

Um (none / 0) (#72)
by trhurler on Thu Jan 19, 2006 at 08:44:21 PM EST

If in fact static checking is adequate, then the static checker should be able to GENERATE the comments from the code, in which case it is stupid for me to do so. If it isn't adequate, then you should STFU.

--
'God dammit, your posts make me hard.' --LilDebbie

[ Parent ]
Um (none / 0) (#77)
by GileadGreene on Thu Jan 19, 2006 at 09:40:50 PM EST

The problem is that there's no way to infer intent from an analysis of code. At best, a static analysis of the kind you seem to be asking for could generate something that will tell you what the code actually does. But those generated comments aren't going to be worth much: there's little gain to be had there over just executing the code. You still need to look at the description that's been generated to see if it does "the right thing" (i.e. what you intended it to do).

What you need is a definition of what the code is intended to be doing (i.e. a specification). That's what the JML annotations (what you are dismissing as comments) are for. The point of static checking against the JML annotations is to verify that what the code does actuall matches your intent (in the same way that static type-checking verifies that your use of variables matches the corresponding type definitions). Take the JML annotations out of the picture, and there's very little point to the whole static-checking exercise, since there's nothing to verify the code against (aside from whatever informal specs you have in your head).

[ Parent ]

I see (none / 0) (#78)
by trhurler on Thu Jan 19, 2006 at 09:56:22 PM EST

Even if I believed all this(and you can probably tell I don't,) why then wouldn't I just take the specification of intent and generate the code? Oh, because it doesn't really capture the intent. That's right.

--
'God dammit, your posts make me hard.' --LilDebbie

[ Parent ]
Er... (3.00 / 2) (#84)
by GileadGreene on Thu Jan 19, 2006 at 11:11:35 PM EST

Or perhaps because it is far easier (in general) to check whether a given algorithm satisifies a given specification than it is to generate an algorithm that satisfies the specification in question. That said, there has been some work on generating code from specific types of formal specs, but it's still research, and isn't applicable to general software development.

[ Parent ]
The intention of the code... (none / 0) (#81)
by skyknight on Thu Jan 19, 2006 at 10:03:30 PM EST

is specified in the code. That's why you bothered with writing it.

It's not much fun at the top. I envy the common people, their hearty meals and Bruce Springsteen and voting. --SIGNOR SPAGHETTI
[ Parent ]
Through the Looking Glass (none / 0) (#83)
by GileadGreene on Thu Jan 19, 2006 at 10:19:24 PM EST

'When I use a word', said Humpty Dumpty in rather a scornful tone, 'it means just what I choose it to mean - neither more nor less.'
(Lewis Carroll, Through the Looking Glass)

[ Parent ]
Well, sure... (none / 0) (#86)
by skyknight on Fri Jan 20, 2006 at 06:46:19 AM EST

There's ambiguity as to what you can call code, but the point still stands. You can't fully spec code's behavior with a modeling language, because otherwise that modeling language would be Turing complete and you'd have obviated writing anything more.

It's not much fun at the top. I envy the common people, their hearty meals and Bruce Springsteen and voting. --SIGNOR SPAGHETTI
[ Parent ]
Specification != Implementation (none / 0) (#88)
by GileadGreene on Fri Jan 20, 2006 at 11:06:45 AM EST

There is a difference between specification and implementation. In a nutshell, specification describes how to recognize correct results, while implementation describes how to get correct results. It's entirely possible to specify what a result should be, without describing how to achieve the result (trivial example: the specification of sqrt(x) is that sqrt(x) * sqrt(x) = x - which tells you absolutely nothing about how to compute sqrt(x)).

Let me put this another way: after you have written your code, do you test it? If so, how do you know that the tests have passed? Answer: because you have some criteria for judging what constitutes a correct result. In other words, you have a specification. Possibly an informal one. Possibly kept only in your head. But nevertheless a specification.

As an aside, the Turing completeness (or lack thereof) of a specification language really has no bearing on the issue. A specification describes different things than an implementation. A simple example is something like unit tests written using jUnit. The tests are written in Java. They constitute a specification (i.e. a description of desired outcomes). And yet there's still a need for an implementation to be written. Also in Java. Same language, two different uses.

[ Parent ]

Sort is a good example (none / 1) (#89)
by Coryoth on Fri Jan 20, 2006 at 01:32:46 PM EST

I always thought sort function on an array or list is a good example of the difference. It's easy to specify a sort function: you want an element to be in the result list if and only if it is in the input list, and you want the result to satisfy some order ">". In JML you would have something like


//@ require input instanceof ArrayList
/*@ ensure result.contains(x) <==> input.contains(x) &&
  @         (forall int i; 0 < i && i < result.size(); result.get(i-1) <= result.get(i))
  @*/

Which is a specification for sort, but doesn't tell you anything about how it is implemented - you have many many options for that.

[ Parent ]

such as implementing it in Prolog $ (none / 0) (#91)
by skyknight on Fri Jan 20, 2006 at 09:53:15 PM EST



It's not much fun at the top. I envy the common people, their hearty meals and Bruce Springsteen and voting. --SIGNOR SPAGHETTI
[ Parent ]
Prolog still requires implementation beyond spec (none / 0) (#96)
by Coryoth on Sat Jan 21, 2006 at 04:12:50 PM EST

An implementation in Prolog is still going to be an implemetation and contain specifics of implementation detail not found in a spec such as I gave. The spec simply tells you what the function does, to provide a working implementation, even in a declarative language, requires you to provide details of how to do it. Take a look at Quicksort in Prolog.

It is very often possible to describe what a function does without having to provie any details about how to do it. In fact mathematics does that all the time.

Are you being deliberately obtuse and missing the point, or do you honestly not understand the difference between "what" and "how"?

Jedidiah.

[ Parent ]

Just barely... (none / 0) (#100)
by skyknight on Mon Jan 23, 2006 at 11:01:53 PM EST

You can more or less define a "sort" routine in Prolog as "an ordering such that all elements are greater than or equal to their preceding element". It's almost as good as quantum computing, except that it's intolerably slow.

It's not much fun at the top. I envy the common people, their hearty meals and Bruce Springsteen and voting. --SIGNOR SPAGHETTI
[ Parent ]
That would be bogosort (nt) (none / 1) (#101)
by Coryoth on Tue Jan 24, 2006 at 12:43:45 AM EST



[ Parent ]
I'm sold. (3.00 / 3) (#68)
by OzJuggler on Thu Jan 19, 2006 at 07:00:41 AM EST

I'm going to try using it in my current project.

Having said that, I'm well aware of the old statistic that 40% of major software projects fail, and most of the time its because of insufficient or inconsistent software requirements - so a formal spec for a 3rd gen programming language will not help you succeed because by the time you start coding the seeds of destruction may already be sown.

But at least 60% of projects do succeed and if a formal spec lets you prevent or detect bugs faster then not only can you deliver something that works properly, you might even be on time too!

Formal specs for programs are usually a waste of time because a typical programmer doesn't make too many mistakes and with stack traces can fix the bugs fairly easily. Also the separation of the spec modelling language from the implementation language makes you feel like you're having to code it twice. And also, let's get real, most business software isn't exactly complicated.

This JML eliminates nearly every excuse I have ever had against using some of the Z-spec theory I was taught back in Uni. So I'm gonna try it out.

The only excuse I have left is that it doesn't seem to cater for multithreaded methods. If your precondition is met at the top and all the other invariants along the way are okay, but somewhere in the middle an object you're reading is changed by another thread, you could still end up not satisfying the method postcondition. On spec it should work, but in practice it won't. How can JML help in that case??

- OzJuggler.
"And I will not rest until every year families gather to spend December 25th together
at Osama's homo abortion pot and commie jizzporium." - Jon Stewart's gift to Bill O'Reilly, 7 Dec 2005.

Apples, oranges, and formal specification (none / 1) (#70)
by GileadGreene on Thu Jan 19, 2006 at 03:24:39 PM EST

...most of the time its because of insufficient or inconsistent software requirements - so a formal spec for a 3rd gen programming language will not help you succeed because by the time you start coding the seeds of destruction may already be sown.

Bingo. There's a difference between requirements and specifications (and between specifications and design). What formal spec does is push the formality back from the actual code, and into the specification - which makes it easier to catch bugs earlier, and more likely that the transition from spec to code will proceed without introducing additional errors. It's not going to help with finding incorrect or incomplete requirements, because requirements definition necessarily deals with the an informal world.

Formal specs for programs are usually a waste of time because a typical programmer doesn't make too many mistakes and with stack traces can fix the bugs fairly easily.

There's a difference between specification and design (or implementation). A specification codifies intent (sqrt: sqrt(x) * sqrt(x) = x), while a design codifies a method (insert algorithm for computing a square root here). The point of tools like JML is to automatically check that the design behaves in accordance with the intent. It's primarily there to help you determine whether or not bugs exist (although it may also help with diagnosing the cause of the bugs, by helping you pinpoint which part of the spec is being broken).

Also the separation of the spec modelling language from the implementation language makes you feel like you're having to code it twice.

If you're "writing it twice" then you're not writing a specification, you're using a specification language to write a design. That will, of course, seem like a total waste of time. But it doesn't negate the usefulness of specification langauges when they are correctly used.

And also, let's get real, most business software isn't exactly complicated.

Ironically, the last time Coryoth posted a story on formal specification one of the objections raised was that business logic was too complex for formal specification.

The only excuse I have left is that it doesn't seem to cater for multithreaded methods. If your precondition is met at the top and all the other invariants along the way are okay, but somewhere in the middle an object you're reading is changed by another thread, you could still end up not satisfying the method postcondition. On spec it should work, but in practice it won't. How can JML help in that case??

JML is principally designed for sequential specification, so it doesn't deal with threads. However, you might want to look at the recent paper Extending JML for Modular Specification and Verification of Multi-Threaded Programs.

[ Parent ]

You're boring, wrong, and irrelevant. (1.33 / 3) (#93)
by OzJuggler on Fri Jan 20, 2006 at 10:47:55 PM EST

Bingo. There's a difference between requirements and specifications (and between specifications and design).
Knowledge isn't a fucking lucky draw prize, dickhead. Insulting other developers is a strange way for you to foster support for better software processes.

Specification is just a word that means diferent things in different contexts. Specs are requirements on code, requirements are specs on designs, designs are requirements of code, and code is a specification on the operation of the computer. To say that requirements and designs are not specifications just makes you look stupid. Insisting these terms have specific disjoint meanings just makes you look anally retentive and it presumes the entirety of the english language exists purely to allow american CS academics to talk to each other.

If you're "writing it twice" then you're not writing a specification
True and irrelevant. You've decided to interpret what I say in whichever way gives you the most opportunity to lecture me. Telling me things I already know is boring. Did it ever cross your fragile mind that I may have been referring to loop conditions - expressions of which are frequently identical in Z and Java? No, never, because that would require giving someone else some credit.

And your little rant is irrelevant because if I did use JML and it helped prevent bugs then playing word games about terminology makes no difference to the software quality. Much less fucking Bingo.

OzJuggler
"And I will not rest until every year families gather to spend December 25th together
at Osama's homo abortion pot and commie jizzporium." - Jon Stewart's gift to Bill O'Reilly, 7 Dec 2005.
[ Parent ]

Ouch. (none / 1) (#94)
by GileadGreene on Fri Jan 20, 2006 at 11:35:02 PM EST

Bingo. There's a difference between requirements and specifications (and between specifications and design).
Knowledge isn't a fucking lucky draw prize, dickhead. Insulting other developers is a strange way for you to foster support for better software processes.

Actually, that "bingo" was intended as shorthand version of "hey, you're right". As in "hey you're right, formal specification won't solve requirements problems". I apologize if you interpreted it in some other way that was insulting. That was most assuredly not my intent.

Insisting these terms have specific disjoint meanings just makes you look anally retentive and it presumes the entirety of the english language exists purely to allow american CS academics to talk to each other.

Actually, the distinction that I was trying to make was originated by a respected English CS academic. He makes a very good case for why the distinction is important (beyond allowing American CS academics to talk to each other). That said, I agree with you that what constitutes a "specification" depends on the layer of abstraction you're working at. But I don't think that negates the value of keeping the concepts separate.

Telling me things I already know is boring.

Again, I apologize. It was not clear to me from your previous comments that you did already know these things.

Did it ever cross your fragile mind that I may have been referring to loop conditions - expressions of which are frequently identical in Z and Java? No, never, because that would require giving someone else some credit.

A fair comment. Although I doubt there are many Z specs that consist entirely of loop invariants, and I doubt there are many Java programs that consist only of loops invariants either. So while there may be a small amount of duplication, I can't imagine a situation where I'd end up coding everything twice. Your mileage may vary I suppose.

[ Parent ]

Okay okay, I was a bit too nasty, (none / 0) (#95)
by OzJuggler on Sat Jan 21, 2006 at 04:47:04 AM EST

Sorry.

There I said it. Print it out and frame it if you want to.

I'm not familiar with "Bingo!" being used in any way other than sarcasm, so some misunderstanding there.

I still don't believe I ever said that JML users would _actually_ be coding the whole thing twice. I only said it feels like it. As to how it could feel that way was ambiguous, but I thought you filled in the gaps on that one in a self-serving manner.

This reminds me of the time an "expert" on system engineering visited my employer to impart his many years of wisdom to anyone who would show up. I had barely graduated from Uni at the time, so I thought I had nothing to lose by going along to hear what he had to say. His background was in electronics, but he was talking about software. Pretty much the first question asked at the end of the presentation was about the role and value of formal specifications in achieving reliability. He responded with words to the effect of "Oh them! Haha. They can't even write a specification for a bubble sort, much less a complex system!"

At this point I began to silently fume that there was no difference between the specification for a bubble sort and a quick-sort or any other kind of sort, because the specification for any sort is the same and it takes just one simple line to spell out the post condition: that the elements are sorted. If you go to the next level of detail and specify the Hoare triples for achieving that postcondition in a particular way then its not so much a spec as an implementation. I couldn't believe this so-called "expert" could dismiss an entire approach just because he knew less about the basics of the topic than I did.

At least I can admit that I don't use formal specs because I frequently make use of well-tested open source components, the types of applications I usually deal with aren't exactly complicated, I'm lazy, and it just doesn't seem worth it most of the time. But ignorance is not my excuse.

- OzJuggler
"And I will not rest until every year families gather to spend December 25th together
at Osama's homo abortion pot and commie jizzporium." - Jon Stewart's gift to Bill O'Reilly, 7 Dec 2005.
[ Parent ]

lol (1.20 / 5) (#102)
by Run4YourLives on Tue Jan 24, 2006 at 02:17:21 PM EST

If you program in Java it could definitely make your life easier.

"Easier" and "Java" should never be used together in a sentence. Unless that sentence is:

"Ruby is mother-fucking way easier to work with then Java"

(I didn't see any anti-java comments here, so I thought I'd add one, just for the sake of it.)
:-)

It's slightly Japanese, but without all of that fanatical devotion to the workplace. - CheeseburgerBrown

s/then/than/, please (1.50 / 2) (#106)
by MrHanky on Sun Jan 29, 2006 at 09:17:37 AM EST

as in 'vim is way easier to work with than emacs'.


"This was great, because it was a bunch of mature players who were able to express themselves and talk politics." Lettuce B-Free, on being a total fucking moron for Ron Paul.
[ Parent ]
Nah (none / 1) (#107)
by jolly st nick on Fri Feb 03, 2006 at 01:09:30 PM EST

Java itself isn't such a horrible disaster. It's biggest fault have been fixed in 1.5 with autoboxing and somewhat cleaner integration of collections and iterators into the language itself.

The problem with too many Java programmers is they're too eager to "drink the cool-aid", whatever the flavor of the month is. Consequently they make their life harder than need be. They tolerate too much complexity and let it bleed into their code. If you do your job right, working on a problem in Java (or any other language) gets easier and easier. Groovy goes a bit farther and lets you overload operators, which can be a double edged sword, but I'm a huge believer in the tersest readable code. That pretty much closes the gap with scripting languages.

[ Parent ]

assert (2.50 / 2) (#105)
by DodgyGeezer on Fri Jan 27, 2006 at 08:57:25 AM EST

Seems like assertions would be more appropriate.  Weren't they added to the last major version of Java?  I find them invaluable for writing good code in C++.

Assertion patterns (none / 1) (#108)
by GileadGreene on Mon Feb 06, 2006 at 08:55:20 PM EST

Essentially what JML does is conveniently encode a bunch of standard patterns for assertions. Sure, you could perhaps achieve the same effect with custom assertion statements, but it's likely to get messy for some of the more complex properties you might want to check for. JML makes things standardized, easily expressible, and (for many properties) statically checkable.

[ Parent ]
Something Every Java Programmer Should Know | 107 comments (90 topical, 17 editorial, 0 hidden)
Display: Sort:

kuro5hin.org

[XML]
All trademarks and copyrights on this page are owned by their respective companies. The Rest 2000 - Present Kuro5hin.org Inc.
See our legalese page for copyright policies. Please also read our Privacy Policy.
Kuro5hin.org is powered by Free Software, including Apache, Perl, and Linux, The Scoop Engine that runs this site is freely available, under the terms of the GPL.
Need some help? Email help@kuro5hin.org.
My heart's the long stairs.

Powered by Scoop create account | help/FAQ | mission | links | search | IRC | YOU choose the stories!