Option to copy over specifications for traits

[seebees]

When working with abstract modules the specifications are copied over automatically.
It would be nice to add something similar for trait .

[robin-aws]

You're proposing a workaround for #2500 I assume? Do you mean literally copy the text of the specifications from a trait into the definition of a class that extends it?

[seebees]

Not quite.

I don't see any reason per se
that Dafny requires that I copy these things over.
I'm guessing that the implementation detail
of how abstract module literally copies code is in play,
but the customer experience should be the same yes?

The following currently fails
with the method must provide an equal or more detailed postcondition than in its parent trait.
I'm proposing that it would succeed.

  trait Foo {
    method Bar() returns (i: int)
      ensures 10 < i < 100
  }

  class {:magic} Baz extends Foo {

    method Bar() returns (i: int)
    {
      return 15;
    }
  }

Similar to

abstract module Foo {

  method Bar() returns (i: int)
    ensures 10 < i < 100

}

module Baz refines Foo {

  method Bar() returns (i: int)
  {
    return 15;
  }

}

[robin-aws]

Ah got it, thanks for clarifying. So this would be a usability improvement to avoid having to copy text around.

Reasonable idea, but I know this is coming up in the context of #2500 - I'm going to update that issue and continue discussion about how to fix that issue specifically, which may or may not involve this feature.