feat: Parameterized Tests with Method Source in C#/Java

[tbean79]

This branch edits the C# and Java compilers to emit parameterized testing code when the attribute {:test "MethodSource"...} is specified on a unit test. The name of the method source should be provided as a string following the "MethodSource" parameter.

Here's an example:

        static method Mult_Source() returns (testInputs : seq<(int, int, int)>)
        {
            return [
                (2, 3, 6),
                (40, -2, -80),
                (-7, -7, 49)
            ];
        }

        method {:test "MethodSource", "Mult_Source"} test_mult_shouldMultTwoArguments(a : int, b : int, expected : int) 
        requires expected == a * b 
        {
            var product := Calculator.mult(a, b);
            Assertions.assertEquals(expected, product);
        }

In order for the cross-compiled test code to execute properly, there are a few things the programmer must know beforehand:

• The specified name should be a string and should match the name of the actual method source
• The return type should be a sequence of tuples
• The types inside each tuple must match the types of the parameters that the unit test is expecting

I've edited the Attributes.md documentation to make the programmer aware of these necessities. If you'd like me to put them in a more visible place, I would be happy to do so.

This solution is not framework-agnostic; the Java compiler creates JUnit-specific annotations while the C# compiler does the same with XUnit such as [Theory]. I don't perceive this to be a problem, given that the C# compiler already uses [Fact] when {:test} is present.

On the subject of [Fact], this branch also edits the Java compiler to behave similarly to the C# compiler when encountering {:test} (this time without a "MethodSource" parameter). Similar to [Fact], the Java Compiler emits an @org.junit.jupiter.api.Test annotation.

I can see how the string "MethodSouce" may cause some confusion, since the idea of a Method Source really only exists inside JUnit. XUnit's equivalent is called MemberData. I would be happy to change this keyword as needed.

[robin-aws]

Thanks for the contribution @tbean79! I'll provide a full review soon, but first off I thought of a cleaner alternative to the magic reflection-like semantics here:

        static function Mult_Source(): seq<(int, int, int)>
        {
            [
                (2, 3, 6),
                (40, -2, -80),
                (-7, -7, 49)
            ];
        }

        method {:test "ExpressionSource", Mult_Source()} test_mult_shouldMultTwoArguments(a : int, b : int, expected : int) 
        requires expected == a * b 
        {
            var product := Calculator.mult(a, b);
            Assertions.assertEquals(expected, product);
        }

This is possible because attribute arguments can be full expressions and not just string literals. I'm more comfortable starting with this kind of source, although I imagine in the future we will want more options.

[tbean79]

Thank you, @robin-aws. What other sources are you envisioning besides expressions?

The resolver doesn't seem to like an invocation expression inside the attributes. More precisely, for the above example, I'm getting the error: expression is not allowed to invoke a method (Mult_Source).

Is there a specific workaround that I'm missing?

[robin-aws]

Thank you, @robin-aws. What other sources are you envisioning besides expressions?

The resolver doesn't seem to like an invocation expression inside the attributes. More precisely, for the above example, I'm getting the error: expression is not allowed to invoke a method (Mult_Source).

Is there a specific workaround that I'm missing?

Ah yes, attribute arguments have to be expressions, so they can call functions but not methods. That's why I tweaked the example to use a function.

The main reason I'm suggesting this is to avoid introducing any implicit reflection in the API of this feature. I'm nervous about that because I hesitate to assume that all target languages will support enough runtime reflection for this to work. I don't believe it's tractable in C++ for example.

I'm suggesting making the testing data a compile-time constant instead so that in the worst case, the compiler can literally emit multiple copies of the test method. It would be similar to the implementation of /runAllTests, which generates a main method to invoke each test method, and is almost entirely target language agnostic. For this initial PR you could stick to the strategy of just supporting C# and Java by relying on their runtime reflection-based versions, but at least this way we know support for other languages can be added later.

FYI there is already some constant folding implemented, in the context of determining the right native type for a given subset type: https://github.com/dafny-lang/dafny/blob/master/Source/DafnyCore/Resolver.cs#L3792-L3798 It would make sense to extract that somewhere shared and use it here too. I notice it doesn't support function calls, but you could avoid that if you used a constant instead of a nullary function:

const Mult_Source: seq<(int, int, int)> :=
    [
        (2, 3, 6),
        (40, -2, -80),
        (-7, -7, 49)
    ];

method {:test "ExpressionSource", Mult_Source} test_mult_shouldMultTwoArguments(a : int, b : int, expected : int) 
requires expected == a * b 
{
    var product := Calculator.mult(a, b);
    Assertions.assertEquals(expected, product);
}

[janderson4671]

Hello @robin-aws, I am working on this PR in place of @tbean79. I have made changes to this PR to reflect the desired functionality for obtaining test inputs from an expression source. I have run into an issue with the java-compiler when trying to access the "Mult_Source" expression in the generated Java code. The constant variable "Mult_Source" is transformed into a non-static method that returns a Dafny sequence of 3-Tuples. The method that calls the "Mult_Source" in the generated java code is a static method. This causes an error when running because a non-static method cannot be called in a static context.

A solution that I have found for this is to simply make "Mult_Source" a statically constant variable. This transforms it into a static method in the generated Java code.

static const Mult_Source: seq<(int, int, int)> :=
    [
        (2, 3, 6),
        (40, -2, -80),
        (-7, -7, 49)
    ];

method {:test "ExpressionSource", Mult_Source} test_mult_shouldMultTwoArguments(a : int, b : int, expected : int) 
requires expected == a * b 
{
    var product := Calculator.mult(a, b);
    Assertions.assertEquals(expected, product);
}

Are there any issues or concerns with having the "Mult_Source" being declared as a static constant?

Also I have tested this on the C# compiler and it seems agnostic to whether "Mult_Source" is static or not.