uprm-inso4117-2023-2024-s2 / semester-project-study-pet

semester-project-study-pet created by GitHub Classroom
1 stars 3 forks source link

[Lecture Topic Task] Make sure the project utilizes Hoare Logic and document how does it do it in the documentation #178

Closed PinkSylvie closed 6 months ago

PinkSylvie commented 6 months ago

Hoare logic is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. Examples of Hoare logic are: pyrefine, https://www.key-project.org/, frama-c

Make sure the project utilizes Hoare Logic and document how does it do it with at least one meaningful example in the documentation. A recommendation the professor gives for this tasks is that if you want to use tool support, but cannot find a tool for the project's language, you can rewrite that function in a different language for which there's a tool available.

irsaris commented 6 months ago

Hello, please suggest urgency and difficulty scores.

DiegoLIRodriguez commented 6 months ago

Previous testing issues had a 4 diificulty and a 6 urgency, since this specific task requires external knowledge of Hoare logic and tools, I suggest upping the difficulty to 5.

So: Difficulty 5 Urgency 6

Fabian-J commented 6 months ago

An example of Hoare Logic has been provided. I couldn't get any tools working so I opted to do a manual analysis.