### Run Jennisys Example

Source: https://github.com/dafny-lang/dafny/blob/master/Source/Jennisys/README.txt

Execute a Jennisys example file using the Jennisys executable. Ensure you are in the Jennisys directory.

```bash
cd Jennisys
bin/Debug/Jennisys.exe examples/<name>.jen
```

--------------------------------

### Install Go Imports Tool

Source: https://github.com/dafny-lang/dafny/blob/master/docs/Installation.md

Install the 'goimports' tool, which is a dependency for compiling Dafny to Go.

```bash
go install golang.org/x/tools/cmd/goimports@latest
```

--------------------------------

### Install Pre-commit Hooks

Source: https://github.com/dafny-lang/dafny/wiki/INSTALL

Installs pre-commit hooks for verifying C# file style. Ensure you have pip installed.

```bash
pip install pre-commit
pre-commit install
```

--------------------------------

### Install .NET SDK on macOS

Source: https://github.com/dafny-lang/dafny/wiki/INSTALL

Installs the .NET SDK, a prerequisite for building Dafny from source on macOS. Uses the Homebrew package manager.

```bash
brew install dotnet-sdk
```

--------------------------------

### Install Pre-commit Hooks (Linux)

Source: https://github.com/dafny-lang/dafny/wiki/INSTALL

Installs the pre-commit framework and configures it for the Dafny repository. This helps maintain code style consistency.

```bash
pip3 install pre-commit
pre-commit install
```

--------------------------------

### Example Release Note File: Feature

Source: https://github.com/dafny-lang/dafny/blob/master/docs/dev/README.md

This is an example of a release note file for a new feature. The filename uses a descriptive name and kind.

```text
new-toast-patterns.feat

Two new toast patterns:
- Dafny waterfall logo
-Dafny haircut logo
(They are the same.)
```

--------------------------------

### Running AutoExtern Example Command

Source: https://github.com/dafny-lang/dafny/blob/master/Source/AutoExtern/README.md

An example command demonstrating how to run the AutoExtern tool with specific file paths for the C# project, Dafny template, and output files.

```bash
$ dotnet run Library.csproj NS Library.dfy.template CSharpModel.dfy Library.dfy Library.cs
```

--------------------------------

### Quick Test Dafny Installation (Linux Binary)

Source: https://github.com/dafny-lang/dafny/blob/master/docs/Installation.md

Run a quick test script to verify your Dafny installation on Linux.

```bash
$INSTALL/dafny/quicktest.sh
```

--------------------------------

### Install Dafny via NuGet

Source: https://github.com/dafny-lang/dafny/blob/master/docs/Installation.md

Install Dafny globally as a .NET tool using the NuGet package manager.

```bash
dotnet tool install --global dafny
```

--------------------------------

### Install Pre-commit Hooks (macOS)

Source: https://github.com/dafny-lang/dafny/wiki/INSTALL

Installs the pre-commit framework using Homebrew and configures it for the Dafny repository on macOS.

```bash
brew install pre-commit
pre-commit install
```

--------------------------------

### Initial Function Example

Source: https://github.com/dafny-lang/dafny/blob/master/docs/HowToFAQ/FAQFunctionUnroll.md

This example demonstrates a scenario where a function's recursive application might not automatically unroll enough for proof.

```dafny
lemma {:my_lemma} Lem1(n: nat) requires n > 0
  ensures n == 0
{
  if n > 0 {
    // Lem1(n-1);
    // Lem1(n-1);
    Lem1(n-1);
  }
}
```

--------------------------------

### Install Z3 for macOS

Source: https://github.com/dafny-lang/dafny/wiki/INSTALL

Installs Z3 for macOS using a Makefile target. This is a convenient way to get the required Z3 version.

```bash
make z3-mac
```

--------------------------------

### Install Coverlet and ReportGenerator .NET Tools

Source: https://github.com/dafny-lang/dafny/wiki/Running-Dafny's-test-suite

