Services rendered by legacy systems that have evolved over decades are vital to many industries. Therefore, reengineering of these systems must ensure that the new systems provide the same functionalities as their ancestors, while exploiting new technologies. Reengineering involves reverse engineering an application from code to a higher level abstraction, and then reimplementing on a new platform. Ability to obtain the abstraction at requirements level enables maximum use of new development techniques and tools in reimplementation. Use of formal methods in specifying requirements helps eliminating unambiguity while enhancing confidence in consistency and correctness. This thesis presents a formal approach to reverse a program written in a C subset into a functional specification in Z notation, including (i) a description of the abstractions used in the reverse engineering process, (ii) a method to obtain these abstractions from a program written in a C subset, (iii) a method to derive the formal requirements specification from the abstractions, and (iv) a com arison of the logical strength of three sets of conditions to justify the correctness of the derived specification, as well as their application in reverse engineering.