Whiley v0.6.1 Released!

Finally, after almost a year since the last release, we have two new releases of Whiley! v0.6.0 was released on June 1st 2022, and was quickly followed by v0.6.1 which included an important bug fix. The main difference is that Whiley is now partly written in Rust and deployed using cargo (see install for details).

Change Log

A summary of the main changes since v0.5.3:

• Improved Verification. Verification in Whiley continues to get stronger with further improvements to the Boogie backend (see this post and our paper for more info). The Boogie backend is now the default verification toolchain and passes >95% of tests.

• Command-Line Tool (Repo). The command-line tool wy for building and verifying Whiley programs is now written in Rust. In essence, this provides a wrapper around the existing Java components (see this post for more). This also adds support for the commands clean (#1092) and init (#26), amongst other things.

• Old Syntax (#1096). The ability to reason about heap structures has improved dramatically and, in particular, now supports old() syntax (following JML, Dafny and similar systems). This gives the ability to reason about the state of the heap prior to a method:

  method inc(&int x)
  ensures old(*x) < *x:
    *x = *x + 1
  

  Here, old(*x) < *x effective says that the value at *x must increase after calling this method. See RFC#67 for further discussion

• Property Syntax (#1102, #1151, #1157). The syntax for properties has become more expressive with the ability to specify the return value, and use if statements and variable declarations within the body:

  property sum(int[] xs, int i) -> (int r):
    if i < 0 || i >= |xs|:
      return 0
    else:
      return xs[i] + sum(xs,i+1)
  

  See RFC#102 for further discussion (though note the implement syntax differs somewhat).

• Exponentiation Operator (#1124). Support has been added for the exponentiation operator x ** y which returns x to the power of y. Thus, for example, 2 ** 4 returns 16. A precondition of this operator is that y cannot be negative.

• Test File Format (#978, #1149). A new test file format has been developed for improved testing of the compiler. This now allows a single test to describe multiple files and offers a dynamic view of files. That is, a single test can test a file followed by changes to that file. The following illustrates such a test:

  ====
  >>> main.whiley
  function f(int x, int y) -> int:
    return x ** y
  
  public export method test():
    assume f(2,-1) == 2
  ---
  E713 main.whiley 2,15
  E730 main.whiley 2,15
  ====
  >>> main.whiley 5:6
    assume f(2,1) == 2
    assume f(2,2) == 4
  ---
  E730 main.whiley 2,15
  =====
  >>> main.whiley 1:2
  function f(int x, int y) -> int
  requires y >= 0:
  ---
  

  This test proposes an initial file main.whiley that should produce errors E713 and E730 upon compilation. Then, in the next frame, the file is updated by replacing line 5 with two lines — after which a compile error (E730) should still be reported. The final frame introduces a precondition to function f which prevents an error being reported that y could be negative in x ** y. See also RFC#110 for a more in depth discussion.

• Array/Record Update Operator (#1129). The array update xs[x:=y] and record update r[f:=x] operators have been added for use within specification elements (e.g. requires clauses) and property declarations.

• Unsafe Syntax (#1093). A new modifier unsafe is now supported, though some questions remain over its semantic. Currently, it indicates that a function or method should not be verified (hence, it is unsafe). Calling unsafe methods or functions does not require the caller is unsafe. However, a strict mode can be enabled which does enforce this stricter requirement.

• Bug Fixes (e.g. #1132, #1142, #1128, #1120, #1103, #1101, #1097, #1098). As usual there have been plenty of bug fixes, and I’ve only included a sample of them to the left.