Partial Correctness of a Fibonacci Algorithm
| Autor: | Artur Korniłowicz |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
Discrete mathematics
68q60 Fibonacci number Correctness nominative data 03b70 Applied Mathematics 020207 software engineering 0102 computer and information sciences 02 engineering and technology 01 natural sciences program verification fibonacci sequence Computational Mathematics 03b35 010201 computation theory & mathematics QA1-939 0202 electrical engineering electronic engineering information engineering Mathematics |
| Zdroj: | Formalized Mathematics, Vol 28, Iss 2, Pp 187-196 (2020) |
| ISSN: | 1898-9934 1426-2630 |
| Popis: | 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]. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|