Install the coverlet.console and dotnet-reportgenerator-globaltool .NET tools globally. These are required for measuring code coverage.

```sh
dotnet tool install --global coverlet.console
```

```sh
dotnet tool install --global dotnet-reportgenerator-globaltool
```

--------------------------------

### Install wget on macOS

Source: https://github.com/dafny-lang/dafny/wiki/INSTALL

Installs the wget utility using Homebrew, which may be needed for downloading Z3 binaries if not using the `make z3-mac` target.

```bash
brew install wget
```

--------------------------------

### Run Quick Test of Dafny Installation (Linux)

Source: https://github.com/dafny-lang/dafny/wiki/INSTALL

Executes a quick test script to verify the Dafny installation. This helps ensure that the build and basic functionality are working correctly.

```bash
dafny/Scripts/quicktest.sh
```

--------------------------------

### Basic Parser Example

Source: https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/src/Std/Parsers/DEBUGGING.md

This example demonstrates a simple parser for space-separated numbers. It is used to illustrate debugging techniques.

```dafny
import opened Std.Parsers.StringBuilders

const pDoc :=
  WS.e_I(Nat)   // Space then nat
  .Rep()        // Zero or more times
  .I_e(WS)      // Then space
  .End()        // Then end

method Main() {
  var input := " 1 2 3 4 ";
  var result := pDoc.Apply(input);
  expect result.ParseFailure?;
  print FailureToString(input, result);
}
```

--------------------------------

### Run Dafny (Windows Binary)

Source: https://github.com/dafny-lang/dafny/blob/master/docs/Installation.md

Execute Dafny from the command line after installing the Windows binary.

```bash
Dafny.exe
```

--------------------------------

### Example Release Note File: Bug Fix

Source: https://github.com/dafny-lang/dafny/blob/master/docs/dev/README.md

This is an example of a release note file for a bug fix. The filename indicates the issue number and kind.

```text
1234.fix

Dafny will now detect and report burning toast.
```

--------------------------------

### Basic Match Statement Examples

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/Statements.md

Demonstrates basic usage of the match statement with a list and an integer. The first example matches against a list pattern (Nil or Cons), while the second matches against integer values and a wildcard.

```dafny
match list {
  case Nil => {}
  case Cons(head,tail) => print head;
}
match x
case 1 =>
  print x;
case 2 =>
  var y := x*x;
  print y;
case _ =>
  print "Other";
  // Any statement after is captured in this case.

```

--------------------------------

### Dafny Newtype Conversion Example

Source: https://github.com/dafny-lang/dafny/blob/master/docs/HowToFAQ/FAQNewtype.md

Illustrates the type conversion rules between integers and newtypes in Dafny. This example requires the 'FAQNewtype.dfy' file.

```dafny
{% include_relative FAQNewtype.dfy %}
```

--------------------------------

### Start DafnyLanguageServer with .NET CLI

Source: https://github.com/dafny-lang/dafny/blob/master/Source/DafnyLanguageServer/README.md

Run the Dafny language server using the .NET CLI.

```shell
dotnet DafnyLanguageServer.dll
```

--------------------------------

### Run Dafny (macOS Binary)

Source: https://github.com/dafny-lang/dafny/blob/master/docs/Installation.md

Execute Dafny from the command line after installing the macOS binary.

```bash
$INSTALL/dafny/dafny
```

--------------------------------

### Start Dafny Language Server

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/UserGuide.md

Starts the Dafny Language Server, which implements the Language Server Protocol (LSP) for Dafny. This server is used by IDE extensions like the Dafny VSCode extension.

```bash
dafny server
```

--------------------------------

### Install LaTeX Packages for Reference Manual (macOS)

Source: https://github.com/dafny-lang/dafny/wiki/INSTALL

Installs necessary LaTeX packages (basictex, pandoc, framed, tcolorbox, environ, trimspaces) required for building the Dafny reference manual on macOS. It also updates the PATH and the TeX Live Manager.

