Have you ever tried writing out a long proof by hand, on a piece of paper or a blackboard? No longer do you need to go through the ordeal of proving the correctness of a programme with these arcane methods, for our product allows you to prove programmes on a computer. You can easily type in and edit parts of the proof as you require, and the programme can automatically check the programme and report back is still lacking from your programme. This product is intended for use with the Program Correctness course. As such, we implemented features to allow the teacher of the course, our customer, to make assignments for the students. These assignments consist of the programme to be proven, with a pre- and post-condition. The students then have to fill in the assertions between lines to complete the proof. Their progress is stored, so there is no need to finish the whole proof in one sitting. Each student has an overview of the assignments they can make, which also shows if the exercises have been completed or not. It is also possible to provide feedback to the customer by filling out a form, for example about a bug or if you have a question about an exercise.
Our customer is Hans-Dieter A. Hiep, a PhD student active as researcher at the CWI and teacher at LIACS as part of Leiden University. He intends to use the Interactive Theorem Prover for the course Program Correctness, an elective for third year Computer Science students, among others. He gave us the tool, which was made by students of this course last year, and asked us to expand on it, adding certain logic elements as well as allowing him to give assignments through the tool for students to practice. Our collaboration with Drs. Hiep went very smoothly. We kept in touch regularly through emails and meetings to discuss problems and questions and show demos. He clearly told us which functionality he needed to be implemented so that he could use the tool in the course from next semester onwards, and then gave us a lot of freedom to figure out how we wanted to do this.
We worked in a team of 6 students. Quite early on, we decided to split into two groups of 3. One group would work on implementing the new logical features, while the other team would work on adding functionalities to the frontend. This includes making user account, creating new assignments for the users and giving feedback/asking questions to the client. By splitting the workload like this, the Frontend team members did not have to learn about all the logic rules in detail, giving them more time to work on the application. The Logic team members also had extra roles. One member was the scrum master, another the product owner, and the third member was in charge of checking the pull requests (except for his own). We feel the split was a fair one, and think that in the end, everyone has contributed a sufficient amount. Near the end of the project, we all put in the work to finish everything on time, even though most of us had a lot of other deadlines as well. This meant deviating a little from our original intended workload split, but we didn't mind and made it work.