Rise4Fun tutorial is out of date about nullable arrays

[abeln]

In the Arrays section of the tutorial (https://rise4fun.com/Dafny/tutorial/Guide), the first code sample with the Find method reads:

method Find(a: array<int>, key: int) returns (index: int)
   requires a != null
   ensures 0 <= index ==> index < a.Length && a[index] == key
{
   // Can you write code that satisfies the postcondition?
   // Hint: you can do it with one statement.
}

Dafny complains that array<int> is non-nullable. The error message suggests replacing it with array?<int> instead, which works.

The rest of the code samples in that section also need to be updated in the same way.

[RustanLeino]

Even better, leave the type as it is and delete the requires clause. Thanks for pointing this out.

[fabiomadge]

We didn't catch all of them: https://github.com/dafny-lang/dafny/blob/master/docs/OnlineTutorial/guide.md#arrays

[davidcok]

Rise4Fun is obsolete, but I did add a clarifying sentence about null arrays to the online tutorial