```bash
brew install --cask basictex
brew install pandoc
eval "$(/usr/libexec/path_helper)"
sudo tlmgr update --self
sudo tlmgr install framed tcolorbox environ trimspaces
```

--------------------------------

### Dafny Cardinality Expression Examples

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/Expressions.md

Use the `|c|` syntax to get the cardinality of finite collections like sets, sequences, multisets, and maps. Cardinality is not defined for infinite collections.

```dafny
|s|
```

```dafny
|s[1..i]|
```

--------------------------------

### Trait Declaration Example

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/Modules.md

Illustrates a basic trait declaration with functions.

```dafny
trait Tr {
  function F(x: int): int { 10 }
  function G(x: int): int { 12 }
  function H(x: int): int { 14 }
}
```

--------------------------------

### Build and run integrated Python/Dafny example

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/integration-py/IntegrationPython.md

Commands to build the Dafny file and then execute a Python script that imports and uses the Dafny module. This demonstrates a common integration pattern.

```bash
dafny build --target:py Demo2.dfy
```

```bash
PYTHONPATH=.:Demo2-py python3 Demo2x.py
```

--------------------------------

### Basic Forall Statement Examples

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/Statements.md

Demonstrates the basic syntax of forall statements for array assignment, lemma invocation, and proof with ensures clauses.

```dafny
forall i | 0 <= i < a.Length {
  a[i] := 0;
}
```

```dafny
forall i | 0 <= i < 100 {
  P(i); // P a lemma
}
```

```dafny
forall i | 0 <= i < 100
  ensures i < 1000 {
}
```

--------------------------------

### Install Node.js Dependencies for JavaScript Compilation

Source: https://github.com/dafny-lang/dafny/wiki/INSTALL

Installs the 'bignumber.js' npm package, which is required for compiling Dafny to JavaScript. Ensure Node.js is installed.

```bash
npm install bignumber.js
```

--------------------------------

### Subsequence Slices Suffix Examples

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/Expressions.md

Shows how to apply subsequence slices to a sequence to produce a sequence of subsequences.

```dafny
a[ 0 : 2 : 3 ]
```

```dafny
a[ e1 : e2 : e3 ]
```

```dafny
a[ 0 : 2 : ]
```

--------------------------------

### Install Emacs Package

Source: https://github.com/dafny-lang/dafny/blob/master/docs/Installation.md

Install the 'boogie-friends' Emacs package for Dafny support. Ensure the flycheck-dafny-executable path is correctly set to your Dafny installation.

```Emacs Lisp
(setq flycheck-dafny-executable "[path to dafny]/dafny/Scripts/dafny")
```

--------------------------------

### Subsequence Suffix Examples

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/Expressions.md

Demonstrates how to extract subsequences from sequences or arrays using various range specifications.

```dafny
a[lo .. hi ]
```

```dafny
(e)[ lo .. ]
```

```dafny
e[ .. hi ]
```

```dafny
e[ .. ]
```

--------------------------------

### Install Python and Pip on Linux

Source: https://github.com/dafny-lang/dafny/wiki/INSTALL

Installs Python 3 and its package installer (pip) on Ubuntu-based Linux systems. This is a prerequisite for building Dafny from source.

```bash
sudo apt install python3 python3-pip
```

--------------------------------

### Create Plugin Directory

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/Plugins.md

Steps to set up a new directory for a Dafny plugin project.

```bash
mkdir PluginTutorial
cd PluginTutorial
```

--------------------------------

### Install Dafny via Brew (macOS)

Source: https://github.com/dafny-lang/dafny/blob/master/docs/Installation.md

Install Dafny on macOS using the Homebrew package manager.

```bash
brew install dafny
```

--------------------------------

### Dafny Factorial Function Example

Source: https://github.com/dafny-lang/dafny/blob/master/docs/QuickReference.md

An example of a recursive function declaration for Factorial, including a precondition and postcondition.

