Hoare logic is the logic base of computer programming. It is used to describe verification of general programs. Separation logic as an extension of Hoare logic, provides supports for high order features used in modern programming languages. Step-indexed model is used to define self-referential predicates. Step-indexed logic is widely used in various program verification tools based on interactive theorem prover, but the reasoning based on step index logic is more complex and complicated than that based on classical logic. On step-indexed model, it is also able to define the non-step-indexed semantics under classical logic system which is more concise and clearer, and independent of the number of steps. Aiming at studying the relationship between stepping index logic and non-stepping index logic, it is found that the two logics are not equivalent. This study summarizes the propositions involved in practical program verification, finds out their common characteristics, and gives the constraint conditions of assertions about program states. The semantics of assertions in step-indexed logic and non-step-indexed logic are defined respectively, and the equivalence of the two semantics is proved under the constraint conditions. All the above definitions and proofs are formalized in Coq. Finally, the future research directions are discussed preliminarily.