Support generating test running code when using dafny translate

[keyboardDrummer]

Summary

Add an option --with-test-runner to dafny translate so that it generates a main method that runs all the tests, similar to what dafny test does.

Background and Motivation

Currently Dafny programs can run tests using dafny test. However, for Dafny programs that use external code with external dependencies, it might not be possible to compile them using dafny test.

Proposed Feature

See summary

Alternatives

Alternative 0: by default, let dafny translate generate a runTests file that contains a main method that will run the tests. Generating annotations for a particular target language testing framework, such as is done for C# and XUnit now, will only be done when using a back-end specific option.

Alternative 1: Increase the functionality of dafny test so that is support builds with external code and external dependencies.

Alternative 2: enable dafny translate to always generate code for tests that can be executed using a target language testing framework, like is currently done for the C# back-end which generates XUnit tests.

[keyboardDrummer]

Related PR that adds support for generating translates tests for Java: #2395

[keyboardDrummer]

I'm in favor of alternative 0 because it scales well. Alternative 2 relies on the subjective choice of which testing framework to choose, and adds extra work for each back-end.

[davidcok]

Note that #3769 has already implemented Alternative #1 in response to a different customer request (namely to add the functionality to dafny test).

[robin-aws]

I'm more in favor with the --with-test-runner option than alternative 0: emitting a main method by default would mean you can't easily use dafny translate to generate code in a project that needed its own main method. Especially since dafny translate doesn't currently know whether you're translating tests or not, and I think it would be a bit surprising/brittle to dynamically guess at this based on whether the Dafny source has any {:test} methods.

In addition, the C# compiler currently adds [Xunit.Fact] attributes and some code to check IsFailure on results, unless /runAllTests is provided. That means dafny translate cs currently always does that, and we should have an explicit option to stop it so that we're at least not introducing the dependency on xUnit.