A theory of totally correct logic program transformations