Update termination.md (#21)

- Removed imports of well-founded orders
- Added naming convention for domains for custom well-founded orders
- Added example showing that ADTs can be used as termination measures

Author: marcoeilers

src/termination-custom-orders.md

@@ -41,6 +41,8 @@ v1 <_ v2 <==> decreasing(v1, v2) && bounded(v2)
 The necessary properties of `decreasing` and `bounded` for values of type `T` can be defined via axioms. For the `MyInt` type from before, suitable axioms would be:
 
 ```viper
+import <decreases/declaration.vpr>
+
 domain MyIntWellFoundedOrder {
   axiom {
     forall i1: MyInt, i2: MyInt :: {decreasing(i1, i2)}
@@ -55,7 +57,8 @@ domain MyIntWellFoundedOrder {
 
 > **Note**
 >
-> The functions `decreasing` and `bounded` must be declared by the Viper program to verify, which is easiest done by importing `decreases/declaration.vpr`. This is also what the predefined orders, e.g., `decreases/int.vpr`, do.
+> The functions `decreasing` and `bounded` must be declared by the Viper program to verify, which is easiest done by importing `decreases/declaration.vpr`, as shown in the example. This is also what the predefined orders do.
+> Viper uses a naming convention where the well-founded order for type `T` should be defined in a domain called `TWellFoundedOrder`; giving it a different name will result in a warning.
 
 > **Exercise**
 > * Change the `factorial` function in the program above such that parameter `m` is used as its termination measure. The termination check should then fail because no well-founded order for `MyInt` has been defined.

src/termination-measures.md

@@ -61,8 +61,22 @@ function length(this: Ref): Int
 >
 > Change the body of `length` to just the recursive call `length(this)`. Which error message do you expect?
 
+Additionally, Viper's ADT plugin automatically generated well-founded orders for any ADT defined in the program. Thus, ADT values can also be used as termination measures:
+
+```silver-runnable
+adt List[T] {
+    Nil() 
+    Cons(hd: T, tl: List[T])
+}
+
+function llen(l: List[Int]): Int
+    decreases l
+{
+    l.isNil ? 0 : 1 + llen(l.tl)
+}
+```
+
 Final remarks:
 
 * Note that `PredicateInstance` is an internal Viper type, and currently supported only in decreases tuples. The `nested` function is also internal and cannot be used by users.
-* For simplicity, all standard well-founded orders can be imported via `decreases/all.vpr`.
 * Users can also define [custom well-founded orders](./termination-custom-orders.md).

src/termination-mutual-recursion.md

@@ -42,5 +42,4 @@ function fun2(x: Int): Int
 At indirectly recursive calls, two decreases tuples are compared by lexicographical order of their longest commonly typed prefix (as does, e.g., Dafny). E.g., for the indirectly recursive call `fun2(y-1)` in function `fun1`, Viper verifies that `y-1 <_ y`, while for the recursive call `fun1(y, false)`, it verifies that `y <_ y || (y == y && false <_ b)`.
 
 > **Exercise**
-> * Comment the import of `bool.vpr`, and reverify the program. Can you explain the resulting verification error?
 > * In the above example, change the call `fun1(x-1, true)` to `fun1(x, true)` -- the program still verifies. That's because Viper appends a `Top` element (an internal value of any type, larger than any other value) to each tuple, a neat trick also implemented by, e.g., Dafny and F*. Can you explain how this helps with checking termination of the call `fun1(x, true)`?

src/termination-syntax.md

@@ -32,5 +32,3 @@ For the first recursive call `ack(m - 1, 1)`, and the second (outer) recursive c
 > **Exercise**
 >
 > Swap the tuple elements, i.e., change the decreases clause to `n, m`. For which of the recursive calls do you expect error messages?
-
-The well-founded order over tuples need not be imported (and cannot be customised). However, the well-founded orders of the types appearing in the tuple must be.