## Proving Correctness of Algorithm using Hoare

A place to discuss the science of computers and programs, from algorithms to computability.

Formal proofs preferred.

Moderators: phlip, Moderators General, Prelates

anggha.satya11
Posts: 15
Joined: Thu Jan 26, 2012 4:42 am UTC
Contact:

### Proving Correctness of Algorithm using Hoare

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.
Last edited by anggha.satya11 on Wed Feb 22, 2012 6:28 am UTC, edited 1 time in total.

Laguana
Posts: 49
Joined: Sat Jan 19, 2008 10:13 pm UTC

### 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.

Xami
Posts: 74
Joined: Tue Sep 29, 2009 8:29 pm UTC

### 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
Last edited by Xami on Thu Feb 23, 2012 3:37 pm UTC, edited 1 time in total.

anggha.satya11
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.

notzeb
Without Warning
Posts: 627
Joined: Thu Mar 08, 2007 5:44 am UTC
Location: a series of tubes

### Re: Proving Correctness of Algorithm using Hoare

How about Edmond's matching algorithm?
Zµ«V­jÕ«ZµjÖ­Zµ«VµjÕ­ZµkV­ZÕ«VµjÖ­Zµ«V­jÕ«ZµjÖ­ZÕ«VµjÕ­ZµkV­ZÕ«VµjÖ­Zµ«V­jÕ«ZµjÖ­ZÕ«VµjÕ­ZµkV­ZÕ«ZµjÖ­Zµ«V­jÕ«ZµjÖ­ZÕ«VµjÕ­Z

headprogrammingczar
Posts: 3072
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

Return to “Computer Science”

### Who is online

Users browsing this forum: No registered users and 6 guests