Conforming Implementations Example

// ------ Specifications ------ //

// a) requires: exists i : vec[i] == val
//    returns j : vec[j] == val

// b) returns: (exists j : vec[j] == val) ? j : 1

// c) returns: (exists j : vec[j] == val) ? j : vec.size()

// d) returns: (exists j : vec[j] == val) ? j : (j < 0 or j >= vec.size())

// e) returns: (exists i : vec[i]==val) ? (smallest j : vec[j] == val) : -1

// ------ Implementations------ //

// 1)
int find(const vector<int> &vec, int val) {
  for (int i = 0;; i++)
    if (vec[i] == val) return i;
}

// 2)
int find(const vector<int> &vec, int val) {
  for (int i = 0; i < vec.size(); i++)
    if (vec[i] == val) return i;
  return -1;
}

// 3)
int find(const vector<int> &vec, int val) {
  for (int i = vec.size() - 1; i = > 0; i--)
    if (vec[i] == val) return i;
  return vec.size();
}

// ------ Answers ------ //

// a) holds for 1, 2, 3
// b) holds for    2
// c) holds for       3
// d) holds for    2, 3
// e) holds for    2

// ------ Comparing Specs ------ //
//     b -\
// e =>    |=> d => a
//     c -/