You might want to look at something like:

http://en.wikipedia.org/wiki/Formal_semantics_of_programming...

I seem to remember that Dijkstra was keen on identifying weakest preconditions of different statements that can be used to prove a program correct.

However, I warn you that if you try this you will soon find out what this kind of formal reasoning about programs never caught on that widely - at least for imperative programs.