But the spec usually has some implicit assumptions. Usually it's "app doesn't leak memory" in the same way nobody explicitly specifies "result of an addition of natural numbers should match ...".
We don't go around saying "oh, you didn't want modulo 5 arithmetic? You should've put that in the spec, not rely on some contrived absolute truth".
