@pre 0 <= l && u < |a| @post rv <-> exists ix. (l <= ix && ix <= u && a[ix] = e) bool LinearSearch(int[] a, int l, int u, int e) { for @L: true (int i := l; i <= u; i := i + 1) { if (a[i] = e) return true; } return false; }