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.
Proving Correctness of Algorithm using Hoare
Moderators: phlip, Moderators General, Prelates

 Posts: 15
 Joined: Thu Jan 26, 2012 4:42 am UTC
 Contact:
Proving Correctness of Algorithm using Hoare
Last edited by anggha.satya11 on Wed Feb 22, 2012 6:28 am UTC, edited 1 time in total.
Re: Proving Algorithm using Hoare
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.
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.
Re: Proving Algorithm using Hoare
I would guess Laguana OP meant "task to prove an algorithm" and then has free choice over which to pick
edit: idk
edit: idk
Last edited by Xami on Thu Feb 23, 2012 3:37 pm UTC, edited 1 time in total.

 Posts: 15
 Joined: Thu Jan 26, 2012 4:42 am UTC
 Contact:
Re: Proving Algorithm using Hoare
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.
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.
Re: Proving Correctness of Algorithm using Hoare
How about Edmond's matching algorithm?
Zµ«VjÕ«ZµjÖZµ«VµjÕZµkVZÕ«VµjÖZµ«VjÕ«ZµjÖZÕ«VµjÕZµkVZÕ«VµjÖZµ«VjÕ«ZµjÖZÕ«VµjÕZµkVZÕ«ZµjÖZµ«VjÕ«ZµjÖZÕ«VµjÕZ
 headprogrammingczar
 Posts: 3067
 Joined: Mon Oct 22, 2007 5:28 pm UTC
 Location: Beaming you up
Re: Proving Correctness of Algorithm using Hoare
Binary tree search, perhaps?
<quintopia> You're not crazy. you're the goddamn headprogrammingspock!
<Weeks> You're the goddamn headprogrammingspock!
<Cheese> I love you
<Weeks> You're the goddamn headprogrammingspock!
<Cheese> I love you
Who is online
Users browsing this forum: No registered users and 1 guest