# Algorithm correctness: partial correctness, termination and total correctness of nondeterministic adjacent-swap sorting

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-algorithm-correctness/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-algorithm-correctness-01 · production-20261019-adopted-96



## Goal and scope

In a finite-state model M whose states are the six permutations of (1,2,3), with initial state (3,2,1), each step may nondeterministically swap any adjacent inverted pair, and Halt={(1,2,3)}. With the postcondition 'increasing, and a rearrangement of the input', prove partial correctness, termination and total correctness of M, using the ranking function inv (the number of inversions) to show every execution takes at most 3 steps and every maximal execution stops in Halt. Then use the variant M′ (any adjacent pair may be swapped) to show that one successful path and partial correctness do not give total correctness, and the variant M″ (a wrong halting condition) to show that termination does not give correctness.

Works inside the MKO's scope: the finite-state model of the preceding entry, with Halt states as execution endpoints (assumption a1); the model is nondeterministic and the obligations concern every possible execution (assumption a2). General Hoare-logic rules, fairness and the semantics of real programming languages are not treated, and the canonical MKO and its English edition are not changed.





## Givens and symbols


- order_basics
- nat_induction
- finite_counting_basics
- numeric_evaluation


- G1 — Model M=(S,Init,Step,Halt): S is the six permutations 123, 132, 213, 231, 312, 321 of (1,2,3); Init={321}; for s=(x1,x2,x3)∉Halt there is an edge s→(x2,x1,x3) if x1>x2 and an edge s→(x1,x3,x2) if x2>x3; Halt={123}, and halt states have no outgoing edges (MKO assumption a1).
- G2 — Postcondition Q(s): the three entries of s are increasing (x1<x2<x3) and are a rearrangement of the entries {1,2,3} of the input 321. Precondition: the initial state lies in Init.
- G3 — Variant M′: S, Init and Halt as in M, but for s∉Halt either adjacent pair may be swapped, inverted or not. Variant M″: S, Init and the swap rule as in M (only adjacent inverted pairs), but Halt″={s∈S ∣ x1<x2}, with edges out of Halt″ truncated.
- G4 — M is nondeterministic: every obligation concerns every possible execution from Init, and one successful path is not a proof (MKO assumption a2). Here termination quantifies over maximal executions (including infinite executions). A finite nonmaximal execution is an extendible prefix and need not already have reached Halt.


- s=(x_1,x_2,x_3) — a state: a permutation of 1, 2, 3, abbreviated x1x2x3, e.g. 321
- Q(s) — the postcondition: increasing and a rearrangement of the input
- \mathrm{inv}(s) — the inversion count [x1>x2]+[x1>x3]+[x2>x3]
- [P] — 1 if P is true, 0 otherwise
- \mathrm{PC},\ \mathrm{T},\ \mathrm{TC} — partial correctness, termination, total correctness
- M',\ M'' — the two contrast variants





## Rules and sources


- order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
- nat_induction · prerequisite — Principle of induction: for a family P(n) starting at n₀, if P(n₀) holds and P(n)⇒P(n+1) for every n≥n₀, then P(n) holds for every n≥n₀.
- finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
- subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
- cartesian_product_def · prerequisite — Cartesian product: A×B is the set of ordered pairs (a,b) with a∈A and b∈B; (a,b)=(c,d) ⇔ a=c and b=d.
- def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
- contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
- add_comm · prerequisite — Commutativity of addition: u+v=v+u.
- case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
- eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
- add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
- mko_algorithm_correctness_def · cited — Relative to initial conditions and a postcondition, partial correctness says every halt reached from a legal initial state satisfies the postcondition. Termination says every legal execution eventually reaches a halt. Total correctness is their conjunction. · mko-algorithm-correctness
- mko_computational_model_def · cited — A finite abstract model (S,Init,Step,Halt) with Init,Halt⊆S and Step⊆S×S; executions start in Init, follow Step and end on entering Halt; a state without successors is not automatically in Halt. · mko-computational-model
- L_succ · lemma — In M, every s∈S∖Halt has at least one adjacent inverted pair and hence at least one Step-successor.
- L_rank · lemma — In M, if (s,s′)∈Step then inv(s′)=inv(s)−1.





## Main derivation

S01 · definitionBefore

S=\{123,132,213,231,312,321\},\ \mathrm{Init}=\{321\},\ \mathrm{Halt}=\{123\}

