Implementation and Specification of a Simple Polygon Triangulation Algorithm in Isabelle/HOL

Unexpected behaviour in software can be both expensive and time-consuming toresolve. Unit-testing is a common method used to gain confidence in the correctnessof implementations where the basic idea is to simulate a finite set of input-values and check if the program produces the expected outputs. This method is far from perfectas bugs are still present and a great concern in software. Formal verification have insome cases been successfully used to prove correctness in programs when exhaustiveunit-testing was infeasible. This approach relies on using formal methods to provewhether the I/O-behaviour of the implementation is equivalent to its formal specification. Computational geometry is a field that has become increasingly relevant in the industry. Numerous of algorithms in this field have a multitude of applications and are used to help solving real-life problems. As the systems using geometry algorithmsscale the need for its' components to function properly grows more critical. Formal verification can be a great tool for this task as it can prove the correctness of the components, essentially eliminating implementation bugs. Little research is howeverbeing done on formal verification in computational geometry even though it could supplement the flaws of unit testing, as seen in some other fields. In this project, the first few steps of formal verification is performed. A program thattriangulates a simple polygon is implemented in Isabelle/HOL, followed up by a formalspecification of the program. In other words, the pre- and postconditions for simple polygon triangulation are specified, which could be used for verification of theimplementation. The results show that formal verification is applicable for thisprogram as the expected I/O-behaviour for the program was naturally translated intoa formal specification