<abstract xmlns="http://www.w3.org/1999/xhtml">In this paper we present a formalization in the Mizar system [3],[1] of the partial correctness of the algorithm:<preformat preformat-type="transcription">
i := val.1
j := val.2
n := val.3
s := val.4
while (i &lt;> n)
 i := i + j
 s := s * i
return s
</preformat>computing the factorial of given natural number n, where variables <monospace>i, n, s</monospace> are located as values of a <monospace>V-valued Function, loc</monospace>, as: <monospace>loc/.1 = i, loc/.3 = n</monospace> and <monospace>loc/.4 = s</monospace>, and the constant <monospace>1</monospace> is located in the location <monospace>loc/.2 = j</monospace> (set <monospace>V</monospace> represents simple names of considered nominative data [16]).This work continues a formal verification of algorithms written in terms of simple-named complex-valued nominative data [6],[8],[14],[10],[11],[12]. 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 [13],[15],[7],[5].</abstract>

In this paper we present a formalization in the Mizar system [3],[1] of the partial correctness of the algorithm:
i := val.1
j := val.2
n := val.3
s := val.4
while (i <> n)
 i := i + j
 s := s * i
return s
computing the factorial of given natural number n, where variables i, n, s are located as values of a V-valued Function, loc, as: loc/.1 = i, loc/.3 = n and loc/.4 = s, and the constant 1 is located in the location loc/.2 = j (set V represents simple names of considered nominative data [16]).This work continues a formal verification of algorithms written in terms of simple-named complex-valued nominative data [6],[8],[14],[10],[11],[12]. 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 [13],[15],[7],[5].

Partial Correctness of a Factorial Algorithm

Formalized Mathematics

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

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

In this paper we present a formalization in the Mizar system [3],[1] of the partial correctness of the algorithm:
i := val.1
j := val.2
n := val.3
s :=...

Partial Correctness of a Factorial Algorithm

Publié en ligne: 20 juil. 2019

Pages: 181 - 187

Accepté: 27 mai 2019

DOI: https://doi.org/10.2478/forma-2019-0017

Mots clés
factorial, nominative data, program verification

© 2019 Adrian Jaszczak et al., published by Sciendo

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

Partial Correctness of a Factorial Algorithm

Publié en ligne: 20 juil. 2019

Pages: 181 - 187

Accepté: 27 mai 2019

DOI: https://doi.org/10.2478/forma-2019-0017

Mots clésfactorial, nominative data, program verification

© 2019 Adrian Jaszczak et al., published by Sciendo

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

Mots clés
factorial, nominative data, program verification