Partial Correctness of a Power Algorithm
| Autor: | Adrian Jaszczak |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
68q60
Correctness nominative data 03b70 Applied Mathematics 020207 software engineering 0102 computer and information sciences 02 engineering and technology 01 natural sciences 68t37 Power (physics) power program verification Computational Mathematics 03b35 Computer engineering 010201 computation theory & mathematics QA1-939 0202 electrical engineering electronic engineering information engineering Mathematics |
| Zdroj: | Formalized Mathematics, Vol 27, Iss 2, Pp 189-195 (2019) |
| ISSN: | 1898-9934 1426-2630 |
| Popis: | 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]. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|