CITS5501 lab 9 (week 10) – Formal methods  – solutions

Reading

It is strongly suggested you complete the recommended readings for weeks 1-9 before attempting this lab/workshop.

A. Applicability of formal methods

Discuss the following scenarios. Would you use formal methods for any of the following systems? If so, which systems, and why? Do you think the enterprise developing the system would share your view?

1. The next version of Confectionery Crush Story, a web– and mobile-app–based puzzle video game your company develops. The game is available for both Android and iOS mobile devices, and the previous version grossed over $US 1 billion in revenue.

2. Exemplarex, software produced for Windows and MacOS operating systems and licensed to educational institutions. The software semi-automatically invigilates exams set by the institutions: machine-learning techniques are used to analyse audio and video of exam candidates to identify possible academic misconduct.

3. The online banking website provided by a major Australian bank, EastPac. Over 5 million customers use the website to perform banking transactions on personal or business bank accounts.

4. A radiation therapy system used to treat cancer patients. The system has two principal components:

   • A radiation therapy machine that delivers controlled doses of radiation to tumour sites, controlled by an embedded software system.
   • A treatment database that includes details of the treatment given to each patient.

B. Introduction to Dafny

Dafny is a “verification-aware” programming language. The compiler for the language incorporates a program verifier – as you write a program, the verifier checks to see whether what you have written can be proved correct, and flags any errors.

Gitpod

You can compile (as well as run) Dafny programs using Gitpod, which provides you with an online development environment based on Microsoft VS Code. (Other installation options are also available, but using Gitpod is normally the easiest way.¹)

Visit https://gitpod.io/#https://github.com/arranstewart-dev/dafny-gitpod in your browser. Gitpod will download a Docker image containing the Dafny compiler, and create an online IDE environment (this may take a couple of minutes).

Once it appears, open the “sample.dfy” file in the editor, and an “editor extension” will be installed which tells the editor how to highlight Dafny code and show errors.

(You can ignore any error messages saying the “dafny-lang.ide-cscode extension is not synced” – those are a limitation of the VS Code setup, and can’t easily be got rid of.)

Toward the bottom of the screen is also a “Terminal” tab, which gives you command-line access to the virtual machine in which Microsoft VS Code is running. Typing dafny /help in the terminal will display the compiler online help (warning: it’s very long).

Dafny assertions

Take a look at the sample source file in VS Code:

method Main() {
  print "hello, Dafny\n";
  assert 10 < 2;
}

