Java textbookSOD
-
/** * Returns true if and only if the list is empty. * * @pre true * @post @result <=> size() > 0 * @post @nochange */ public boolean isEmpty();
So basically,
isEmpty()
returns true if and only if the list is empty and also true if and only if the list has more than 0 elements.Then they go on to explain that
<=>
is an operator that determines if two things are equal and that@result
is the return value of the function and@nochange
is true if the object has not changed.There's also a footnote that says that
@pre
and@post
aren't actually supported by anything and they're just there for the book because apparently the compiler reads documentation comments in their world.
-
Oh, and the book has repeated use of the non-word "invaraint"
-
I vaguely remembered from school that <=> is supposed to mean something like equality in logic operations. Quick google later and...
Hmm... I think I want my hasty like back.
-
If only there were some Java operator that tested if two booleans were equal... Something like
==
...
-
But is "
==
" truly a properly rigorous "biconditional logical connective between statements", which is what we clearly need here? We don't want to leave people confused with such sloppy simplifications, Ben.
-
They're the same for the logic of booleans (in both classical and intuitionistic flavours). It's just that ⇔ has a heritage in a combination of ⇒ and ⇐ whereas = is more closely related to ordered sets than logical connectives.
(Font WTF: the ⇐ is a different size in this font from the ⇒ and ⇔ despite being in virtually the place in the Unicode BMP plane. It's not like nobody should have noticed that they were so badly out.)
-
-
No, but I'm sure
===
would be. At least it is something akin to an identity equivalence in other languages. Java may lag behind PHP on this one.
-
My post was brought to you by the Department of Redundancy Department it seems…
-
Redundant Department of Redundancy Department
RRTFY.
Filed Under: Reduntantily reduntified that for you
-
Tautology is awesome.
-
Discourse is emailing me a random subset of the replies to this topic. There doesn't seem to be a pattern at all.
-
Is there even a pattern to the replies to any topic here on WTDWTF that Dicksores could use as a guide‽
Wouldn't a pattern be considered us Doing It Wrong™ according to our community mores?
-
-
Correction acceptable.
-
BTW… How do I get this marked as read/ignore? Since it does crash my browser?
-
I've drained that particular swamp. BTW, 64-bit Chrome 37 didn't crash, but it was pretty continually pegging a core, making that particular tab pretty slow.
@Matches, please don't do that any more.
-
⇔
is a logical equvalence. However
<=>
is the spaceship operator1 which means something entirely different.
1The fact Java does not have it notwithstanding.
Filed under: was result abducted by aliens, or did alliens bring it?
-
-
That looks like a TIE
bomberinterceptor to me.
-
It takes quite a bit to stand out as a Java WTF.
-
To be fair, there is actually a system that can read, understand, and attempt to prove the correctess of pre/post conditions expressed in a similar way as those comments.
It's just labor-intensive to use, infectious, and, if memory serves, doesn't support past Java 1.4. I'm not sure it was much beyond a research project, but it was actually usable for small programs.
-
Some of the commercial support systems for developing safety-critical software might be a place to look for this sort of thing. They tend to be expensive and difficult to use, but a bit cheaper than other methods when extremely high levels of safety assurance are needed. (OTOH, they might instead focus on supporting something like C where it is possible to more tightly constrain the memory management.)
Don't need such things myself. Thank god.