Have a personal or library account? Click to login
Mizar Analysis of Algorithms: Preliminaries Cover

Mizar Analysis of Algorithms: Preliminaries

Open Access
|Jun 2008

Abstract

Algorithms and its parts - instructions - are formalized as elements of if-while algebras. An if-while algebra is a (1-sorted) universal algebra which has 4 operations: a constant - the empty instruction, a binary catenation of instructions, a ternary conditional instruction, and a binary while instruction. An execution function is defined on pairs (s, I), where s is a state (an element of certain set of states) and I is an instruction, and results in states. The execution function obeys control structures using the set of distinguished true states, i.e. a condition instruction is executed and the continuation of execution depends on if the resulting state is in true states or not. Termination is also defined for pairs (s, I) and depends on the execution function. The existence of execution function determined on elementary instructions and its uniqueness for terminating instructions are shown.

DOI: https://doi.org/10.2478/v10037-007-0011-x | Journal eISSN: 1898-9934 | Journal ISSN: 1426-2630
Language: English
Page range: 87 - 110
Published on: Jun 9, 2008
In partnership with: Paradigm Publishing Services
Publication frequency: 1 issue per year

© 2008 Grzegorz Bancerek, published by University of Białystok
This work is licensed under the Creative Commons License.

Volume 15 (2007): Issue 3 (September 2007)