```dafny
function Factorial(n: int): int
  requires 0 <= n
  ensures 1 <= Factorial(n)
{
  if n == 0 then 1 else Factorial(n-1) * n
}
```

--------------------------------

### Create Dotnet Class Library

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/Plugins.md

Command to create a new .NET class library project for the plugin.

```bash
dotnet new classlib
```

--------------------------------

### Prepare Release Branch and Update Files

Source: https://github.com/dafny-lang/dafny/blob/master/docs/dev/RELEASE.md

Use this script to prepare for a new release. It checks repository status, creates a release branch, and updates build and release note files.

```bash
Scripts/prepare_release.py $VER prepare --source-branch <this branch>
```

--------------------------------

### Download and Build Dafny from Source (Linux)

Source: https://github.com/dafny-lang/dafny/wiki/INSTALL

Clones the Dafny repository and builds the executable. Ensure .NET 6.0 is installed beforehand. The `--recurse-submodules` flag is important for fetching all necessary components.

```bash
git clone https://github.com/dafny-lang/dafny.git --recurse-submodules
cd dafny
make exe
```

--------------------------------

### Trivially close-ended quantifier example

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/Types.md

An example of a universally quantified statement over integers, which is trivially close-ended as it does not involve object references.

```dafny
forall x: int :: x <= Square(x)
```

--------------------------------

### Run TestDafny CLI Help

Source: https://github.com/dafny-lang/dafny/blob/master/Source/TestDafny/README.md

Execute this command to display the general help text for the TestDafny command-line interface.

```bash
dotnet run --project Source/TestDafny/TestDafny.csproj
```

--------------------------------

### Dafny While Loop Example

Source: https://github.com/dafny-lang/dafny/blob/master/docs/OnlineTutorial/guide.md

A basic example of a 'while' loop in Dafny. This loop increments a counter 'i' until it reaches the value of 'n'.

```dafny
method m(n: nat)
{
  var i := 0;
  while i < n
  {
    i := i + 1;
  }
}
```

--------------------------------

### Aggregated Release Notes Example

Source: https://github.com/dafny-lang/dafny/blob/master/docs/dev/README.md

This shows how individual release note files are aggregated into the main RELEASE_NOTES.md file, including automatic PR linking.

```markdown
## New features

- Two new toast patterns:
  - Dafny waterfall logo
  - Dafny haircut logo
  (They are the same.)
  (https://github.com/dafny-lang/dafny/pull/5678)

## Bug fixes

-Dafny will now detect and report burning toast. (https://github.com/dafny-lang/dafny/pull/1234)
```

--------------------------------

### Set Comprehension Example with Tuples in Dafny

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/Expressions.md

Provides an example of a set comprehension that generates tuples based on quantified variables and conditions.

```dafny
var S := set x:nat, y:nat | x < y < 3 :: (x, y)
```

--------------------------------

### Creating and Comparing Sets

Source: https://github.com/dafny-lang/dafny/blob/master/docs/OnlineTutorial/Sets.md

Demonstrates initializing sets using display notation and comparing them for equality. The type of an empty set may be inferred from its usage.

```dafny
method m()
{
  var s1 := {}; // the empty set
  var s2 := {1, 2, 3}; // set contains exactly 1, 2, and 3
  assert s2 == {1,1,2,3,3,3,3}; // same as before
  assert s1 != s2;  // sets with different elements are different
  var s3, s4 := {1,2}, {1,4};
}
```

--------------------------------

### Dafny Type Definitions for Is Expression Examples

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/Expressions.md

Defines traits and classes used in examples illustrating the 'is' type test expression.

```dafny
trait A {
}
trait B<X> {
}
class C<Y> extends B<Y> {
}
class D<Y(==)> extends B<set<Y>> {
}
class E extends B<int> {
}
class F<Z> extends A {
}
```

--------------------------------

### Dafny Name Conflict Example

