Loop-invariant, Hoare-logik

Hej!

Jag har fastnat på vad sling-invarianten för det här programmet bör vara. Det enda jag kommer på är x=(x-y)+y men det känns fel då det egentligen inte säger något mer än att x=x. 

Vad borde invarianten för det här programmet vara?