-
Notifications
You must be signed in to change notification settings - Fork 2
/
index.html
98 lines (87 loc) · 4.91 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
<!doctype html>
<html lang="en">
<head>
<meta charset="utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1">
<title>Dafny</title>
<link href="style.css" rel="stylesheet">
<meta name="description" content="The Dafny Programming and Verification Language and tools.">
<meta name="author" content="Dafny project">
<meta property="og:title" content="Dafny">
<meta property="og:type" content="website">
<meta property="og:url" content="https://dafny.org">
<meta property="og:description" content="The Dafny Programming and Verification Language and tools">
<meta property="og:image" content="image.png">
<link rel="icon" href="images/dafny-favicon.png" type="image/png">
<link rel="icon" href="images/dafny-favicon.svg" type="image/svg+xml">
</head>
<body>
<header>
<h1>The Dafny Programming and Verification Language</h1>
<!-- VERSION INFO HERE-->
</header>
<nav>
<h2>Quick Links</h2>
<ul>
<li><a href="https://github.com/dafny-lang/dafny/wiki/INSTALL"><b>Installation</b></a>
(or a <a href="https://marketplace.visualstudio.com/items?itemName=dafny-lang.ide-vscode">VSCode plugin for Dafny</a>)</li>
<li><a href="./latest/DafnyRef/DafnyRef">Dafny Reference Manual and User Guide</a></li>
<li><a href="./latest/toc">Dafny Resources for Users</a></li>
<li><a href="https://github.com/dafny-lang/dafny">Dafny GitHub project (for developers of the Dafny tools themselves)</a></li>
<li><a href="Snapshots">Other documentation snapshots</a></li>
<li><a href="https://mitpress.mit.edu/9780262546232/program-proofs"><i><b note="We can deemphasize this announcement on March 2024 or later">Book on Program Proofs using Dafny!:</b></i> <I>Program Proofs</i>, by Rustan Leino, MIT Press</a></li>
</ul>
<h2><a href="https://dafny.org/blog"><b>Blog</b></a><iframe src="/blog/" style="display:none"></iframe></h2>
</nav>
<main>
<p>
<img id="logo" src="images/dafny-logo.jpg" alt="The Dafny logo, showing the word Dafny in blue next to wavy black and blue lines.">
<b>Dafny</b> is a verification-aware programming language that has native support for recording specifications
and is equipped with a static program verifier.
By blending sophisticated automated reasoning with familiar programming idioms and tools,
Dafny empowers developers to write provably correct code (w.r.t. specifications).
It also compiles Dafny code to familiar development environments such as C#, Java, JavaScript, Go and Python (with more to come) so Dafny can integrate with your existing workflow.
Dafny makes rigorous verification an integral part of development,
thus reducing costly late-stage bugs that may be missed by testing.
</p>
<p>
In addition to a verification engine to check implementation against specifications,
the Dafny ecosystem includes several compilers,
plugins for common software development IDEs,
a LSP-based Language Server,
a code formatter,
a reference manual,
tutorials,
power user tips,
books,
the experiences of professors teaching Dafny,
and the accumulating expertise of industrial projects using Dafny.
</p>
<p>Dafny has support for common programming concepts such as </p>
<ul>
<li>mathematical and bounded integers and reals, bit-vectors, classes, iterators, arrays, tuples, generic types, refinement and inheritance,</li>
<li><a href="./latest/DafnyRef/DafnyRef#sec-inductive-datatypes">inductive datatypes</a> that can have methods and are suitable for pattern matching,</li>
<li><a href="./latest/DafnyRef/DafnyRef#sec-co-inductive-datatypes">lazily unbounded datatypes</a>,</li>
<li><a href="./latest/DafnyRef/DafnyRef#sec-subset-types">subset types</a>, such as for bounded integers,</li>
<li><a href="./latest/DafnyRef/DafnyRef#sec-lambda-expressions">lambda expressions</a> and functional programming idioms,</li>
<li>and <a href="./latest/DafnyRef/DafnyRef#sec-collection-types">immutable and mutable data structures</a>.</li>
</ul>
<p>Dafny also offers an extensive toolbox for mathematical proofs about software, including</p>
<ul>
<li><a href="./latest/DafnyRef/DafnyRef#sec-quantifier-domains">bounded and unbounded quantifiers</a>,</li>
<li><a href="./latest/DafnyRef/DafnyRef#sec-calc-statement">calculational proofs</a> and the ability to use and prove lemmas,</li>
<li><a href="./latest/DafnyRef/DafnyRef#sec-specification-clauses">pre- and post-conditions, termination conditions, loop invariants, and read/write specifications</a>.</li>
</ul>
<figure id="snapshot">
<img src="images/Demo.png" alt="A snippet of code shown in the VSCode IDE showing an implementation of the Dutch national flag problem written in Dafny. IDE extensions are showing successes and failures in verification reported by the Dafny Language Server running in real time.">
<figcaption>Dafny running in Visual Studio Code</figcaption>
</figure>
</main>
<script>
var frame = document.querySelector("iframe");
frame.addEventListener( "load", function(e) {
frame.outerHTML = x.contentWindow.document.querySelector("ul.post-list").outerHTML
} );
</script>
</body>
</html>