Whiley

Hybrid OO/functional language compiling to the JVM. Supports preconditions, postconditions, and static verification to catch divide-by-zero, out-of-bounds, and null dereference at compile time.