<abstract xmlns="http://www.w3.org/1999/xhtml">In the paper we give a formalization in the Mizar system <xref ref-type="bibr" rid="j_forma-2018-0013_ref_002_w2aab3b7b5b1b6b1ab1ab2Aa">[2</xref>, <xref ref-type="bibr" rid="j_forma-2018-0013_ref_001_w2aab3b7b5b1b6b1ab1ab1Aa">1</xref>] of the rules of an inference system for an extended Floyd-Hoare logic with partial pre- and post-conditions which was proposed in <xref ref-type="bibr" rid="j_forma-2018-0013_ref_007_w2aab3b7b5b1b6b1ab1ab7Aa">[7</xref>, <xref ref-type="bibr" rid="j_forma-2018-0013_ref_009_w2aab3b7b5b1b6b1ab1ab9Aa">9</xref>]. The rules are formalized on the semantic level. The details of the approach used to implement this formalization are described in <xref ref-type="bibr" rid="j_forma-2018-0013_ref_005_w2aab3b7b5b1b6b1ab1ab5Aa">[5]</xref>.We formalize the notion of a semantic Floyd-Hoare triple (for an extended Floyd-Hoare logic with partial pre- and post-conditions) <xref ref-type="bibr" rid="j_forma-2018-0013_ref_005_w2aab3b7b5b1b6b1ab1ab5Aa">[5]</xref> which is a triple of a pre-condition represented by a partial predicate, a program, represented by a partial function which maps data to data, and a post-condition, represented by a partial predicate, which informally means that if the pre-condition on a program’s input data is defined and true, and the program’s output after a run on this data is defined (a program terminates successfully), and the post-condition is defined on the program’s output, then the post-condition is true.We formalize and prove the soundness of the rules of the inference system <xref ref-type="bibr" rid="j_forma-2018-0013_ref_009_w2aab3b7b5b1b6b1ab1ab9Aa">[9</xref>, <xref ref-type="bibr" rid="j_forma-2018-0013_ref_007_w2aab3b7b5b1b6b1ab1ab7Aa">7</xref>] for such semantic Floyd-Hoare triples. For reasoning about sequential composition of programs and while loops we use the rules proposed in <xref ref-type="bibr" rid="j_forma-2018-0013_ref_003_w2aab3b7b5b1b6b1ab1ab3Aa">[3]</xref>.The formalized rules can be used for reasoning about sequential programs, and in particular, for sequential programs on nominative data <xref ref-type="bibr" rid="j_forma-2018-0013_ref_004_w2aab3b7b5b1b6b1ab1ab4Aa">[4]</xref>. Application of these rules often requires reasoning about partial predicates representing preand post-conditions which can be done using the formalized results on the Kleene algebra of partial predicates given in <xref ref-type="bibr" rid="j_forma-2018-0013_ref_008_w2aab3b7b5b1b6b1ab1ab8Aa">[8]</xref>.</abstract>

In the paper we give a formalization in the Mizar system [2, 1] of the rules of an inference system for an extended Floyd-Hoare logic with partial pre- and post-conditions which was proposed in [7, 9]. The rules are formalized on the semantic level. The details of the approach used to implement this formalization are described in [5].We formalize the notion of a semantic Floyd-Hoare triple (for an extended Floyd-Hoare logic with partial pre- and post-conditions) [5] which is a triple of a pre-condition represented by a partial predicate, a program, represented by a partial function which maps data to data, and a post-condition, represented by a partial predicate, which informally means that if the pre-condition on a program’s input data is defined and true, and the program’s output after a run on this data is defined (a program terminates successfully), and the post-condition is defined on the program’s output, then the post-condition is true.We formalize and prove the soundness of the rules of the inference system [9, 7] for such semantic Floyd-Hoare triples. For reasoning about sequential composition of programs and while loops we use the rules proposed in [3].The formalized rules can be used for reasoning about sequential programs, and in particular, for sequential programs on nominative data [4]. Application of these rules often requires reasoning about partial predicates representing preand post-conditions which can be done using the formalized results on the Kleene algebra of partial predicates given in [8].

An Inference System of an Extension of Floyd-Hoare Logic for Partial Predicates

Formalized Mathematics

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

{"article-title":"An Inference System of an Extension of Floyd-Hoare Logic for Partial Predicates"}

In the paper we give a formalization in the Mizar system [2, 1] of the rules of an inference system for an extended Floyd-Hoare logic with partial pre- and...

An Inference System of an Extension of Floyd-Hoare Logic for Partial Predicates

Pubblicato online: 24 dic 2018

Pagine: 159 - 164

Accettato: 29 giu 2018

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

Parole chiave
Floyd-Hoare logic, Floyd-Hoare triple, inference rule, program verification

© 2018 Ievgen Ivanov et al., published by Sciendo

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

An Inference System of an Extension of Floyd-Hoare Logic for Partial Predicates

Pubblicato online: 24 dic 2018

Pagine: 159 - 164

Accettato: 29 giu 2018

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

Parole chiaveFloyd-Hoare logic, Floyd-Hoare triple, inference rule, program verification

© 2018 Ievgen Ivanov et al., published by Sciendo

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

Parole chiave
Floyd-Hoare logic, Floyd-Hoare triple, inference rule, program verification