Add support for Java mocking

[cassidywaldrip]

Fixes #

This branch adds support for mocking and the creation of fresh objects to the Java compiler (functionality that already exists for the C# compiler).

Mocking in Java is similar to mocking in C#. The only significant difference between the two at this point is that the Mockito library for Java does not support mocking fields (C#'s Moq does). So, the grammar for mocking in Java is:

S = FORALL | EQUALS | S && S EQUALS = ID.ID (ARGLIST) == EXP // stubs a method call | EQUALS && EQUALS FORALL = forall SKOLEMS :: EXP ==> EQUALS ARGLIST = ID // this can be one of the skolem variables | EXP // this exp may not reference any of the skolems | ARGLIST, ARGLIST SKOLEMS = ID : ID | SKOLEMS, SKOLEMS

Here is an example of using the {:synthesize} attribute for creating a fresh method and for creating a mock.

class Even {

    var value: int;

    function method IsValid() : bool reads this
    {
        this.value % 2 == 0
    }

    constructor(value: int) 
        requires value % 2 == 0
        ensures this.IsValid()
    {
        this.value := value;
    }

    function method Sum(a: int, b: int) : int 
    {
        a + b
    }
}

static method {:synthesize} freshEven() returns (e:Even) ensures fresh(e)

static method {:synthesize} MockSum() returns (e:Even) 
    ensures fresh(e) 
    ensures e.Sum(2, 2) == 3

The methods annotated with {:synthesize} are automatically translated to the following Java:

public static EvenAddition_Compile.Even freshEven() {
  return new EvenAddition_Compile.Even();
}

public static EvenAddition_Compile.Even MockSum() {
  EvenAddition_Compile.Even eMock = org.mockito.Mockito.mock(EvenAddition_Compile.Even.class);
  org.mockito.Mockito.when(eMock.Sum(java.math.BigInteger.valueOf(2L), java.math.BigInteger.valueOf(2L))).thenReturn(java.math.BigInteger.valueOf(3L));
  return eMock;
}

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[cpitclaudel]

Thanks! I saw that part. Given that the feature is growing (to support more languages), I'm wondering whether the whole mocking / testing aspect shouldn't be developed out-of tree.

[keyboardDrummer]

Thanks! I saw that part. Given that the feature is growing (to support more languages), I'm wondering whether the whole mocking / testing aspect shouldn't be developed out-of tree.

Without a stable public API for DafnyPipeline, I don't see how this could be developed from another repository without often breaking. How do you see that working?

[cpitclaudel]

How do you see that working?

I was hoping we could use this as a way to develop a stable plugin API sufficient for this use case

[keyboardDrummer]

How do you see that working?

I was hoping we could use this as a way to develop a stable plugin API sufficient for this use case

My guess is that getting to an API that we would feel comfortable calling stable would require some refactoring. By keeping this consumer in our repository, we can do such refactorings without breaking them. I think we should drive this the other way around, wait for a problem that occurs from having too much in a single repository, and then allocate time to define the API and separate something out to a new repo.

[cpitclaudel]

Got it, thanks!

[cpitclaudel]

Sorry, clicked the wrong button :/

[hirataqdees]

Hi Dafny team,
We, at ARI, are looking into generating some Java tests from a Dafny model, and it would be great if this CR is reviewed/merged with the mainline! :)

Thanks

[keyboardDrummer]

Hi Dafny team, We, at ARI, are looking into generating some Java tests from a Dafny model, and it would be great if this CR is reviewed/merged with the mainline! :)

Thanks

Could you resolve the merge conflicts in the PR?

[robin-aws]

Glad to see there's interest in this PR @hirataqdees!

@cassidywaldrip - we need to get a clearer view of what the proposed changes are here before we can review, especially the {:synthesize} semantics changes. There are remnants of other changes in here that are muddying the waters. Can you please update from master and resolve the conflicts?

[cassidywaldrip]

Hi @robin-aws, I updated from master and resolved the conflicts. Let me know if there are other issues that come up. I'll try to be available to fix them right away.

[robin-aws]

Thanks for tidying this up! I've added one comment we should address before I review the rest, and my apologies for not having all the state paged into my head from the last time we discussed it. :) On the other hand, having thought on this for a while may have changed the strength of my opinion on it.

[robin-aws]

My intention for suggesting the name {:synthesize ... } for this feature was to keep the semantics as abstract as possible: create an object whose behavior aligns with the specification. Using a mocking framework is just one possible implementation strategy, and one that could change in the future: alternatively you could actually synthesize source code in the target language that obeys the specification.

I'm concerned about committing to the semantics of {:synthesize "fresh"}, since AFAICT those semantics are to return a new instance of an object without invoking any constructor. Depending on the compilation strategy, that could easily create an object that causes errors/crashes/exceptions when used, rather than the intention (I believe) of producing a valid but underspecified object, whose fields are initialized arbitrarily.

It seems to me that it is only valid to use {:synthesize "fresh"} if fresh(o) is literally the only specified post-condition. Could you switch implementation strategies automatically based on that instead? Alternatively, could you stick with the mocking implementation instead, in the name of simplicity? (I recall we discussed this earlier but I can't recall the reason for wanting to make this distinction).

[cassidywaldrip]

I have updated this branch so that it matches the C# version of synthesize. I did this by using spies instead of mocks. By using spies, the need for a "fresh" argument is eliminated, as fields can be accessed and updated in a spy (they could not be with a mock). A spy allows for the same customization of behavior as a mock. The difference is that a spy comes with all the functionality of a real object by default, and that functionality can be changed, whereas a mock comes with none of the functionality of a real object by default, so everything must be added.

[robin-aws]

Excellent, I'm so much happier with that! Thanks for sticking with this for the better outcome. :)

Please do revert this documentation change since it's not needed any more, aside from the Java specific remarks below.

[robin-aws]

Great news on not needing "mock" / "fresh" any more! I've done a proper review now and I think we're pretty close here.

(since I can't comment on deleted files) Why was DafnyTests.csproj deleted?

[robin-aws]

Excellent, I'm so much happier with that! Thanks for sticking with this for the better outcome. :)

Please do revert this documentation change since it's not needed any more, aside from the Java specific remarks below.

[robin-aws]

This generally LGTM, but it seems like there's a ripe opportunity to introduce a common base class for this and the CsharpSynthesizer class to reduce the duplication. I don't want to further delay this PR now that we're better aligned on the design, but I'd appreciate it if you could time-box a bit of time to refactor - if it becomes a rathole I'd settle for a TODO comment.

[cassidywaldrip]

Hi! I introduced a common Synthesizer base class and fixed the things you suggested.

[robin-aws]

LGTM! Just a couple final bookkeeping tasks, if you please:

1. Remove the line here stating that the Java backend doesn't support synthesis? https://github.com/dafny-lang/dafny/blob/master/Source/DafnyCore/Compilers/Compiler-java.cs#L47. That will update the reference manual's table of supported features per compiler.
2. Add a docs/dev/2024.feat file with a release note for this, something along the lines of "The Java backend now supports the {:synthesize} attribute".
3. Update the PR description to account for the design change since it was first cut (I'll use it as the commit message when we squash and merge this)

Thanks so much for the contribution!