Writing tests in Dafny

[franck44]

Dafny offers some basic support to write simple tests. The main ingredient are:

• tag a method with {:test}
• the method may not have parameters
• use expect to check the test results
• run the tests in f.dfy with dafny /runAllTests:1 /noVerify /compile:4 f.dfy [There is another more powerful techniques using compilation to c# /runAllTests:0 that I have not investigated]

For example, a test for the program test_Execute_01 in test.dfy may look like so:

include "../../dafny/evm.dfy"

import opened Int
import opened EVM

// Arbitrary limit for now
const GASLIMIT : nat := 100;

// Check most simple program possible
method {:test} test1()
{
  var x := 3;
  // Initialise EVM
  var tx := Context.Create(0xabcd,[]);
  var vm := EVM.Create(tx,map[],GASLIMIT,[PUSH1, x, PUSH1, 0x0, MSTORE, PUSH1, 0x1, PUSH1, 0x1F, RETURN]);
  // PUSH1 x
  vm := EVM.Execute(vm);
  // PUSH1 0x2
  vm := EVM.Execute(vm);
  // MSTORE
  vm := EVM.Execute(vm);
  // PUSH
  vm := EVM.Execute(vm);
  // PUSH
  vm := EVM.Execute(vm);
  // RETURN
  vm := EVM.Execute(vm);
  //
  expect vm.data == [x+1], ("failed. vm.data=", vm.data); //, "failed";
}

and the execution yields:

> dafny /runAllTests:1 /noVerify /compile:4 /Users/franck/development/evm-dafny/src/test/dafny/test1.dfy

Dafny program verifier did not attempt verification
Running...

test1: FAILED
        /Users/franck/development/evm-dafny/src/test/dafny/test1.dfy(30,2): (failed. vm.data=, [3])
Test failures occurred: see above.

note: the test fails as the result should be [x] not [x + 1].

[DavePearce]

This command-line works:

dafny /runAllTests:1 /noVerify /compile:4 /compileTarget:java src/test/dafny/test.dfy

The test above appears to fail .. which I think is right?

[DavePearce]

I suggest we add /runAllTests:1 to the gradle build. Then you can add {:test} directives to your hearts desire!

[DavePearce]

Ok, this is now done. Running gradle build now also means anything in the directory src/test/dafny directory will be verified and executed with /runAllTests:1. This works, but there are at least two very annoying things:

1. (Exit Code) Dafny does not report a non-zero exit code upon failure. That means gradle cannot detect a test failure from runAllTests. You can see it says on the console output that it failed, but you have to notice it.
2. (Code gen) The code gen output always produces a lot of junk about Additional target code written to and I cannot seem to stop that.

I will raise issues on the Dafny repo about these two things as they would improve our process.

[DavePearce]

Also also:

1. @franck44 checked in a file src/test/dafny/test1.dfy which contained the test above (and a bunch of commented out stuff --- not pretty).
2. Therefore, I merged that single test into the existing file src/test/dafny/test.dfy and remove test1.dfy.

In general, we can add more files in that src/test/dafny directory, for sure.

[DavePearce]

See https://github.com/dafny-lang/dafny/issues/2513

And in researching that, I have figured out the solution to the code gen output issue above. You can use compileVerbose:0 to suppress that output. I will action that now.