Missing explanations of statements and declarations

src/language-top.md

@@ -9,6 +9,7 @@ field next: Ref
 
 * Declared by keyword `field`
 * Every object has all fields (there are no classes in Viper)
+* Several fields may be declared at once, e.g., `field val: Int, next: Ref`
 * See the [section on permissions](./permissions.md) for examples
 
 ## Methods
@@ -28,6 +29,7 @@ method QSort(xs: Seq[Ref]) returns (ys: Seq[Ref])
   * Hence calls _cannot_ be used in specifications
 * Modular verification of methods and method calls
   * The body may include some number of _statements_ (including recursive calls)
+  * The body is optional: a method without a body is _abstract_. Since verification is modular, calls to abstract methods are verified against their specification as usual; abstract methods are useful, e.g., to model the behaviour of library code
   * The body is invisible at call site (changing the body does not affect client code)
   * The precondition is checked before the method call (more precisely, it is [_exhaled_](./permissions-inhale-exhale.md))
   * The postcondition is assumed after the method call (more precisely, it is [_inhaled_](./permissions-inhale-exhale.md))
@@ -91,6 +93,21 @@ domain Pair[A, B] {
 * Useful for specifying custom mathematical theories
 * See the [section on domains](./domains.md) for details
 
+## Algebraic data types {#intro-adts}
+
+```viper
+adt List[T] {
+  Nil()
+  Cons(value: T, tail: List[T])
+}
+```
+
+* Declared by keyword `adt` (provided by a plugin that is enabled by default)
+* Have a name, which is introduced as an additional _type_ in the Viper program, and may have type parameters (e.g. `T` above)
+* The body declares the _constructors_ of the datatype (e.g. `Nil` and `Cons` above)
+* Viper automatically generates _destructors_ (e.g. `xs.value`, `xs.tail`) and _discriminators_ (e.g. `xs.isNil`, `xs.isCons`)
+* See the [section on the ADT plugin](./domains-adt.md) for details
+
 ## Macros
 
 ```viper

src/statements-assignments.md

@@ -21,3 +21,9 @@ to all (possibly none) fields listed comma-separated within the parentheses. As
 *all* fields declared in the Viper program. Note that neither method calls nor
 object creation are expressions. Hence, they must not occur as receivers, method
 arguments, etc.; instead of nesting these constructs, one typically assigns their results first to local variables, and then uses these.
+
+Viper additionally supports some more flexible forms of declarations and assignments:
+
+* Local variable declarations may declare several variables at once, e.g., `var a: Ref, b: Ref, c: Int`.
+* Local variable declarations may include an initial assignment, e.g., `var x: Int := 5`; the right-hand side may also be a method call or object creation, e.g., `var y: Ref := new(*)`.
+* Heap locations and newly-declared local variables may occur on the left-hand sides of method calls and object creations, e.g., `x.f := new(...)` and `a, x.f := m(...)`.

src/statements-control.md

@@ -87,3 +87,57 @@ follows:
 3. Exhale the loop invariant.
 
 Analogous to functions, Viper does also *not* check loop (or method) termination per default, see the [chapter on termination](./termination.md) for more details. Alternatively, custom termination checks can be encoded through suitable assertions (see the *labelled old expressions* described in the [section on expressions](./expressions-multi.md)).
+
+## Labels and gotos
+
+In addition to the structured control flow constructs shown above, Viper supports labels and unconditional jumps:
+
+```viper
+label l
+goto l
+```
+
+A `label` statement declares a program point with the given name. Labels serve two purposes: they can be the target of `goto` statements, and they can be referred to in [labelled old expressions](./expressions-multi.md) `old[l](e)`. A `goto` statement transfers control to the given label. Since Viper is primarily an intermediate language, gotos are mainly intended for encoding the unstructured control flow of front-end languages (for example, `break` and `continue` statements, or early returns); Viper programs must not use gotos to create *irreducible* control flow (e.g., jumps from outside a loop into the middle of the loop body).
+
+A `goto` that jumps out of a `while` loop exits the loop *without* checking the loop invariant; permissions held before the loop that were not transferred into it via the invariant become available again after the jump. Loops can also be created by jumping *backwards* to a label. To support invariants for such loops, `label` declarations may be directly followed by `invariant` clauses; a label's stated invariant is used only if the label is in fact a loop head. Both features are illustrated in the following example:
+
+```viper,editable,playground
+method firstPositive(xs: Seq[Int]) returns (idx: Int)
+  ensures idx >= 0 ==> idx < |xs| && xs[idx] > 0
+{
+  idx := -1
+  var i: Int := 0
+  while (i < |xs|)
+    invariant 0 <= i && i <= |xs|
+    invariant idx == -1
+  {
+    if (xs[i] > 0) {
+      idx := i
+      // exits the loop; the invariant idx == -1 does not hold here,
+      // but invariants are not checked when jumping out of a loop
+      goto done
+    }
+    i := i + 1
+  }
+  label done
+}
+
+method countdown(n: Int)
+  requires 0 <= n
+{
+  var i: Int := n
+  // this label is the head of a loop created by the backward goto
+  // below, so its invariant is used to verify the loop
+  label head
+    invariant 0 <= i
+  if (i > 0) {
+    i := i - 1
+    goto head
+  }
+  assert i == 0
+}
+```
+
+> **Exercise**
+> * In `countdown`, remove the `invariant` clause on the label `head`. Which assertion fails, and why?
+> * In `firstPositive`, remove the `goto done` statement (so that the loop always runs to completion). The invariant `idx == -1` now fails to verify — why was it not checked before, when the `goto` statement was still present?