Abstract: As a specification language, temporal logic is powerful enough in expressing the properties for program.In order to prove the theorem that expresses the property using temporal logic formula in a prototype verification system (PVS), this paper establishes a semantics model for temporal logic as well as the semantics interpretation.As an example, a program for solving the square root for an integer is investigated.Some properties of this program are specified in temporal logic formulas.An interface for verifying program by PVS is provided.

Key words: semantics, program properties, temporal logic, PVS