Home » forums » LtU Forum

Picky libraries, picky languages?

STL has some complexity requirements specified. (Dunno how much people really meet them, or what the constant factors are, of course.) I often find myself scratching my head trying to figure out what, if any, specification the Java standard libraries are following in terms of e.g. performance and behavioural contracts.

To what degree do people value the idea of providing a standard library for a language that is super well specified w.r.t. things like time and space complexity, suitability for concurrency, behavioural patterns, use of nulls, etc.? (Personally, as a library consumer, I think that would all be the bee's knees.) It sure seems like a rarity.

Further, to what degree should such things be available as core concepts in a language? Are various complexity metrics describable in any design-by-contract systems? It would possibly be neat to declare that a method has a certain running time complexity, and then have the compiler and tools chain that information together throughout the call tree (I'm not expecting them to prove the declared complexities). And ways to put assertions or requirements in bounding those values.

I've poked around but haven't turned up any great refs, thanks for any info/pointers.

I guess to some degree I see this all being aimed at correctness by construction vs. relying too much on post-hoc testing.

By raould at 2007-05-23 23:28 | LtU Forum | previous forum topic | next forum topic | other blogs | 5643 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

The only thing I can think

The only thing I can think of at the moment is Rico Mariani's paper (and blog). He often writes on the subject of complexity annotations in the context of .Net libraries, although it's more of a "wouldn't it be great if..." sort of thing.

By Wolf Logan at Thu, 2007-05-24 00:11 | login or register to post comments

Re: wouldn't it be great

Sounds like me. Thanks for the reference.

Interestingly, in 2003 Bertrand Meyers said, "These are performance contracts, and it's a quite interesting research area. I think there will be usable results in this area in the next few years, but it falls beyond the realm of Design by Contract as it is generally understood in practice today."

By raould at Thu, 2007-05-24 01:29 | login or register to post comments

RIP Sather

(too bad Sather is dead.)

By raould at Thu, 2007-05-24 01:43 | login or register to post comments

See: Sized Types

Sized Types.

By naasking at Thu, 2007-05-24 01:57 | login or register to post comments

JML has some support

I agree that it would be lovely to have such information specified where possible for libraries. If you want reuse to really work it helps if you know exactly what code can and cannot do (ideally spelled out in a way that is actually integrated into the code you want to use via contracts or similar). On that front JML does provide support for some of this for Java with duration and working_space clauses, which allow you to specify bounds on a method's max running time (in JVM cycles) and working space. I'm not sure how good the tools are for verifying those contracts are, but they do support modular reasoning.

The paper primarily referred to in the JML docs is this one, but you also be interested in this paper on loop bounds using JML, and this paper on heap allocation bound verification with JML.

By Leland McInnes at Thu, 2007-05-24 04:05 | login or register to post comments

Sweet

That is cool. I think that while Java has lots of... issues, the subculture around it of tools is pretty amazing: JML, FindBugs, Daikon, etc. I just wish the language itself wasn't so unattractive to me (I am and have been on and off a full time Java developer so it isn't said in some really obnoxious way, just more matter-of-factly :-)

By raould at Thu, 2007-05-24 19:42 | login or register to post comments

I agree

There are some amazing tools for Java, and I really like JML. It does, however, seem awfully kluged on -- I'd much rather see that sort of thing properly integrated as a part of language from the get go (it is, after all, entirely optional and developers who don't want it can simply not write any contracts). I really wish something like Scala would pick up on JMLs ideas and just integrate it straight into the language.

By Leland McInnes at Thu, 2007-05-24 20:52 | login or register to post comments

The design discussion for

The design discussion for the Ada container library may be of interest. A good place to start is AI-302.

By Ehud Lamm at Thu, 2007-05-24 10:17 | login or register to post comments

Praxis expected

Thanks, I was wondering if good old Ada would have something to offer - I really expected to quickly find stuff along these line in the Praxis Ada work, but didn't easily turn up anything explicit. There's the general docs / whitepapers (some links in the main post here above) attitude they take.

By raould at Thu, 2007-05-24 19:39 | login or register to post comments