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

Sign in / Sign up

Export Citation Format

Share Document