Source: https://github.com/dafny-lang/dafny/blob/master/docs/HowToFAQ/FAQNameConflict.md

This example demonstrates a name conflict where a module and a datatype share the same name, leading to resolution errors.

```dafny
module Test {
  datatype Result = Ok(int) | Error(string)

  method Test() {
    var r := Ok(5)
  }
}
```

--------------------------------

### Compile and Run Go Code with 'go run'

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/UserGuide.md

Compile and run the generated Go code using 'go run'. This requires navigating to the output directory and setting environment variables.

```bash
(cd A-go; GO111MODULE=auto GOPATH=`pwd` go run src/A.go)
```

--------------------------------

### Various Import Syntaxes

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/Modules.md

Illustrates the different syntaxes available for importing modules, including aliasing, qualified imports, and selective imports.

```dafny
import A
import opened B
import A = B
import A : B
import A.B
import A`E
import X = A.B`{E,F}
```

--------------------------------

### Dafny Extensionality Example

Source: https://github.com/dafny-lang/dafny/blob/master/docs/HowToFAQ/onepage.md

Provides an example demonstrating Dafny's need for explicit proof of set equality before reasoning about function application on those sets.

```dafny
assert s + {x} == {x} + s + {x};
assert G(s + {x}) == G({x} + s + {x});
```

--------------------------------

### Dafny Sub-module Refinement Example

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/Refinement.md

Demonstrates abstract module declarations and how modules can refine parent modules, importing declarations from the refinement result.

```dafny
abstract module P {
  module A { const i := 5 }
  abstract module B { type T }
}

module X refines P {
  module B' refines P.B { type T = int }
  module C { const k := 6}
}

module M {
  import X
  method m() {
    var z: X.B'.T := X.A.i + X.C.k;
  }
}
```

--------------------------------

### C# Source Code Example

Source: https://github.com/dafny-lang/dafny/blob/master/Source/AutoExtern/README.md

An example of C# code defining an interface and a class with a field and a property. This code serves as input for the AutoExtern tool.

```csharp
namespace NS;

public interface Intf {
  public string Prop { get; }
}

public class Impl : Intf {
  public int Field;
  public string Prop => Field.ToString();
}
```

--------------------------------

### Test Dafny Installation

Source: https://github.com/dafny-lang/dafny/blob/master/docs/dev/RELEASE.md

After the pull request is merged, reinstall Dafny using Homebrew and verify the installed version. It is recommended to test on a different machine if possible.

```bash
brew reinstall dafny
```

```bash
dafny /version
```

--------------------------------

### Proof Forall Statement Example

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/Statements.md

Demonstrates a proof forall statement used to establish equality between elements in two different states based on domain intersection.

```dafny
forall p | p in DomSt(stCombinedC.st) && p in DomSt(stExecC.st)
  ensures GetSt(p, stCombinedC.st) == GetSt(p, stExecC.st)
{
  assert DomSt(stCombinedC.st) <= DomSt(stExecC.st);
  assert stCombinedC.st == Restrict(DomSt(stCombinedC.st),
                                               stExecC.st);
}
```

--------------------------------

### Install Z3 Version 4.12.1 on Ubuntu

Source: https://github.com/dafny-lang/dafny/wiki/INSTALL

Installs a specific version of the Z3 solver required by Dafny on Ubuntu. This command uses a Makefile target for convenience.

```bash
make z3-ubuntu
```

--------------------------------

### Invalid Identifier Starting with Underscore in Dafny

Source: https://github.com/dafny-lang/dafny/blob/master/docs/HowToFAQ/Errors-Parser.md

User-declared identifiers cannot start with an underscore, as these are reserved for internal use. Single underscores in match statements act as wildcards.

```dafny
const _myconst := 5
```

--------------------------------

### Dafny Update and Call Statement Example

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/Statements.md

Demonstrates various update and call statement syntaxes including method calls, parallel assignments, havoc assignments, and such-that assignments.

