by **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.