scholarly journals Partial Correctness of a Factorial Algorithm

2019 ◽  
Vol 27 (2) ◽  
pp. 181-187
Author(s):  
Adrian Jaszczak ◽  
Artur Korniłowicz
Keyword(s):  
Formal Verification ◽  
Natural Number ◽  
Hoare Logic ◽  
Inference System ◽  
Partial Correctness ◽  
Complex Valued

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].

scholarly journals Partial Correctness of a Power Algorithm

2019 ◽  
Vol 27 (2) ◽  
pp. 189-195
Author(s):  
Adrian Jaszczak
Keyword(s):  
Formal Verification ◽  
Complex Number ◽  
Hoare Logic ◽  
Inference System ◽  
Partial Correctness ◽  
Complex Valued

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

scholarly journals Partial Correctness of a Fibonacci Algorithm

2020 ◽  
Vol 28 (2) ◽  
pp. 187-196
Author(s):  
Artur Korniłowicz
Keyword(s):  
Fibonacci Number ◽  
Iterative Algorithms ◽  
Hoare Logic ◽  
Inference System ◽  
Partial Correctness ◽  
Complex Valued

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].

scholarly journals Partial Correctness of GCD Algorithm

2018 ◽  
Vol 26 (2) ◽  
pp. 165-173
Author(s):  
Ievgen Ivanov ◽  
Artur Korniłowicz ◽  
Mykola Nikitchenko
Keyword(s):  
Greatest Common Divisor ◽  
Hoare Logic ◽  
Natural Numbers ◽  
Inference System ◽  
Partial Correctness ◽  
Euclid’S Algorithm ◽  
System 2 ◽  
Euclid's Algorithm ◽  
Complex Valued

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].

scholarly journals Reasoning about Partial Correctness Assertions in Isabelle/HOL

2020 ◽  
Vol 27 (3) ◽  
pp. 84-101
Author(s):  
Alfio Ricardo Martini
Keyword(s):  
Formal Verification ◽  
Broad Class ◽  
Object Oriented ◽  
Concurrent Programs ◽  
Proof Assistant ◽  
Hoare Logic ◽  
Partial Correctness ◽  
Human Understanding ◽  
Isabelle Proof Assistant

Hoare Logic has a long tradition in formal verification and has been continuously developed and used to verify a broad class of programs, including sequential, object-oriented and concurrent programs. The purpose of this work is to provide a detailed and accessible exposition of the several ways the user can conduct, explore and write proofs of correctness of sequential imperative programs with Hoare logic and the ISABELLE proof assistant. With the proof language Isar, it is possible to write structured, readable proofs that are suitable for human understanding and communication.

scholarly journals General Theory and Tools for Proving Algorithms in Nominative Data Systems

2020 ◽  
Vol 28 (4) ◽  
pp. 269-278
Author(s):  
Adrian Jaszczak
Keyword(s):  
General Theory ◽  
Iterative Algorithms ◽  
Data Systems ◽  
Hoare Logic ◽  
Inference System ◽  
The Future ◽  
Complex Valued

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].

scholarly journals Natural Hoare Logic: Towards formal verification of programs from logical forms of natural language specifications

2021 ◽  
Author(s):  
Jayaraj Poroor
Keyword(s):  
Natural Language ◽  
Formal Verification ◽  
Domain Knowledge ◽  
Semantic Content ◽  
Hoare Logic ◽  
Critical Systems ◽  
Semantic Parsing ◽  
Natural Language Text ◽  
Safety Requirements ◽  
Formal Framework

Formal verification provides strong guarantees of correctness of software, which are especially important in safety or security critical systems. Hoare logic is a widely used formalism for rigorous verification of software against specifications in the form of pre-condition/post-condition assertions. The advancement of semantic parsing techniques and higher computational capabilities enable us to extract semantic content from natural language text as formal logical forms, with increasing accuracy and coverage. This paper proposes a formal framework for Hoare logic-based formal verification of imperative programs using logical forms generated from compositional semantic parsing of natural language assertions. We call our reasoning approach Natural Hoare Logic. This enables formal verification of software directly against safety requirements specified by a domain expert in natural language. We consider both declarative assertions of program invariants and state change as well as imperative assertions that specify commands which alter the program state. We discuss how the reasoning approach can be extended using domain knowledge and a practical approach for guarding against semantic parser errors.

scholarly journals On incorrectness logic and Kleene algebra with top and tests

2022 ◽  
Vol 6 (POPL) ◽  
pp. 1-30
Author(s):  
Cheng Zhang ◽  
Arthur Azevedo de Amorim ◽  
Marco Gaboardi
Keyword(s):  
Equational Theory ◽  
Program Transformations ◽  
Hoare Logic ◽  
Compiler Optimizations ◽  
Partial Correctness ◽  
Seminal Work ◽  
Kleene Algebra

Kleene algebra with tests (KAT) is a foundational equational framework for reasoning about programs, which has found applications in program transformations, networking and compiler optimizations, among many other areas. In his seminal work, Kozen proved that KAT subsumes propositional Hoare logic, showing that one can reason about the (partial) correctness of while programs by means of the equational theory of KAT. In this work, we investigate the support that KAT provides for reasoning about incorrectness, instead, as embodied by O'Hearn's recently proposed incorrectness logic. We show that KAT cannot directly express incorrectness logic. The main reason for this limitation can be traced to the fact that KAT cannot express explicitly the notion of codomain, which is essential to express incorrectness triples. To address this issue, we study Kleene Algebra with Top and Tests (TopKAT), an extension of KAT with a top element. We show that TopKAT is powerful enough to express a codomain operation, to express incorrectness triples, and to prove all the rules of incorrectness logic sound. This shows that one can reason about the incorrectness of while-like programs by means of the equational theory of TopKAT.

Sign in / Sign up

Export Citation Format

Share Document