Relevant bibliographies by topics / Floyd-Hoare logic

Contents

  1. Journal articles
  2. Dissertations / Theses
  3. Book chapters

Academic literature on the topic 'Floyd-Hoare logic'

Author: Grafiati
Published: 4 June 2021
Last updated: 13 February 2022

Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles

Select a source type:

Consult the lists of relevant articles, books, theses, conference reports, and other scholarly sources on the topic 'Floyd-Hoare logic.'

Next to every source in the list of references, there is an 'Add to bibliography' button. Press on it, and we will generate automatically the bibliographic reference to the chosen work in the citation style you need: APA, MLA, Harvard, Chicago, Vancouver, etc.

You can also download the full text of the academic publication as pdf and read online its abstract whenever available in the metadata.

Journal articles on the topic "Floyd-Hoare logic"

1

Bloom, Stephen L., and Zoltán Ésik. "Floyd-Hoare logic in iteration theories." Journal of the ACM (JACM) 38, no. 4 (1991): 887–934. http://dx.doi.org/10.1145/115234.115352.

Full text
APA, Harvard, Vancouver, ISO, and other styles
2

Ying, Mingsheng. "Floyd--hoare logic for quantum programs." ACM Transactions on Programming Languages and Systems 33, no. 6 (2011): 1–49. http://dx.doi.org/10.1145/2049706.2049708.

Full text
APA, Harvard, Vancouver, ISO, and other styles
3

NIKITCHENKO, Mykola, and Andrii KRYVOLAP. "Properties of Inference Systems for Floyd-Hoare Logic with Partial Predicates." Acta Electrotechnica et Informatica 13, no. 4 (2013): 70–78. http://dx.doi.org/10.15546/aeei-2013-0052.

Full text
APA, Harvard, Vancouver, ISO, and other styles
4

Ivanov, Ievgen, Artur Korniłowicz, and Mykola Nikitchenko. "An Inference System of an Extension of Floyd-Hoare Logic for Partial Predicates." Formalized Mathematics 26, no. 2 (2018): 159–64. http://dx.doi.org/10.2478/forma-2018-0013.

Full text
Abstract:
Summary 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].
APA, Harvard, Vancouver, ISO, and other styles
5

Ivanov, Ievgen, Artur Korniłowicz, and Mykola Nikitchenko. "Partial Correctness of GCD Algorithm." Formalized Mathematics 26, no. 2 (2018): 165–73. http://dx.doi.org/10.2478/forma-2018-0014.

Full text
Abstract:
Summary 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].
APA, Harvard, Vancouver, ISO, and other styles
6

Jaszczak, Adrian. "General Theory and Tools for Proving Algorithms in Nominative Data Systems." Formalized Mathematics 28, no. 4 (2020): 269–78. http://dx.doi.org/10.2478/forma-2020-0024.

Full text
Abstract:
Summary In this paper we introduce some new definitions for sequences of operations and extract general theorems about properties of iterative algorithms encoded in nominative data language [20] in the Mizar system [3], [1] in order to simplify the process of proving algorithms in the future. This paper continues verification of algorithms [10], [13], [12], [14] written in terms of simple-named complex-valued nominative data [6], [8], [18], [11], [15], [16]. 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 postconditions [17], [19], [7], [5].
APA, Harvard, Vancouver, ISO, and other styles
7

Korniłowicz, Artur. "Partial Correctness of a Fibonacci Algorithm." Formalized Mathematics 28, no. 2 (2020): 187–96. http://dx.doi.org/10.2478/forma-2020-0016.

Full text
Abstract:
Summary 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 := 0 s := 0 b := 1 c := 0 while (i <> n) c := s s := b b := c + s i := i + 1 return 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].
APA, Harvard, Vancouver, ISO, and other styles
8

Sain, Ildikó. "An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic." Notre Dame Journal of Formal Logic 30, no. 4 (1989): 563–73. http://dx.doi.org/10.1305/ndjfl/1093635239.

Full text
APA, Harvard, Vancouver, ISO, and other styles
9

Jaszczak, Adrian. "Partial Correctness of an Algorithm Computing Lucas Sequences." Formalized Mathematics 28, no. 4 (2020): 279–88. http://dx.doi.org/10.2478/forma-2020-0025.

Full text
Abstract:
Summary In this paper we define some properties about finite sequences and verify the partial correctness of an algorithm computing n-th element of Lucas sequence [23], [20] with given P and Q coefficients as well as two first elements (x and y). The algorithm is encoded in nominative data language [22] in the Mizar system [3], [1]. i := 0 s := x b := y c := x while (i <> n) c := s s := b ps := p*s qc := q*c b := ps − qc i := i + j return s This paper continues verification of algorithms [10], [14], [12], [15], [13] written in terms of simple-named complex-valued nominative data [6], [8], [19], [11], [16], [17]. 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 [18], [21], [7], [5].
APA, Harvard, Vancouver, ISO, and other styles
10

Jaszczak, Adrian, and Artur Korniłowicz. "Partial Correctness of a Factorial Algorithm." Formalized Mathematics 27, no. 2 (2019): 181–87. http://dx.doi.org/10.2478/forma-2019-0017.

Full text
Abstract:
Summary 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].
APA, Harvard, Vancouver, ISO, and other styles

