<abstract xmlns="http://www.w3.org/1999/xhtml">In this paper we introduce some notions to facilitate formulating and proving properties of iterative algorithms encoded in nominative data language [19] in the Mizar system [3], [1]. It is tested on verification of the partial correctness of an algorithm computing <italic>n</italic>-th Fibonacci number:
<disp-quote><monospace>i := 0</monospace><monospace>s := 0</monospace><monospace>b := 1</monospace><monospace>c := 0</monospace><monospace>while (i &lt;> n)</monospace>  <monospace>c := s</monospace>  <monospace>s := b</monospace>  <monospace>b := c + s</monospace>  <monospace>i := i + 1</monospace><monospace>return s</monospace></disp-quote>
This paper continues verification of algorithms [10], [13], [12] written in terms of simple-named complex-valued nominative data [6], [8], [17], [11], [14], [15]. The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data [9]. Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic [2], [4] with partial pre- and post-conditions [16], [18], [7], [5].</abstract>

In this paper we introduce some notions to facilitate formulating and proving properties of iterative algorithms encoded in nominative data language [19] in the Mizar system [3], [1]. It is tested on verification of the partial correctness of an algorithm computing n-th Fibonacci number:
i := 0s := 0b := 1c := 0while (i <> n)  c := s  s := b  b := c + s  i := i + 1return s
This paper continues verification of algorithms [10], [13], [12] written in terms of simple-named complex-valued nominative data [6], [8], [17], [11], [14], [15]. The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data [9]. Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic [2], [4] with partial pre- and post-conditions [16], [18], [7], [5].

Partial Correctness of a Fibonacci Algorithm

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

{"article-title":"Partial Correctness of a Fibonacci Algorithm"}

In this paper we introduce some notions to facilitate formulating and proving properties of iterative algorithms encoded in nominative data language [19] in...

Partial Correctness of a Fibonacci Algorithm

Publié en ligne: 09 janv. 2021

Pages: 187 - 196

Accepté: 31 mai 2020

DOI: https://doi.org/10.2478/forma-2020-0016

Mots clés
nominative data, program verification, Fibonacci sequence

© 2020 Artur Korniłowicz, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Partial Correctness of a Fibonacci Algorithm

Publié en ligne: 09 janv. 2021

Pages: 187 - 196

Accepté: 31 mai 2020

DOI: https://doi.org/10.2478/forma-2020-0016

Mots clésnominative data, program verification, Fibonacci sequence

© 2020 Artur Korniłowicz, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Mots clés
nominative data, program verification, Fibonacci sequence