Dafny 2.1.0

Dafny version 2.1.0 mainly introduces non-null types, more precise type inference in the presence of subset types, full checks that functions do not depend on the allocation state, and an expanded selection of variance annotations. Some of these changes are not backwards compatible, but the changes required to bring older programs up to version 2.1.0 are usually not large.

Another change is that Visual Studio support has been moved to VS 2017, .NET version 4.5. Building under Mono still works, but only without using Code Contracts (which don't seem to be available on Mono).

In more detail, the changes over version 2.0.0 are as follows:

Language

• Non-null types.

  A declaration of a class or trait C gives rise to two types, C? and C.

  Type C? is the possibly null reference type for C objects. Previously in Dafny, this was the only type the class or trait gave rise to and it then had the different name C.

  Type C is a non-null version of C?. It is a defined as the subset type:

  type C = c: C? | c != null
  

  Note that the ? is part of the name of the class C?. It is not a suffix operator, so there cannot be any space between the C and the ?. Also, if a class C has type parameters, then these are mentioned after the type names C? and C, for example, C?<int> and C<int>.

  In some places in the program text, a class or trait name is expected. In particular, a trait name is expected after the extends keyword in a class declaration and a class name is expected in a new allocation. Note that these names, because they are class and trait names, not type names, do not end with a ?.

• Dafny has a built-in trait object and any number of built-in array classes (array, array2, array3, ...). Each of these also gives rise to two types, as in object? and object, array? and array, array2? and array2, etc.

• If the literal null is compared with an expression of a non-null type, Dafny will emit a warning that the result of the test can be determined at compile time. For example, if p has a non-null type and S is a set whose element type is a non-null type, then both p != null and null in S will generate said warning.

• The subset types declared in a program form a hierarchy (that is, a tree), where the parent of a subset type is its given base type. This hierarchy is part of the subtype relation in Dafny. For example, nat is a subtype of int, and for any class or trait C, C is a subtype of C?. In addition, for every class or trait C that extends a trait Tr, type C? is a subtype of Tr? and type C is a subtype of Tr.

  As a consequence of these rules, note that the subtype relation is not just a hierarhcy.

  Suppose X is a subset type whose base type is C. It then follows that X is a subtype of C, which in turn is a subtype of C?. However, the declaration of X only gives rise to one type. In particular, it does not also give rise to a type X?. In other words, any user-defined subset type of C? or C is only a subtype of it.

• Type inference is now more precise. Whereas before it would not infer subset types like nat or --> (but instead their base type, int and ~>), now it will try to infer such types. In some cases, this will not make a noticeable, but there are two cases where the difference may be important.

  One case is that type arguments more easily will be inferred as subset types. For example, suppose the usual datatype List has a co-variant type parameter and suppose xs is a variable declared to have type List<nat>. Expression Cons(55, xs) may now be inferred to have type List<nat> as well. This is beneficial for verification, because in an assignment like xs := Cons(55, xs);, the verifier only needs to check that 55 satisfies the constraint of nat. Previously, it was more likely that Cons(55, xs) would be inferred to have type List<int>, in which case the assignment xs := Cons(55, xs); put the burden on the verifier to check that Cons(55, xs) produces a value that actually satisfies List<nat>.

  The other case where the more precise type inference can make a noticeable difference is in comprehensions like quantifications and set comprehensions. Suppose P is a predicate declared to take a parameter of type nat and consider an expression forall x :: P(x) ==> 0 <= x. If x has type nat, then this quantifier is a tautology. If x has type int, then the expression is not well-formed, because the subexpression P(x) would not satisfy the type conditions of P. For this example, Dafny will infer the type of x to be nat.

  As another example, of a quantifier, suppose P and Q are both predicates that take a nat argument. Then, Dafny will infer x to have type nat in forall x :: 0 <= x && P(x) ==> Q(x) as well. So, in this example, since x is inferred to be of type nat, the antecedent 0 <= x is redundant and can be omitted.

  As a third example, suppose neg is a subset type of int that stands for the negative integers, P is a predicate that takes an argument of type nat, and Q is a predicate that takes an argument of type neg. Consider the following expression:

  forall x :: (0 <= x ==> P(x)) && (0 < x ==> Q(x))
  

  For this expression, Dafny will infer that x has type int. In an alternative design, inference might have resulted in the type nat or neg, each of which would render one of the conjuncts trivially satisfied, or resulted in error message like "overconstrained type".

• Allow more RHSs of const declarations.

• The possible variance indicators on type parameters has been expanded. The possibilities are:

  • + (co-variance, strict)
    Enclosing type is monotonic in the type parameter.
    The parameter is not used in expanding positions (that is, it is not used left of any arrow).

  • * (co-variance, relaxed)
    Enclosing type is monotonic in the type parameter.
    Other than that, use of the parameter is unrestricted (in particular, it may be used to the left of an arrow).

  • (default variance, denoted by not giving any of the other variance indicators explicitly) (non-variance, strict)
    Different given parameters produce non-comparable types.
    The parameter is not used in expanding positions (that is, it is not used left of any arrow).

  • ! (non-variance, relaxed)
    Different given parameters produce non-comparable types.
    Other than that, use of the parameter is unrestricted (in particular, it may be used to the left of an arrow).

  • - (contra-variance)
    Enclosing type is anti-monotonic in the type parameter.
    Consequentially, every use of the parameter is to the left of some arrow.

• Strict positivity is used to forbid type definitions where differences in cardinalities would give rise to a logical contradiction.

• Added type-parameter characteristic (!new), which says that the type does not include any references, and thus does not depend on the allocation state. It can be used to restrict type parameters so that functions can use the type in unbounded quantifications.

• Opaque types at the very topmost scope are always implicitly (!new).

Verification

• Support for customizable error messages (useful for tools built on top of Dafny).

• Removed the notoriously bad seq axiom. (More precisely, rewrote it to have a good trigger.)

• Some performance improvements.

• Improved and expanded on the syntactic bounds discovery in comprehensions.

IDE

• Visual Studio mode is for VS 2017

Compiler

• Some bug fixes, for example to work around some questionable designs around the use of null in the .NET collection libraries.

Command-line options

• Command-line option /titrace spills out debug trace information from the type inference process. Previously, this debug trace information was hidden under an #if, but now it can be turned on without having to recompile Dafny.

• Added /noExterns flag, which ignores :extern attributes.

• Started implementing a /allocated:4 mode.

Miscellaneous

• Include Code Contracts for VS 2017. This requires Code Contracts to have been installed (for some version of Visual Studio, like VS 2015) on the machine.

• Various bug fixes.