Victorian Safe Cracker
Tech used: VDM-SL, Isabelle
[ GitHub ]
Slightly different in that no program was created, this project looked at modelling how an optimal (or close to) program would solve a Safecracker 40 puzzle.
(Image courtesy of Crux Puzzles)
The model was built using VDM-SL in Overture. After it was built and tested, I began translating it into Isabelle, a proof assistant. From a correct translation, the VDM model could be improved further to create a more optimised version of it. The goal would be that after the model has been built and proven, it could then be translated into a real life program.
The module I did this coursework for was called Software Verification, and it taught the importance of building a solid model for a project before jumping straight into development. It helps to reduce the amount of tearing down and rebuilding of code if its based on a mathematically-correct model.