\[ \{v = V \wedge v.size = N\} \] \[ b := min(v) \] \[ \{b = ((\exists i | 0 \le i \lt N : (\forall j | 0 \le j \lt N : v[i] \le v[j])) \wedge v = V)\} \]
\[ \{v = V \wedge v.size = N\} \] \[ b := rotateRight(v) \] \[ \{b = (v[0] = V[N-1] \wedge (\forall | 1 \le i \lt N: V[i] = v[i-1]))\} \]
\[ \{v = V \wedge v.size = N\} \] \[ b := largestLast(v) \] \[ \{b = (\exists i | 0 \le i \lt N - 1: (\forall j | 0 \le j \lt N: v[i] \le v[j]) \wedge v = V)\} \]