<abstract xml:lang="en" xmlns="http://www.w3.org/1999/xhtml"><p>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 (<italic>s, I</italic>), where <italic>s</italic> is a state (an element of certain set of states) and <italic>I</italic> 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 (<italic>s, I</italic>) and depends on the execution function. The existence of execution function determined on elementary instructions and its uniqueness for terminating instructions are shown.</p></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.

Mizar Analysis of Algorithms: Preliminaries

Department of Theoretical Computer Science, Białystok Technical University, Poland

Formalized Mathematics

{"article-title":"Mizar Analysis of Algorithms: Preliminaries"}

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...

Mizar Analysis of Algorithms: Preliminaries

Publicado en línea: 09 jun 2008

Páginas: 87 - 110

DOI: https://doi.org/10.2478/v10037-007-0011-x

This content is open access.