fix: Use {:test} and {:synthesize} in automatically generated tests

[Dargones]

This PR makes test generation code produce methods annotated with {:test} and {:synthesize}, which can then be automatically compiled to C# by the Dafny compiler (and in future to other languages). This approach is much simpler than the one previously used, which is to manually insert Java reflection code.

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

[atomb]

This is a nice improvement. Thanks!

[Dargones]

Thank you for catching the typo, @atomb! Have committed it (but that dismisses the review)

[Dargones]

Thank you for updating this, @MikaelMayer! The failing test (EnsuresPriorityWorksEvenIfRemovingMethodsWhileTypo) seems to be unrelated to this PR and failing for some of the recent commits to master as well. Am I right that it must have something to do with the Language Server?

[MikaelMayer]

Thank you for updating this, @MikaelMayer! The failing test (EnsuresPriorityWorksEvenIfRemovingMethodsWhileTypo) seems to be unrelated to this PR and failing for some of the recent commits to master as well. Am I right that it must have something to do with the Language Server?

Yes you are right. @keyboardDrummer and I are working hard to resolve the bug here:
#2352
So basically, you can just wait. Thanks for your patience.