In this paper we continue development of formal verification tools for algorithms using the framework of nominative data and Floyd-Hoare logic with partial pre- and postconditions in the Mizar proof assistant. We define operations of sequential composition of several programs, formalize and show soundness of new inference rules which can be used to prove partial correctness of programs involving these operations in the context of partial pre- and postconditions. A process of verification of the partial correctness of exemplary algorithms is described.
The framework is intended to be used for practical verification of the correctness of programs. One of its implementations is done in the Mizar proof assistant [BBG+15, GKN15]. Nominative data with simple names and complex values and basic operations on them are defined in [INKK17]. An algebra of programs over partial predicates and binominative functions on nominative data including among others operators of a programming language (e.g. assignment, skip, conditional if statement and a while loop) are defined in [KIN18, IKN18b, IKN18c]. An inference system of an extension of Floyd-Hoare logic for partial predicates and soundness of the rules are formalized in [IKN18a]. An example – the subtraction-based version of Euclid’s algorithm computing the greatest common divisor of natural numbers – how to use all this stuff is presented in [IKN18d].
In this paper we report on our continuation [KKNI17a, KKNI17b, KKNI17c] of formalization of the framework in Mizar including three more inference rules for unconditional composition of 3, 4, and 5 programs and proofs of the correctness of two algorithms: computing the natural power of a complex number and factorial of a natural number. 2
Having mathematical tools mentioned above we have proved in Mizar the correctness of two algorithms: the natural power of a complex number [Jas19] and factorial of a natural number [JK19] with the following pseudocodes:
Pseudocode of factorial algorithm: i := val.1; j := val.2; n := val.3; s := val.4; while ( i <> n ) i := i + j; s := s * i; return s;
Pseudocode of power algorithm: i := val.1; j := val.2; b := val.3; n := val.4; s := val.5; while ( i <> n ) i := i + j; s := s * b; return s;
Both algorithms consist of three parts: the initialization of variables, the main while loop, and the result returning statement. Moreover, in factorial we have only one input value and in power two input values: base and exponent. At the end we return s as the results of algorithms.
Formalization of the algorithms in Mizar has been divided into few separate parts. Because both algorithms are similar, we can take a closer look into just one of them, let us choose the power algorithm. To formulate it we introduced several Mizar functors representing various components of the algorithm: the initialization of variables: definition let V,A,loc,val; func power_var_init(A,loc,val) -> SCBinominativeFunction of V,A equals PP_composition(
SC_assignment(denaming(V,A,val.1), loc/.1), SC_assignment(denaming(V,A,val.2), loc/.2), SC_assignment(denaming(V,A,val.3), loc/.3), SC_assignment(denaming(V,A,val.4), loc/.4), SC_assignment(denaming(V,A,val.5), loc/.5) ); end; the loop body: end; the entire loop: definition let V,A,loc; func power_loop_body(A,loc) -> SCBinominativeFunction of V,A equals
PP_composition(
SC_assignment(addition(A,loc/.1,loc/.2),loc/.1),
SC_assignment(multiplication(A,loc/.5,loc/.3),loc/.5) ); definition let V,A,loc; func power_main_loop(A,loc) -> SCBinominativeFunction of V,A equals
PP_while(PP_not(Equality(A,loc/.1,loc/.4)),power_loop_body(A,loc)); end; the initialization composed with the loop: definition let V,A,loc,val; func power_main_part(A,loc,val) -> SCBinominativeFunction of V,A equals
PP_composition(power_var_init(A,loc,val),power_main_loop(A,loc)); and finally the entire program where the returning statement is added: definition let V,A,loc,val,z; func power_program(A,loc,val,z) -> SCBinominativeFunction of V,A equals
PP_composition(power_main_part(A,loc,val), SC_assignment(denaming(V,A,loc/.5),z));
Because we work in the paradigm of nominative data those definitions take sets V and A as names and values, respectively. Moreover, V-valued functions loc represents formally locations in memory where variables are stored, and functions val keep values of variables.
The partial correctness of programs in our framework is expressed as the validity of semantic Floyd-Hoare triples [IKN18a] of the form <*p,f,r*> is SFHT of D, where p represents a precondition, f represents a program, and r represents a postcondition, all defined over a set D. In the case of the power algorithm it takes the form: <* valid_power_input(V,A,val,b0,n0), power_program(A,loc,val,z), valid_power_output(A,z,b0,n0) *> is SFHT of ND(V,A) where valid_power_input is the precondition representing the valid input and valid_power_output is the postcondition representing the valid output, both involving the complex base b0 and the natural exponent n0. All components of the triple are defined over the set ND(V,A) of all nominative data over sets V and A.
The discussed algorithm contains a while loop, which verification requires an invariant. For this purpose we defined the predicate: definition let V,A,loc,b0,n0,d; pred power_inv_pred A,loc,b0,n0,d means ex d1 being NonatomicND of V,A st d = d1 & { loc/.1, loc/.2, loc/.3, loc/.4, loc/.5 } c= dom d1 & d1.(loc/.2) = 1 & d1.(loc/.3) = b0 & d1.(loc/.4) = n0 & ex S being Complex, I being Nat st I = d1.(loc/.1) & S = d1.(loc/.5) & S = b0|^I; end; which describes that every state d1 includes all required memory locations, initial values 1, b0 and n0 are always in the same locations, and S is always equal to b0I. It is used to prove that initialization of variables and each iteration of the loop fulfill the condition.
With this structure we could start proving the correctness of the algorithms. Detailed proofs are available in the Mizar Mathematical Library [BBG+18, Jas19, JK19].
Apart from the formal verification of the correctness of mentioned algorithms we also defined operations for composition of 3, 4 and 5 instructions. Moreover, we defined inference rules describing how to prove the correctness of programs involving these operations and proved their soundness. In the case of the composition of 3 instructions the rule is: fpg f1 fqg; fqg f2 frg; f qg f2 frg; frg f3 fsg; f rg f3 fsg
fpg f1 f2 f3 fsg As one can notice, the rule above is different than in the standard Floyd-Hoare logic would be. The reason of that is because we also consider a case where results of programs f1 and f2 do not belong to the domains of the partial conditions q and r, respectively. In the standard case all pre- and postconditions would be total.
The operations and rules allowed us to use one composition instead of several binary compositions. 3
In this paper we have shown how to verify the correctness of algorithms in the Mizar proof assistant using nominative data and a variant of Floyd-Hoare logic on the example of algorithms computing the natural power of a complex number and factorial of a natural number. On these simple examples it can be observed that various algorithms have almost same structure and in many cases there are very similar formalization steps. In the future we want to detect and define more general structures of algorithms written in our environment and to use particular Mizar constructions, like structures and schemes, to formulate the algorithms and make reasoning on them. For example, we can define a Mizar structure containing the input, output, constant values, the main program, and possibly other components of programs as separate fields of the structure.
Another way of extension of our framework is to define new instructions in the language and new inference rules about the instructions within our variant of logic. For example, we can introduce an instruction for the composition of arbitrary n instructions instead of compositions of two, three, four and more instructions separately, and for loop instruction and adequate inference rules. It will make easier writing algorithms with sequences of compositions and make shorter proofs of properties of the algorithms.
The ultimate goal of the project is to build a complete formal tool for verifying the correctness of complex algorithms. These algorithms could be then implemented, for example, in some safety-critical software. Soon, almost every aspect of our life will be connected with computer programs, so it is important to make sure that algorithms that they will be using are designed and implemented correctly. [Flo67]
Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198, 2015. https://doi.org/10.1007/s10817-015-9345-1 V. M. Glushkov. Automata theory and formal microprogram transformations. Cybernetics, 1(5):1–8, Sep 1965.
C.A.R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576–580, 1969. [IKN18a] Ievgen Ivanov, Artur Korniłowicz, and Mykola Nikitchenko. An inference system of an extension of Floyd-Hoare logic for partial predicates. Formalized Mathematics, 26(2):159–164, 2018. https: //doi.org/10.2478/forma-2018-0013 [IKN18b] Ievgen Ivanov, Artur Korniłowicz, and Mykola Nikitchenko. On algebras of algorithms and specifications over uninterpreted data. Formalized Mathematics, 26(2):141–147, 2018. https://doi.org/ 10.2478/forma-2018-0011
Ievgen Ivanov, Artur Korniłowicz, and Mykola Nikitchenko. On an algorithmic algebra over simplenamed complex-valued nominative data. Formalized Mathematics, 26(2):149–158, 2018. https: //doi.org/10.2478/forma-2018-0012 [JK19]
Adrian Jaszczak. Partial correctness of a power algorithm. Formalized Mathematics, 27(2), 2019. Accepted for publication.