After

\mathrm{Init},\mathrm{Halt}\subseteq S,\ \mathrm{Step}\subseteq S\times S,\ |S|=3!=6

Conditions: none

Rule: def_intro · Uses: G1

Leaf basis: def_intro + subset_def + cartesian_product_def + finite_counting_basics

Confirm that M is a finite model in the MKO's sense. 321 and 123 lie in S. Swapping two entries of a permutation gives another permutation of 1, 2, 3, so both ends of every edge lie in S, and Step⊆S×S. S has exactly 3!=6 elements. 123 has no adjacent inverted pair, so it has no outgoing edges anyway, consistent with Halt states being endpoints.



S02 · definitionBefore

M,\ Q

After

\mathrm{PC}:\ \text{every halt reached satisfies}\ Q;\quad \mathrm{T}:\ \text{every maximal execution is finite and ends in Halt};\quad \mathrm{TC}=\mathrm{PC}\wedge\mathrm{T}

Conditions: none

Rule: def_unfold · Uses: G2, G4, mko_algorithm_correctness_def

Leaf basis: def_unfold + mko_algorithm_correctness_def

Write out the partial/total-correctness obligations, quantifying termination precisely over maximal executions. PC: every execution from Init that reaches Halt ends in a state satisfying Q. T: every maximal execution from Init is finite and ends in Halt, equivalently there is no infinite execution and no finite maximal execution ending outside Halt. A finite nonmaximal prefix need not have reached Halt already. TC is PC together with T, and all nondeterministic choices must be covered (G4).



S03 · theorem_applicationBefore

s\in S\setminus\mathrm{Halt}

After

x_1>x_2\ \vee\ x_2>x_3,\ \text{so}\ \mathrm{Post}(s)\ne\varnothing

Conditions: none

Rule: L_succ · Uses: G1

Leaf basis: contrapositive + order_basics

Apply Lemma L_succ (proved in S03.1 and S03.2): a state outside Halt always has an adjacent inverted pair and hence a successor, so it cannot be stuck. This is the part of the termination argument that rules out getting stuck.



S04 · definitionBefore

s=(x_1,x_2,x_3)

After

\mathrm{inv}(s)=[x_1>x_2]+[x_1>x_3]+[x_2>x_3]\ge 0;\ \mathrm{inv}(321)=3,\ \mathrm{inv}(231)=\mathrm{inv}(312)=2,\ \mathrm{inv}(213)=\mathrm{inv}(132)=1,\ \mathrm{inv}(123)=0

Conditions: none

Rule: def_intro · Uses: G1

Leaf basis: def_intro + numeric_evaluation

Define the ranking function inv(s): the number of position pairs (i,j) with i<j and x_i>x_j. It is a sum of three 0-or-1 terms, so it is a natural number between 0 and 3. Compute it for all six states (recomputable as N2 to N7).



S05 · theorem_applicationBefore