Dissertations / Theses on the topic "Floyd-Hoare logic"

1

Lundberg, Didrik. "Provably Sound and Secure Automatic Proving and Generation of Verification Conditions." Thesis, KTH, Teoretisk datalogi, TCS, 2018. http://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-239441.

Full text
Abstract:
Formal verification of programs can be done with the aid of an interactive theorem prover. The program to be verified is represented in an intermediate language representation inside the interactive theorem prover, after which statements and their proofs can be constructed. This is a process that can be automated to a high degree. This thesis presents a proof procedure to efficiently generate a theorem stating the weakest precondition for a program to terminate successfully in a state upon which a certain postcondition is placed. Specifically, the Poly/ML implementation of the SML metalanguage is used to generate a theorem in the HOL4 interactive theorem prover regarding the properties of a program written in BIR, an abstract intermediate representation of machine code used in the PROSPER project.<br>Bevis av säkerhetsegenskaper hos program genom formell verifiering kan göras med hjälp av interaktiva teorembevisare. Det program som skall verifieras representeras i en mellanliggande språkrepresentation inuti den interaktiva teorembevisaren, varefter påståenden kan konstrueras, som sedan bevisas. Detta är en process som kan automatiseras i hög grad. Här presenterar vi en metod för att effektivt skapa och bevisa ett teorem som visar sundheten hos den svagaste förutsättningen för att ett program avslutas framgångsrikt under ett givet postvillkor. Specifikt använder vi Poly/ML-implementationen av SML för att generera ett teorem i den interaktiva teorembevisaren HOL4 som beskriver egenskaper hos ett program i BIR, en abstrakt mellanrepresentation av maskinkod som används i PROSPER-projektet.
APA, Harvard, Vancouver, ISO, and other styles

Book chapters on the topic "Floyd-Hoare logic"

1

Bloom, Stephen L., and Zoltán Ésik. "Floyd-Hoare Logic." In Iteration Theories. Springer Berlin Heidelberg, 1993. http://dx.doi.org/10.1007/978-3-642-78034-9_15.

Full text
APA, Harvard, Vancouver, ISO, and other styles
2

Roşu, Grigore, Chucky Ellison, and Wolfram Schulte. "Matching Logic: An Alternative to Hoare/Floyd Logic." In Algebraic Methodology and Software Technology. Springer Berlin Heidelberg, 2011. http://dx.doi.org/10.1007/978-3-642-17796-5_9.

Full text
APA, Harvard, Vancouver, ISO, and other styles
3

Nikitchenko, Mykola, Ievgen Ivanov, Artur Korniłowicz, and Andrii Kryvolap. "Extended Floyd-Hoare Logic over Relational Nominative Data." In Information and Communication Technologies in Education, Research, and Industrial Applications. Springer International Publishing, 2018. http://dx.doi.org/10.1007/978-3-319-76168-8_3.

Full text
APA, Harvard, Vancouver, ISO, and other styles
4

Gaboardi, Marco, Shin-ya Katsumata, Dominic Orchard, and Tetsuya Sato. "Graded Hoare Logic and its Categorical Semantics." In Programming Languages and Systems. Springer International Publishing, 2021. http://dx.doi.org/10.1007/978-3-030-72019-3_9.

Full text
Abstract:
AbstractDeductive verification techniques based on program logics (i.e., the family of Floyd-Hoare logics) are a powerful approach for program reasoning. Recently, there has been a trend of increasing the expressive power of such logics by augmenting their rules with additional information to reason about program side-effects. For example, general program logics have been augmented with cost analyses, logics for probabilistic computations have been augmented with estimate measures, and logics for differential privacy with indistinguishability bounds. In this work, we unify these various approaches via the paradigm of grading, adapted from the world of functional calculi and semantics. We propose Graded Hoare Logic (GHL), a parameterisable framework for augmenting program logics with a preordered monoidal analysis. We develop a semantic framework for modelling GHL such that grading, logical assertions (pre- and post-conditions) and the underlying effectful semantics of an imperative language can be integrated together. Central to our framework is the notion of a graded category which we extend here, introducing graded Freyd categories which provide a semantics that can interpret many examples of augmented program logics from the literature. We leverage coherent fibrations to model the base assertion language, and thus the overall setting is also fibrational.
APA, Harvard, Vancouver, ISO, and other styles
5

Kryvolap, Andrii, Mykola Nikitchenko, and Wolfgang Schreiner. "Extending Floyd-Hoare Logic for Partial Pre- and Postconditions." In Information and Communication Technologies in Education, Research, and Industrial Applications. Springer International Publishing, 2013. http://dx.doi.org/10.1007/978-3-319-03998-5_18.

Full text
APA, Harvard, Vancouver, ISO, and other styles
6

Ivanov, Ievgen, and Mykola Nikitchenko. "Inference Rules for the Partial Floyd-Hoare Logic Based on Composition of Predicate Complement." In Information and Communication Technologies in Education, Research, and Industrial Applications. Springer International Publishing, 2019. http://dx.doi.org/10.1007/978-3-030-13929-2_4.

Full text
APA, Harvard, Vancouver, ISO, and other styles
We offer discounts on all premium plans for authors whose works are included in thematic literature selections. Contact us to get a unique promo code!

To the bibliography