Merge pull request #33 from dafny-lang/snapshot-v4_2_0

snapshot v4 2 0

Snapshots.md

@@ -7,6 +7,7 @@ layout: default
 
 - [Current development version](https://dafny.org/dafny)
 - [Latest release snapshot](https://dafny.org/latest)
+- [v4.2.0](https://dafny.org/v4.2.0)
 - [v4.1.0](https://dafny.org/v4.1.0)
 - [v4.0.0](https://dafny.org/v4.0.0)
 - [v3.12.0](https://dafny.org/v3.12.0)

latest/Compilation/AutoInitialization.md

@@ -35,7 +35,7 @@ Dafny supports the following kinds of types:
   subset is characterized by a constraint on `B`)
 
 In addition, there are _type synonyms_ (which are just that--synonyms for other types) and
-_opaque types_ (which cannot be compiled, so they don't play a role here).
+_abstract types_ (which cannot be compiled, so they don't play a role here).
 
 Notes:
 * `nat` is a built-in subset type of `int`

latest/DafnyRef/Attributes.md

@@ -151,7 +151,7 @@ Ignore the declaration (after checking for duplicate names).
 
 * to alter the `CompileName` of entities such as modules, classes, methods, etc.,
 * to alter the `ReferenceName` of the entities,
-* to decide how to define external opaque types,
+* to decide how to define external abstract types,
 * to decide whether to emit target code or not, and
 * to decide whether a declaration is allowed not to have a body.
 
@@ -163,7 +163,7 @@ A common use case of `{:extern}` is to avoid name clashes with existing library
 
 - `{:extern}`: Dafny will use the Dafny-determined name as the `CompileName` and not affect the `ReferenceName`
 - `{:extern s1}`: Dafny will use `s1` as the `CompileName`, and replaces the last portion of the `ReferenceName` by `s1`.
-     When used on an opaque type, s1 is used as a hint as to how to declare that type when compiling.
+     When used on an abstract type, s1 is used as a hint as to how to declare that type when compiling.
 - `{:extern s1, s2}` Dafny will use `s2` as the `CompileName`.
      Dafny will use a combination of `s1` and `s2` such as for example `s1.s2` as the `ReferenceName`
      It may also be the case that one of the arguments is simply ignored.
@@ -175,7 +175,13 @@ For more detail on the use of `{:extern}`, see the corresponding [section](#sec-
 
 ## 11.2. Attributes on functions and methods
 
-### 11.2.1. `{:autoReq}`
+### 11.2.1. `{:abstemious}`
+
+The `{:abstemious}` attribute is appropriate for functions on codatatypes.
+If appropriate to a function, the attribute can aid in proofs that the function is _productive_.
+See [the section on abstemious functions](#sec-abstemious) for more description.
+
+### 11.2.2. `{:autoReq}`
 For a function declaration, if this attribute is set true at the nearest
 level, then its `requires` clause is strengthened sufficiently so that
 it may call the functions that it calls.
@@ -212,7 +218,7 @@ function g(y:int, b:bool) : bool
 }
 ```
 
-### 11.2.2. `{:axiom}` {#sec-axiom}
+### 11.2.3. `{:axiom}` {#sec-axiom}
 The `{:axiom}` attribute may be placed on a function or method.
 It means that the post-condition may be assumed to be true
 without proof. In that case also the body of the function or
@@ -224,18 +230,18 @@ To prevent Dafny from running all these checks, one would use [`{:verify false}`
 
 The compiler will still emit code for an [`{:axiom}`](#sec-axiom), if it is a [`function`, a `method` or a `function by method`](#sec-function-declarations) with a body.
 
-### 11.2.3. `{:compile}`
+### 11.2.4. `{:compile}`
 The `{:compile}` attribute takes a boolean argument. It may be applied to
 any top-level declaration. If that argument is false, then that declaration
 will not be compiled at all.
 The difference with [`{:extern}`](#sec-extern) is that [`{:extern}`](#sec-extern)
 will still emit declaration code if necessary,
 whereas `{:compile false}` will just ignore the declaration for compilation purposes.
 
-### 11.2.4. `{:extern <name>}` {#sec-extern-method}
+### 11.2.5. `{:extern <name>}` {#sec-extern-method}
 See [`{:extern <name>}`](#sec-extern).
 
-### 11.2.5. `{:fuel X}` {#sec-fuel}
+### 11.2.6. `{:fuel X}` {#sec-fuel}
 The fuel attribute is used to specify how much "fuel" a function should have,
 i.e., how many times the verifier is permitted to unfold its definition.  The
 `{:fuel}` annotation can be added to the function itself, in which
@@ -258,11 +264,11 @@ fewer assert statements), but it may also increase verification time,
 so use it with care.  Setting the fuel to 0,0 is similar to making the
 definition opaque, except when used with all literal arguments.
 
-### 11.2.6. `{:id <string>}`
+### 11.2.7. `{:id <string>}`
 Assign a custom unique ID to a function or a method to be used for verification
 result caching.
 
-### 11.2.7. `{:induction}` {#sec-induction}
+### 11.2.8. `{:induction}` {#sec-induction}
 The `{:induction}` attribute controls the application of
 proof by induction to two contexts. Given a list of
 variables on which induction might be applied, the
@@ -312,7 +318,32 @@ lemma Correspondence()
 }
 ```
 
-### 11.2.8. `{:opaque}` {#sec-opaque}
+### 11.2.9. `{:only}` {#sec-only-functions-methods}
+
+`method {:only} X() {}` or `function {:only} X() {}`  temporarily disables the verification of all other non-`{:only}` members, e.g. other functions and methods, in the same file, even if they contain [assertions with `{:only}`](#sec-only).
+
+<!-- %no-check -->
+```dafny
+method {:only} TestVerified() {
+  assert true;                  // Unchecked
+  assert {:only} true by {      // Checked
+    assert true;                // Checked
+  }
+  assert true;                  // Unchecked
+}
+
+method TestUnverified() {
+  assert true;                  // Unchecked
+  assert {:only} true by {      // Unchecked because of {:only} Test()
+    assert true;                // Unchecked
+  }
+  assert true;                  // Unchecked
+}
+```
+
+`{:only}` can help focusing on a particular member, for example a lemma or a function, as it simply disables the verification of all other lemmas, methods and functions in the same file. It's equivalent to adding [`{:verify false}`](#sec-verify) to all other declarations simulatenously on the same file. Since it's meant to be a temporary construct, it always emits a warning.
+
+### 11.2.10. `{:opaque}` {#sec-opaque}
 
 _This attribute is replaced by the keyword `opaque`; the attribute is deprecated._
 
@@ -324,7 +355,7 @@ or if the programmer specifically asks to see it via the statement `reveal foo()
 
 More information about the Boogie implementation of `{:opaque}` is [here](https://github.com/dafny-lang/dafny/blob/master/docs/Compilation/Boogie.md).
 
-### 11.2.9. `{:print}` {#sec-print}
+### 11.2.11. `{:print}` {#sec-print}
 This attribute declares that a method may have print effects,
 that is, it may use `print` statements and may call other methods
 that have print effects. The attribute can be applied to compiled
@@ -334,11 +365,11 @@ allowed to use a `{:print}` attribute only if the overridden method
 does.
 Print effects are enforced only with `--track-print-effects`.
 
-### 11.2.10. `{:priority}`
+### 11.2.12. `{:priority}`
 `{:priority N}` assigns a positive priority 'N' to a method or function to control the order
 in which methods or functions are verified (default: N = 1).
 
-### 11.2.11. `{:rlimit}` {#sec-rlimit}
+### 11.2.13. `{:rlimit}` {#sec-rlimit}
 
 `{:rlimit N}` limits the verifier resource usage to verify the method or function at `N * 1000`.
 This is the per-method equivalent of the command-line flag `/rlimit:N`.
@@ -384,14 +415,14 @@ To give orders of magnitude about resource usage, here is a list of examples ind
 
 Note that, the default solver Z3 tends to overshoot by `7K` to `8K`, so if you put `{:rlimit 20}` in the last example, the total resource usage would be `27K`.
 
-### 11.2.12. `{:selective_checking}`
+### 11.2.14. `{:selective_checking}`
 Turn all assertions into assumptions except for the ones reachable from after the
 assertions marked with the attribute `{:start_checking_here}`.
 Thus, `assume {:start_checking_here} something;` becomes an inverse
 of `assume false;`: the first one disables all verification before
 it, and the second one disables all verification after.
 
-### 11.2.13. `{:tailrecursion}`
+### 11.2.15. `{:tailrecursion}`
 This attribute is used on method declarations. It has a boolean argument.
 
 If specified with a `false` value, it means the user specifically
@@ -407,7 +438,7 @@ recursion was explicitly requested.
 * If `{:tailrecursion true}` was specified but the code does not allow it,
 an error message is given.
 
-### 11.2.14. `{:test}` {#sec-test-attribute}
+### 11.2.16. `{:test}` {#sec-test-attribute}
 This attribute indicates the target function or method is meant
 to be executed at runtime in order to test that the program is working as intended.
 
@@ -445,25 +476,27 @@ harness that supplies input arguments but has no inputs of its own and that
 checks any output values, perhaps with `expect` statements. The test harness
 is then the method marked with `{:test}`.
 
-### 11.2.15. `{:timeLimit N}` {#sec-time-limit}
+### 11.2.17. `{:timeLimit N}` {#sec-time-limit}
 Set the time limit for verifying a given function or method.
 
-### 11.2.16. `{:timeLimitMultiplier X}`
+### 11.2.18. `{:timeLimitMultiplier X}`
 This attribute may be placed on a method or function declaration
 and has an integer argument. If `{:timeLimitMultiplier X}` was
 specified a `{:timeLimit Y}` attribute is passed on to Boogie
 where `Y` is `X` times either the default verification time limit
 for a function or method, or times the value specified by the
 Boogie `-timeLimit` command-line option.
 
-### 11.2.17. `{:verify false}` {#sec-verify}
+### 11.2.19. `{:verify false}` {#sec-verify}
      
 Skip verification of a function or a method altogether,
 not even trying to verify the well-formedness of postconditions and preconditions.
 We discourage using this attribute and prefer [`{:axiom}`](#sec-axiom),
 which performs these minimal checks while not checking that the body satisfies the postconditions.
 
-### 11.2.18. `{:vcs_max_cost N}` {#sec-vcs_max_cost}
+If you simply want to temporarily disable all verification except on a single function or method, use the [`{:only}`](#sec-only-functions-methods) attribute on that function or method.
+
+### 11.2.20. `{:vcs_max_cost N}` {#sec-vcs_max_cost}
 Per-method version of the command-line option `/vcsMaxCost`.
 
 The [assertion batch](#sec-assertion-batches) of a method
@@ -472,7 +505,7 @@ number, defaults to 2000.0. In
 [keep-going mode](#sec-vcs_max_keep_going_splits), only applies to the first round.
 If [`{:vcs_split_on_every_assert}`](#sec-vcs_split_on_every_assert) is set, then this parameter is useless.
 
-### 11.2.19. `{:vcs_max_keep_going_splits N}` {#sec-vcs_max_keep_going_splits}
+### 11.2.21. `{:vcs_max_keep_going_splits N}` {#sec-vcs_max_keep_going_splits}
 
 Per-method version of the command-line option `/vcsMaxKeepGoingSplits`.
 If set to more than 1, activates the _keep going mode_ where, after the first round of splitting,
@@ -483,22 +516,22 @@ case an error is reported for that assertion).
 Defaults to 1.
 If [`{:vcs_split_on_every_assert}`](#sec-vcs_split_on_every_assert) is set, then this parameter is useless.
 
-### 11.2.20. `{:vcs_max_splits N}` {#sec-vcs_max_splits}
+### 11.2.22. `{:vcs_max_splits N}` {#sec-vcs_max_splits}
 
 Per-method version of the command-line option `/vcsMaxSplits`.
 Maximal number of [assertion batches](#sec-assertion-batches) generated for this method.
 In [keep-going mode](#sec-vcs_max_keep_going_splits), only applies to the first round.
 Defaults to 1.
 If [`{:vcs_split_on_every_assert}`](#sec-vcs_split_on_every_assert) is set, then this parameter is useless.
 
-### 11.2.21. `{:vcs_split_on_every_assert}` {#sec-vcs_split_on_every_assert}
+### 11.2.23. `{:vcs_split_on_every_assert}` {#sec-vcs_split_on_every_assert}
 Per-method version of the command-line option `/vcsSplitOnEveryAssert`.
 
 In the first and only verification round, this option will split the original [assertion batch](#sec-assertion-batches)
 into one assertion batch per assertion.
 This is mostly helpful for debugging which assertion is taking the most time to prove, e.g. to profile them.
 
-### 11.2.22. `{:synthesize}` {#sec-synthesize-attr}
+### 11.2.24. `{:synthesize}` {#sec-synthesize-attr}
 
 The `{:synthesize}` attribute must be used on methods that have no body and
 return one or more fresh objects. During compilation, 
@@ -532,7 +565,7 @@ BOUNDVARS = ID : ID
           | BOUNDVARS, BOUNDVARS
 ```
 
-### 11.2.23. `{:options OPT0, OPT1, ... }` {#sec-attr-options}
+### 11.2.25. `{:options OPT0, OPT1, ... }` {#sec-attr-options}
 
 This attribute applies only to modules. It configures Dafny as if
 `OPT0`, `OPT1`, … had been passed on the command line.  Outside of the module,
@@ -578,6 +611,8 @@ For example, in `assert B ==> (assert {:only "after"} true; C)`, `C` is actually
 
 As soon as a declaration contains one `assert {:only}`, none of the postconditions are verified; you'd need to make them explicit with assertions if you wanted to verify them at the same time.
 
+You can also isolate the verification of a single member using [a similar `{:only}` attribute](#sec-only-functions-methods).
+
 ### 11.3.2. `{:focus}` {#sec-focus}
 `assert {:focus} X;` splits verification into two [assertion batches](#sec-assertion-batches).
 The first batch considers all assertions that are not on the block containing the `assert {:focus} X;`
@@ -669,9 +704,38 @@ Overrides the `/subsumption` command-line setting for this assertion.
 `{:subsumption 0}` checks an assertion but does not assume it after proving it.
 You can achieve the same effect using [labelled assertions](#sec-labeling-revealing-assertions).
 
+### 11.3.5. `{:error "errorMessage", "successMessage"}` {#sec-error-attribute}
+Provides a custom error message in case the assertion fails.
+As a hint, messages indicating what the user needs to do to fix the error are usually better than messages that indicate the error only.
+For example:
+
+<!-- %check-resolve -->
+```dafny
+method Process(instances: int, price: int)
+  requires {:error "There should be an even number of instances", "The number of instances is always even"} instances % 2 == 0
+  requires {:error "Could not prove that the price is positive", "The price is always positive"} price >= 0
+{
+}
+method Test()
+{
+  if * {
+    Process(1, 0); // Error: There should be an even number of instances
+  }
+  if * {
+    Process(2, -1); // Error: Could not prove that the price is positive
+  }
+  if * {
+    Process(2, 5); // Success: The number of instances is always even
+                   // Success: The price is always positive
+  }
+}
+```
+
+The success message is optional but is recommended if errorMessage is set.
+
 ## 11.4. Attributes on variable declarations
 
-### 11.4.1. `{:assumption}`
+### 11.4.1. `{:assumption}` {#sec-assumption}
 This attribute can only be placed on a local ghost bool
 variable of a method. Its declaration cannot have a rhs, but it is
 allowed to participate as the lhs of exactly one assignment of the

latest/DafnyRef/Expressions.md

@@ -1107,8 +1107,8 @@ map from explicit mappings. For example:
 
 <!-- %check-resolve -->
 ```dafny
-const m := map[1 := "a", 2 := "b"];
-ghost const im := imap[1 := "a", 2 := "b"];
+const m := map[1 := "a", 2 := "b"]
+ghost const im := imap[1 := "a", 2 := "b"]
 ```
 
 See [Section 5.5.4](#sec-maps) for more details on maps and imaps.
@@ -1825,6 +1825,21 @@ Method calls, object-allocation calls (`new`), function calls, and
 datatype constructors can be called with both positional arguments
 and named arguments.
 
+Formal parameters have three ways to indicate how they are to be passed in:
+- nameonly: the only way to give a specific argument value is to name the parameter
+- positional only: these are nameless parameters (which are allowed only for datatype constructor parameters)
+- either positional or by name: this is the most common parameter
+
+A parameter is either required or optional:
+- required: a caller has to supply an argument
+- optional: the parameter has a default value that is used if a caller omits passing a specific argument
+
+The syntax for giving a positional-only (i.e., nameless) parameter does not allow a default-value expression, so a positional-only parameter is always required.
+
+At a call site, positional arguments are not allowed to follow named arguments. Therefore, if `x` is a nameonly parameter, then there is no way to supply the parameters after `x` by position. 
+Thus, any parameter that follows `x` must either be passed by name or have a default value. 
+That is, if a later (in the formal parameter declaration) parameter does not have a default value, it is effectively nameonly. 
+
 Positional arguments must be given before any named arguments.
 Positional arguments are passed to the formals in the corresponding
 position. Named arguments are passed to the formal of the given
@@ -1837,32 +1852,7 @@ 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. Formal Parameters and Default-Value Expressions
-
-The formal parameters of a method, constructor in a class, iterator,
-function, or datatype constructor can be declared with an expression
-denoting a _default value_. This makes the parameter _optional_,
-as opposed to _required_. All required parameters must be declared
-before any optional parameters. All nameless parameters in a datatype
-constructor must be declared before any `nameonly` parameters.
-
-The default-value expression for a parameter is allowed to mention the
-other parameters, including `this` (for instance methods and instance
-functions), but not the implicit `_k` parameter in least and greatest
-predicates and lemmas. The default value of a parameter may mention
-both preceding and subsequent parameters, but there may not be any
-dependent cycle between the parameters and their default-value
-expressions.
-
-The well-formedness of default-value expressions is checked independent
-of the precondition of the enclosing declaration. For a function, the
-parameter default-value expressions may only read what the function's
-`reads` clause allows. For a datatype constructor, parameter default-value
-expressions may not read anything. A default-value expression may not be
-involved in any recursive or mutually recursive calls with the enclosing
-declaration.
-
-## 9.38. Compile-Time Constants {#sec-compile-time-constants}
+## 9.37. 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
@@ -1903,7 +1893,7 @@ 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.39. List of specification expressions {#sec-list-of-specification-expressions}
+## 9.38. 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.
 

latest/DafnyRef/Features.md

@@ -39,8 +39,9 @@
 | [Subtype constraints in quantifiers](#sec-quantifier-expression) |  X  |  X  |  X  |  X  |  X  |  X  |  X  |
 | [Tuples with more than 20 arguments](#sec-tuple-types) |  |  X  |  X  |  |  X  |  X  |  X  |
 | [Unicode chars](##sec-characters) |  X  |  X  |  X  |  X  |  X  |  |  X  |
-| [Converting values to strings](##sec-print-statement) |  X  |  X  |  X  |  X  |  X  |  |  X  |
-| [Legacy CLI without commands](###sec-dafny-commands) |  X  |  X  |  X  |  X  |  X  |  X  |  |
+| [Converting values to strings](#sec-print-statement) |  X  |  X  |  X  |  X  |  X  |  |  X  |
+| [Legacy CLI without commands](#sec-dafny-commands) |  X  |  X  |  X  |  X  |  X  |  X  |  |
+| [Separate compilation](#sec-compilation) |  X  |  |  X  |  X  |  X  |  X  |  X  |
 
 [^compiler-feature-forall-note]: 'Sequentializing' a `forall` statement refers to compiling it directly to a series of nested loops
     with the statement's body directly inside. The alternative, default compilation strategy