Correctness of Programs Calculating Matrices

Abstract – In this paper, we first propose three functions for the complex number, extraction of the real part, and extraction of the imaginary part by a C program. Then, we use these functions to define addition, subtraction, multiplication, division, inverse, conjugate, scalar product, minus, zero, and unity. We want to construct programs that are related to correct logically. Vectors of complex addition, subtraction, scalar product, minus, and inner products are introduced using definitions and theorems related to complex numbers. Then, we present four definitions related to the addition of matrices of complex numbers. We also transfer C language into the Mizar language and verify it. In the future, many functions will be developed which can be used to reduce construction periods and generate high-performance systems. 1