Mizar Analysis of Algorithms: Algorithms over Integers
Grzegorz Bancerek (2008)
Formalized Mathematics
Similarity:
This paper is a continuation of [5] and concerns if-while algebras over integers. In these algebras the only elementary instructions are assignment 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 arithmetic operations. States are functions from a given set of locations into integers. A variable is a function...