```dafny
class C { var f: int }
class D {
  var i: int
  constructor (i: int) {
    this.i := i;
  }
}
method q(i: int, j: int) {}
method r() returns (s: int, t: int) { return 2,3; }
method m() {
  var ss: int, tt: int, c: C?, a: array<int>, d: D?;
  q(0,1);
  ss, c.f := r();
  c := new C;
  d := new D(2);
  a := new int[10];
  ss, tt := 212, 33;
  ss :| ss > 7;
  ss := *;
}
```

--------------------------------

### Dafny Module Import and Access Example

Source: https://github.com/dafny-lang/dafny/blob/master/docs/HowToFAQ/onepage.md

Demonstrates valid and invalid module import and member access scenarios in Dafny. Shows how to import sibling modules and access their members, while highlighting restrictions on accessing enclosing modules.

```dafny
module A {
  module B {
    const S1 := 10
  }
}

const S2 := 21
const S3 := C.D.A.B.S1 // OK

module C {
  module D {
    import A // OK - A is sibling of C
    import A.B // OK
    import E // OK - E is sibling of D
    import E.F // OK
    // import C // NOT OK - C is enclosing module
    // import EE = C.E // NOT OK -- can't access enclosing module
    // const X := S2 // NOT OK -- can't access top-level module
    const Y := B.S1 // OK - B is imported module
  }
  module E {
    module F {
    }
  }
}
```

--------------------------------

### Install Kramdown and Webrick for Jekyll

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/README.md

Apply this diff to the GemFile to ensure compatibility with Jekyll, especially for Windows or Ruby 3.0 users. Run 'bundle install' after applying the changes.

```diff
gem "kramdown", ">= 2.3.1"
+gem "webrick"
```

--------------------------------

### Build Dafny Project (CLI)

Source: https://github.com/dafny-lang/dafny/wiki/INSTALL

Builds the Dafny project using the .NET CLI. Ensure you are in the correct directory after cloning the repository.

```bash
dotnet build dafny\Source\Dafny.sln
```

--------------------------------

### Build DafnyRuntimePython Distribution Package

Source: https://github.com/dafny-lang/dafny/blob/master/Source/DafnyRuntime/DafnyRuntimePython/BUILDING.md

Sets up the virtual environment, cleans old build artifacts, and builds the distribution package for DafnyRuntimePython.

```bash
# Set up the build tooling
$ make setup-venv

# Remove old build artifacts
$ make clean-package

# Build the distribution package
$ make build-package
```

--------------------------------

### Sequence Access and Slicing Examples in Dafny

Source: https://github.com/dafny-lang/dafny/blob/master/docs/OnlineTutorial/ValueTypes.md

Provides examples of accessing the last element of a sequence, slicing the last element, and various ways to represent the whole sequence using slicing.

```dafny
var s := [1, 2, 3, 4, 5];
  assert s[|s|-1] == 5; //access the last element
  assert s[|s|-1..|s|] == [5]; //slice just the last element, as a singleton
  assert s[1..] == [2, 3, 4, 5]; // everything but the first
  assert s[..|s|-1] == [1, 2, 3, 4]; // everything but the last
  assert s == s[0..] == s[..|s|] == s[0..|s|]; // the whole sequence
```

--------------------------------

### Build and run Dafny program with Go target

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/integration-go/IntegrationGo.md

Combines the build and run steps for a Dafny program targeting Go in a single command.

```bash
dafny run --target:go A.dfy
```

--------------------------------

### Sequence Comprehension Error Example

Source: https://github.com/dafny-lang/dafny/blob/master/docs/HowToFAQ/ERROR_SeqComp.md

This example demonstrates the scenario where a sequence comprehension might lead to the 'function precondition could not be proved' error. It requires explicit handling of function preconditions.

```dafny
function F(i: nat) : nat
{
  i
}

method M() {
  var s := [F(i) for i := 0 .. 5];
}
```

```text
ERROR: function precondition could not be proved
ERROR: function precondition could not be proved
```

