snapshot v4 3 0 (#35)

- Removing old latest
- Documentation snapshot for v4.3.0

Snapshots.md

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

latest/Compilation/AutoInitialization.md

@@ -10,8 +10,9 @@ enforce that each value assigned to a variable is indeed a value of that variabl
 type. Since the type of a variable never changes, this ensures type safety, provided
 a variable is assigned before it is used. But what about any uses before then?
 
-If a variable is used before it has been assigned, Dafny still arranges for the
-variable to be initialized with _some_ value of the variable's type.
+If a variable is used before it has been assigned, Dafny still--in certain situations,
+like for array elements or when a variable is explicitly assigned `*`--arranges for
+the variable to be initialized with _some_ value of the variable's type.
 To accomplish this, the compiler needs to have the ability to emit an expression that
 produces a value of a given type. This is possible for many, but not all, types.
 
@@ -122,13 +123,16 @@ Auto-init types
 ---------------
 
 A type is called an _auto-init type_ if it is legal for a program to use a variable of
-that type before the variable has been initialized.
+that type before the variable has been initialized (or, for local variables, if the
+variable has only been assigned `*`).
 
 For example, `char` is an auto-init type. Therefore, the following is a legal program
 snippet:
 
-    var ch: char;
-    print ch, "\n";  // this uses ch before ch has been explicitly assigned
+    var ch: char := *;
+    print ch, "\n";  // this uses ch at a time when ch has only been assigned *
+    var arr: array<char> := new char[100];
+    print arr[5], "\n";  // this uses arr[5] before ch has been explicitly assigned
 
 A compiler is permitted to assign _any_ value to `ch`, so long as that value is of
 type `char`. In fact, the compiler is free to emit code that chooses a different
@@ -154,14 +158,14 @@ type                                             | default-valued expression
 `int`                                            | `BigInteger.Zero`
 `real`                                           | `BigRational.ZERO`
 `bool`                                           | `false`
-`char`                                           | `D`
+`char`                                           | `D` (because `\0` is not visible when printed as part of a string, so `D` leads to fewer surprises)
 bitvectors                                       | `0` or `BigInteger.Zero`
 `ORDINAL`                                        | `BigInteger.Zero`
 integer-based `newtype` without `witness` clause | same as for base type, cast appropriately
 real-based `newtype` without `witness` clause    | same as for base type, cast appropriately
 `newtype` `NT` with `witness` clause             | `NT.Witness`
 possibly-null reference types                    | `null`
-non-null array types                             | empty array of the appropriate type
+non-null array types                             | array of the appropriate type with every dimension having length 0
 type parameter `T`                               | `td_T.Default()`
 collection type `C<TT>`                          | `C<TT>.Empty`
 datatype or co-datatype `D<TT>`                  | `D<TT>.Default(E, ...)`
@@ -218,7 +222,7 @@ public static readonly B Witness = W;
 Each datatype and co-datatype has a _grounding constructor_. For a `datatype`, the grounding
 constructor is selected when the resolver ascertains that the datatype is nonempty. For a
 `codatatype`, the selection of the grounding constructor lacks sophistication--it is just the
-first of the given constructors.
+first of the given constructors. (Note, the grounding constructor might be ghost.)
 
 If the datatype is not an auto-init type, then there's nothing more to say about its default
 value. If it is an auto-init type, then the following explanations apply.
@@ -238,7 +242,10 @@ public static DT<TT> Default(T e, ...) {
 ```
 
 The parameters to this `Default` method are the default values for each of the type parameters
-used by the grounding constructor.
+used by the grounding constructor. (If the datatype's type parameters include some auto-init
+type parameters, then type descriptors for them are also passed in to both `Default` and
+`create_GroundingCtor`, not illustrated in the example just shown. More about such type descriptors
+in a section below.)
 
 If the (co-)datatype has no type parameters (note: that is, no type parameters at all--the
 "used parameters" are not involved here), then the default value is pre-computed and reused:
@@ -372,8 +379,7 @@ public static Dafny.TypeDescriptor<D<TT>> _TypeDescriptor(Dafny.TypeDescriptor<T
 }
 ```
 
-where the list of type parameters denoted by `T, ...` are the auto-init type parameters from `TT`.
-
+where the list of type parameters denoted by `T, ...` are the "used" type parameters from `TT`.
 
 ## Subset types
 
@@ -445,14 +451,23 @@ class Cl<T> {
 }
 ```
 
+### Type parameter of a (co-)datatype
+
+If `T` is a type parameter of a (co-)datatype, then `td_T` is a field of the object
+representing each (co-)datatype value.
+
+### Type parameter of a `newtype`
+
+Newtypes don't take type parameters.
+
 ### Type parameters of a trait
 
 To obtain type descriptors in function and method implementations that are given
 in a trait, the function or method definition compiled into the companion class
 takes additional parameters that represent type descriptors for the type parameters
 of the trait.
 
-### Type parameter of a class or trait used in a static method or function
+### Type parameter of a class, trait, (co-)datatype, or abstract type used in a static method or static function
 
 In C#, the type parameters of a class are available in static methods. However,
 any type descriptors of the class are stored in instance fields, since the target
@@ -477,12 +492,6 @@ class Class<A> {
 }
 ```
 
-### Type parameter of a `newtype` or (co-)datatype
-
-If `T` is a type parameter of a (co-)datatype, then the target code for any function
-or method takes additional parameters that represent type descriptors for the type
-parameters of the enclosing type.
-
 Type parameters and type descriptors for each type
 --------------------------------------------------
 
@@ -511,7 +520,7 @@ TYPE                                | TP  | TD  | TP  | TD  | TP  | TD   | TP  |
   instance member `<B(0)>`          | B   | B   | B   | B   |     | B    |     | B   |
   static member `<B(0)>`            | B   | B   | B   | B   |     | B    |     | B   |
 `datatype<A(0)>`
-  instance member `<B(0)>`          | B   | A,B | B   | A,B |     | A,B  |     | A,B |
+  instance member `<B(0)>`          | B   | B   | B   | B   |     | B    |     | B   |
   static member `<B(0)>`            | B   | A,B | A,B | A,B |     | A,B  |     | A,B |
 `trait<A(0)>`
   instance member `<B(0)>`          | B   | B   | B   | B   |     | B    |     | B   |
@@ -524,7 +533,7 @@ TYPE                                | TP  | TD  | TP  | TD  | TP  | TD   | TP  |
 *) type descriptors for functions don't actually seem necessary (but if functions have them,
 then const's need them, too)
 
-If the type parameters `A` and `B` does not have the `(0)` characteristic, then it is dropped
+If a type parameter among `A` and `B` does not have the `(0)` characteristic, then it is dropped
 from the TD column.
 
 This table is implemented in the `TypeArgDescriptorUse` method in the compiler.

latest/DafnyRef/Attributes.md

@@ -176,7 +176,6 @@ For more detail on the use of `{:extern}`, see the corresponding [section](#sec-
 ## 11.2. Attributes on functions and methods
 
 ### 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.
@@ -218,30 +217,49 @@ function g(y:int, b:bool) : bool
 }
 ```
 
-### 11.2.3. `{:axiom}` {#sec-axiom}
+### 11.2.3. `{:autoRevealDependencies k}` {#sec-autorevealdependencies}
+When setting `--default-function-opacity` to `autoRevealDependencies`, the `{:autoRevealDependencies k}` attribute can be set on methods and functions to make sure that only function dependencies of depth `k` in the call-graph or less are revealed automatically. As special cases, one can also use `{:autoRevealDependencies false}` (or `{:autoRevealDependencies 0}`) to make sure that no dependencies are revealed, and `{:autoRevealDependencies true}` to make sure that all dependencies are revealed automatically.
+
+For example, when the following code is run with `--default-function-opacity` set to `autoRevealDependencies`, the function `p()` should verify and `q()` should not.
+<!-- %no-check -->
+```dafny
+   function t1() : bool { true }
+   
+   function t2() : bool { t1() }
+
+   function {:autoRevealDependencies 1} p() : (r: bool) 
+     ensures r
+   { t1() }
+   
+   function {:autoRevealDependencies 1} q() : (r: bool) 
+     ensures r
+   { t2() }
+```
+
+### 11.2.4. `{: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
 method may be omitted.
 
 The `{:axiom}` attribute only prevents Dafny from verifying that the body matches the post-condition.
-Dafny still verifies the well-formedness of pre-conditions, of post-conditions, and of the body if provided.
+Dafny still verifies the [well-formedness](#sec-assertion-batches) of pre-conditions, of post-conditions, and of the body if provided.
 To prevent Dafny from running all these checks, one would use [`{:verify false}`](#sec-verify), which is not recommended.
 
 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.4. `{:compile}`
+### 11.2.5. `{: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.5. `{:extern <name>}` {#sec-extern-method}
+### 11.2.6. `{:extern <name>}` {#sec-extern-method}
 See [`{:extern <name>}`](#sec-extern).
 
-### 11.2.6. `{:fuel X}` {#sec-fuel}
+### 11.2.7. `{: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
@@ -264,11 +282,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.7. `{:id <string>}`
+### 11.2.8. `{:id <string>}`
 Assign a custom unique ID to a function or a method to be used for verification
 result caching.
 
-### 11.2.8. `{:induction}` {#sec-induction}
+### 11.2.9. `{: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
@@ -318,7 +336,7 @@ lemma Correspondence()
 }
 ```
 
-### 11.2.9. `{:only}` {#sec-only-functions-methods}
+### 11.2.10. `{: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).
 
@@ -343,18 +361,6 @@ method TestUnverified() {
 
 `{: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._
-
-Ordinarily, the body of a function is transparent to its users, but
-sometimes it is useful to hide it. If a function `foo` or `bar` is given the
-`{:opaque}` attribute, then Dafny hides the body of the function,
-so that it can only be seen within its recursive clique (if any),
-or if the programmer specifically asks to see it via the statement `reveal foo(), bar();`.
-
-More information about the Boogie implementation of `{:opaque}` is [here](https://github.com/dafny-lang/dafny/blob/master/docs/Compilation/Boogie.md).
-
 ### 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
@@ -487,16 +493,20 @@ 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.19. `{:verify false}` {#sec-verify}
+### 11.2.19. `{:transparent}` {#sec-transparent}
+
+By default, the body of a function is transparent to its users. This can be overridden using the `--default-function-opacity` command line flag. If default function opacity is set to `opaque` or `autoRevealDependencies`, then this attribute can be used on functions to make them always non-opaque.
+
+### 11.2.20. `{: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.
+not even trying to verify the [well-formedness](#sec-assertion-batches) 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.
 
 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}
+### 11.2.21. `{: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
@@ -505,7 +515,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.21. `{:vcs_max_keep_going_splits N}` {#sec-vcs_max_keep_going_splits}
+### 11.2.22. `{: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,
@@ -516,22 +526,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.22. `{:vcs_max_splits N}` {#sec-vcs_max_splits}
+### 11.2.23. `{: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.23. `{:vcs_split_on_every_assert}` {#sec-vcs_split_on_every_assert}
+### 11.2.24. `{: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.24. `{:synthesize}` {#sec-synthesize-attr}
+### 11.2.25. `{: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, 
@@ -565,7 +575,7 @@ BOUNDVARS = ID : ID
           | BOUNDVARS, BOUNDVARS
 ```
 
-### 11.2.25. `{:options OPT0, OPT1, ... }` {#sec-attr-options}
+### 11.2.26. `{: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,
@@ -809,6 +819,9 @@ Removed:
 - :dllimport
 - :handle
 
+Deprecated:
+- :opaque : This attribute has been promoted to a first-class modifier for functions. Find more information [here](#sec-opaque).
+
 ## 11.7. Other undocumented verification attributes
 
 A scan of Dafny's sources shows it checks for the

latest/DafnyRef/CommandLineOptions.md

@@ -1,3 +1,3 @@
 # 16. Full list of legacy command-line options {#sec-full-command-line-options} <!-- PDFOMIT -->
-For the on-line version only, the output of `dafny -?` follows. Note that with the advent of [dafny commands](#sec-dafny-commands), many options are only applicable to some (if any) commandsi, some are renamed, and some are obsolete and will eventually be removed. <!--PDFOMIT-->
+For the on-line version only, the output of `dafny -?` follows. Note that with the advent of [dafny commands](#sec-dafny-commands), many options are only applicable to some (if any) commands, some are renamed, and some are obsolete and will eventually be removed. <!--PDFOMIT-->
 {% include_relative Options.txt %} <!-- PDFOMIT -->

latest/DafnyRef/Expressions.md

@@ -459,7 +459,7 @@ The _specification_ is a list of clauses `requires E` or
 expression.
 
 _body_ is an expression that defines the function's return
-value.  The body must be well-formed for all possible values of the
+value.  The body must be [well-formed](#sec-assertion-batches) for all possible values of the
 parameters that satisfy the precondition (just like the bodies of
 named functions and methods).  In some cases, this means it is
 necessary to write explicit `requires` and `reads` clauses.  For
@@ -468,7 +468,7 @@ example, the lambda expression
 ```dafny
 x requires x != 0 => 100 / x
 ```
-would not be well-formed if the `requires` clause were omitted,
+would not be [well-formed](#sec-assertion-batches) if the `requires` clause were omitted,
 because of the possibility of division-by-zero.
 
 In settings where functions cannot be partial and there are no
@@ -1374,7 +1374,7 @@ where the bound variable is of a reference type. In non-ghost contexts,
 it is not allowed, because--even though the resulting set would be
 finite--it is not pleasant or practical to compute at run time.
 
-[^set-of-objects-not-in-functions]: In order to be deterministic, the result of a function should only depend on the arguments and of the objects  it [reads](#sec-reads-clause), and Dafny does not provide a way to explicitly pass the entire heap as the argument to a function. See [this post](https://github.com/dafny-lang/dafny/issues/1366#issuecomment-906785889) for more insights.
+[^set-of-objects-not-in-functions]: In order to be deterministic, the result of a function should only depend on the arguments and of the objects  it [reads](#sec-reads-clause), and Dafny does not provide a way to explicitly pass the entire heap as the argument to a function. See [this post](https://github.com/dafny-lang/dafny/issues/1366) for more insights.
 
 The universe in which set comprehensions are evaluated is the set of all
 _allocated_ objects, of the appropriate type and satisfying the given predicate.