Reasoning about program transformations :imperative programming and flow of data