<abstract xml:lang="en" xmlns="http://www.w3.org/1999/xhtml">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 from the states into the locations and an expression is a function from the states into integers. Additional conditions (computability) 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.MML identifier: AOFA I00, version: 7.8.10 4.100.1011</abstract>

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 from the states into the locations and an expression is a function from the states into integers. Additional conditions (computability) 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.MML identifier: AOFA I00, version: 7.8.10 4.100.1011

Mizar Analysis of Algorithms: Algorithms over Integers

Formalized Mathematics

{"article-title":"Mizar Analysis of Algorithms: Algorithms over Integers"}

This paper is a continuation of [5] and concerns if-while algebras over integers. In these algebras the only elementary instructions are assignment...

Mizar Analysis of Algorithms: Algorithms over Integers

Publicado en línea: 20 mar 2009

Páginas: 177 - 194

DOI: https://doi.org/10.2478/v10037-008-0024-0

This content is open access.