snapshot v4 4 0 (#36)

- Removing old latest
- Documentation snapshot for v4.4.0

Snapshots.md

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

latest/DafnyRef/Expressions.md

@@ -900,7 +900,6 @@ Examples:
 ```dafny
 allocated(c)
 allocated({c1,c2})
-allocated@L(c)
 ```
 
 For any expression `e`, the expression `allocated(e)` evaluates to `true`

latest/DafnyRef/Features.md

@@ -37,11 +37,15 @@
 | [Externally-implemented constructors](#sec-extern-decls) |  X  |  |  |  X  |  X  |  X  |  X  |
 | [Auto-initialization of tuple variables](#sec-tuple-types) |  X  |  X  |  X  |  X  |  X  |  X  |  X  |
 | [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  |
+| [Tuples with more than 20 arguments](##sec-compilation-built-ins) |  |  X  |  X  |  |  X  |  X  |  X  |
+| [Arrays with more than 16 dimensions](##sec-compilation-built-ins) |  |  X  |  X  |  |  X  |  X  |  X  |
+| [Arrow types with more than 16 arguments](##sec-compilation-built-ins) |  |  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  |  |
 | [Separate compilation](#sec-compilation) |  X  |  |  X  |  X  |  X  |  X  |  X  |
+| [All built-in types in runtime library](#sec-compilation-built-ins) |  X  |  X  |  X  |  X  |  X  |  |  X  |
+| [Execution coverage report](#sec-dafny-test) |  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

latest/DafnyRef/Grammar.md

@@ -515,7 +515,7 @@ For example, in the quantifier domain `i | 0 <= i < |s|, y <- s[i] | i < y`, the
 because the range attached to `i` ensures `i` is a valid index in the sequence `s`.
 
 Allowing per-variable ranges is not fully backwards compatible, and so it is not yet allowed by default;
-the `--quantifier-syntax:4` option needs to be provided to enable this feature (See [Section 13.8.5](#sec-controlling-language)).
+the `--quantifier-syntax:4` option needs to be provided to enable this feature (See [Section 13.9.5](#sec-controlling-language)).
 
 ### 2.7.5. Numeric Literals ([grammar](#g-literal-expression)) {#sec-numeric-literals}
 

latest/DafnyRef/GrammarDetails.md

@@ -782,8 +782,7 @@ InvariantClause_ =
 
 ````grammar
 ReadsClause(allowLemma, allowLambda, allowWild) =
-  "reads"
-  { Attribute }
+  "reads" { Attribute }
   PossiblyWildFrameExpression(allowLemma, allowLambda, allowWild)
   { "," PossiblyWildFrameExpression(allowLemma, allowLambda, allowWild) }
 ````

latest/DafnyRef/Options.txt

@@ -106,13 +106,24 @@ Usage: dafny [ option ... ] [ filename ... ]
       `opaque` means functions are always opaque so the opaque keyword is not needed, and functions must be revealed everywhere needed for a proof.
 
   /generalTraits:<value>
-      0 (default) - Every trait implicitly extends 'object', and thus is a reference type. Only traits and classes can extend traits.
-      1 - A trait is a reference type iff it or one of its ancestor traits is 'object'. Any type with members can extend traits.
+      legacy (default) - Every trait implicitly extends 'object', and thus is a reference type. Only traits and reference types can extend traits.
+      datatype - A trait is a reference type only if it or one of its ancestor traits is 'object'. Any non-'newtype' type with members can extend traits.
+      full - (don't use; not yet completely supported) A trait is a reference type only if it or one of its ancestor traits is 'object'. Any type with members can extend traits.
 
   /ntitrace:<value>
       0 (default) - Don't print debug information for the new type system.
       1 - Print debug information for the new type system.
 
+  /readsClausesOnMethods:<value>
+      0 (default) - Reads clauses on methods are forbidden.
+      1 - Reads clauses on methods are permitted (with a default of 'reads *').
+
+  /standardLibraries:<value>
+      0 (default) - Do not allow Dafny code to depend on the standard libraries included with the Dafny distribution.
+      1 - Allow Dafny code to depend on the standard libraries included with the Dafny distribution.
+      See https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/README.md for more information.
+      Not compatible with the /unicodeChar:0 option.
+
   /titrace:<value>
       0 (default) - Don't print type-inference debug information.
       1 - Print type-inference debug information.
@@ -485,6 +496,7 @@ Usage: dafny [ option ... ] [ filename ... ]
   /printWithUniqueIds : print augmented information that uniquely
                    identifies variables
   /printUnstructured : with /print option, desugars all structured statements
+  /printPassive :  with /print option, prints passive version of program
   /printDesugared : with /print option, desugars calls
   /printLambdaLifting : with /print option, desugars lambda lifting
 
@@ -501,6 +513,8 @@ Usage: dafny [ option ... ] [ filename ... ]
                 unroll loops, following up to n back edges (and then some)
   /soundLoopUnrolling
                 sound loop unrolling
+  /doModSetAnalysis
+                automatically infer modifies clauses
   /printModel:<n>
                 0 (default) - do not print Z3's error model
                 1 - print Z3's error model
@@ -642,8 +656,6 @@ Usage: dafny [ option ... ] [ filename ... ]
   /smokeTimeout:<n>
                 Timeout, in seconds, for a single theorem prover
                 invocation during smoke test, defaults to 10.
-  /causalImplies
-                Translate Boogie's A ==> B into prover's A ==> A && B.
   /typeEncoding:<t>
                 Encoding of types when generating VC of a polymorphic program:
                    m = monomorphic (default)
@@ -663,6 +675,10 @@ Usage: dafny [ option ... ] [ filename ... ]
                 Without pruning, due to the unstable nature of SMT solvers,
                 a change to any part of a Boogie program has the potential 
                 to affect the verification of any other part of the program.
+
+                Only use this if your program contains uses clauses
+                where required, otherwise pruning will break your program.
+                More information can be found here: https://github.com/boogie-org/boogie/blob/afe8eb0ffbb48d593de1ae3bf89712246444daa8/Source/ExecutionEngine/CommandLineOptions.cs#L160
   /printPruned:<file>
                 After pruning, print the Boogie program to the specified file.
   /relaxFocus   Process foci in a bottom-up fashion. This way only generates
@@ -684,6 +700,13 @@ Usage: dafny [ option ... ] [ filename ... ]
                 This option is implemented by renaming variables and reordering
                 declarations in the input, and by setting solver options that have
                 similar effects.
+  /trackVerificationCoverage
+                Track and report which program elements labeled with an
+                `{:id ...}` attribute were necessary to complete verification.
+                Assumptions, assertions, requires clauses, ensures clauses,
+                assignments, and calls can be labeled for inclusion in this
+                report. This generalizes and replaces the previous
+                (undocumented) `/printNecessaryAssertions` option.
 
   ---- Verification-condition splitting --------------------------------------
 
@@ -752,7 +775,7 @@ Usage: dafny [ option ... ] [ filename ... ]
                 Limit the number of seconds spent trying to verify
                 each procedure
   /rlimit:<num>
-                Limit the Z3 resource spent trying to verify each procedure
+                Limit the Z3 resource spent trying to verify each procedure.
   /errorTrace:<n>
                 0 - no Trace labels in the error output,
                 1 (default) - include useful Trace labels in error output,

latest/DafnyRef/Specifications.md

@@ -58,7 +58,7 @@ of all the given Attributes. The order of conjunctions
 can be important: earlier conjuncts can set conditions that
 establish that later conjuncts are well-defined.
 
-The attributes recognized for requires clauses are discussed in [Section 11.3](#sec-verification-attributes-on-assertions).
+The attributes recognized for requires clauses are discussed in [Section 11.4](#sec-verification-attributes-on-assertions).
 
 A requires clause can have [custom error and success messages](#sec-error-attribute).
 
@@ -86,7 +86,7 @@ The order of conjunctions
 can be important: earlier conjuncts can set conditions that
 establish that later conjuncts are well-defined.
 
-The attributes recognized for ensures clauses are discussed in [Section 11.3](#sec-verification-attributes-on-assertions).
+The attributes recognized for ensures clauses are discussed in [Section 11.4](#sec-verification-attributes-on-assertions).
 
 An ensures clause can have [custom error and success messages](#sec-error-attribute).
 
@@ -464,6 +464,12 @@ function g()
   reads o, oo
 function h()
   reads { o }
+method f()
+  reads *
+method g()
+  reads o, oo
+method h()
+  reads { o }
 ```
 
 Functions are not allowed to have side effects; they may also be restricted in
@@ -479,19 +485,32 @@ able to give invariants to preserve it in this case, it gets even more
 complex when manipulating data structures. In this case, framing is
 essential to making the verification process feasible.
 
-It is not just the body of a function that is subject to `reads`
+By default, methods are not required to list the memory location they read.
+However, there are use cases for restricting what methods can read as well.
+In particular, if you want to verify that imperative code is safe to execute concurrently when compiled,
+you can specify that a method does not read or write any shared state,
+and therefore cannot encounter race conditions or runtime crashes related to
+unsafe communication between concurrent executions.
+See [the `{:concurrent}` attribute](#sec-concurrent-attribute) for more details.
+
+It is not just the body of a function or method that is subject to `reads`
 checks, but also its precondition and the `reads` clause itself.
 
 A `reads` clause can list a wildcard `*`, which allows the enclosing
-function to read anything. In many cases, and in particular in all cases
+function or method to read anything. 
+This is the implicit default for methods with no `reads` clauses,
+allowing methods to read whatever they like.
+The default for functions, however, is to not allow reading any memory.
+Allowing functions to read arbitrary memory is more problematic:
+in many cases, and in particular in all cases
 where the function is defined recursively, this makes it next to
 impossible to make any use of the function. Nevertheless, as an
 experimental feature, the language allows it (and it is sound).
 If a `reads` clause uses `*`, then the `reads` clause is not allowed to
 mention anything else (since anything else would be irrelevant, anyhow).
 
 A `reads` clause specifies the set of memory locations that a function,
-lambda, or iterator may read. The readable memory locations are all the fields
+lambda, or method may read. The readable memory locations are all the fields
 of all of the references given in the set specified in the frame expression
 and the single fields given in [`FrameField`](#sec-frame-expression) elements of the frame expression.
 For example, in
@@ -546,7 +565,7 @@ another function. For example, function `Sum` adds up the values of
 ```dafny
 function Sum(f: int ~> real, lo: int, hi: int): real
   requires lo <= hi
-  requires forall i :: lo <= i < hi ==> f.requires(i)
+  requires forall i :: f.requires(i)
   reads f.reads
   decreases hi - lo
 {
@@ -562,9 +581,29 @@ read. More precise would be to specify that `Sum` reads only what `f`
 reads on the values from `lo` to `hi`, but the larger set denoted by
 `reads f.reads` is easier to write down and is often good enough.)
 
+Without such `reads` function, one could also write the more precise
+and more verbose:
+<!-- %check-verify -->
+```dafny
+function Sum(f: int ~> real, lo: int, hi: int): real
+  requires lo <= hi
+  requires forall i :: lo <= i < hi ==> f.requires(i)
+  reads set i, o | lo <= i < hi && o in f.reads(i) :: o
+  decreases hi - lo
+{
+  if lo == hi then 0.0 else
+    f(lo) + Sum(f, lo + 1, hi)
+}
+```
+
 Note, only `reads` clauses, not `modifies` clauses, are allowed to
 include functions as just described.
 
+Iterator specifications also allow `reads` clauses,
+with the same syntax and interpretation of arguments as above,
+but the meaning is quite different!
+See [Section 5.11](#sec-iterator-types) for more details.
+
 ### 7.1.6. Modifies Clause ([grammar](#g-modifies-clause)) {#sec-modifies-clause}
 
 Examples:
@@ -581,12 +620,11 @@ method Q()
   modifies o, p`f
 ```
 
-Frames also affect methods. Methods are not
-required to list the things they read. Methods are allowed to read
+By default, methods are allowed to read
 whatever memory they like, but they are required to list which parts of
 memory they modify, with a `modifies` annotation. These are almost identical
 to their `reads` cousins, except they say what can be changed, rather than
-what the value of the function depends on. In combination with reads,
+what the definition depends on. In combination with reads,
 modification restrictions allow Dafny to prove properties of code that
 would otherwise be very difficult or impossible. Reads and modifies are
 one of the tools that allow Dafny to work on one method at a time,
@@ -684,10 +722,12 @@ class C {
 }
 ```
 
-A method specification consists of zero or more `modifies`, `requires`,
+A method specification consists of zero or more `reads`, `modifies`, `requires`,
 `ensures` or `decreases` clauses, in any order.
-A method does not have `reads` clauses because methods are allowed to
-read any memory.
+A method does not need `reads` clauses in most cases,
+because methods are allowed to read any memory by default,
+but `reads` clauses are supported for use cases such as verifying safe concurrent execution.
+See [the `{:concurrent}` attribute](#sec-concurrent-attribute) for more details.
 
 ## 7.3. Function Specification ([grammar](#g-function-specification)) {#sec-function-specification}
 
@@ -735,7 +775,7 @@ and `yield ensures` clauses.
 An iterator specification applies both to the iterator's constructor
 method and to its `MoveNext` method.
 - The `reads` and `modifies`
-clauses apply to both of them. 
+clauses apply to both of them (but `reads` clauses have a [different meaning on iterators](#sec-iterator-types) than on functions or methods).
 - The `requires` and `ensures` clauses apply to the constructor.
 - The `yield requires` and `yield ensures` clauses apply to the `MoveNext` method.
 
@@ -746,6 +786,8 @@ Examples of iterators, including iterator specifications, are given in
 - a decreases clause is used to show that the iterator will eventually terminate
 - a yield requires clause is a precondition for calling `MoveNext`
 - a yield ensures clause is a postcondition for calling `MoveNext`
+- a reads clause gives a set of memory locations that will be unchanged after a `yield` statement
+- a modifies clause gives a set of memory locations the iterator may write to
 
 ## 7.6. Loop Specification ([grammar](#g-loop-specification)) {#sec-loop-specification}
 

latest/DafnyRef/Statements.md

@@ -1854,7 +1854,7 @@ Examples of this form of assert are given in the section of the [`reveal`](#sec-
 
 An assert statement may have a label, whose use is explained in [Section 8.20.1](#sec-reveal-assertions).
 
-The attributes recognized for assert statements are discussed in [Section 11.3](#sec-verification-attributes-on-assertions).
+The attributes recognized for assert statements are discussed in [Section 11.4](#sec-verification-attributes-on-assertions).
 
 Using `...` as the argument of the statement is deprecated.