# Prove it

Posted by daniel on July 14, 2003 at 4:44 AM PDT

It's not always easy to prove that two things are equivalent. There are
the straightforward cases from high school geometry of those stupid
proofs that two triangles are equivalent using SAS (Side angle side), ASA,
or one of those other rules. But even in geometry equivalence can get more
interesting. Consider these three statements.

• Given a line and a point not on that line, there is exactly one line
through the given point parallel to the given line.
• The sum of the interior angles of a triangle is 180 degrees.
• The area of a triangle is proportional to the product of its base
and height.

Those three statements don't seem related at all and yet they are
equivalent. That's where the fun begins. Similarly in programming there
are easy cases of programs we know are equivalent. We can change
`for` loops to `while` loops or replace the names of
variables, methods, or classes with friendlier names. Replacing a
`case` statement with a State pattern may be harder to spot. In
today's java.net feature we link to
Bill Venner's interview with James Gosling about Gosling's new project
named Jackpot.

In Analyze
`this`!
, Gosling talks about how Jackpot helps programmers
analyze, visualize, and refactor programs. Gosling describes an example of
a refactoring.

Moving a method isn't just cutting and pasting text. It's a lot
more than renaming the parameters and swizzling them around, because you really
want to be able to do things like construct forwarding methods. When you construct
forwarding methods, they're different from the original methods.

You can't just replace all uses of the forwarding method by uses of the moved
method, because they actually behave slightly differently. The difference is
usually around what happens when the pivot parameter is null . That can lead
you into a deep morass of essentially theorem proving about properties of the
code fragments that you're moving, to understand how they behave with respect
to null . And you can treat all kinds of code manipulation that way.

In today's featured Weblogs Amy Fowler asks href="http://weblogs.java.net/pub/wlg/244"> "Would you run in flipflops
. Her entry looks at the benefits of having user experience dictate
the UI. Her extended example is the Apple iTunes music store whose
interface is simple, non-flashy, and intuitive enough that she's buying
way more music than she might otherwise. Eitan Suez reviews a recent book
written by java.net blogger Will Iverson in the entry
"Impressions of 'Mac OS X
for Java Geeks'"
.

In Also Today, we link to an entertaining way for novice
released
CodeRally
. In the xml.com article href="http://www.xml.com/pub/a/2003/07/09/xmlapis.html"> A Survey of APIs
and Techniques for Processing XML
, Dare Obasanjo looks at curser based
and pull model based parsing in addition to the familiar push and tree
models SAX and DOM.

Steve Mallett, the Java Today news editor has gathered the following
Java Today News Headlines : href="http://today.java.net/today/news/"> "Jakarta POI 2.0-pre2 Released",
"Jakarta Element Construction Set 1.4.2 Released", "blojsom blogware 1.9.4 released",
and "JD4X has gone beta!".

Once this page is no longer featured as the front page of href="http://today.java.net"> Java Today it will be archived at href="http://today.java.net/today/archive/index_07142003.html">
http://today.java.net/today/archive/index_07142003.html. You can
access other past issues by changing the address appropriately.