Abstract | ||
---|---|---|
This paper is a continuation of [5] and concerns if-while alge-bras 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. |
Year | DOI | Venue |
---|---|---|
2008 | 10.2478/v10037-008-0024-0 | FORMALIZED MATHEMATICS |
DocType | Volume | Issue |
Journal | 16 | 2 |
ISSN | Citations | PageRank |
1898-9934 | 0 | 0.34 |
References | Authors | |
0 | 1 |
Name | Order | Citations | PageRank |
---|---|---|---|
Grzegorz Bancerek | 1 | 96 | 19.74 |