Whiley

Whiley supports so-called [[algebraic data type|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) . . . → Read More: Thinking about Recursive Constrained Types in Whiley

The notion of [[precondition|pre-]] and [[postcondition|post-conditions]] is well understood in the context of software verification.  However, Whiley deviates from the norm by combining them into a single condition.  The following illustrates a simple Whiley function:

int f(int x) where x > $ && $ > 0: return x-1

Here, $ represents the return value.  . . . → Read More: Thinking about Pre- and Post-Conditions in Whiley

Here is the latest update for the Whiley-to-Java Compiler.  It now weighs in at around 47KLOC, spread over 272 classes.  There are 379+ distinct test inputs, which give rise to around 615 actual JUnit tests.  Anyway, the list of improvements includes:

Fixed numerous outstanding bugs Improved reporting of syntax errors Added list append Added . . . → Read More: Whiley v0.2.8 Released!