Skip to content

by method bodies on refined methods are ignored #2231

Open
@cpitclaudel

Description

@cpitclaudel

Dafny accepts the following:

module Base {
  predicate method A()
}

module Derived refines Base {
  predicate A... {
    false
  } by method {
    return Uh?;
  }
}

Metadata

Metadata

Assignees

Labels

difficulty: good-first-issueGood first issueshas-workaround: noThere are no known workaroundskind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` labelpart: resolverResolution and typechecking

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions