Summary
Dafny is a verification-ready programming language. As you type in your program, Dafny's verifier constantly looks over your shoulder, flags any errors, shows you counterexamples, and congratulates you when your code matches your specifications. When you're done, Dafny can compile your code to C#, Java, JavaScript or Go (more to come!), so it can integrate with your existing workflow. Dafny will give you assurance that your code meets the specifications you write, while letting you write both code and specifications in the Dafny programming language itself. Since verification is an integral part of development, it will thus reduce the risk of costly late-stage bugs that are typically missed by testing. Dafny has support for common programming concepts such as classes and trait inheritance, inductive datatypes that can have methods and are suitable for pattern matching, lazily unbounded datatypes, subset types e.g. for bounded integers, lambdas, and immutable and mutable data structures. Dafny also offers an extensive toolbox for mathematical proofs, such as unbounded and bounded quantifiers, calculational proofs, pre- and post-conditions, termination conditions, loop invariants, and read/write specifications.
Versions
v4.10.0 :: 0 :: gentoo
- Modified
- License
- MIT
- Keywords
- amd64
- USE flags
- debug test
v4.9.1 :: 0 :: gentoo
- Modified
- License
- MIT
- Keywords
- amd64
- USE flags
- debug test
v4.9.0 :: 0 :: gentoo
- Modified
- License
- MIT
- Keywords
- ~amd64
- USE flags
- debug test
v4.8.1 :: 0 :: gentoo
- Modified
- License
- MIT
- Keywords
- amd64
- USE flags
- debug test
v4.8.0 :: 0 :: gentoo
- Modified
- License
- MIT
- Keywords
- amd64
- USE flags
- debug test
USE flags
General
- debug
- Enable extra debug codepaths, like asserts and extra output. If you want to get meaningful backtraces see https://wiki.gentoo.org/wiki/Project:Quality_Assurance/Backtraces
- test
- Enable dependencies and/or preparations necessary to run tests (usually controlled by FEATURES=test but can be toggled independently)
Dependencies
dev-java / java-config : Java environment configuration query tool
Runtime Dependencies
dev-java / java-config : Java environment configuration query tool
dev-lang / dafny-bin : Verification-aware programming language
sci-mathematics / z3 : An efficient theorem prover
virtual / dotnet-sdk : Virtual for .NET SDK
Depending packages
dev-lang / dafny-bin : Verification-aware programming language
Change logs
- Repository mirror & CI · gentoo
Merge updates from master - Arthur Zamarin · gentoo
dev-lang/dafny: Stabilize 4.10.0 amd64, #951433
Signed-off-by: Arthur Zamarin <arthurzam@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Sam James · gentoo
dev-lang/dafny: Stabilize 4.9.1 amd64, #950605
Signed-off-by: Sam James <sam@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: Stabilize 4.8.1 amd64, #942017
Closes: https://bugs.gentoo.org/942017 Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: bump to 4.10.0
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: bump to 4.9.1
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Michał Górny · gentoo
Rename dev-python/{OutputCheck → outputcheck}
Signed-off-by: Michał Górny <mgorny@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Matt Jolly · gentoo
*/*: update for slotted Rust
Tidyups: - $(cargo_crate_uris) - Rust BDEPENDS come from the eclass except in very rare circumstances (RUST_OPTIONAL=1) - RUST_M{AX,IN}_VER where required. - Suboptimal crate separator (`-` -> `@`) Signed-off-by: Matt Jolly <kangie@gentoo.org> Closes: https://github.com/gentoo/gentoo/pull/39218 Signed-off-by: Matt Jolly <kangie@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: remove tests failing with GCC 14
Closes: https://bugs.gentoo.org/942775 Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: bump to 4.9.0
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: drop old 4.7.0
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Sam James · gentoo
dev-lang/dafny: Stabilize 4.8.0 amd64, #940558
Signed-off-by: Sam James <sam@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: bump to 4.8.1
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: bump to 4.8.0
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Maciej Barć · gentoo
dev-lang/dafny: drop old 4.6.0
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Arthur Zamarin · gentoo
dev-lang/dafny: Stabilize 4.7.0 amd64, #937075
Signed-off-by: Arthur Zamarin <arthurzam@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: bump to 4.7.0
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: drop old 4.5.0
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Sam James · gentoo
dev-lang/dafny: Stabilize 4.6.0 amd64, #932860
Signed-off-by: Sam James <sam@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: drop old 4.4.0-r1
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Maciej Barć · gentoo
dev-lang/dafny: disable broken c++ tests
Closes: https://bugs.gentoo.org/930488 Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Matoro Mahri · gentoo
dev-lang/dafny: Stabilize 4.5.0 amd64, #930160
Signed-off-by: Matoro Mahri <matoro_gentoo@matoro.tk> Signed-off-by: Ionen Wolkens <ionen@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: use edo instead of edob
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: bump to 4.6.0
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: disable tests requiring cargo
Closes: https://bugs.gentoo.org/927242 Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: add missing psutil test dependency
Closes: https://bugs.gentoo.org/927225 Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: bump to 4.5.0
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: drop old 4.3.0-r1
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: Stabilize 4.4.0-r1 amd64, #922370
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: bring Java support back
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: bump to 4.4.0
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Sam James · gentoo
dev-lang/dafny: Stabilize 4.3.0-r1 amd64, #917307
Signed-off-by: Sam James <sam@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: patch out .NET framework
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: clean environment in pkg_setup
force clean _JAVA_OPTIONS Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Maciej Barć · gentoo
dev-lang/dafny: drop old 4.2.0
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: bump to 4.3.0
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: add "go" test dependency
Closes: https://bugs.gentoo.org/914372 Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: add missing src_unpack to support git
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
dev-lang/dafny: new package; add 4.2.0
Signed-off-by: Maciej Barć <xgqt@gentoo.org>