<abstract xmlns="http://www.w3.org/1999/xhtml"><p>In this paper we present a formalization in the Mizar system <xref ref-type="bibr" rid="j_forma-2018-0014_ref_002_w2aab3b7b6b1b6b1ab1ab2Aa">[2</xref>, <xref ref-type="bibr" rid="j_forma-2018-0014_ref_001_w2aab3b7b6b1b6b1ab1ab1Aa">1</xref>] of the correctness of the subtraction-based version of Euclid’s algorithm computing the greatest common divisor of natural numbers. The algorithm is written in terms of simple-named complex-valued nominative data <xref ref-type="bibr" rid="j_forma-2018-0014_ref_011_w2aab3b7b6b1b6b1ab1ac11Aa">[11</xref>, <xref ref-type="bibr" rid="j_forma-2018-0014_ref_004_w2aab3b7b6b1b6b1ab1ab4Aa">4]</xref>.</p><p>The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data <xref ref-type="bibr" rid="j_forma-2018-0014_ref_007_w2aab3b7b6b1b6b1ab1ab7Aa">[7]</xref>. Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic with partial pre- and post-conditions <xref ref-type="bibr" rid="j_forma-2018-0014_ref_008_w2aab3b7b6b1b6b1ab1ab8Aa">[8</xref>, <xref ref-type="bibr" rid="j_forma-2018-0014_ref_010_w2aab3b7b6b1b6b1ab1ac10Aa">10</xref>, <xref ref-type="bibr" rid="j_forma-2018-0014_ref_005_w2aab3b7b6b1b6b1ab1ab5Aa">5</xref>, <xref ref-type="bibr" rid="j_forma-2018-0014_ref_003_w2aab3b7b6b1b6b1ab1ab3Aa">3</xref>].</p></abstract>

In this paper we present a formalization in the Mizar system [2, 1] of the correctness of the subtraction-based version of Euclid’s algorithm computing the greatest common divisor of natural numbers. The algorithm is written in terms of simple-named complex-valued nominative data [11, 4].The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data [7]. Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic with partial pre- and post-conditions [8, 10, 5, 3].

Partial Correctness of GCD Algorithm

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

{"article-title":"Partial Correctness of GCD Algorithm"}

In this paper we present a formalization in the Mizar system [2, 1] of the correctness of the subtraction-based version of Euclid’s algorithm computing the...

Partial Correctness of GCD Algorithm

Publicado en línea: 24 dic 2018

Páginas: 165 - 173

Aceptado: 29 jun 2018

DOI: https://doi.org/10.2478/forma-2018-0014

Palabras clave
greatest common divisor, nominative data, program verification

© 2018 Ievgen Ivanov et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Partial Correctness of GCD Algorithm

Publicado en línea: 24 dic 2018

Páginas: 165 - 173

Aceptado: 29 jun 2018

DOI: https://doi.org/10.2478/forma-2018-0014

Palabras clavegreatest common divisor, nominative data, program verification

© 2018 Ievgen Ivanov et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Palabras clave
greatest common divisor, nominative data, program verification