Comment by ambulancechaser

spec is wholly independent of the pre/post conditions.