Formal specification-based inspection is a practical program verification technique for detecting requirement-related faults and can be applied at any time before or after the code is completed. A high level of automated support for specification-based inspection is desirable as it will help to enhance efficiency and reduce human errors during inspection. To achieve this goal, the open problem of how to link the components in a formal specification to those in the corresponding program must be addressed first, since it is a prerequisite for inspection. By taking advantage of the multi-dimensional attributes of the components in a SOFL formal specification, which are mostly remained in their implementation, we have proposed an approach to establishing trace links between a SOFL formal specification and its corresponding complete code after programming in our previous work. This paper solves the challenge of establishing trace links between a SOFL specification and the incomplete code during programming. The method is comprised of four steps: preprocessing the formal specification, extracting the intermediate states and final states of the multidimensional attributes for components in the specification and the current state of those in its corresponding programs, calculating the similarity, and predicting traceability links through filtering and ranking. A comparative evaluation of the proposed method, using two selected modules of the SOFL formal specification of an ATM system and its Java implementation, demonstrates an improvement in precision than existing latent semantic indexing (LSI) that is an information retrieval-based method.