# Algorithms

Separate a program’s behavior from its specification. Exhaustive finite domains expose ordering, multiplicity, empty-input, and duplicate-value errors.

## Definitions

- **Input contract**: A precise set of admissible inputs, including sizes and value ranges.
- **Postcondition**: The relation between the original input and the returned output.
- **Oracle**: A separately implemented reference property used to accept or reject a candidate.

## Acceptance procedure

1. Enumerate every list in the declared alphabet and length bound.
2. Run the candidate insertion-sort implementation without modifying the source input.
3. Compare each result with the reference ordering, including repeated elements.
4. Reject immediately with an input witness if ordering or multiplicity differs.

## Complexity

For alphabet size k and maximum length n, this family checks Σ kⁱ inputs for i=0…n. Insertion sort performs O(n²) comparisons in its worst case.

## Common failure

Sortedness alone does not prove that an output preserves the input multiset.

## Extensions

Add stability certificates for tagged records or an unbounded inductive invariant.

## Instances

- KL-FCS-001: Insertion sort over a finite domain — Correct over the stated input domain: yes
- KL-FCS-012: Longer binary lists — Correct over the stated input domain: yes
- KL-FCS-013: Five-symbol sorting domain — Correct over the stated input domain: yes

## References

- https://ocw.mit.edu/courses/6-006-introduction-to-algorithms-fall-2011/