Differences from the book

• Assignment is written v = e; rather than v := e;.
• Equality is written e == f rather than e = f.
• Boolean connectives are written && (and), || (or), ! (not), -> (implies), <-> (iff). Precedence is the same as defined in Chapter 1; use parentheses when you are unsure.
• The length of an array is written length(a) rather than |a|.
• All variables of a function must be declared in a declare section that sits between the function prototype and the function body. See BubbleSort.pi.
• Formal arguments can be modified, unlike in the book. However, every formal argument a has associated with it an implicit variable a_0 that stores a's value upon function entry. This variable can be used in annotations.
• Most programs begin with the declaration #include "arrays.pi", which declares the existence of certain predicates about arrays. Always remember to include this line in programs whose specifications say something interesting about arrays. Again, see BubbleSort.pi.
• Restricted quantification over array indices (as defined in Chapter 12) is written as follows:
  • forall(ix, l, u, F[ix]), which is true iff F[ix] is true for every index ix ranging in [l, u] (remember that l and u are numeric expressions, often not constants). Quantifying without (symbolic) bounds is not useful when reasoning about bounded arrays.
  • exists(ix, l, u, F[ix])
  Quantified variables are declared by the global declaration define int ix = ?. See SortedUnion.pi.
• Array predicates correspond to those of Chapters 5, 6, and 11:
  • eq(a, b, l, u), which is true iff (if and only if) arrays a and b are equal in range [l, u], where l and u are any numerical expressions not involving function calls.
  • sorted(a, l, u), which is true iff array a is sorted in range [l, u].
  • partitioned(a, l1, u1, l2, u2), which is true iff array a is such that elements in range [l1, u1] have values at most the minimum value of the elements in the range [l2, u2].
  These predicates are short-hand. For example, write eq(a, b, l, u) as forall(ix, l, u, a[ix] == b[ix]); and write sorted(a, l, u) as forall(ix, l, u, forall(jx, ix, u, a[ix] <= a[jx])).