tag:blogger.com,1999:blog-37274183.post5835150400949209181..comments2024-03-29T09:38:32.582+03:00Comments on Java: Developing On The Streets: InvariantsAnonymoushttp://www.blogger.com/profile/15900841850889743147noreply@blogger.comBlogger2125tag:blogger.com,1999:blog-37274183.post-62627854777876883812007-08-27T22:43:00.000+03:002007-08-27T22:43:00.000+03:00I knew that I should be very careful walking into ...I knew that I should be very careful walking into the minefield of overloaded terminology. Obviously, I did set off one or two...<BR/><BR/>So, let me reiterate the basic definitions. I think you should try to read this post in-light of these definitions (in other words: try to ignore other definitions for the term 'invariants')<BR/><BR/>When I say invariants I mean a set of conditions on the program's state (stack & heap) at a certain code-site. I am assuming that given an actual snapshot of the memory (taken during the execution of the program) it is possible to decide whether these conditions hold. On the other hand, I don't require the provability of these conditions.<BR/><BR/>Then I am saying that sometimes there is a gap between the expectations of the programmer and the actual code that he writes. That's why I distinguish between expected- and actual- invariants<BR/><BR/>Once these two defining are in place, we can discuss the various devices that help a programmer minimize the gap between the expected and actual invariants in his program.Anonymoushttps://www.blogger.com/profile/15900841850889743147noreply@blogger.comtag:blogger.com,1999:blog-37274183.post-16620975540663096622007-08-25T20:35:00.000+03:002007-08-25T20:35:00.000+03:00Me again. A few comments, mostly on terminology:Fo...Me again. A few comments, mostly on terminology:<BR/><BR/>For starters, most of your examples are not invariants, but rather preconditions. Invariants are a different kind of assertions (in loops, or in classes). Only the linked-list example presents a real (class) invariant. And your first example (main's args) is very different, since it can't be computationally verified (you can tell if n < 0, but how can you tell the command line args from random noise?).<BR/><BR/>Next, the claim that "most bugs are caused by a program that fails to keep its invariants" is a very strong claim, and I'm not sure how founded it is. Don't underestimate the popularity of plain algorithmic bugs.<BR/><BR/>Next, calling those asserts "design by contract" is doing injustice to DbC. In DbC, the assertions are an important part of a method's documentation -- just as the argument types are. In the Java case, you have to read the source code to find the assertions. True DbC also supports several features that are very hard to implement using Java assertions, such as the ability to check class invariants after every public method is called, <I>except</I> if that method was called internally, from another method of the same class. Done manually, you need to examine the stack (or maintain paperwork) for that.<BR/><BR/>Finally, unless I'm mistaken, the "sequence" you mention near the end is commonly called the class's <I>protocol</I>. I'm not aware of language-level protocol-enforcing mechanisms, though I wouldn't be surprised if these do exist. I do know that some static analyzers can find (some) protocol violations; I've worked on such tools back in my IBM days.<BR/> -- TCAnonymousnoreply@blogger.com