As you may or may not know, my research work has to do with the verification of object oriented programs, in particular those that are concurrent and use or implement object protocols. The name of my tool is NIMBY, and it's a part of PLURAL which is Kevin's single-threaded verification tool.
I recently was able to mostly verify the implementation of a program that creates an object, shares the object between two threads, and then permanently reacquires thread-local permission to the object. This is sort of a litmus test for many concurrent analyses, and I was quite happy at how naturally it fit into our analysis framework. You can take a look at the verified code here. Other verified programs I tend to post here.
I guess it's been a while since I've seen any Java, but man.. that's a crazy language. What's the deal with all the @'s?
ReplyDeleteLol. Okay, good question. Java has a language feature, since version 1.5, known as annotations. Annotations, in the words of the Java marketing people, allow you to add "meta-data" to Java classes and class members. This information hangs around and can be queried as run-time. But that's not why we use it.
ReplyDeleteAnnotations can also be used as a way of extending Java's type system. Here we are extending Java's type system with annotations describing the aliasing patterns of your program. Then our tool checks that these annotations are consistent at compile-time.
You can read more here:
http://java.sun.com/j2se/1.5.0/docs/guide/language/annotations.html
Note that C# has the same thing, they are just called attributes. Nice!