Mizar Analysis of Algorithms: Algorithms over

Summary. This paper is a continuation of [5] and concerns if-while alge-bras over integers. In these algebras the only elementary instructions are assign-ment instructions. The instruction assigns to a (program) variable a value which is calculated for the current state according to some arithmetic expression. The expression may include variables, constants, and a limited number of arithme-tic operations. States are functions from a given set of locations into integers. A variable is a function from the states into the locations and an expression is a function from the states into integers. Additional conditions (computabili-ty) limit the set of variables and expressions and, simultaneously, allow to write algorithms in a natural way (and to prove their correctness). As examples the proofs of full correctness of two Euclid algorithms (with modulo operation and subtraction) and algorithm of exponentiation by squaring are given