Allow redeclaring trait methods #6280

keyboardDrummer · 2025-06-24T12:39:53Z

What was changed?

Allow overriding instance methods

How has this been tested?

Added test overrides.dfy and updated existing tests

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

robin-aws

SO excited for this, but still exercising caution

robin-aws · 2025-06-24T17:18:38Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/overrides.dfy

+
+trait T {
+  method foo() returns (r: int)  {
+    return 3;


I would add ensures r >= 3, ensures r >= 5, etc to all the foo methods and a few precise assertions in Main that depend on the concrete types, just to show that verification is aware of the overriding and not just allowing them to be declared but ignoring them.

just to show that verification is aware of the overriding and not just allowing them to be declared but ignoring them.

Overriding bodyless members and narrowing the contract was already allowed and is already tested. This test focusses on the bodies and for that it needs to run the code and inspect the result, which it does. I've renamed the test to redeclare_body.dfy

I still think testing that the contract narrowing works when there's overriding is worth it from an opaque testing coverage POV, but if you think the coverage is adequate given how this is all implemented I won't block on that.

I still think testing that the contract narrowing works when there's overriding

You're right. I'll add it

robin-aws · 2025-06-24T17:20:10Z

Source/DafnyCore/AST/Members/MethodOrFunction.cs

        $"To silence this warning, please add an {{:axiom}} attribute or use the option '--allow-external-contracts'");
    }
-    if (!AutoGeneratedOrigin.Is(Origin) && HasVerifyFalseAttribute) {
+    if (!AutoGeneratedOrigin.Is(Origin) && HasVerifyFalseAttribute && !resolver.Options.Get(CommonOptionBag.AllowAxioms)) {


Still blocking on this as per #6279, but AFAICT you can remove those changes from this PR?

robin-aws · 2025-06-24T17:28:37Z

...IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeMemberResolution.dfy.expect

-GeneralNewtypeMemberResolution.dfy(103,14): Error: field 'Items' is inherited from type 'map' and is not allowed to be re-declared in newtype 'Map'
-GeneralNewtypeMemberResolution.dfy(107,14): Error: field 'Keys' is inherited from type 'imap' and is not allowed to be re-declared in newtype 'IMap'
-GeneralNewtypeMemberResolution.dfy(108,14): Error: field 'Values' is inherited from type 'imap' and is not allowed to be re-declared in newtype 'IMap'
+GeneralNewtypeMemberResolution.dfy(51,13): Error: fully defined function 'F' is inherited from trait 'Bool' and is not allowed to be re-declared


These are regressions, the error message is referring to Bool as if it's a trait, but it's actually a newtype. Probably there's another place this is checked past the part you changed that just needs tweaking?

Thanks, fixed it.

robin-aws · 2025-06-24T17:30:47Z

Source/DafnyCore/Resolver/ModuleResolver.cs

-        if (trait is not TraitDecl) {
-          reporter.Error(MessageSource.Resolver, member.Origin,
-            $"{traitMember.WhatKindAndName} is inherited from {trait.WhatKindAndName} and is not allowed to be re-declared in {cl.WhatKindAndName}");
-        } else if (traitMember.IsStatic) {


Awesome that this seems to be all that's needed, but I think we're in Chesterton's Fence territory and I want to hear from @RustanLeino that there isn't some secret soundness reasons for this we aren't seeing. :)

I think you could argue that Dafny should not allow providing a body for the same member twice, since both bodies must satisfy the contract so having two is redundant. That said, I think putting unspecified behavior in the body, like logging, is a valid use-case so it should be allowed.

It's even more important for compiled code, because you can provide a body that's semantically equivalent but much more efficient! IOW it should be allowed for the same reason we have function-by-method :) I'm really looking forward to declaring these kinds of default implementations once in the traits instead of copying them over and over: https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/src/Std/Actions/Producers.dfy#L878-L910

This is a fairly plausible motivation for why it wasn't allowed historically though, especially if traits were added before the first compiler.

Awesome that this seems to be all that's needed, but I think we're in Chesterton's Fence territory and I want to hear from @RustanLeino that there isn't some secret soundness reasons for this we aren't seeing. :)

Prefer that we merge and revert if there's a problem. If someone added this restriction to avoid a soundness bug, then they should have added a test that checks whether the soundness bug is there, but there is not such test (since all the tests are passing).

I absolutely agree that's the optimal approach and would like to think that's what either of us would have done :) but I don't want to trust that whoever set this up in years past would have.

How about keeping this behind an internal flag for the near future, so we can use this functionality right away but buy ourselves some time before we need to feel confident on soundness for general use?

RustanLeino

Here are some additional tests to add.

Refinement checks

Robin had suggests adding some tests that make sure the right specs are used. Good that you've added such. In addition, please add tests that ensure that refinement tests are still being done (that is, to make sure the verifier doesn't skip those when it sees the base method already has a body).