(s,s')\in\mathrm{Step}

After

\mathrm{inv}(s')=\mathrm{inv}(s)-1

Conditions: none

Rule: L_rank · Uses: S04, G1

Leaf basis: def_unfold + add_comm + numeric_evaluation

Apply Lemma L_rank (proved separately for the two kinds of swap in S05.1 and S05.2): every step lowers the inversion count by exactly 1. This is a proof for every kind of edge, not an observation at a few sample states.



S06 · induction_baseBefore

(t_k)\ \text{an execution of}\ M,\ t_0\in\mathrm{Init}

After

\mathrm{inv}(t_0)=\mathrm{inv}(321)=3

Conditions: none

Rule: nat_induction · Uses: S04, G1

Leaf basis: nat_induction + numeric_evaluation

Consider any execution (t_k). t0∈Init={321}, so inv(t0)=3. This is the base case (k=0) of the invariant inv(t_k)=3−k.



S07 · induction_stepBefore

\mathrm{inv}(t_k)=3-k,\ (t_k,t_{k+1})\in\mathrm{Step}

After

\mathrm{inv}(t_{k+1})=(3-k)-1=3-(k+1)

Conditions: none

Rule: nat_induction · Uses: S06, S05

Leaf basis: nat_induction + eq_replace + add_assoc

Assume inv(t_k)=3−k and that the execution has a next state t_{k+1}. By L_rank, inv(t_{k+1})=inv(t_k)−1=(3−k)−1=3−(k+1). So inv(t_k)=3−k for every index k of the execution. Preservation is proved for every step, whichever edge is chosen at a nondeterministic branch.



S08 · impliesBefore

\mathrm{inv}(t_k)=3-k\ge 0

After

k\le 3:\ \text{every execution has at most 3 steps; no infinite execution}

Conditions: none

Rule: order_basics · Uses: S07, S04

Leaf basis: order_basics + nat_induction

inv is never below 0, so every index k of an execution satisfies 3−k≥0, i.e. k≤3. Hence every execution has at most 4 states and 3 steps, and no infinite execution exists. This is the ranking-function argument: a nonnegative integer that strictly decreases at every step cannot decrease forever.



S09 · impliesBefore

\text{every execution is finite}

After

\text{every maximal execution ends in Halt:}\ \mathrm{T}

Conditions: none

Rule: contrapositive · Uses: S08, S03

Leaf basis: contrapositive + mko_computational_model_def

By S08 every execution is finite; it can be extended while its last state has a successor, at most up to 3 steps, so every execution extends to a maximal one whose last state has no successor. By the contrapositive of L_succ (S03), a state without successors lies in Halt. Thus every maximal execution from Init is finite and ends in Halt, and every finite prefix extends to such a halting execution. Termination T holds as defined in S02.



S10 · impliesBefore

t_{\mathrm{last}}\in\mathrm{Halt}=\{123\}

After

Q(123):\ 1<2<3\ \wedge\ \{1,2,3\}=\{1,2,3\}\ \Rightarrow\ \mathrm{PC}

Conditions: none

Rule: mko_algorithm_correctness_def · Uses: S01, G1, G2

Leaf basis: mko_algorithm_correctness_def + order_basics

Every execution reaching Halt ends at 123. 123 is increasing, and its entries are a rearrangement of the entries of the input 321 (S01: every state is a permutation of 1, 2, 3, and swaps do not change the entries). So Q holds at every reachable halt state, and partial correctness PC holds.



S11 · impliesBefore

\mathrm{PC},\ \mathrm{T}

After

\mathrm{TC}=\mathrm{PC}\wedge\mathrm{T}\ \text{holds for}\ M

Conditions: none

Rule: and_intro_elim · Uses: S09, S10, S02

Leaf basis: and_intro_elim + mko_algorithm_correctness_def

Conjoin PC from S10 and T from S09; by the definition in S02 this is total correctness: every maximal execution from 321 terminates, and on termination outputs the increasing rearrangement 123.



S12 · impliesBefore

\text{reachable graph from}\ 321

After

321\to 231\to 213\to 123,\quad 321\to 312\to 132\to 123

Conditions: none

Rule: mko_computational_model_def · Uses: G1, S11

Leaf basis: mko_computational_model_def + case_analysis

A finite model can be cross-checked with its complete reachable graph. 321 has two successors: swapping the first pair gives 231, swapping the last pair gives 312. 231 has only its last pair inverted, giving 213; 312 has only its first pair inverted, giving 132; 213 gives 123; 132 gives 123. So there are exactly two maximal executions, each of 3 steps, equal to inv(321), both ending at 123. This agrees with S07 to S11; the general proof, however, comes from S05 to S10 and does not depend on this graph.



S13 · impliesBefore

M':\ 321\to 231\to 213\to 123\ \text{exists}

After

t_{2k}=321,\ t_{2k+1}=231\ \text{is infinite}\ \Rightarrow\ \neg\mathrm{T},\ \neg\mathrm{TC}\ \text{for}\ M'

Conditions: none

Rule: quantifier_negation · Uses: G3, S02

Leaf basis: quantifier_negation + case_analysis + mko_algorithm_correctness_def

In M′ the successful path 321→231→213→123 still exists, and Halt is still {123}, so PC still holds. But M′ allows swapping non-inverted pairs: swapping the first pair of 321 gives 231, and swapping the first pair of 231 returns to 321, neither in Halt. The sequence t_{2k}=321, t_{2k+1}=231 is a legal infinite execution, so T fails and TC fails. Neither one successful path nor PC yields total correctness (the misconception identified in the MKO).



S14 · impliesBefore

M'':\ \mathrm{Halt}''=\{s\mid x_1<x_2\}=\{123,132,231\}

After

321\to 231\in\mathrm{Halt}'',\ \neg Q(231)\ \Rightarrow\ \neg\mathrm{PC},\ \neg\mathrm{TC}\ \text{for}\ M''

Conditions: none

Rule: quantifier_negation · Uses: G3, G2, S02

Leaf basis: quantifier_negation + mko_algorithm_correctness_def

In M″ there are only two maximal executions from 321: 321→231 (231 has 2<3, so it is in Halt″ and stops) and 321→312→132 (132 is in Halt″ and stops). Both stop, so T holds; but the halt state 231 is not increasing (3>1), so Q(231) is false, PC fails, and TC fails too. Termination by itself does not guarantee correctness.







## Substeps and lemmas

S03.1 · impliesBefore

\neg(x_1>x_2)\ \wedge\ \neg(x_2>x_3)

After

x_1<x_2<x_3

Conditions: x_1,x_2,x_3\ \text{distinct}

Rule: order_basics · Uses: order_basics, contrapositive

Leaf basis: order_basics + contrapositive

Prove the contrapositive: if there is no adjacent inverted pair, then s∈Halt. The three entries of a permutation are distinct, so by trichotomy 'not x1>x2' with x1≠x2 gives x1<x2; likewise x2<x3. So x1<x2<x3.



S03.2 · impliesBefore

x_1<x_2<x_3,\ \{x_1,x_2,x_3\}=\{1,2,3\}

After

(x_1,x_2,x_3)=(1,2,3)\in\mathrm{Halt}

Conditions: none

Rule: order_basics · Uses: S03.1, order_basics

Leaf basis: order_basics + contrapositive

x1 is smaller than the other two entries (x1<x2 and, by transitivity, x1<x3), so x1 is the least element 1 of {1,2,3}; x3 is larger than the other two, so x3=3; what remains is x2=2. Hence s=123∈Halt. S03.1 and S03.2 together prove L_succ by contraposition.



S05.1 · impliesBefore

x_1>x_2,\ s'=(x_2,x_1,x_3)

After

\mathrm{inv}(s')=0+[x_2>x_3]+[x_1>x_3]=\mathrm{inv}(s)-1

Conditions: x_1>x_2

Rule: def_unfold · Uses: S04, G1

Leaf basis: def_unfold + add_comm + order_basics

Swap the first two entries: inv(s′)=[x2>x1]+[x2>x3]+[x1>x3]. Since x1>x2, [x2>x1]=0. And inv(s)=[x1>x2]+[x1>x3]+[x2>x3]=1+[x1>x3]+[x2>x3]. The remaining two terms only change places (commutativity of addition), so inv(s′)=inv(s)−1.



S05.2 · impliesBefore

x_2>x_3,\ s'=(x_1,x_3,x_2)

After

\mathrm{inv}(s')=[x_1>x_3]+[x_1>x_2]+0=\mathrm{inv}(s)-1

Conditions: x_2>x_3

Rule: def_unfold · Uses: S04, G1

Leaf basis: def_unfold + add_comm + order_basics + case_analysis

Swap the last two entries: inv(s′)=[x1>x3]+[x1>x2]+[x3>x2]. Since x2>x3, [x3>x2]=0, while inv(s)=[x1>x2]+[x1>x3]+1. So inv(s′)=inv(s)−1. S05.1 and S05.2 cover both kinds of edge in M, proving L_rank.







## Reverse audits


- S14 · premise_audit · G3, G2, quantifier_negation — Refuting PC needs one reached halt state violating Q; the verdict on T comes from the complete enumeration of the two maximal executions.
- S13 · premise_audit · G3, S02, quantifier_negation — One infinite execution refutes the universal T. Indices split into even and odd, covering every n≥0; the two alternating edges 321→231 and 231→321 are both edges of M′.
- S12 · premise_audit · G1, mko_computational_model_def — The reachable graph counts as complete only if all successors of every reachable state are listed; all six states are handled here.
- S11 · sufficient_goal_reduction · S02, S09, S10, and_intro_elim — Goal TC; by definition PC together with T is necessary and sufficient, and both were proved forwards above without assuming TC.
- S10 · premise_audit · S01, G2, mko_algorithm_correctness_def — PC speaks only about halt states that are reached; it does not imply T, which S09 proves separately.
- S09 · premise_audit · S08, S03, contrapositive — T needs two facts: no infinite execution (S08) and no getting stuck (S03); neither can be dropped.
- S08 · premise_audit · S07, S04, order_basics — It needs inv≥0 and a decrease of exactly 1 per step. It rules out infinite executions only; whether they stop in Halt is S09.
- S07 · premise_audit · S06, S05, nat_induction — The induction step uses L_rank for every edge; the arithmetic identity is checked as a degree-one polynomial identity in N8.
- S06 · premise_audit · S04, G1, nat_induction — The invariant holds at the initial state; preservation is S07.
- S05.2 · premise_audit · S04, def_unfold, add_comm, case_analysis — M has only these two kinds of edge, so the two cases are exhaustive.
- S05.1 · premise_audit · S04, def_unfold, add_comm — It needs the condition x1>x2, which is exactly the condition under which M allows this swap.
- S05 · premise_audit · L_rank, S04 — The lemma depends on 'only inverted pairs are swapped'; in M′ swapping a non-inverted pair raises inv, and the lemma does not apply.
- S04 · premise_audit · def_intro, numeric_evaluation — This step only defines and computes and derives no execution property; inv≥0 follows directly from the definition.
- S03.2 · premise_audit · S03.1, order_basics — It needs s to be a permutation of 1, 2, 3 (S01).
- S03.1 · premise_audit · order_basics, contrapositive — It needs distinct entries; with repeated values, 'not greater' would give only 'less than or equal'.
- S03 · premise_audit · L_succ, G1 — It holds for the swap rule of M; for M″ the states outside its halt set must be checked separately.
- S02 · premise_audit · mko_algorithm_correctness_def, G4 — This step only unfolds the definitions. PC by itself does not require any execution to stop, so PC alone can hold vacuously.
- S01 · premise_audit · G1, mko_computational_model_def, finite_counting_basics — This step only checks that the data form a model; 'swapping preserves being a permutation' is also the source of the 'rearrangement of the input' half of the postcondition (N1 recomputes 3!).





## Error controls and negative controls

One successful path is not total correctnessThe misconception identified in the MKO is taking one successful trace, or 'correct output but possibly non-terminating', as total correctness. M′ has the successful path 321→231→213→123 and satisfies PC, yet has an infinite execution (S13). In a nondeterministic model the obligations concern every execution (MKO assumption a2).

Partial correctness can hold vacuouslyPC only requires reached halt states to satisfy Q. A model that never stops (for example with the single edge 321→321 and Halt unreachable) has no halt state to check, so PC holds vacuously while T fails. So PC cannot stand in for TC (MKO paragraph 2).

An invariant must be proved for every step'inv drops by 1 at each step' was proved in S05 for both kinds of edge in M. Observing it only on sample transitions, for example seeing 321→231 take inv from 3 to 2 in M′, would miss the edge 231→321 taking inv from 2 to 3. Establishment plus preservation at every step is what makes a proof (MKO paragraph 1).


- M′ has the successful path 321→231→213→123, so M′ is totally correct → reject — M′ has the infinite execution alternating 321→231→321→231 forever, so T fails.
- M′ is partially correct, so M′ terminates → reject — PC does not include termination; for M′, PC holds and T fails.
- Every execution of M″ stops, so M″ is totally correct → reject — M″ can stop at 231, which is not increasing, so PC fails.
- A program that never halts is not partially correct → reject — When no halt state is ever reached, PC holds vacuously; such a program is not totally correct, but it is partially correct.





## Result and limitations

For M: each step lowers the inversion count by exactly 1, so every execution takes at most 3 steps; every non-halt state has a successor, so every maximal execution stops at 123; 123 satisfies the postcondition. So M is partially correct, terminating and totally correct; its reachable graph has exactly two maximal executions, each of 3 steps. M′ is partially correct and has a successful path, but has the infinite execution alternating 321 and 231, so it is not totally correct; M″ terminates but can stop at the unsorted 231, so it is not partially correct.


- Hoare-style specifications, the general ranking-function method, nondeterministic fairness and the bridge to real program semantics (MKO formal next) are not built here; this guide handles one explicit finite model only.





## Verification and source binding

8 declared checks for this guide; only the listed expressions are covered.


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 9ce0cffb4623aaaff23ae8c54c93395ecd56ec9621219ba8168ae49c7873d238
- original source SHA-256: 9ce0cffb4623aaaff23ae8c54c93395ecd56ec9621219ba8168ae49c7873d238
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-algorithm-correctness-01.json)