General Theory and Tools for Proving Algorithms in Nominative Data Systems
| Autor: | Adrian Jaszczak |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
68q60
Theoretical computer science nominative data 03b70 Applied Mathematics inference rules 020207 software engineering 0102 computer and information sciences 02 engineering and technology 68v20 Nominative case 01 natural sciences program verification Computational Mathematics General theory 010201 computation theory & mathematics QA1-939 0202 electrical engineering electronic engineering information engineering Data system Rule of inference Mathematics |
| Zdroj: | Formalized Mathematics, Vol 28, Iss 4, Pp 269-278 (2020) |
| ISSN: | 1898-9934 |
| Popis: | 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]. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|