I think this qualifies as a 'gotcha'

I was writing some Java code today. I'm writing a plug-in for Eclipse that will actually insert some Java annotations (e.g., @Override) into your code automatically.

Unfortunately, every time I ran my plug-in, the annotations were being inserted without the @ sign (e.g., Override). I couldn't figure out what was going on, looking at the code that generates the text:

String annotation_text = ...
StringBuilder sb = new StringBuilder('@');
sb.append(annotation_text);
sb.append(newline);

Finally, I hovered over the StringBuilder constructor to figure out which constructor I was calling. Low and behold, I'm calling this one:
java.lang.StringBuilder.StringBuilder(int capacity)

In other words, by using single quotes, I am specifying the character '@' which is then implicitly cast to an int. Hmm... This doesn't seem so bad at first, but there's an asymmetry in the API. If I use this constructor:
new StringBuilder("@");
I get the behavior I expect, a string builder initialized to the at sign.

Moreover, there are append methods that take a single character:
sb.append('@');
Adds the single at sign character to the stream. So, knowing about this method, and the string constructor of the StringBuilder, I naturally assumed there was a character constructor as well... NOT SO FAST BECKMAN.

Trip to Agra

Classic Taj
Originally uploaded by DixiePistols

This past weekend I went to Agra! Agra is a city in India famous for the Taj Mahal, the landmark that Americans like me most identify with India. Since I'd never been, and this is my third trip to India (!!) I felt like I really should make the trip.

To cut to the chase, it was awesome. I was expecting a cool building that was kind of a tourist trap, but this was an amazing building that was kind of a tourist trap. Probably the most amazing piece of architecture I have ever seen. And as they say, pictures do not do it justice. It is much larger than I'd imagined, and thanks to its elevated location, it appears to be hovering in mid-air. The two hours that I spend at the Taj Mahal were more than worth the entire weekend trip.

And what a gnarly trip it was... It's not really that easy to get to from Bangalore. I flew to Delhi early Saturday morning, and then took a train to Agra. On Sunday, I hired a car from Agra to Delhi, and then flew back to Bangalore. It was stressful as hell. The train was hot because I wasn't in an A/C section because I didn't make reservations early enough. (Lesson: make train reservations early in India!) I took a car on the way back because the only trains still available were at like 6 in the morning. The trip, which was only 200km, took four hours. I spent almost the whole time alternating between worrying about dying (my driver was, um, aggressive) and worrying about missing my flight.

But some things went well. Even though my itinerary was crazy it all worked out. The hotel where I stayed (The Taj Plaza) was cheap, pretty nice, within walking distance of the Taj and full of helpful employees. Recommended. Also, on Sunday morning I went to the breakfast buffet at the Oberoi Amar Villas hotel. The hotel itself is unbelievably expensive, and the buffet was expensive by local standards, but the food was really good! Recommended.

Validating XML against a Schema

If you ever have to write XML, and you need that XML to validate against a schema (and by the way, if you ever had to do this, I'm so sorry...) it turns out that Visual Studio is a great environment for this. It will tell you where you're XML is wrong and more importantly WHY. So many of the online validators would just say you have a problem without giving you any suggestions on how to fix it.

For the record, I am using Visual Studio 2008 Professional.

Yes. I am in India.

I made it to Bangalore! The trip was extremely painful, mostly because it was long, but it did have a few highlights:

1. In Charles de Gaulle airport there is a "resting" room that has lounge-style chairs that you can actually lie on and go to sleep, and it's free! What?! I took a lil' nap there in between my two nine hour flights.
2. I saw five movies. Best one? Probably Crazy Heart. Worst one? Definitely Bride Wars.

At Microsoft things are about like I remember. TONS of paper work to go through on the first couple of days, but I actually managed to make some progress on my project. There are a few things about India that I forgot to remember:

1. The mangoes are ridiccio! There's a snack area here at MSRI that has free stuff for us. They have mangoes, not the green kind but the yellow kind, and they are soooo good.
2. The streets are unbelievably hectic. I'll spend the first week jumping at the sound of horns and fearful that I will be hit while walking on the edge of the street (because the sidewalks are not really navigable).
3. People call you "boss." Really love that.

Beginning of the Summer, Travel, etc.

Well folks, it's been and continues to be a very busy period in my life! The semester is ending. I traveled a whole lot this past year. I'm going to India, again! And the summer is beginning. So let me just bring you all up to date.

The short story is, I am going to Bangalore, India, and I am leaving tomorrow. I'm going to work on a project at Microsoft Research, India that's related to my thesis, but also related to work they do there, so it's a good match. Some of you may know that I was there back in 2007, and had an awesome time. Well I am pumped to be going back. I'll be working with the same person, Aditya Nori, and to a lesser extent with Sriram Rajamani, who is on my thesis committee. This is going to be a more concentrated research trip, since I'll only be there for May, and we have a project to start and finish, but I'll still have some time to be a tourist.

When I get back, I have a bunch of research to get to in my final push to be doctored on. I'll be glad to be back in Pittsburgh for an extended time. I love graduate school, and I love all the great travel opportunities it has provided me with, but I also love my friends in Pittsburgh, and it'll be nice to be here for the summer.

If this post seems a little frantic, it's because I am frantically getting ready! Am I packed? Of course not! But I'll figure something out...

Nearest Neighbor

Hey. Just learned about a cool data structure for computational geometry called, KD-Trees. Yes, it's sort of embarrassing that I've just now learned about them, but what can I say? I still think they are cool. Anyway, KD-Trees are like binary trees but for points in space. They make it really easy (well, fast) to do things like search for the nearest point in a set to some given point.

SO, I quickly hacked up a nearest neighbor application. It generates a bunch of random points, and then when you click highlights the nearest point in red. Yay.




Click here to download the JAR if you want to run it. It's on of those runnable Jars... remember those? Ah, Java... I tried to make it an Applet, but that process was even more ridiculous.

Proof of Soundness for a Typestate Checker with Locks

Right now I am working on (what I hope will be) the last major theoretical effort of my thesis. I need to do another proof. Way back when I wrote this paper for OOPSLA in 2008, I did a proof of soundness for my language, a language that used atomic blocks for mutual exclusion. Right now, I'm doing the same thing but for a language that uses synchronized blocks. In other words, a language that is more Java-like.

Proofs are pretty painful for me, and the last one I did was really complicated, so rather than merely update the old proof to add locks, I am actually rewriting and simplifying (I think?) a whole bunch of stuff.

One of the biggest questions for me is a question that is important whenever you are doing a proof for a language with references; how will I define a well-typed heap? A well-typed heap means a runtime heap that is consistent with the type-checking facts that were known statically. In my system, every thread is an expression, and each one has its own type-checking context. They all much be consistent with the heap. Furthermore, in anticipation of my proof of preservation (where I have to show that after a step, the heap will still be well-typed) I think that my definition of a well-typed heap will have to include the following condition:

At most one thread can know statically the exact state of an object.

In my last proof I had a similar condition, but it was really unweildy to work with. I wonder how I can simplify this desire?