Introduction
Have you ever wondered if a program really does what it’s supposed to — mathematically?
Most programmers test code manually, but there’s a formal way to prove program correctness: it’s called Hoare Logic.
In this post, we’ll:
- Introduce Hoare Logic and its basic idea
- Show how it applies to Python
if/else statements
- Connect it to algebraic models of loops
- Give you an intuitive way to “prove your code”
By the end, you’ll see how logic meets code, and how mathematics can verify programs.
1. What is Hoare Logic?
Hoare Logic was introduced by C. A. R. Hoare in 1969. It’s a method to reason about program correctness using Hoare triples:
[
{P}\ S\ {Q}
]
Where:
- (P) = Precondition (what must be true before the code)
- (S) = Statement (the program code)
- (Q) = Postcondition (what will be true after the code, if it terminates)
Example:
x = 5
y = x + 2
- Precondition (P): (x = 5)
- Statement (S):
y = x + 2
- Postcondition (Q): (y = 7)
So we can write the Hoare triple:
[
{x = 5}\ y = x + 2\ {y = 7}
]
✅ This triple is mathematically correct.
2. Proving if/else Statements
Hoare Logic has a rule for conditionals:
[
\frac{{P \wedge B}\ S_1\ {Q},\ {P \wedge \neg B}\ S_2\ {Q}}{{P}\ \text{if } B \text{ then } S_1 \text{ else } S_2\ {Q}}
]
In plain words:
- If the condition (B) is true → (S_1) executes correctly
- If (B) is false → (S_2) executes correctly
- Then the entire
if/else is correct
Python Example:
x = 10
if x > 5:
y = 1
else:
y = 2
- Precondition (P):
x = 10
- Condition (B):
x > 5
- Postcondition (Q):
y = 1
Check:
- (x > 5) → executes
y = 1 ✅ Correct
- (x <= 5) → would execute
y = 2 (not taken in this case)
Hoare triple:
[
{x = 10}\ \text{if } x > 5\ \text{then } y=1\ \text{else } y=2\ {y=1}
]
3. Connecting Hoare Logic to Algebraic Models
In my research, I represent conditionals as algebraic functions:
def f(x):
if x == 0:
return 0
else:
return 1
0 → false, 1 → true- Precondition:
x ∈ {0,1}
- Postcondition: output ∈ {0,1}
Mathematically:
[
f(x) = \begin{cases}
0 & \text{if } x=0 \
1 & \text{if } x=1
\end{cases}
]
Notice how this matches Hoare logic:
- Precondition (P): (x \in {0,1})
- Statement (S):
if/else
- Postcondition (Q): output ∈ {0,1}
✅ Algebraic function = Hoare triple in practice
4. Loops: Summations and Hoare Invariants
Hoare Logic handles loops using loop invariants:
[
{I \wedge B}\ S\ {I}
]
Where:
- (I) = Loop invariant (true before and after every iteration)
- (B) = Loop condition
For Python for loops, I model them as summations over arithmetic progressions:
for i in range(0, 5):
sum += i
range(0,5) → 0,1,2,3,4- Algebraic model:
[
\sum_{i=0}^{4} i = 10
]
- Precondition:
sum = 0
- Postcondition:
sum = 10
Again, this is Hoare Logic applied numerically:
[
{sum = 0}\ \text{for } i \text{ in range(0,5)}\ {sum = 10}
]
5. Why This Matters
- You can prove code correctness without running it
- Combine algebraic models + Hoare Logic for clearer reasoning
- This makes Python programs mathematically verifiable
Even simple programs can be formally verified, giving you confidence in correctness and runtime behavior.
6. Conclusion
Hoare Logic provides a mathematical framework for proving program correctness, and algebraic models of conditionals and loops give a computational perspective.
By combining both:
if/else → algebraic functions = Hoare triplesfor loops → summations = Hoare invariants
You get a powerful, accessible, and mathematically sound way to reason about programs.
References
- Hoare, C. A. R. (1969). An Axiomatic Basis for Computer Programming. Communications of the ACM, 12(10), 576–580.
- Jadon, P. (2026). A Theoretical Framework for Conditional Statements: Modeling If/Else as Algebraic Functions. Zenodo. https://doi.org/10.5281/zenodo.18758094
- Jadon, P. (2026). A Mathematical Framework for Python Loops: Modeling For-Loops as Finite Summations. Zenodo. https://doi.org/10.5281/zenodo.18772270
]
