Hoare logic for Recursive

[anggha.satya11]

Hi everyone. I wanna proof the correctness of Strassen program. It is for multiplying 2 matrices. That program contains recursive function to itself. I wanna proof this program using Hoare proof system. But, until now I haven't found the proof system for program contains recursive. Is there anyone can help me?

Thank you very much.