This paper aims to provide a rigorous foundation for defining the meanings of programs in programming languages, establishing standards for proving properties such as correctness, equivalence, and termination. The approach centers on the concept of an interpretation, which associates propositions with control flow connections in a program. Conditions are imposed on each command to ensure that if a command is entered with a true proposition, it will be exited with a true proposition. This ensures that the program's behavior can be proven by induction. The paper also discusses the proof of termination by showing that each step of the program decreases some entity that cannot decrease indefinitely. The semantic definition of a programming language is based on a syntactic definition, specifying which phrases represent commands and the conditions for interpretations around each command. The paper demonstrates these concepts using a flowchart language and fragments of ALGOL. Definitions are provided for flowcharts, interpretations, and verification conditions, emphasizing the importance of verifying that the interpretation holds for all commands in the program.This paper aims to provide a rigorous foundation for defining the meanings of programs in programming languages, establishing standards for proving properties such as correctness, equivalence, and termination. The approach centers on the concept of an interpretation, which associates propositions with control flow connections in a program. Conditions are imposed on each command to ensure that if a command is entered with a true proposition, it will be exited with a true proposition. This ensures that the program's behavior can be proven by induction. The paper also discusses the proof of termination by showing that each step of the program decreases some entity that cannot decrease indefinitely. The semantic definition of a programming language is based on a syntactic definition, specifying which phrases represent commands and the conditions for interpretations around each command. The paper demonstrates these concepts using a flowchart language and fragments of ALGOL. Definitions are provided for flowcharts, interpretations, and verification conditions, emphasizing the importance of verifying that the interpretation holds for all commands in the program.