Thoughts on Loop Invariants

With the recent addition of for and while loops to Whiley, I’ve been able to fiddle around with loop invariants and already I noticed a few things. Consider this little program:

Java Pathfinder

Recently, Simon Doherty gave a short talk on using Java Pathfinder to find bugs in Java programs. Java Pathfinder is a model checker for Java code, particularly suited to reasoning about multi-threaded code and finding concurrency bugs.

James Bach on Software Testing

I’ve just been watching this YouTube presentation by James Bach: James has a very tongue-in-cheek style, which I rather like, and he’s obviously not a great fan of the academic establishment:

The X10 Programming Language

X10 is an interesting and relatively new language from IBM being developed as part of DARPA’s High Productivity Computing Systems program. X10 is designed for high-performance parallel programming using a partitioned global address space model.

Thinking about Recursive Constrained Types in Whiley

Whiley supports so-called Algebraic Data Types for constructing tree-like data structures. For example, an expression tree might be defined like so: define ADD as 1 define SUB as 2 define MUL as 3 define DIV as 4 define binop as {ADD,SUB,MUL,DIV} define expr as int | (binop op, expr lhs, expr rhs) Using this definition for expr, we can create a variety of trees representing compound arithmetic expressions.