The aim of this assignment is to use the SPARK Ada toolset to implement and verify the correctness and security of a small command-line Password Manager utility. We implement the functionality of the password manager program in SPARK Ada, and use the SPARK Prover to prove that it is free of runtime errors and, additionally, that it is also secure.

The program we have to implement is a command-line utility for managing website passwords. It takes input from the terminal (i.e. standard input, aka stdin). The specific requirement is described in Assignment 3.

20/20