Implementation of the Composition-nominative Approach to Program Formalization in Mizar

Abstract

In this paper we describe an ongoing work on implementation of the composition-nominative approach to program formalization in Mizar proof assistant based on the first-order logic and axiomatic set theory. The further aim of this work is development of a formal verification tool for software which processes and communicates with complex forms of data.

Keywords

• Formal methods
• program semantics
• semistructured data
• formalization
• proof assistant