VERIFICATION OF MIGHT’S DELETION ALGORITHM OF RED-BLACK TREE USING LIQUID HASKELL

• Main Author: Afkar Makmur, Hafizh
• Format: Final Project
• Language: Indonesia
• Online Access: https://digilib.itb.ac.id/gdl/view/57231
• Institution: Institut Teknologi Bandung

The increasing demand for software creates a pressing demand for an infallible program. One of the tools developed for this purpose is Liquid Haskell for Haskell programming language. The characteristic of Liquid Haskell that is automatic and can be used without modifying the source code ease the verification process so much compared to previous verification programs. But then there’s a question of whether Liquid Haskell can really verify all programs that are written in Haskell Language. One of the most popular case examples to study formal method is the verification case of Red-Black Tree data structure. In 2010, Matthew Might created a deletion algorithm for Red-Black Tree data structure with a purpose to create a deletion algorithm that is more elegant than algorithms that have been written before. This data structure is simple have a very clear and easy to write specification so this program can be an ideal target to prove whether Liquid Haskell can verify a code that’s written by other people in the real world. The result of verification and analysis of the code shows that most of the code can be verified by Liquid Haskell but there are 3 parts of the program that fails the verification. Those parts are line code that’s related to QuickCheck testing, Binary Search Tree property, and the last line in balance function. Because of that, there are several code modifications that are applied as an example of a valid code that can be verified successfully by Liquid Haskell.