Proving properties of Pascal programs in MIZAR 2

DOI10.1007/BF00265684MaRDI QIDQ1058285zbMATH OpenOpenAlexFDO

Authors Piotr Rudnicki, Włodzimierz Drabent

Publication date 1985

Published in Acta Informatica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf00265684

zbMATH Keywords

MIZAR 2Pascal language constructspredicate calculussemantics

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

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.

Recommendations

• The mathematical construction of a program
• scientific article; zbMATH DE number 4172362
• scientific article; zbMATH DE number 4147469
• scientific article; zbMATH DE number 4006266
• scientific article; zbMATH DE number 3858395

Cited in

(2)

• Implementation of the composition-nominative approach to program formalization in Mizar
• The mathematical construction of a program

Describes a project that uses

Uses Software

• Mizar

This page was built for publication: Proving properties of Pascal programs in MIZAR 2

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1058285)