Proving properties of Pascal programs in MIZAR 2 (Q1058285)

In this paper we present the so called natural semantics for a subset of Pascal programming language. A set of sentences of first order predicate calculus defines the meaning of the Pascal language constructs. The meaning of a specific program is defined separately by another set of sentences which can be generated automatically. Both these sets together constitute axiomatics of a theory, called the theory of a specific program. The axiomatics is built in such a way that its logical consequences describe all the computational processes defined by the program. Proofs of properties for two small programs are discussed in detail. These properties and their proofs are recorded in the MIZAR 2 language - a computer formalization of predicate calculus. MIZAR 2 proof checker was used to verify the proofs.