--------------------------------

### Build Dafny Reference Manual

Source: https://github.com/dafny-lang/dafny/wiki/INSTALL

Command to build the Dafny reference manual from the source distribution. This requires the LaTeX dependencies to be installed.

```bash
make refman
```

--------------------------------

### Dafny Server 'verify' Query Example

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/VSCodeIDE.md

This snippet shows an example of a 'verify' query sent to the Dafny Server. It includes the command, the base64 encoded JSON payload, and the end-of-message marker.

```dafny
verify
eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvcHJpbnRUb29sdGlwcyIsIi90aW1lTGltaXQ6MjAiXSwi
ZmlsZW5hbWUiOiJ0cmFuc2NyaXB0Iiwic291cmNlIjoibWV0aG9kIEEoYTppbnQpIHJldHVybnMg
KGI6IGludCkge1xuICBiIDo9IGE7XG4gIGFzc2VydCBmYWxzZTtcbn1cbiIsInNvdXJjZUlzRmls
ZSI6ZmFsc2V9
[[DAFNY-CLIENT: EOM]]
```

--------------------------------

### Manually Download and Unpack Z3 (Ubuntu)

Source: https://github.com/dafny-lang/dafny/wiki/INSTALL

Provides an alternative method to install Z3 version 4.12.1 on Ubuntu by manually downloading and extracting the binary zip file. Dafny expects the Z3 executable in `dafny/Binaries/z3/`.

```bash
cd dafny/Binaries
wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip
unzip z3-4.12.1-x64-ubuntu-20.04-bin.zip
mv z3-4.12.1 z3
```

--------------------------------

### Dafny Well-Founded Order Example

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/Topics.md

Demonstrates the use of well-founded orders with a recursive datatype in Dafny. This example verifies a loop that terminates based on the structural inclusion of a datatype value within a set.

```dafny
datatype D = D(s: set<D>)

method TestD(dd: D) {
  var d := dd;
  while d != D({})
    decreases d
  {
    var x :| x in d.s;
    d := x;
  }
}
```

--------------------------------

### Sequence Element Access and Slicing Examples (Dafny)

Source: https://github.com/dafny-lang/dafny/blob/master/docs/OnlineTutorial/Sequences.md

Provides examples of accessing the last element of a sequence, slicing a single element, and various ways to represent the entire sequence using slicing.

```dafny
method m()
{
  var s := [1, 2, 3, 4, 5];
  assert s[|s|-1] == 5; //access the last element
  assert s[|s|-1..|s|] == [5]; //slice just the last element, as a singleton
  assert s[1..] == [2, 3, 4, 5]; // everything but the first
  assert s[..|s|-1] == [1, 2, 3, 4]; // everything but the last
  assert s == s[0..] == s[..|s|] == s[0..|s|]; // the whole sequence
}
```

--------------------------------

### Run TestDafny Verb Help

Source: https://github.com/dafny-lang/dafny/blob/master/Source/TestDafny/README.md

Use this command to get help for a specific verb within the TestDafny CLI, such as 'for-each-compiler'.

```bash
dotnet run --project Source/TestDafny/TestDafny.csproj -- for-each-compiler --help
```

--------------------------------

### Module Import Example (Corrected)

Source: https://github.com/dafny-lang/dafny/blob/master/docs/HowToFAQ/FAQModuleImport.md

Shows the corrected way to import declarations into a nested module by adding an explicit 'open' statement within the submodule.

```dafny
{% include_relative FAQModuleImport1.dfy %}
```

--------------------------------

### Dafny Example: Extending Traits Across Modules

Source: https://github.com/dafny-lang/dafny/blob/master/docs/HowToFAQ/FAQTerminationFalse.md

This example demonstrates how to use `{:termination false}` on a trait to allow classes in other modules to extend it. Omitting this attribute would result in a compilation error.

