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

Euclid's Algorithm Revisited

1967 ◽  
Vol 60 (4) ◽  
pp. 358
Author(s):  
B. L. Foster
Keyword(s):  
Automatic Machine ◽  
Greatest Common Divisor ◽  
Machine Computation ◽  
Euclid’S Algorithm ◽  
Integer Division ◽  
Euclid's Algorithm

Since integer division reduces to repeated subtraction, Euclid's algorithm for finding the greatest common divisor may be recast in terms of subtraction. This is done, for example, in Trakhtenbrot,1 for automatic machine computation.

scholarly journals Computational Thinking in Mathematics and Computer Science: What Programming Does to Your Head

2021 ◽  
Vol 11 (1) ◽  
pp. 346-363
Author(s):  
Al Cuoco ◽  
Paul Goldenberg
Keyword(s):  
Computer Science ◽  
Classical Result ◽  
Computational Thinking ◽  
Computer Programs ◽  
The Other ◽  
Greatest Common Divisor ◽  
Euclid’S Algorithm ◽  
And Mathematics ◽  
Euclid's Algorithm

How you think about a phenomenon certainly influences how you create a program to model it. The main point of this essay is that the influence goes both ways: creating programs influences how you think. The programs we are talking about are not just the ones we write for a computer. Programs can be implemented on a computer or with physical devices or in your mind. The implementation can bring your ideas to life. Often, though, the implementation and the ideas develop in tandem, each acting as a mirror on the other. We describe an example of how programming and mathematics come together to inform and shape our interpretation of a classical result in mathematics: Euclid's algorithm that finds the greatest common divisor of two integers.

Ancient Algorithms

2020 ◽  
pp. 9-24
Author(s):  
Chris Bleakley
Keyword(s):  
Prime Numbers ◽  
Pythagorean Theorem ◽  
Greatest Common Divisor ◽  
Stepping Stones ◽  
Euclid’S Algorithm ◽  
Ancient Mesopotamia ◽  
Euclid's Algorithm ◽  
Modern Cryptography

Chapter 1 traces the origins of algorithms from ancient Mesopotamia to Greece in the 2th century BC. The oldest known algorithms were inscribed on clay tablets by the Babylonians more than 4,000 years ago. The clay tablets document algorithms ranging from geometry to accountancy. One tablet in particular - YBC 7289 - indicates knowledge of the Pythagorean Theorem thousands of years before its supposed invention by the ancient Greeks. The Greeks made other advances in algorithms. Euclid’s algorithm determines the greatest common divisor of two numbers. The Sieve of Eratosthenes finds prime numbers. Both algorithms proved to be important stepping stones to modern cryptography - the mathematics of secret messages.

Euclid's Algorithm for the Greatest Common Divisor

2013 ◽  
Author(s):  
Jerry Lodder ◽  
David Pengelley ◽  
Desh Ranjan
Keyword(s):  
Greatest Common Divisor ◽  
Euclid’S Algorithm ◽  
Euclid's Algorithm

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

2. Multiplying and dividing

2020 ◽  
pp. 14-37
Author(s):  
Robin Wilson
Keyword(s):  
Number Theory ◽  
Greatest Common Divisor ◽  
Common Multiple ◽  
Least Common Multiple ◽  
Euclid’S Algorithm ◽  
Division Rule ◽  
Perfect Squares ◽  
Euclid's Algorithm

‘Multiplying and dividing’ looks at multiples and divisors, focusing on the least common multiple and greatest common divisor of two numbers. We use Euclid’s algorithm as a method for computing the greatest common divisor of two numbers by using the division rule repeatedly. Perfect squares (integers that are the product of two equal integers) feature throughout number theory. Tests are given for divisibility by certain small numbers. An ancient method called ‘casting out nines’, was developed in India in around the year 1000, based on the argument that a number and its digital sum leave the same remainder when divided by 9. We can still use this method to verify the accuracy (or otherwise) of arithmetical calculations.

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

2018 ◽  
Vol 26 (2) ◽  
pp. 159-164
Author(s):  
Ievgen Ivanov ◽  
Artur Korniłowicz ◽  
Mykola Nikitchenko
Keyword(s):  
Input Data ◽  
Partial Function ◽  
Hoare Logic ◽  
Sequential Programs ◽  
Inference System ◽  
Semantic Level ◽  
System 2 ◽  
Partial Predicate ◽  
Partial Predicates ◽  
Post Condition

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

Sign in / Sign up

Export Citation Format

Share Document