I'm taking a class in University which involves proving the correctness of computer programs and I'm really bad a proofs, I don't really understand them at all.
Can anyone tell me if my proof actually makes any sense, I frequently think I've written a proof but usually I've proved nothing.
Given this (T1 is a function that takes another function (F) as one of its parameters):
T1(F,x,y) == if y = 0 then x else F(x−1,y−1)
I had to suggest a fixed point solution, I suggested:
f1(x,y) == x - y
Because T1 is a recursive function that implements subtraction. And below I had to prove my suggestion was correct.
To show T1(f1) = f1 T1(f1, x, y) == if y = 0 then x else f1(x−1,y−1) if y = 0 then x else (x-1) - (y-1) if y = 0 then x else x - y - 2 x - y - 2 = f1(x-1,y-1) x - y = f1(x,y)
Does my proof have some obvious hole in it that I'm not seeing or is there some mistake I can't see, I think it works but I'm not really sure why it proves anything?