Specify the problem before the procedure
An algorithm is a finite, precise procedure for transforming allowed inputs into an output satisfying a contract. Correctness depends on that contract: returning any match is different from returning the first match.
fun firstIndex(values: IntArray, target: Int): Int {
for (index in values.indices) {
if (values[index] == target) return index
}
return -1
}
The input can be empty and may contain duplicates. The loop visits indexes in increasing order, so the first returned match is the earliest one. If the loop finishes, every element has been checked and the sentinel -1 means no match.
An invariant explains correctness: before checking index i, no earlier position contains the target. Initialization establishes that claim for an empty prefix; each failed comparison extends it by one element. The bounded loop also proves termination.
Exercise
Trace the function on [7, 2, 7] with targets seven and three. Write tests for empty input, a match at either end, and duplicates. Change the contract to return every matching index.
Check: state input assumptions, output meaning, invariant, and termination argument before discussing speed.