Facundo Uferer
The Hoare Triple {P} C {Q}: The Mathematical Contract
If precondition P holds before block C runs, then postcondition Q holds unfailingly when it finishes. This is the formal contract between a specification and its implementation.
valores != null && length > 0 Awaiting test… maximoActual = maximo(valores) Idle ∀x ∈ valores: x ≤ maximoActual Awaiting test… Loop Invariants: The State That Never Breaks
An invariant is a logical statement that holds before the loop starts, after every iteration, and when it ends, guaranteeing the postcondition. In maximo(), it states: valores[0..i-1] has been scanned and maximoActual is its maximum.
Before starting: segment [0..-1] is empty, the invariant holds trivially.
Total Correctness and the Bound Function: V = n − i
Partial correctness guarantees that if the loop terminates, the answer is correct. Total correctness also requires it to terminate: a positive integer bound function that strictly decreases each iteration proves it.
V starts at n = 8. Each iteration reduces it by 1. While V stays positive, the loop may continue; it can never go negative.
The Interactive Big-O Notation Chart
Big-O describes how running time scales as the input size N grows toward infinity, ignoring constants and lower-order terms to focus on the dominant factor.
Best, Worst, and Average Case in a Linear Search
An algorithm does not have a single speed: linear search is O(1) in the best case if the value sits at the front, and O(N) in the worst case if it is absent. Unless stated otherwise, the worst case is usually reported.
Searching for value 12 in the array: