CUT TO:
INT. PROJECT ARCHIVE — STORYBOARD ROOM
The USER opens Formally Verified Dutch National Flag Algorithm.
DIVAKAR DESSAI
Let's run through the shots.
CASE FILE / SENG2011 / Formal Verification / Algorithms
Formally Verified Dutch National Flag AlgorithmProving a Sorting Algorithm Correct
Implemented and formally verified the Dutch National Flag sorting algorithm using Dafny predicates, loop invariants and multisets.
01–02 / OPENING SEQUENCE
Establishing the world
01 / Establishing Shot
The Problem
Implementing the sorting algorithm was only one part of the task; the implementation also had to be formally proven to produce a correctly ordered permutation of the original input.
02 / Wide Shot
The Context
The assignment extended Dafny verification into algorithm correctness and loop reasoning.
03 / CHARACTER NOTE
DIVAKAR'S ROLE
Subject
Divakar Dessai
Production
Formally Verified Dutch National Flag Algorithm
Take
03 / Role
Role notes
DIVAKAR DESSAI
I implemented the algorithm and constructed the predicates, invariants and multiset properties required for Dafny to prove correctness.
04 / CLOSE-UP
THE ENGINEERING CHALLENGE
The loop invariants needed to be strong enough to establish the final result while remaining preserved after every swap and pointer update.
05 / TRACKING SHOT
THE APPROACH
A plan emerges.
I partitioned the array conceptually into red, white, unknown and blue regions and described each region with invariants. A multiset equality property ensured values could not disappear or be introduced during sorting.
06 / INSERT SHOTS
KEY FEATURES
The system takes shape.
07 / DIRECTOR'S NOTES
DESIGN DECISIONS
Things we decided along the way
01
Expressed partially sorted regions explicitly through invariants.
02
Used multisets to prove permutation preservation independently from ordering.
03
Separated general sortedness from colour-specific algorithm behaviour.
design decisions
somewhere mid-build
08 / RETAKES
WHAT WENT WRONG
Naturally, not everything cooperates.
09 / FINAL SHOT
THE OUTCOME
ProblemBuildOutcome
01
Implemented a formally verified sorting algorithm.
02
Developed practical understanding of loop invariants.
03
Learned how implementation and proof obligations influence one another.
10 / PRODUCTION NOTES
TECH STACK
The tools behind the scenes.
DafnyLoop InvariantsMultisetsFormal Verification
11 / BEHIND THE SCENES
LINKS
FADE OUT.
USER closes the file.
One project down. A few more stories left.
DIVAKAR DESSAI
Pick another?