Termination

Make sure that virtually dispatched calls are properly checked for termination

trait T extends object {
  method M() {
    if this is C {
      var c := this as C;
      c.M(); // error: cannot prove termination
    }
  }
  method N() {
  }
}

class C extends T {
  method M() {
    var t := this as T;
    t.M(); // error: cannot prove termination
  }
  method N() {
    var t := this as T;
    t.N(); // error: cannot prove termination
  }
}

Diamond property

The following should not be allowed:

trait W { method M() { } }
trait X extends W { method M() { } }
trait Y extends W { method M() { } }
trait Z extends X, Y { } // error: Z inherits M with a body in two different ways

Dafny already gives an error in Z if W does not give a body for M. Please add a test that makes sure this error is reported also if W does give a body for M. In fact, an error should also be reported if Z also re-declares M with a body.

RustanLeino · 2025-06-30T23:02:39Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/overrides.dfy

+}
+
+trait T2 extends T {
+  method foo() returns (r: int)  {


Rename foo Foo here and throughout to adhere to standard Dafny naming conventions.

RustanLeino · 2025-06-30T23:04:57Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/redeclare_body.dfy

+  var t: T := t2;
+  var rt := t.foo();
+  assert rt >= 3;
+  print rc, ", ", rd, ", ", re, ", ", rf, ", ", rt, ", ", rt2;


Also good to have some tests that cause verification failures, lest all of the assertions above pass because of an accidental contradiction in the generated Boogie.

RustanLeino · 2025-06-30T23:07:37Z

Source/DafnyCore/Resolver/ModuleResolver.cs


-        var traitMember = member.OverriddenMember;
-        var trait = traitMember.EnclosingClass;
-        if (trait is not TraitDecl) {


The removal of this test is a regression. It used to trigger the error GeneralNewtypeMemberResolution.dfy(48,11), which is now missing.

RustanLeino · 2025-06-30T23:08:33Z

...IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeMemberResolution.dfy.expect

@@ -1,13 +1,12 @@
 GeneralNewtypeMemberResolution.dfy(6,8): Error: mutable fields are allowed only in reference types (consider declaring the field as a 'const')
-GeneralNewtypeMemberResolution.dfy(48,11): Error: method 'PrintMe' is inherited from newtype 'Bool' and is not allowed to be re-declared in newtype 'BoolBool'


The removal of the branch trait is not TraitDecl in ModuleResolver.cs is what's causing this error message to disappear. The test is needed.

RustanLeino · 2025-06-30T23:22:18Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/overrides.dfy

+  var rd := d.foo();
+  var e := new E;
+  var re := e.foo();
+  var f := new F;


I would add : F as well, just in case type inference gets the crazy idea to make the type of f T2 as well.

RustanLeino · 2025-06-30T23:24:32Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/overrides.dfy

+    return 6;
+  }
+}
+


Also add a datatype G extends T = ... to the tests.

- windows-2019 is deprecated by GitHub Actions - Updated all workflow files to use windows-2022 - Issue dafny-lang#1906 that previously blocked windows-2022 is now closed - Files updated: - .github/workflows/release-downloads-nuget.yml - .github/workflows/release-downloads.yml - .github/workflows/xunit-tests-reusable.yml - .github/workflows/integration-tests-reusable.yml

Chores don't warrant news items as they have no user-visible impact

- Scripts/package.py also referenced windows-2019 for release packaging - Updated to windows-2022 for consistency with CI workflows - Ensures release packages are built with current Windows runner

Rustan is reviewing

Co-authored-by: Mikaël Mayer <[email protected]>

robin-aws · 2025-07-03T15:16:59Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/redeclare_body_resolution.dfy

+trait Common { method M() { } }
+trait Left extends Common { method M() { } }
+trait Right extends Common { method M() { } }
+trait Both extends Left, Right { } // error: Z inherits M with a body in two different ways


Minor: no Z in the actual test case

robin-aws · 2025-07-03T15:20:14Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/redeclare_body_resolution.dfy

Minor: snake case file names look out of place to me (but open to being convinced it's better for some reason)

robin-aws · 2025-07-03T15:21:52Z

docs/dev/news/6280.feat

@@ -0,0 +1 @@
+Dafny classes and traits can now redeclare members defined by traits they inherit from.


Should be only methods and not all members, right?

robin-aws · 2025-07-03T15:22:58Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/redeclare_body_verification.dfy

Is there a case where verification of a call only succeeds because a class overrides a trait method and provides a stronger specification? I thought there was one in an earlier version I don't see now.

Added a test

robin-aws

🚀

Robin reviewed

RustanLeino · 2025-07-07T19:37:17Z

Thanks, @keyboardDrummer and @robin-aws!

keyboardDrummer marked this pull request as ready for review June 24, 2025 13:48

keyboardDrummer requested a review from robin-aws June 24, 2025 15:20

keyboardDrummer changed the title ~~Overrides~~ Allow redeclaring trait methods Jun 24, 2025

robin-aws previously requested changes Jun 24, 2025

View reviewed changes

keyboardDrummer requested a review from robin-aws June 25, 2025 10:58

RustanLeino previously requested changes Jun 30, 2025

View reviewed changes

fabiomadge added 3 commits July 1, 2025 16:35

chore: Remove unnecessary news entry

1401b68

Chores don't warrant news items as they have no user-visible impact

chore: Update package.py to use windows-2022

c176d72

- Scripts/package.py also referenced windows-2019 for release packaging - Updated to windows-2022 for consistency with CI workflows - Ensures release packages are built with current Windows runner

keyboardDrummer requested a review from RustanLeino July 1, 2025 15:57

keyboardDrummer enabled auto-merge (squash) July 1, 2025 15:57

fabiomadge and others added 2 commits July 1, 2025 21:17

Apply suggestions from code review

a30e6f1

Co-authored-by: Mikaël Mayer <[email protected]>

All changes

3d7b4e3

keyboardDrummer force-pushed the overrides branch from e908e3d to 3d7b4e3 Compare July 2, 2025 11:14

keyboardDrummer added 2 commits July 2, 2025 15:05

Merge branch 'chore/fix-windows-ci-targets' into overrides

d2c89fb

Add more tests

55a870e

robin-aws requested changes Jul 3, 2025

View reviewed changes

Improvements

fc82396

keyboardDrummer requested a review from robin-aws July 3, 2025 16:06

robin-aws approved these changes Jul 3, 2025

View reviewed changes

keyboardDrummer merged commit af2aafb into dafny-lang:master Jul 3, 2025
22 checks passed

keyboardDrummer deleted the overrides branch July 3, 2025 18:56

botantony mentioned this pull request Aug 26, 2025

dafny 4.11.0 Homebrew/homebrew-core#234941

Merged

		@@ -1,13 +1,12 @@
		GeneralNewtypeMemberResolution.dfy(6,8): Error: mutable fields are allowed only in reference types (consider declaring the field as a 'const')
		GeneralNewtypeMemberResolution.dfy(48,11): Error: method 'PrintMe' is inherited from newtype 'Bool' and is not allowed to be re-declared in newtype 'BoolBool'

		@@ -0,0 +1 @@
		Dafny classes and traits can now redeclare members defined by traits they inherit from. No newline at end of file

Allow redeclaring trait methods #6280

Allow redeclaring trait methods #6280

Uh oh!

Conversation

keyboardDrummer commented Jun 24, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What was changed?

How has this been tested?

Uh oh!

robin-aws left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

keyboardDrummer Jun 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

keyboardDrummer Jun 25, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

keyboardDrummer Jun 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

RustanLeino left a comment

Choose a reason for hiding this comment

Refinement checks

Termination

Diamond property

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

robin-aws left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

RustanLeino commented Jul 7, 2025

Uh oh!

keyboardDrummer commented Jun 24, 2025 •

edited

Loading

keyboardDrummer Jun 26, 2025 •

edited

Loading

keyboardDrummer Jun 25, 2025 •

edited

Loading

keyboardDrummer Jun 26, 2025 •

edited

Loading