```dafny
module foo1 {

  trait {:termination false} Foo {
    method bar()
  }

  class Baz{

    static method boz(foo: Foo){ foo.bar(); }

  }
}
module foo2 {

  import opened foo1

  class Boz extends Foo {

    method bar(){
      Baz.boz(this);
    }
  }
}
```

--------------------------------

### Dafny Set Refinement with Helper Function

Source: https://github.com/dafny-lang/dafny/blob/master/docs/HowToFAQ/FAQSetConstructor.md

This example shows an alternative way to construct finite sets by using a helper function that explicitly refines a known finite set. This approach allows Dafny to verify finiteness.

```dafny
module test {

  ghost const things: set<int>

  function RefineThings(condition: int -> bool): set<int>
  {
    set t: int | t in things && condition(t)
  }

  function ThisIsOk(): set<int> {
    set i: int | i in things && i > 0
  }

  function ThisIsOkAgain(): set<int> {
    RefineThings(i => i > 0)
  }
}
```

--------------------------------

### Dafny {:autoReq} Attribute Example

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/Attributes.md

The {:autoReq} attribute strengthens a function's requires clause to satisfy calls to other functions. This example shows how it automatically deduces a requires clause for function 'g'.

```dafny
function f(x:int) : bool
  requires x > 3
{
  x > 7
}

// Should succeed thanks to auto_reqs
function {:autoReq} g(y:int, b:bool) : bool
{
  if b then f(y + 2) else f(2*y)
}
```

```dafny
function f(x:int) : bool
  requires x > 3
{
  x > 7
}
function g(y:int, b:bool) : bool
  requires if b then y + 2 > 3 else 2 * y > 3
{
  if b then f(y + 2) else f(2*y)
}
```

--------------------------------

### Dafny Error Example: Empty Map Initialization

Source: https://github.com/dafny-lang/dafny/blob/master/docs/HowToFAQ/ERROR_NoLHS.md

This example demonstrates the error when initializing a map with a 'such-that' predicate on an empty map. Dafny requires proof that a value satisfying the predicate exists.

```dafny
method Test(m: map[int,int])
{
  var x :| x in m;
  assert false;
}
```

--------------------------------

### Dafny Project File Configuration

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/UserGuide.md

Example of a Dafny project file (`dfyconfig.toml`) specifying included and excluded files, base configurations, and project-specific options.

```toml
includes = ["src/**/*.dfy"]
excludes = ["**/ignore.dfy"]

base = ["../commonOptions.dfyconfig.toml"]

[options]
enforce-determinism = true
warn-shadowing = true
```

--------------------------------

### Dafny Parameter Binding Syntax

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/Expressions.md

Illustrates basic parameter binding syntax, including simple positional arguments and named arguments with optimization.

```dafny
a
a, b
a, optimize := b
```

--------------------------------

### Dafny Class Instantiation with Initialization Method

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/Types.md

Shows the shorthand for allocating a new instance and invoking an initialization method.

```dafny
c := new C;
c.Init(args);
```

--------------------------------

### Dafny Class and Method Example

Source: https://github.com/dafny-lang/dafny/blob/master/docs/dev/TypeSystemRefresh.md

Demonstrates a Dafny class 'Cell' with a constructor and a method 'Tricky' that involves nullable types and loops. This example illustrates the mutual dependency between name resolution and type inference.

```dafny
class Cell {
  var data: bv32
  constructor (data: bv32) {
    this.data := data;
  }
}

method Tricky() {
  var c := null; // Cell?
  var s := 0; // bv32
  for i := 0 to 100 {
    if c == null {
      c := new Cell(s + 10);
    }
    s := s + c.data;
  }
}
```

--------------------------------

### Basic As and Is Expressions in Dafny

Source: https://github.com/dafny-lang/dafny/blob/master/docs/DafnyRef/Expressions.md

Demonstrates the basic syntax for type conversion ('as') and type testing ('is') in Dafny.

```dafny
e as MyClass
i as bv8
e is MyClass
```