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, Prelates, Moderators General

Proving Correctness of Algorithm using Hoare

Postby anggha.satya11 » Mon Feb 20, 2012 10:58 am UTC

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.
anggha.satya11
 
Posts: 14
Joined: Thu Jan 26, 2012 4:42 am UTC

Re: Proving Algorithm using Hoare

Postby Laguana » Mon Feb 20, 2012 1:01 pm UTC

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.
Laguana
 
Posts: 49
Joined: Sat Jan 19, 2008 10:13 pm UTC

Re: Proving Algorithm using Hoare

Postby Xami » Mon Feb 20, 2012 3:25 pm UTC

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.
Xami
 
Posts: 74
Joined: Tue Sep 29, 2009 8:29 pm UTC

Re: Proving Algorithm using Hoare

Postby anggha.satya11 » Wed Feb 22, 2012 6:27 am UTC

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.
anggha.satya11
 
Posts: 14
Joined: Thu Jan 26, 2012 4:42 am UTC

Re: Proving Correctness of Algorithm using Hoare

Postby notzeb » Wed Feb 22, 2012 9:04 am UTC

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
User avatar
notzeb
Without Warning
 
Posts: 573
Joined: Thu Mar 08, 2007 5:44 am UTC
Location: a series of tubes

Re: Proving Correctness of Algorithm using Hoare

Postby headprogrammingczar » Wed Feb 22, 2012 1:19 pm UTC

Binary tree search, perhaps?
<quintopia> You're not crazy. you're the goddamn headprogrammingspock!
<Weeks> You're the goddamn headprogrammingspock!
<Cheese> I love you
User avatar
headprogrammingczar
 
Posts: 3026
Joined: Mon Oct 22, 2007 5:28 pm UTC
Location: Beaming you up


Return to Computer Science

Who is online

Users browsing this forum: No registered users and 1 guest