snapshot v4 6 0 (#43)

- Removing old latest
- Documentation snapshot for v4.6.0

Snapshots.md

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

latest/DafnyRef/Attributes.md

@@ -398,7 +398,7 @@ in which methods or functions are verified (default: N = 1).
 `{:resource_limit N}` limits the verifier resource usage to verify the method or function to `N`.
 
 This is the per-method equivalent of the command-line flag `/rlimit:N` or `--resource-limit N`.
-If using [`{:vcs_split_on_every_assert}`](#sec-vcs_split_on_every_assert) as well, the limit will be set for each assertion.
+If using [`{:isolate_assertions}`](#sec-isolate_assertions) as well, the limit will be set for each assertion.
 
 The attribute `{:rlimit N}` is also available, and limits the verifier resource usage to verify the method or function to `N * 1000`. This version is deprecated, however.
 
@@ -422,10 +422,10 @@ To give orders of magnitude about resource usage, here is a list of examples ind
   }
   ```
 
-* 40K total resource usage using [`{:vcs_split_on_every_assert}`](#sec-vcs_split_on_every_assert)
+* 40K total resource usage using [`{:isolate_assertions}`](#sec-isolate_assertions)
 <!-- %check-verify -->
   ```dafny
-  method {:vcs_split_on_every_assert} f(a: bool, b: bool) {
+  method {:isolate_assertions} f(a: bool, b: bool) {
     assert a: (a ==> b) <==> (!b ==> !a);
     assert b: (a ==> b) <==> (!b ==> !a);
     assert c: (a ==> b) <==> (!b ==> !a);
@@ -608,7 +608,7 @@ The [assertion batch](#sec-assertion-batches) of a method
 will not be split unless the cost of an [assertion batch](#sec-assertion-batches) exceeds this
 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.
+If [`{:isolate_assertions}`](#sec-isolate_assertions) is set, then this parameter is useless.
 
 ### 11.2.23. `{:vcs_max_keep_going_splits N}` {#sec-vcs_max_keep_going_splits}
 
@@ -619,18 +619,18 @@ until we succeed proving them, or there is only one
 single assertion that it timeouts (in which
 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.
+If [`{:isolate_assertions}`](#sec-isolate_assertions) is set, then this parameter is useless.
 
 ### 11.2.24. `{: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.
+If [`{:isolate_assertions}`](#sec-isolate_assertions) is set, then this parameter is useless.
 
-### 11.2.25. `{:vcs_split_on_every_assert}` {#sec-vcs_split_on_every_assert}
-Per-method version of the command-line option `/vcsSplitOnEveryAssert`.
+### 11.2.25. `{:isolate_assertions}` {#sec-isolate_assertions}
+Per-method version of the command-line option<span id="sec-vcs_split_on_every_assert"></span> `/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.

latest/DafnyRef/Expressions.md

@@ -1716,7 +1716,7 @@ e[ .. ]
 A subsequence suffix applied to a sequence produces a new sequence whose
 elements are taken from a contiguous part of the original sequence. For
 example, expression `s[lo..hi]` for sequence `s`, and integer-based
-numerics `lo` and `hi` satisfying `0 <= lo <= hi <= |s|`. See
+numeric bounds `lo` and `hi` satisfying `0 <= lo <= hi <= |s|`. See
 [the section about other sequence expressions](#sec-other-sequence-expressions) for details.
 
 A subsequence suffix applied to an array produces a _sequence_ consisting of 

latest/DafnyRef/Types.11.expect

@@ -1,3 +1,3 @@
-text.dfy(11,25): Error: argument at index 1 ('d') might not be allocated in the two-state function's previous state
+text.dfy(11,25): Error: argument at index 1 for parameter 'd' could not be proved to be allocated in the two-state function's previous state -- if you add 'new' before the parameter declaration, like 'new d: Cell', arguments can refer to expressions possibly unallocated in the previous state
 
 Dafny program verifier finished with 2 verified, 1 error

latest/DafnyRef/Types.12.expect

@@ -1,3 +1,3 @@
-text.dfy(10,27): Error: argument at index 0 ('c') might not be allocated in the two-state function's previous state
+text.dfy(10,27): Error: argument at index 0 for parameter 'c' could not be proved to be allocated in the two-state function's previous state -- if you add 'new' before the parameter declaration, like 'new c: Cell', arguments can refer to expressions possibly unallocated in the previous state
 
 Dafny program verifier finished with 2 verified, 1 error

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(10,9): Related location
+text.dfy(10,9): Related location: this proposition could not be proved
 
 Dafny program verifier finished with 1 verified, 1 error

latest/DafnyRef/Types.26.expect

@@ -1,2 +1,2 @@
-text.dfy(3,9): Error: type parameter (T) passed to type A must support nonempty (got Q) (perhaps try declaring abstract type 'Q' on line 2 as 'Q(00)', which says it can only be instantiated with a nonempty type)
+text.dfy(3,9): Error: type parameter (T) passed to type A must be nonempty (got Q) (perhaps try declaring abstract type 'Q' on line 2 as 'Q(00)', which says it can only be instantiated with a nonempty type)
 1 resolution/type errors detected in text.dfy

latest/DafnyRef/Types.9.expect

@@ -1,3 +1,3 @@
-text.dfy(10,10): Error: type parameter (T) passed to type ResultN must support no references (got C)
-text.dfy(12,10): Error: type parameter (T) passed to type ResultN must support no references (got array<int>)
+text.dfy(10,10): Error: type parameter (T) passed to type ResultN must contain no references (got C)
+text.dfy(12,10): Error: type parameter (T) passed to type ResultN must contain no references (got array<int>)
 2 resolution/type errors detected in text.dfy

latest/DafnyRef/Types.md

@@ -1085,9 +1085,10 @@ same name.
 
 #### 5.5.3.4. Other Sequence Expressions {#sec-other-sequence-expressions}
 In addition, for any sequence `s` of type `seq<T>`, expression `e`
-of type `T`, integer-based numeric `i` satisfying `0 <= i < |s|`, and
-integer-based numerics `lo` and `hi` satisfying
-`0 <= lo <= hi <= |s|`, sequences support the following operations:
+of type `T`, integer-based numeric index `i` satisfying `0 <= i < |s|`, and
+integer-based numeric bounds `lo` and `hi` satisfying
+`0 <= lo <= hi <= |s|`, noting that bounds can equal the length of the sequence,
+sequences support the following operations:
 
  expression         | precedence | result type | description
  -------------------|:---:|:---:|----------------------------------------
@@ -1859,7 +1860,7 @@ the newtype operations are defined only if the result satisfies the
 predicate `Q`, and likewise for the literals of the
 newtype.
 
-For example, suppose `lo` and `hi` are integer-based numerics that
+For example, suppose `lo` and `hi` are integer-based numeric bounds that
 satisfy `0 <= lo <= hi` and consider the following code fragment:
 <!-- %no-check -->
 ```dafny
@@ -2408,8 +2409,9 @@ an error message is generated.
 
 One-dimensional arrays support operations that convert a stretch of
 consecutive elements into a sequence.  For any array `a` of type
-`array<T>`, integer-based numerics `lo` and `hi` satisfying
-`0 <= lo <= hi <= a.Length`, the following operations each yields a
+`array<T>`, integer-based numeric bounds `lo` and `hi` satisfying
+`0 <= lo <= hi <= a.Length`, noting that bounds can equal the array's length,
+the following operations each yields a
 `seq<T>`:
 
  expression          | description

latest/DafnyRef/UserGuide.md

@@ -1434,7 +1434,7 @@ The fundamental unit of verification in `dafny` is an _assertion batch_, which c
 * If the verifier says it is correct,[^smt-encoding] it means that all the assertions hold.
 * If the verifier returns a counterexample, this counterexample is used to determine both the failing assertion and the failing path.
   In order to retrieve additional failing assertions, `dafny` will again query the verifier after turning previously failed assertions into assumptions.[^example-assertion-turned-into-assumption] [^caveat-about-assertion-and-assumption]
-* If the verifier returns `unknown` or times out, or even preemptively for difficult assertions or to reduce the chance that the verifier will ‘be confused’ by the many assertions in a large batch, `dafny` may partition the assertions into smaller batches[^smaller-batches]. An extreme case is the use of the `/vcsSplitOnEveryAssert` command-line option or the [`{:vcs_split_on_every_assert}` attribute](#sec-vcs_split_on_every_assert), which causes `dafny` to make one batch for each assertion.
+* If the verifier returns `unknown` or times out, or even preemptively for difficult assertions or to reduce the chance that the verifier will ‘be confused’ by the many assertions in a large batch, `dafny` may partition the assertions into smaller batches[^smaller-batches]. An extreme case is the use of the `/vcsSplitOnEveryAssert` command-line option or the [`{:isolate_assertions}` attribute](#sec-isolate_assertions), which causes `dafny` to make one batch for each assertion.
 
 [^smt-encoding]: The formula sent to the underlying SMT solver is the negation of the formula that the verifier wants to prove - also called a VC or verification condition. Hence, if the SMT solver returns "unsat", it means that the SMT formula is always false, meaning the verifier's formula is always true. On the other side, if the SMT solver returns "sat", it means that the SMT formula can be made true with a special variable assignment, which means that the verifier's formula is false under that same variable assignment, meaning it's a counter-example for the verifier. In practice and because of quantifiers, the SMT solver will usually return "unknown" instead of "sat", but will still provide a variable assignment that it couldn't prove that it does not make the formula true. `dafny` reports it as a "counter-example" but it might not be a real counter-example, only provide hints about what `dafny` knows.
 
@@ -1450,7 +1450,7 @@ Here is how you can control how `dafny` partitions assertions into batches.
 
 * [`{:focus}`](#sec-focus) on an assert generates a separate assertion batch for the assertions of the enclosing block.
 * [`{:split_here}`](#sec-split_here) on an assert generates a separate assertion batch for assertions after this point.
-* [`{:vcs_split_on_every_assert}`](#sec-vcs_split_on_every_assert) on a function or a method generates one assertion batch per assertion
+* [`{:isolate_assertions}`](#sec-isolate_assertions) on a function or a method generates one assertion batch per assertion
 
 We discourage the use of the following _heuristics attributes_ to partition assertions into batches.
 The effect of these attributes may vary, because they are low-level attributes and tune low-level heuristics, and will result in splits that could be manually controlled anyway.
@@ -2679,7 +2679,7 @@ Legacy options:
 
 * `-vcsSplitOnEveryAssert` - prove each (explicit or implicit) assertion
   in each procedure separately. See also the attribute
-  [`{:vcs_split_on_every_assert}`](#sec-vcs_split_on_every_assert) for
+  [`{:isolate_assertions}`](#sec-isolate_assertions) for
   restricting this option on specific procedures. By default, Boogie
   attempts to prove that every assertion in a given procedure holds all
   at once, in a single query to an SMT solver. This usually performs

latest/HowToFAQ/Errors-Refinement.md

@@ -80,78 +80,68 @@ module Q refines P {
 
 A submodule M within a module that is refining some base module must refine some submodule M in the base module.
 
-## **Error: type declaration '_name_' is not allowed to change the requirement of supporting equality** {#ref_mismatched_equality}
-
-<!-- TODO -->
-
-## **Error: type declaration '_name_' is not allowed to change the requirement of supporting auto-initialization** {#ref_mismatched_auto_init}
-
-<!-- TODO -->
-
-## **Error: type declaration '_name_' is not allowed to change the requirement of being nonempty** {#ref_mismatched_nonempty}
-
-<!-- TODO -->
-
-## **Error: a type declaration that requires equality support cannot be replaced by this trait** {#ref_trait_mismatched_equality}
-
-<!-- TODO -->
-
-## **Error: a type declaration that requires equality support cannot be replaced by a codatatype** {#ref_equality_support_precludes_codatatype}
+## **Error: to be a refinement of _kind_ '_name_' declared with (==), _kind_ '_name_' must support equality {#ref_mismatched_type_characteristics_equality}
 
 ```dafny
 module P {
   type T(==)
 }
 module Q refines P {
-  codatatype T = A
+  type T = AlwaysAndForeverMore
+  codatatype AlwaysAndForeverMore = Cons(int, AlwaysAndForeverMore)
 }
 ```
 
-Codatatypes do not generally support equality and so cannot be refinements of an abstract type that declares that it supports equality.
+The abstract type `T` in module `P` says it supports equality, but its attempted refinement in module `Q` does not.
+Codatatypes do not generally support equality and so cannot be refinements of equality-supporting abstract types.
 
-## **Error: type '_name_', which does not support equality, is used to refine an abstract type with equality support** {#ref_mismatched_type_equality_support}
+## **Error: to be a refinement of _kind_ '_name_' declared with (!new), _kind_ '_name_' must contain no references {#ref_mismatched_type_characteristics_noreferences}
 
 ```dafny
 module P {
-  type T(==)
+  type T(!new)
 }
 module Q refines P {
-  codatatype A = B | C
-  type T = A
+  type T = (int, bool, array<real>)
 }
 ```
 
-A refining type must be declared to support equality (with `(==)`) if the base declaration is declared to support equality.
-
+The abstract type `T` in module `P` says it contains no reference, but its attempted refinement in module `Q` does.
+A refining type must support the type characteristics declared of the refined type.
 
-## **Error: type '_name_', which does not support auto-initialization, is used to refine an abstract type that expects auto-initialization** {#ref_mismatched_type_auto_init}
+## **Error: to be a refinement of _kind_ '_name_' declared with (00), _kind_ '_name_' must be nonempty {#ref_mismatched_type_characteristics_nonempty}
 
 ```dafny
 module P {
-  type T(0)
+  type T(00)
 }
 module Q refines P {
-  class A{}
   type T = A
+  class A { }
 }
 ```
 
-A refining type must be declared to be auto-initializing (with `(0)`) if the base declaration is declared auto-initializing.
+The abstract type `T` in module `P` uses the type characteristic `(00)` to say that it is nonempty. However, a class type is
+not generally known to be nonempty, so `A` cannot be used as a refinement for `T` in `Q`.
 
+For this particular situation, a possible remedy would be to instead use `type T = A?`, since the nullable type `A?` is known to be nonempty.
 
-## **Error: type '_name_', which may be empty, is used to refine an abstract type expected to be nonempty** {#ref_mismatched_type_nonempty}
+## **Error: to be a refinement of _kind_ '_name_' declared with (0), _kind_ '_name_' must support auto-initialization {#ref_mismatched_type_characteristics_autoinit}
 
 ```dafny
 module P {
-  type T(00)
+  type T(0)
 }
 module Q refines P {
-  class A{}
   type T = A
+  class A { }
 }
 ```
 
-A refining type must be declared to be non-empty (with `(00)`) if the base declaration is declared non-empty.
+The abstract type `T` in module `P` uses the type characteristic `(00)` to say that it can be auto-initialized. However, a class type does
+not support auto-initialization, so `A` cannot be used as a refinement for `T` in `Q`.
+
+For this particular situation, a possible remedy would be to instead use `type T = A?`, since the nullable type `A?` does support auto-initialization.
 
 ## **Error: a _kind_ (_name_) cannot declare members, so it cannot refine an abstract type with members** {#ref_mismatched_type_with_members}
 

latest/HowToFAQ/Errors.md

@@ -42,6 +42,10 @@ Italicized words in the given messages indicate variable content.
 {% include_relative Errors-Resolver3.md %}
 {% include_relative Errors-Rewriter.md %}
 
+# **Refinement Errors**
+
+{% include_relative Errors-Refinement.md %}
+
 # **Verification Errors**
 
 _This section is a work in progress_

latest/Snapshots.md

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