Home

Download

Tutorial

Pi Programs
πVC Tutorial
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 shorthand. 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])).
Home

Download

Tutorial

Pi Programs
© 2007, Aaron Bradley and Zohar Manna
Direct questions, comments, and cool Pi programs to arbrad{Shift+2}cs.stanford.edu.