Proving Correctness of Algorithm using Hoare

[anggha.satya11]

Hi guys! I have a task (my master thesis) to prove the correctness of an algorithm using Hoare logic. But until now, I'm still confuse when try to choose the algorithm. Do you have any ideas which algorithm I can proof with Hoare logic? Or maybe there's anyone who expert in Hoare logic because I have some question about that..

Thanks in advance.

[Laguana]

You've been asked to prove anything at all? Sounds strange to me, unless it is more of a "Play around with this new idea to get used to it" type of question.

Some thoughts: Pick something that is purely stack based. Hoare logic does not cope well with the heap/pointers. Pick something simple; can you code up a function that calculates triangular numbers? Can you then prove that it does in fact do that?

I wouldn't claim to be an expert on Hoare logic, but I am familiar with it, and I'm sure others here are as well if you have specific questions.

[Xami]

I would guess Laguana OP meant "task to prove an algorithm" and then has free choice over which to pick

edit: idk

[anggha.satya11]

Thank you very much Xami and Laguana for the reply.

Hmm..actually, what I meant with the task here is my master thesis in Computer Science. My general ideas for my thesis are: explore an algorithm in Java or other programming language (this is why I need help for choosing the algorithm), proving the correctness of it using Hoare logic manually, and then my expectation is "write" the proof in theorem prover.

Unfortunately, until now I'm still confusing in choosing the algorithm. I have to choose any algorithm that very useful in computer science but I don't wanna just choose it arbitrary and some how I can't proof it using Hoare logic. Can you help me please?

Thanks in advance.

[notzeb]

How about Edmond's matching algorithm?

[headprogrammingczar]

Binary tree search, perhaps?