snapshot v4 8 1 (#44)

- **Removing old latest**
- **Documentation snapshot for v4.8.1**

Snapshots.md

@@ -7,6 +7,7 @@ layout: default
 
 - [Current development version](https://dafny.org/dafny)
 - [Latest release snapshot](https://dafny.org/latest)
+- [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)
 - [v4.4.0](https://dafny.org/v4.4.0)

latest/DafnyRef/Attributes.md

@@ -270,7 +270,7 @@ using integration with the target language environment.
 Currently, the only way to satisfy this requirement is to ensure that the specification
 of the function or method includes the equivalent of `reads {}` and `modifies {}`.
 This ensures that the code does not read or write any shared mutable state,
-although it is free to write and write newly allocated objects.
+although it is free to read and write newly allocated objects.
 
 ### 11.2.7. `{:extern <name>}` {#sec-extern-method}
 See [`{:extern <name>}`](#sec-extern).

latest/DafnyRef/Expressions.5.expect

@@ -0,0 +1,3 @@
+text.dfy(2,9): Error: assertion might not hold
+
+Dafny program verifier finished with 0 verified, 1 error

latest/DafnyRef/Expressions.md

@@ -632,6 +632,7 @@ old(x)
 allocated(x)
 unchanged(x)
 fresh(e)
+assigned(x)
 ```
 
 These expressions are never l-values. They include
@@ -644,6 +645,7 @@ These expressions are never l-values. They include
 - [unchanged expressions](#sec-unchanged-expression)
 - [old expressions](#sec-old-expression)
 - [cardinality expressions](#sec-cardinality-expression)
+- [assigned expressions](#sec-assigned-expression)
 
 ## 9.20. Literal Expressions ([grammar](#g-literal-expression)} {#sec-literal-expression}
 
@@ -1851,7 +1853,53 @@ value for each optional parameter, and must never name
 non-existent formals. Any optional parameter that is not given a value
 takes on the default value declared in the callee for that optional parameter.
 
-## 9.37. Compile-Time Constants {#sec-compile-time-constants}
+## 9.37. Assigned Expressions {#sec-assigned-expression}
+
+Examples:
+<!-- %no-check -->
+```dafny
+assigned(x)
+```
+
+For any variable, constant, out-parameter, or object field `x`,
+the expression `assigned(x)` evaluates to `true` in a state
+if `x` is definitely assigned in that state.
+
+See [Section 12.6](#sec-definite-assignment) for more details on definite assignment.
+
+## 9.38. Termination Ordering Expressions {#sec-termination-ordering-expressions}
+
+When proving that a loop or recursive callable terminates, Dafny
+automatically generates a proof obligation that the sequence of
+expressions listed in a `decreases` clause gets smaller (in the
+[lexicographic termination ordering](#sec-decreases-clause)) with each
+iteration or recursive call. Normally, this proof obligation is purely
+internal. However, it can be written as a Dafny expression using the
+`decreases to` operator.
+
+The Boolean expression `(a, ..., b decreases to a', ..., b')` encodes
+this ordering. For example, the following assertions are valid:
+<!-- %check-verify -->
+```dafny
+method M(x: int, y: int) {
+  assert (1 decreases to 0);
+  assert (true, false decreases to false, true);
+  assert (x, y decreases to x - 1, y);
+}
+```
+
+Conversely, the following assertion is invalid:
+<!-- %check-verify Expressions.5.expect -->
+```dafny
+method M(x: int, y: int) {
+  assert (x decreases to x + 1);
+}
+```
+
+Currently, `decreases to` expressions must be written in parentheses to
+avoid parsing ambiguities.
+
+## 9.39. Compile-Time Constants {#sec-compile-time-constants}
 
 In certain situations in Dafny it is helpful to know what the value of a
 constant is during program analysis, before verification or execution takes
@@ -1892,13 +1940,15 @@ In Dafny, the following expressions are compile-time constants[^CTC], recursivel
 
 [^CTC]: This set of operations that are constant-folded may be enlarged in future versions of `dafny`.
 
-## 9.38. List of specification expressions {#sec-list-of-specification-expressions}
+## 9.40. List of specification expressions {#sec-list-of-specification-expressions}
 
 The following is a list of expressions that can only appear in specification contexts or in ghost blocks.
 
 * [Fresh expressions](#sec-fresh-expression)
 * [Allocated expressions](#sec-allocated-expression)
 * [Unchanged expressions](#sec-unchanged-expression)
 * [Old expressions](#sec-old-expression)
+- [Assigned expressions](#sec-assigned-expression)
 * [Assert and calc expressions](#sec-statement-in-an-expression)
 * [Hash Calls](#sec-hash-call)
+* [Termination ordering expression](#sec-termination-ordering-expressions)

latest/DafnyRef/Modules.md

@@ -352,9 +352,8 @@ Examples:
 ```dafny
 export E extends F reveals f,g provides g,h
 export E reveals *
-export reveals f
+export reveals f,g provides g,h
 export E
-export
 export E ... reveals f
 ```
 
@@ -375,15 +374,16 @@ module using the `import` mechanism.
 An _export set_ enables a module to disallow the
 use of some declarations outside the module.
 
-Export sets have names; those names are used in `import` statements to
-designate which export set of a module is being imported.
-If a module `M` has export sets
-`E1` and `E2`, we can write ``import A = M`E1`` to create a module alias
-`A` that contains only the
-names in `E1`. Or we can write ``import A = M`{E1,E2}`` to import the union
+An export set has an optional name used to disambiguate
+in case of multiple export sets;
+If specified, such names are used in `import` statements
+to designate which export set of a module is being imported.
+If a module `M` has export sets `E1` and `E2`,
+we can write ``import A = M`E1`` to create a module alias
+`A` that contains only the names in `E1`.
+Or we can write ``import A = M`{E1,E2}`` to import the union
 of names in `E1` and `E2` as module alias `A`.
-As before, ``import M`E1`` is an
-abbreviation of ``import M = M`E1``.
+As before, ``import M`E1`` is an abbreviation of ``import M = M`E1``.
 
 If no export set is given in an import
 statement, the default export set of the module is used.

latest/DafnyRef/Options.txt

@@ -1,5 +1,5 @@
 ```
-Use 'dafny --help' to see help for a newer Dafny CLI format.
+Use 'dafny --help' to see help for the new Dafny CLI format.
 Usage: dafny [ option ... ] [ filename ... ]
 
   ---- General options -------------------------------------------------------
@@ -87,10 +87,6 @@ Usage: dafny [ option ... ] [ filename ... ]
       See https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/README.md for more information.
       Not compatible with the /unicodeChar:0 option.
 
-  /unicodeChar:<value>
-      0 - The char type represents any UTF-16 code unit.
-      1 (default) - The char type represents any Unicode scalar value.
-
   /noIncludes
       Ignore include directives.
 
@@ -184,6 +180,11 @@ Usage: dafny [ option ... ] [ filename ... ]
   /verifyAllModules
       Verify modules that come from an include directive.
 
+  /emitUncompilableCode
+      Allow compilers to emit uncompilable code that usually contain useful
+      information about what feature is missing, rather than
+      stopping on the first problem
+
   /separateModuleOutput
       Output verification results for each module separately, rather than
       aggregating them after they are all finished.
@@ -447,6 +448,10 @@ Usage: dafny [ option ... ] [ filename ... ]
 
   /loopUnroll:<n>
                 unroll loops, following up to n back edges (and then some)
+                default is -1, which means loops are not unrolled
+  /extractLoops
+                extract reducible loops into recursive procedures and
+                inline irreducible loops using the bound supplied by /loopUnroll:<n>
   /soundLoopUnrolling
                 sound loop unrolling
   /doModSetAnalysis

latest/DafnyRef/Plugins.md

@@ -6,18 +6,19 @@ without concern for verifying or compiling the program. Or it might modify the p
 and then continue on with verification and compilation with the core Dafny tool. A user plugin might also be used
 in the Language Server and thereby be available in the VSCode (or other) IDE.
 
-_ **This is an experimental aspect of Dafny.**
+_**This is an experimental aspect of Dafny.**
 The plugin API directly exposes the Dafny AST, which is constantly evolving.
 Hence, always recompile your plugin against the binary of Dafny that will be importing your plugin._
 
-Plugins are libraries linked to a `Dafny.dll` of the same version as the language server.
+Plugins are libraries linked to a `Dafny.dll` of the same version as the Language Server.
 A plugin typically defines:
 
 * Zero or one class extending `Microsoft.Dafny.Plugins.PluginConfiguration`, which receives plugins arguments in its method `ParseArguments`, and
-  1) Can return a list of `Microsoft.Dafny.Plugins.Rewriter`s when its method `GetRewriters()` is called by Dafny,
-  2) Can return a list of `Microsoft.Dafny.Plugins.Compiler`s when its method `GetCompilers()` is called by Dafny,
-  3) If the configuration extends the subclass `Microsoft.Dafny.LanguageServer.Plugins.PluginConfiguration`,
-     then it can return a list of `Microsoft.Dafny.LanguageServer.Plugins.DafnyCodeActionProvider`s when its method `GetDafnyCodeActionProviders()` is called by the Dafny Language Server.
+  1. Can return a list of `Microsoft.Dafny.Plugins.Rewriter`s when its method `GetRewriters()` is called by Dafny,
+  2. Can return a list of `Microsoft.Dafny.Plugins.Compiler`s when its method `GetCompilers()` is called by Dafny,
+  3. If the configuration extends the subclass `Microsoft.Dafny.LanguageServer.Plugins.PluginConfiguration`:
+      1. Can return a list of `Microsoft.Dafny.LanguageServer.Plugins.DafnyCodeActionProvider`s when its method `GetDafnyCodeActionProviders()` is called by the Dafny Language Server.
+      2. Can return a modified version of `OmniSharp.Extensions.LanguageServer.Server.LanguageServerOptions` when its method `WithPluginHandlers()` is called by the Dafny Language Server.
 
 * Zero or more classes extending `Microsoft.Dafny.Plugins.Rewriter`.
   If a configuration class is provided, it is responsible for instantiating them and returning them in `GetRewriters()`.
@@ -29,6 +30,7 @@ A plugin typically defines:
   Only a configuration class of type `Microsoft.Dafny.LanguageServer.Plugins.PluginConfiguration` can be responsible for instantiating them and returning them in `GetDafnyCodeActionProviders()`.
 
 The most important methods of the class `Rewriter` that plugins override are
+
 * (experimental) `PreResolve(ModuleDefinition)`: Here you can optionally modify the AST before it is resolved.
 * `PostResolve(ModuleDefinition)`: This method is repeatedly called with every resolved and type-checked module, before verification.
   Plugins override this method typically to report additional diagnostics.
@@ -38,11 +40,12 @@ Plugins are typically used to report additional diagnostics such as unsupported
 
 Note that all plugin errors should use the original program's expressions' token and NOT `Token.NoToken`, else no error will be displayed in the IDE.
 
-## 15.1. Code actions plugin tutorial
+## 15.1. Language Server plugin tutorial
+
+In this section, we will create a plugin that enhances the functionality of the Language Server.
+We will start by showing the steps needed to create a plugin, followed by an example implementation that demonstrates how to provide more code actions and add custom request handlers.
 
-In this section, we will create a plugin to provide more code actions to Dafny.
-The code actions will be simple: Add a dummy comment in front of the first method name,
-if the selection is on the line of the method.
+### 15.1.1. Create plugin project
 
 Assuming the Dafny source code is installed in the folder `dafny/`
 start by creating an empty folder next to it, e.g. `PluginTutorial/`
@@ -51,22 +54,33 @@ start by creating an empty folder next to it, e.g. `PluginTutorial/`
 mkdir PluginTutorial
 cd PluginTutorial
 ```
+
 Then, create a dotnet class project
+
 ```bash
 dotnet new classlib
 ```
+
 It will create a file `Class1.cs` that you can rename
+
 ```bash
-mv Class1.cs PluginAddComment.cs
+mv Class1.cs MyPlugin.cs
 ```
+
 Open the newly created file `PluginTutorial.csproj`, and add the following after `</PropertyGroup>`:
+
 ```xml
   <ItemGroup>
     <ProjectReference Include="../dafny/source/DafnyLanguageServer/DafnyLanguageServer.csproj" />
   </ItemGroup>
 ```
+### 15.1.2. Implement plugin
+
+#### 15.1.2.1. Code actions plugin
 
-Then, open the file `PluginAddComment.cs`, remove everything, and write the imports and a namespace:
+This code action plugin will add a code action that allows you to place a dummy comment in front of the first method name, only if the selection is on the line of the method.
+
+Open the file `MyPlugin.cs`, remove everything, and write the imports and a namespace:
 
 ```csharp
 using Microsoft.Dafny;
@@ -76,18 +90,20 @@ using Microsoft.Dafny.LanguageServer.Language;
 using System.Linq;
 using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
 
-namespace PluginAddComment;
+namespace MyPlugin;
 ```
 
 After that, add a `PluginConfiguration` that will expose all the quickfixers of your plugin.
 This class will be discovered and instantiated automatically by Dafny.
+
 ```csharp
 public class TestConfiguration : PluginConfiguration {
   public override DafnyCodeActionProvider[] GetDafnyCodeActionProviders() {
     return new DafnyCodeActionProvider[] { new AddCommentDafnyCodeActionProvider() };
   }
 }
 ```
+
 Note that you could also override the methods `GetRewriters()` and `GetCompilers()` for other purposes, but this is out of scope for this tutorial.
 
 Then, we need to create the quickFixer `AddCommentDafnyCodeActionProvider` itself:
@@ -102,6 +118,7 @@ public class AddCommentDafnyCodeActionProvider : DafnyCodeActionProvider {
 
 For now, this quick fixer returns nothing. `input` is the program state, and `selection` is where the caret is.
 We replace the return statement with a conditional that tests whether the selection is on the first line:
+
 ```csharp
     var firstTokenRange = input.Program?.GetFirstTopLevelToken()?.GetLspRange();
     if(firstTokenRange != null && firstTokenRange.Start.Line == selection.Start.Line) {
@@ -118,6 +135,7 @@ A `DafnyCodeActionEdit` has a `Range` to remove and some `string` to insert inst
 of the same `DafnyCodeAction` are applied at the same time if selected.
 
 To create a `DafnyCodeAction`, we can either use the easy-to-use `InstantDafnyCodeAction`, which accepts a title and an array of edits:
+
 ```csharp
   return new DafnyCodeAction[] {
     new InstantDafnyCodeAction("Insert comment", new DafnyCodeActionEdit[] {
@@ -127,6 +145,7 @@ To create a `DafnyCodeAction`, we can either use the easy-to-use `InstantDafnyCo
 ```
 
 or we can implement our custom inherited class of `DafnyCodeAction`:
+
 ```csharp
 public class CustomDafnyCodeAction: DafnyCodeAction {
   public Range whereToInsert;
@@ -141,14 +160,72 @@ public class CustomDafnyCodeAction: DafnyCodeAction {
   }
 }
 ```
+
 In that case, we could return:
+
 ```csharp
   return new DafnyCodeAction[] {
     new CustomDafnyCodeAction(firstTokenRange)
   };
 ```
 
+#### 15.1.2.2. Request handler plugin
+
+This request handler plugin enhances the Language Server to support a request with a `TextDocumentIdentifier` as parameter, which will return a `bool` value denoting whether the provided `DocumentUri` has any `LoopStmt`'s in it.
+
+Open the file `MyPlugin.cs`, remove everything, and write the imports and a namespace:
+
+```csharp
+using OmniSharp.Extensions.JsonRpc;
+using OmniSharp.Extensions.LanguageServer.Server;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+using Microsoft.Dafny.LanguageServer.Plugins;
+using Microsoft.Dafny.LanguageServer.Workspace;
+using MediatR;
+using Microsoft.Dafny;
+
+namespace MyPlugin;
+```
+
+After that, add a `PluginConfiguration` that will add all the request handlers of your plugin.
+This class will be discovered and instantiated automatically by Dafny.
+
+```csharp
+public class TestConfiguration : PluginConfiguration {
+  public override LanguageServerOptions WithPluginHandlers(LanguageServerOptions options) {
+    return options.WithHandler<DummyHandler>();
+  }
+}
+```
+
+Then, we need to create the request handler `DummyHandler` itself:
+
+```csharp
+[Parallel]
+[Method("dafny/request/dummy", Direction.ClientToServer)]
+public record DummyParams : TextDocumentIdentifier, IRequest<bool>;
+
+public class DummyHandler : IJsonRpcRequestHandler<DummyParams, bool> {
+  private readonly IProjectDatabase projects;
+  public DummyHandler(IProjectDatabase projects) {
+    this.projects = projects;
+  }
+  public async Task<bool> Handle(DummyParams request, CancellationToken cancellationToken) {
+    var state = await projects.GetParsedDocumentNormalizeUri(request);
+    if (state == null) {
+      return false;
+    }
+    return state.Program.Descendants().OfType<LoopStmt>().Any();
+  }
+}
+```
+
+For more advanced example implementations of request handlers, look at `dafny/Source/DafnyLanguageServer/Handlers/*`.
+
+### 15.1.3. Building plugin
+
 That's it! Now, build your library while inside your folder:
+
 ```bash
 > dotnet build
 ```

latest/DafnyRef/Specifications.2.expect

@@ -1,3 +1,3 @@
-text.dfy(4,2): Warning: note, this loop has no body (loop frame: i)
+text.dfy(4,2): Warning: this loop has no body (loop frame: i)
 
 Dafny program verifier did not attempt verification