diff --git a/Snapshots.md b/Snapshots.md index 857655b..1da0943 100644 --- a/Snapshots.md +++ b/Snapshots.md @@ -7,6 +7,8 @@ layout: default - [Current development version](https://dafny.org/dafny) - [Latest release snapshot](https://dafny.org/latest) +- [v4.10.0](https://dafny.org/v4.10.0) +- [v4.9.1](https://dafny.org/v4.9.1) - [v4.8.1](https://dafny.org/v4.8.1) - [v4.6.0](https://dafny.org/v4.6.0) - [v4.5.0](https://dafny.org/v4.5.0) diff --git a/latest/DafnyRef/Attributes.3.expect b/latest/DafnyRef/Attributes.3.expect index 754570c..eca60fd 100644 --- a/latest/DafnyRef/Attributes.3.expect +++ b/latest/DafnyRef/Attributes.3.expect @@ -1,3 +1,3 @@ -text.dfy(25,14): Error: assertion might not hold +text.dfy(25,6): Error: assertion might not hold Dafny program verifier finished with 0 verified, 1 error diff --git a/latest/DafnyRef/Expressions.5.expect b/latest/DafnyRef/Expressions.5.expect index c9c3ba5..ecbb16a 100644 --- a/latest/DafnyRef/Expressions.5.expect +++ b/latest/DafnyRef/Expressions.5.expect @@ -1,3 +1,3 @@ -text.dfy(2,11): Error: assertion might not hold +text.dfy(2,2): Error: assertion might not hold Dafny program verifier finished with 0 verified, 1 error \ No newline at end of file diff --git a/latest/DafnyRef/Modules.2.expect b/latest/DafnyRef/Modules.2.expect index a992046..a754390 100644 --- a/latest/DafnyRef/Modules.2.expect +++ b/latest/DafnyRef/Modules.2.expect @@ -1,4 +1,4 @@ text.dfy(9,6): Error: value does not satisfy the subset constraints of 'nat' -text.dfy(12,21): Error: assertion might not hold +text.dfy(12,4): Error: assertion might not hold Dafny program verifier finished with 1 verified, 2 errors diff --git a/latest/DafnyRef/Modules.4.expect b/latest/DafnyRef/Modules.4.expect index 6d76343..920194d 100644 --- a/latest/DafnyRef/Modules.4.expect +++ b/latest/DafnyRef/Modules.4.expect @@ -1,3 +1,3 @@ -text.dfy(10,15): Error: assertion might not hold +text.dfy(10,4): Error: assertion might not hold Dafny program verifier finished with 0 verified, 1 error diff --git a/latest/DafnyRef/Plugins.md b/latest/DafnyRef/Plugins.md index 6cb7c29..c044914 100644 --- a/latest/DafnyRef/Plugins.md +++ b/latest/DafnyRef/Plugins.md @@ -230,6 +230,6 @@ That's it! Now, build your library while inside your folder: > dotnet build ``` -This will create the file `PluginTutorial/bin/Debug/net6.0/PluginTutorial.dll`. +This will create the file `PluginTutorial/bin/Debug/net8.0/PluginTutorial.dll`. Now, open VSCode, open Dafny settings, and enter the absolute path to this DLL in the plugins section. Restart VSCode, and it should work! diff --git a/latest/DafnyRef/Statements.10.expect b/latest/DafnyRef/Statements.10.expect index c718935..c19750c 100644 --- a/latest/DafnyRef/Statements.10.expect +++ b/latest/DafnyRef/Statements.10.expect @@ -1,3 +1,3 @@ -text.dfy(8,13): Error: assertion might not hold +text.dfy(8,4): Error: assertion might not hold Dafny program verifier finished with 0 verified, 1 error diff --git a/latest/DafnyRef/Statements.16.expect b/latest/DafnyRef/Statements.16.expect index 6bbd3b3..971d1af 100644 --- a/latest/DafnyRef/Statements.16.expect +++ b/latest/DafnyRef/Statements.16.expect @@ -1,3 +1,3 @@ -text.dfy(17,10): Error: assertion might not hold +text.dfy(17,2): Error: assertion might not hold Dafny program verifier finished with 2 verified, 1 error diff --git a/latest/DafnyRef/Statements.3.expect b/latest/DafnyRef/Statements.3.expect index f267a4c..ce5fed0 100644 --- a/latest/DafnyRef/Statements.3.expect +++ b/latest/DafnyRef/Statements.3.expect @@ -1,5 +1,5 @@ text.dfy(12,2): Warning: this loop has no body (loop frame: i, a, $Heap) -text.dfy(16,11): Error: assertion might not hold -text.dfy(18,16): Error: assertion might not hold +text.dfy(16,2): Error: assertion might not hold +text.dfy(18,2): Error: assertion might not hold Dafny program verifier finished with 1 verified, 2 errors diff --git a/latest/DafnyRef/Statements.5.expect b/latest/DafnyRef/Statements.5.expect index 84d23b8..ed0077a 100644 --- a/latest/DafnyRef/Statements.5.expect +++ b/latest/DafnyRef/Statements.5.expect @@ -1,4 +1,4 @@ -text.dfy(2,14): Error: assertion might not hold -text.dfy(3,11): Error: assertion might not hold +text.dfy(2,2): Error: assertion might not hold +text.dfy(3,2): Error: assertion might not hold Dafny program verifier finished with 0 verified, 2 errors diff --git a/latest/DafnyRef/Statements.6.expect b/latest/DafnyRef/Statements.6.expect index 0dcc07a..5d7469e 100644 --- a/latest/DafnyRef/Statements.6.expect +++ b/latest/DafnyRef/Statements.6.expect @@ -1,3 +1,3 @@ -text.dfy(2,14): Error: assertion might not hold +text.dfy(2,2): Error: assertion might not hold Dafny program verifier finished with 0 verified, 1 error diff --git a/latest/DafnyRef/Statements.7.expect b/latest/DafnyRef/Statements.7.expect index 0dcc07a..5d7469e 100644 --- a/latest/DafnyRef/Statements.7.expect +++ b/latest/DafnyRef/Statements.7.expect @@ -1,3 +1,3 @@ -text.dfy(2,14): Error: assertion might not hold +text.dfy(2,2): Error: assertion might not hold Dafny program verifier finished with 0 verified, 1 error diff --git a/latest/DafnyRef/Statements.8b.expect b/latest/DafnyRef/Statements.8b.expect index 7e599df..0732822 100644 --- a/latest/DafnyRef/Statements.8b.expect +++ b/latest/DafnyRef/Statements.8b.expect @@ -1,4 +1,4 @@ -text.dfy(6,12): Error: function precondition could not be proved +text.dfy(6,13): Error: function precondition could not be proved text.dfy(3,30): Related location: this proposition could not be proved Dafny program verifier finished with 8 verified, 1 error diff --git a/latest/DafnyRef/Statements.opaqueBlock.expect b/latest/DafnyRef/Statements.opaqueBlock.expect index dd8065e..04352d3 100644 --- a/latest/DafnyRef/Statements.opaqueBlock.expect +++ b/latest/DafnyRef/Statements.opaqueBlock.expect @@ -1,3 +1,3 @@ -text.dfy(12,11): Error: assertion might not hold +text.dfy(12,2): Error: assertion might not hold Dafny program verifier finished with 0 verified, 1 error diff --git a/latest/DafnyRef/Topics.3.expect b/latest/DafnyRef/Topics.3.expect index a5f9b7e..66c482d 100644 --- a/latest/DafnyRef/Topics.3.expect +++ b/latest/DafnyRef/Topics.3.expect @@ -1,3 +1,3 @@ text.dfy(6,10): Error: the type of this variable is underspecified -text.dfy(6,15): Error: type parameter 'T' (inferred to be '?') in the function call to 'EmptySet' could not be determined +text.dfy(6,23): Error: type parameter 'T' (inferred to be '?') in the function call to 'EmptySet' could not be determined 2 resolution/type errors detected in text.dfy diff --git a/latest/DafnyRef/Types.19.expect b/latest/DafnyRef/Types.19.expect index 1c238c3..e513b84 100644 --- a/latest/DafnyRef/Types.19.expect +++ b/latest/DafnyRef/Types.19.expect @@ -1,3 +1,3 @@ -text.dfy(9,11): Error: assertion might not hold +text.dfy(9,2): Error: assertion might not hold Dafny program verifier finished with 0 verified, 1 error diff --git a/latest/DafnyRef/Types.20.expect b/latest/DafnyRef/Types.20.expect index b80b729..df1d037 100644 --- a/latest/DafnyRef/Types.20.expect +++ b/latest/DafnyRef/Types.20.expect @@ -1,5 +1,5 @@ text.dfy(26,0): Error: a postcondition could not be proved on this return path -text.dfy(25,10): Related location: this is the postcondition that could not be proved +text.dfy(25,15): Related location: this is the postcondition that could not be proved text.dfy(10,9): Related location: this proposition could not be proved Dafny program verifier finished with 1 verified, 1 error diff --git a/latest/DafnyRef/Types.21.expect b/latest/DafnyRef/Types.21.expect index 6a1e2ac..22303ff 100644 --- a/latest/DafnyRef/Types.21.expect +++ b/latest/DafnyRef/Types.21.expect @@ -1,4 +1,4 @@ text.dfy(8,4): Error: field 'x', which is subject to definite-assignment rules, might be uninitialized at this point in the constructor body -text.dfy(10,13): Error: assertion might not hold +text.dfy(10,4): Error: assertion might not hold Dafny program verifier finished with 0 verified, 2 errors diff --git a/latest/DafnyRef/Types.25.expect b/latest/DafnyRef/Types.25.expect index 5175bdf..9091193 100644 --- a/latest/DafnyRef/Types.25.expect +++ b/latest/DafnyRef/Types.25.expect @@ -1,3 +1,3 @@ -text.dfy(3,13): Error: assertion might not hold +text.dfy(3,4): Error: assertion might not hold Dafny program verifier finished with 0 verified, 1 error diff --git a/latest/DafnyRef/Types.7a.expect b/latest/DafnyRef/Types.7a.expect index df622f2..126cd8b 100644 --- a/latest/DafnyRef/Types.7a.expect +++ b/latest/DafnyRef/Types.7a.expect @@ -1,3 +1,3 @@ -text.dfy(5,11): Error: assertion might not hold +text.dfy(5,2): Error: assertion might not hold Dafny program verifier finished with 0 verified, 1 error diff --git a/latest/DafnyRef/UserGuide.3.expect b/latest/DafnyRef/UserGuide.3.expect index 28143d5..649ca8f 100644 --- a/latest/DafnyRef/UserGuide.3.expect +++ b/latest/DafnyRef/UserGuide.3.expect @@ -1,3 +1,3 @@ -text.dfy(7,13): Error: assertion might not hold +text.dfy(7,4): Error: assertion might not hold Dafny program verifier finished with 0 verified, 1 error diff --git a/latest/DafnyRef/UserGuide.4.expect b/latest/DafnyRef/UserGuide.4.expect index 28143d5..649ca8f 100644 --- a/latest/DafnyRef/UserGuide.4.expect +++ b/latest/DafnyRef/UserGuide.4.expect @@ -1,3 +1,3 @@ -text.dfy(7,13): Error: assertion might not hold +text.dfy(7,4): Error: assertion might not hold Dafny program verifier finished with 0 verified, 1 error diff --git a/latest/DafnyRef/UserGuide.5.expect b/latest/DafnyRef/UserGuide.5.expect index 1ffdb33..4b136e3 100644 --- a/latest/DafnyRef/UserGuide.5.expect +++ b/latest/DafnyRef/UserGuide.5.expect @@ -1,3 +1,3 @@ -text.dfy(6,13): Error: assertion might not hold +text.dfy(6,4): Error: assertion might not hold Dafny program verifier finished with 0 verified, 1 error diff --git a/latest/DafnyRef/UserGuide.md b/latest/DafnyRef/UserGuide.md index 156cb2b..8fd4ce1 100644 --- a/latest/DafnyRef/UserGuide.md +++ b/latest/DafnyRef/UserGuide.md @@ -2732,7 +2732,7 @@ If you have Boogie installed locally, you can run the printed Boogie file with t DOTNET=$(which dotnet) BOOGIE_ROOT="path/to/boogie/Source" -BOOGIE="$BOOGIE_ROOT/BoogieDriver/bin/Debug/net6.0/BoogieDriver.dll" +BOOGIE="$BOOGIE_ROOT/BoogieDriver/bin/Debug/net8.0/BoogieDriver.dll" if [[ ! -x "$DOTNET" ]]; then echo "Error: Dafny requires .NET Core to run on non-Windows systems." @@ -2769,7 +2769,7 @@ The following options are also commonly used: but a large positive number reports more errors per run * `--verification-time-limit:` (was `-timeLimit:`) - limits - the number of seconds spent trying to verify each procedure. + the number of seconds spent trying to verify each assertion batch. ### 13.9.11. Controlling test generation {#sec-controlling-test-gen} diff --git a/latest/DafnyRef/integration-java/IntegrationJava.md b/latest/DafnyRef/integration-java/IntegrationJava.md index cbbaffc..fe1321d 100644 --- a/latest/DafnyRef/integration-java/IntegrationJava.md +++ b/latest/DafnyRef/integration-java/IntegrationJava.md @@ -218,3 +218,6 @@ Often this requires defining a Dafny class that corresponds to the Java class. the Dafny-generated (Java) types and the types used in the desired method. The wrapper will do appropriate conversions and call the desired method. +## Performance notes + +If you have the choice, given a `m: map`, prefer iterating over the map itself like `forall k <- m` rather than over the keys `forall k <- m.Keys`. The latter currently results in `O(N²)` steps, whereas the first one remains linear. diff --git a/latest/HowToFAQ/Errors-Resolver2.md b/latest/HowToFAQ/Errors-Resolver2.md index 8fd0c83..ae80406 100644 --- a/latest/HowToFAQ/Errors-Resolver2.md +++ b/latest/HowToFAQ/Errors-Resolver2.md @@ -168,7 +168,7 @@ and optimizing tail-recursion opportunities in mutually recursive functions. ```dafny function {:tailrecursion} f(n: nat): nat { - if n == 0 then n else var ff := f; ff(n-1) + if n == 0 then n else var r := f(n-1); r } ``` diff --git a/latest/Installation.md b/latest/Installation.md index edecd0f..991e4b0 100644 --- a/latest/Installation.md +++ b/latest/Installation.md @@ -15,7 +15,7 @@ are in the [Dafny project wiki](https://github.com/dafny-lang/dafny/wiki/INSTALL System Requirements =================== -The `dafny tool` is a .NET 6.0 artifact, but it compiles to native executables on supported platforms. +The `dafny tool` is a .NET 8.0 artifact, but it compiles to native executables on supported platforms. That and the Z3 tool are all that is needed to use dafny for verification; additional tools are need for compilation, as described below. @@ -41,7 +41,7 @@ In addition, the Dafny toolkit supplies runtime libraries, either in source form ### C# - Dafny targeting C# produces C#10-compatible source code. -- Only the .NET 6.0 set of tools (which includes the C# compiler) is needed to compile and run the generated C# code. +- Only the .NET 8.0 set of tools (which includes the C# compiler) is needed to compile and run the generated C# code. - The Dafny runtime library is included as C# source along with the generated C# code, so the user can compile those sources and any user code in one project. @@ -86,9 +86,9 @@ For most users, we recommend using Dafny with VS Code, which has an easy install ## Visual Studio Code {#Visual-Studio-Code} 0. Install [Visual Studio Code](https://code.visualstudio.com/) -1. If you are on a Mac or Linux, install .NET 6.0, as described under those platforms below. +1. If you are on a Mac or Linux, install .NET 8.0, as described under those platforms below. 2. In Visual Studio Code, press `Ctrl+P` (or `⌘P` on a Mac), and enter `ext install dafny-lang.ide-vscode`. -3. If you open a `.dfy` file, Dafny VSCode will offer to download and install the latest Dafny. You can also browse extensions: +3. If you open a `.dfy` file, Dafny VSCode will offer to download and install the latest Dafny. You can also browse extensions: ![vs-code-dafny-2 0 1-install](https://user-images.githubusercontent.com/3601079/141353551-5cb5e23b-5536-47be-ba17-e5af494b775c.gif) ## Emacs {#Emacs} @@ -118,7 +118,7 @@ install the correct dependencies for the desired language. To install Dafny on your own machine, -* Install (if not already present) .NET Core 6.0: `https://dotnet.microsoft.com/download/dotnet/6.0` +* Install (if not already present) .NET Core 8.0: `https://dotnet.microsoft.com/download/dotnet/8.0` * Download the windows zip file from the [releases page](https://github.com/dafny-lang/dafny/releases/latest) and **save** it to your disk. * Then, **before you open or unzip it**, right-click on it and select Properties; at the bottom of the dialog, click the **Unblock** button and then the OK button. * Now, open the zip file and copy its contents into a directory on your machine. (You can now delete the zip file.) @@ -130,7 +130,7 @@ Then: ## Linux (Binary) {#linux-binary} To install a binary installation of dafny on Linux (e.g., Ubuntu), do the following: -* Install .NET 6.0. See: `https://docs.microsoft.com/dotnet/core/install/linux` or `sudo apt install dotnet-sdk-6.0` +* Install .NET 8.0. See: `https://docs.microsoft.com/dotnet/core/install/linux` or `sudo apt install dotnet-sdk-8.0` * Install the Linux binary version of Dafny, from `https://github.com/dafny-lang/dafny/releases/latest` * Unzip the downloaded file in a (empty) location of your choice @@ -165,7 +165,7 @@ After the compiler dependencies are installed, you can run a quick test of the i The .NET [NuGet](https://www.nuget.org/) repository collects .NET libraries and tools for easy installation. Dafny is available on NuGet, and can be installed as follows: -* Install .NET 6.0 as described for your platform in one of the subsections above. +* Install .NET 8.0 as described for your platform in one of the subsections above. * Install a binary version of Z3 4.12.1 for your platform from its [GitHub releases page](https://github.com/Z3Prover/z3/releases/tag/Z3-4.12.1) and put the `z3` executable in your `PATH`. * Install Dafny using `dotnet tool install --global dafny` (or leave out the `--global` to use with `dotnet tool run` from the source directory of a .NET project). @@ -181,10 +181,10 @@ Additional instructions are found in the [Dafny User Guide](DafnyRef/DafnyRef#se ### C# (.Net) -Install .NET 6.0: -* Windows) `https://dotnet.microsoft.com/download/dotnet/6.0` -* Linux) Install .NET 6.0. See: `https://docs.microsoft.com/dotnet/core/install/linux` or `sudo apt install dotnet-sdk-6.0` -* Mac) Install .NET 6.0: `brew install dotnet-sdk` or from `https://docs.microsoft.com/dotnet/core/install/macos` +Install .NET 8.0: +* Windows) `https://dotnet.microsoft.com/download/dotnet/8.0` +* Linux) Install .NET 8.0. See: `https://docs.microsoft.com/dotnet/core/install/linux` or `sudo apt install dotnet-sdk-8.0` +* Mac) Install .NET 8.0: `brew install dotnet-sdk` or from `https://docs.microsoft.com/dotnet/core/install/macos` To separately compile and run your program for .NET: diff --git a/latest/OnlineTutorial/Modules.1.expect b/latest/OnlineTutorial/Modules.1.expect index ac319c2..7eaa7bd 100644 --- a/latest/OnlineTutorial/Modules.1.expect +++ b/latest/OnlineTutorial/Modules.1.expect @@ -1,4 +1,4 @@ -text.dfy(27,23): Error: assertion might not hold -text.dfy(37,23): Error: assertion might not hold +text.dfy(27,4): Error: assertion might not hold +text.dfy(37,4): Error: assertion might not hold Dafny program verifier finished with 5 verified, 2 errors diff --git a/latest/OnlineTutorial/Modules.5.expect b/latest/OnlineTutorial/Modules.5.expect index d09a073..18a41e0 100644 --- a/latest/OnlineTutorial/Modules.5.expect +++ b/latest/OnlineTutorial/Modules.5.expect @@ -1,3 +1,3 @@ -text.dfy(13,21): Error: assertion might not hold +text.dfy(13,4): Error: assertion might not hold Dafny program verifier finished with 2 verified, 1 error diff --git a/latest/OnlineTutorial/Sets.1.expect b/latest/OnlineTutorial/Sets.1.expect index 26247f3..1f7b778 100644 --- a/latest/OnlineTutorial/Sets.1.expect +++ b/latest/OnlineTutorial/Sets.1.expect @@ -1,3 +1,3 @@ -text.dfy(4,41): Error: assertion might not hold +text.dfy(4,2): Error: assertion might not hold Dafny program verifier finished with 0 verified, 1 error diff --git a/latest/OnlineTutorial/guide.10.expect b/latest/OnlineTutorial/guide.10.expect index e714f86..6a7d67a 100644 --- a/latest/OnlineTutorial/guide.10.expect +++ b/latest/OnlineTutorial/guide.10.expect @@ -1,14 +1,14 @@ text.dfy(7,0): Error: a postcondition could not be proved on this return path +text.dfy(4,12): Related location: this is the postcondition that could not be proved +text.dfy(7,0): Error: a postcondition could not be proved on this return path text.dfy(5,23): Related location: this is the postcondition that could not be proved text.dfy(7,0): Error: a postcondition could not be proved on this return path text.dfy(6,22): Related location: this is the postcondition that could not be proved -text.dfy(7,0): Error: a postcondition could not be proved on this return path -text.dfy(4,12): Related location: this is the postcondition that could not be proved +text.dfy(16,0): Error: a postcondition could not be proved on this return path +text.dfy(13,12): Related location: this is the postcondition that could not be proved text.dfy(16,0): Error: a postcondition could not be proved on this return path text.dfy(14,23): Related location: this is the postcondition that could not be proved text.dfy(16,0): Error: a postcondition could not be proved on this return path text.dfy(15,22): Related location: this is the postcondition that could not be proved -text.dfy(16,0): Error: a postcondition could not be proved on this return path -text.dfy(13,12): Related location: this is the postcondition that could not be proved Dafny program verifier finished with 0 verified, 6 errors diff --git a/latest/OnlineTutorial/guide.12.expect b/latest/OnlineTutorial/guide.12.expect index 1c238c3..e513b84 100644 --- a/latest/OnlineTutorial/guide.12.expect +++ b/latest/OnlineTutorial/guide.12.expect @@ -1,3 +1,3 @@ -text.dfy(9,11): Error: assertion might not hold +text.dfy(9,2): Error: assertion might not hold Dafny program verifier finished with 0 verified, 1 error diff --git a/latest/OnlineTutorial/guide.7.expect b/latest/OnlineTutorial/guide.7.expect index d3fa2cb..a2e5589 100644 --- a/latest/OnlineTutorial/guide.7.expect +++ b/latest/OnlineTutorial/guide.7.expect @@ -1,3 +1,3 @@ -text.dfy(14,11): Error: assertion might not hold +text.dfy(14,2): Error: assertion might not hold Dafny program verifier finished with 1 verified, 1 error diff --git a/latest/OnlineTutorial/guide.8.expect b/latest/OnlineTutorial/guide.8.expect index 0fb9e44..791d7d9 100644 --- a/latest/OnlineTutorial/guide.8.expect +++ b/latest/OnlineTutorial/guide.8.expect @@ -1,3 +1,3 @@ -text.dfy(11,11): Error: assertion might not hold +text.dfy(11,2): Error: assertion might not hold Dafny program verifier finished with 1 verified, 1 error diff --git a/latest/OnlineTutorial/guide.9.expect b/latest/OnlineTutorial/guide.9.expect index 02e9574..29cca6b 100644 --- a/latest/OnlineTutorial/guide.9.expect +++ b/latest/OnlineTutorial/guide.9.expect @@ -1,3 +1,3 @@ -text.dfy(10,11): Error: assertion might not hold +text.dfy(10,2): Error: assertion might not hold Dafny program verifier finished with 1 verified, 1 error diff --git a/latest/Snapshots.md b/latest/Snapshots.md index 857655b..1da0943 100644 --- a/latest/Snapshots.md +++ b/latest/Snapshots.md @@ -7,6 +7,8 @@ layout: default - [Current development version](https://dafny.org/dafny) - [Latest release snapshot](https://dafny.org/latest) +- [v4.10.0](https://dafny.org/v4.10.0) +- [v4.9.1](https://dafny.org/v4.9.1) - [v4.8.1](https://dafny.org/v4.8.1) - [v4.6.0](https://dafny.org/v4.6.0) - [v4.5.0](https://dafny.org/v4.5.0) diff --git a/latest/VerificationOptimization/VerificationOptimization.md b/latest/VerificationOptimization/VerificationOptimization.md index aa83919..c38198e 100644 --- a/latest/VerificationOptimization/VerificationOptimization.md +++ b/latest/VerificationOptimization/VerificationOptimization.md @@ -608,6 +608,27 @@ As a general rule, designing a program from the start so that it can be broken i * Break methods up into smaller pieces, as well. Because methods are always opaque, this will, in many cases, require adding a contract to each broken-out method. To make this more tractable, consider abstracting the concepts used in those contracts into separate functions, some of which may be opaque. +# Verification fine-tuning + +## Conjunction vs. Nested ifs + +We have witnessed cases where the following code: +```dafny + if (a && b) { + assert true; + } +``` +verifies slower than +```dafny + if (a) { + if (b) { + assert true; + } + } +``` +This is because the well-formedness of `&& b` adds an extra proof obligation, which is empty in this case but not trimmed, so there is an extra `if (a) {}` in the encoding. +Therefore, for verification performance, the nested ifs _could_ verify faster, and we have witnessed one case where it does. In other cases, this difference in translation might trigger butterfly effects and uncover brittleness. + # Summary When you're dealing with a program that exhibits high verification variability, or simply slow or unsuccessful verification, careful encapsulation and information hiding combined with hints to add information in the context of difficult constructs is frequently the best solution. Breaking one large definition with extensive contracts down into several, smaller definitions, each with simpler contracts, can be very valuable. Within each smaller definition, a few internal, locally-encapsulated hints can help the prover make effective progress on goals it might be unable to prove in conjunction with other code. diff --git a/latest/index.html b/latest/index.html index 7f704bf..e42a74e 100644 --- a/latest/index.html +++ b/latest/index.html @@ -31,6 +31,7 @@

Quick Links