Skip to content

Issues: dafny-lang/dafny

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Clear current search query, filters, and sorts
13 Open 22 Closed
13 Open 22 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Dafny 5.0 idea: Unify syntax between functions and methods (WIP) breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability) part: language definition Relating to the Dafny language definition itself
#6180 opened Apr 4, 2025 by robin-aws
3
[PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-encryption-sdk-dafny breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability)
#5486 opened May 23, 2024 by aws-crypto-tools-ci-bot
340
Detect and report use of mixing options that change semantics breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability) crash Dafny crashes on this input, or generates malformed code that can not be executed during 3: execution of incorrect program An bug in the verifier that allows Dafny to run a program that does not correctly implement its spec introduced: pre-2012 invalid translated code The compiler generates invalid code, making the the target language infrastructure crash kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny logic An inconsistency in Dafny's logic (e.g. in the Boogie prelude) priority: not yet Will reconsider working on this when we're looking for work
#3556 opened Feb 16, 2023 by davidcok Library support
@robin-aws
6
Change of argument syntax for reveal statements breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability) kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#2689 opened Sep 2, 2022 by RustanLeino
4
Dafny 4.0 suggestion: Line and Column indexed the same breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability)
#2452 opened Jul 19, 2022 by MikaelMayer
8
Dafny 4 Suggestion: Improvements to iterators breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability)
#2440 opened Jul 18, 2022 by davidcok
2
Dafny 4 suggestion: Replace subset types "type" by "predicate type" breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability) misc: language proposals Proposals for change to the language that go beyon simple enhancement requests
#2368 opened Jul 6, 2022 by MikaelMayer
Dafny 4.0 idea: don't compile included files by default breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability) kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: tools Tools built on top of Dafny
#2359 opened Jul 4, 2022 by robin-aws
2
Dafny 4.0 suggestion: var pattern matching breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability) misc: language proposals Proposals for change to the language that go beyon simple enhancement requests part: language definition Relating to the Dafny language definition itself
#2343 opened Jun 30, 2022 by MikaelMayer
7
Dafny 4.0 suggestion: Get rids of returns keyword to unify function, predicate and methods breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability) misc: language proposals Proposals for change to the language that go beyon simple enhancement requests part: language definition Relating to the Dafny language definition itself
#2342 opened Jun 30, 2022 by MikaelMayer
9
Dafny 4.0 suggestion: for i <- 0 to 10 instead of for i := 0 to 10 breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability) misc: language proposals Proposals for change to the language that go beyon simple enhancement requests part: language definition Relating to the Dafny language definition itself
#2341 opened Jun 30, 2022 by MikaelMayer
4
Dafny 4.0 suggestion: Remove automatic compile-time filtering of subset types breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability) misc: language proposals Proposals for change to the language that go beyon simple enhancement requests part: language definition Relating to the Dafny language definition itself
#2339 opened Jun 30, 2022 by MikaelMayer
3
Default to nameonly Dafny V4 breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability) misc: language proposals Proposals for change to the language that go beyon simple enhancement requests
#2318 opened Jun 29, 2022 by seebees
5
ProTip! Type g i on any issue or pull request to go back to the issue listing page.