You should see that the Dafny compiler reports an assertion violation in line 3; the assertion “\(10 < 2\)” is not true. Now comment out the assertion (using double forward-slashes – “//” – the same as Java.) The code should now compile.

In Dafny, assertions are checked not at run-time (as they are in many languages), but at compile time: if the Dafny compiler cannot prove to its satisfaction that an assertion holds, it will refuse to compile the source code.

Command line compiler

In the “Terminal” tab, you should be able to invoke the dafny command, which lets you compile code to different targets (such as Java, C# and Go) and run the program. The command

$ dafny /version

should print the Dafny version and verify the command works. And the command

$ dafny sample.dfy

will verify and compile the sample.dfy – it is actually short for the command:

$ dafny /compile:1 hello.dfy

Either command should produce output like the following:

Dafny program verifier finished with 0 verified, 0 errors
Compiled assembly into sample.dll

By default, Dafny compiles programs into libraries for use on Windows (.dll files). If you list the directory contents, you will see sample.dll, and a file sample.runtimeconfig.json which the compiler creates.

The following command verifies, compiles, and runs your program:

$ dafny /compile:3 sample.dfy

Main method

Change the name of the Main method to Random (or any other name you wish).

Try compiling, verifying and running the program again:

$ dafny /compile:3 sample.dfy

Although the program verifies and compiles properly, it will not execute and produce any output, because the Dafny runtime looks for a Main method to execute. If it does not find one, no warning or error is produced (you might have intended to create a library, rather than a program), but nothing will be executed.

C. Preconditions

Try compiling and running the following code:

method Main() {
  PrintInt(-1);
}

method PrintInt(x : int)
{
  print "the int is: \n";
  print x;
}

The int -1 should be printed with a message. Now add a precondition to PrintInt, “requires x >= 0”:

method Main() {
  PrintInt(-1);
}

method PrintInt(x : int)
  requires x >= 0
{
  print "the int is: \n";
  print x;
}

If you try compiling again, you will see that Dafny won’t permit you to call the PrintInt method, unless it can verify all the preconditions hold. Change the int being passed from -1 to 1, and you should see the code now compiles.

Create a new file square.dfy consisting of the following code.

method SquareMe(n:int)
{
  assert n*n > 0;
}

and try to verify the program using:

$ dafny square.dfy

It should generate the messages:

square.dfy(3,13): Error: assertion might not hold
Dafny program verifier finished with 0 verified, 1 error

Even though the assertion is true for almost all values of n, it fails for n == 0, and just one failure is enough to make the assertion false. Dafny requires that assertions be true for all possible inputs.

An assertion which is true, however, is the following – try inserting it instead:

assert n!=0 ==> n*n>0

This reads “n*n is greater than 0, if n does not equal 0”. This assertion is true, so Dafny should allow the program to be verified and compiled.

D. Using Dafny features

The following Dafny code is intended to find the position of the largest element of an array. It is only guaranteed to produce a result if the array is non-empty, however. We won’t compile this (yet), but look at the following code:

method FindMax(arr: array<int>) returns (r: int)
{
  var max_val : int := arr[0];
  var max_idx : int := 0;

  var i : int       := 1;

  while (i < arr.Length)
  {
    if arr[i] > max_val
      {
        max_idx := i;
        max_val := arr[i];
      }
    i := i + 1;  
  }
  return max_idx;
}

At what points in the code might we insert the following, and what Dafny keywords would be used?

• preconditions
• postconditions
• loop invariants
• assertions

See if you can state what the preconditions and postconditions are (in English is fine).

method FindMax(arr: array<int>) returns (r: int)
   requires /* **preconditions go here** */
   ensures /* **postconditions go here** */
{

  var max_val : int := arr[0];
  var max_idx : int := 0;

  var i : int       := 1;

  /* **assertions could go anywhere in the body** */

  while (i < arr.Length)
    invariant /* **loop invariants go here** */
  {
    if arr[i] > max_val
      {
        max_idx := i;
        max_val := arr[i];
      }
    i := i + 1;  
  }
  return max_idx;
}

Challenge exercise: If you have some experience with formal logic and would like a challenge, try verifying the above code using the online Dafny verifier. You will probably want to work through the online Dafny tutorial first. This will explain how to use the forall keyword, which we have not covered, but which is needed for the challenge.

method FindMax(arr: array<int>) returns (r: int)
   requires arr.Length > 0
   ensures (0 <= r < arr.Length) && 
    (forall k :: 0 <= k < arr.Length ==> arr[r] >= arr[k])
{

  var max_val : int := arr[0];
  var max_idx : int := 0;

  var i : int       := 1;

  assert i >= 1;
  assert max_idx <= i;

  while (i < arr.Length)
    // probably could get away with fewer loop invariants
    invariant 1 <= i <= arr.Length
    invariant 0 <= max_idx  <= arr.Length
    invariant 0 <= max_idx  <= i
    invariant forall k :: 0 <= k <= i-1 ==> max_val >= arr[k]
    invariant (0 <= max_idx < arr.Length) 
        && (max_val == arr[max_idx]) 
        && (forall k :: 0 <= k <= i-1 ==> arr[max_idx] >= arr[k])
  {
    if arr[i] > max_val
      {
        max_idx := i;
        max_val := arr[i];
      }
    i := i + 1;  
  }
  return max_idx;
}

E. Writing Dafny methods

The following code does not yet compile:

method Max(a: int, b:int) returns (c: int)
  ensures c >= a
{
  return 0; 
}

Write the body of the method Max. It should take two integer parameters and return their maximum. Add appropriate annotations (one is already provided) and make sure your code verifies. Refer to the documentation and tutorials, if necessary.

method Max(a: int, b:int) returns (c: int)
  ensures c >= a
  ensures c >= b
{
  if (b > a) {
    return b;
  } else {
    return a;
  }    
}

F. Project work

If you haven’t yet started on the CITS5501 unit project, now would be a good time to read through the specification.

For project questions requiring code: a Moodle “test area” will be available soon on the CSSE Moodle server which will allow you to run some basic tests of your code. The test area won’t include space for “long-form” English answers, though, since those don’t admit of automated testing.

For project questions requiring long-form answers in English: a final submission area will be made available on Moodle a week before the submission date, where you can submit both code and long English answers to questions. Long-form English answers are written using Moodle’s text editor plugins, of which there are several available. The default editor is called Atto, but you might find others more to your taste. The TinyMCE editor provides finer-grained control over the formatting of your answers, and it’s also possible to write your answers in a markup language such as Markdown. You can read here about the different editors available, and how to select them in your Moodle preferences.