Abstract
We describe a formalization of the nominative algorithmic algebra in the Mizar proof assistant. This algebra is a generalization of Glushkov algorithmic algebras which is well suited for representing semantics and specifying properties of programs on complex data structures which interact with external environment in convenient and unified way. We describe formal definitions and formally proven and checked statements about the carrier sets and operations (program compositions) of this algebra. The obtained results are useful for implementing methods of automated verification of software, for example, for the Internet of Things (IoT) and ensuring safety of IoT systems.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
International Telecommunication Union: Overview of the Internet of Things. ITU-T Recommendation Y.4000/Y.2060, June 2012. http://handle.itu.int/11.1002/1000/11559
Wiedijk, F. (ed.): The Seventeen Provers of the World. Lecture Notes in Artificial Intelligence, vol. 3600. Springer, Heidelberg (2006)
The CompCert project. http://compcert.inria.fr
CakeML: A verified implementation of ML. https://cakeml.org
The seL4 Microkernel. https://sel4.systems
CertiKOS: an extensible architecture for building certified concurrent OS kernels. In: OSDI 2016 Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation, Savannah, GA, USA, 2–4 November 2016 (2016)
Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002)
Kryvolap, A., Nikitchenko, M., Schreiner, W.: Extending Floyd-Hoare logic for partial pre- and postconditions. Communications in Computer and Information Science, vol. 412, pp. 355–378. Springer (2013). http://dx.doi.org/10.1007/978-3-319-03998-5_18
Korniłowicz, A., Kryvolap, A., Nikitchenko, M., Ivanov, I.: An approach to formalization of an extension of Floyd-Hoare logic. In: Proceedings of the 13th International Conference on ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer (ICTERI 2017), Kyiv, Ukraine, 15–18 May 2017. CEUR-WS.org (2017). http://ceur-ws.org/Vol-1844/10000504.pdf
Nikitchenko, N.S.: A composition nominative approach to program semantics, IT-TR 1998-020. Technical report, Technical University of Denmark (1998)
Glushkov, V.: Automata theory and formal transformations of microprograms. Cybernetics 5, 3–10 (1965). (in Russian)
Floyd, R.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science, vol. 19, pp. 19–32 (1967)
Hoare, C.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969). doi:10.1145/363235.363259
Nikitchenko, M., Shkilniak, S.: Algebras and logics of partial quasiary predicates. Algebra Discret. Math. 23(2), 263–278 (2017)
Skobelev, V., Nikitchenko, M., Ivanov, I.: On algebraic properties of nominative data and functions. Commun. Comput. Inf. Sci. 469, 117–138 (2014). doi:10.1007/978-3-319-13206-8_6
Grabowski, A., Korniłowicz, A., Naumowicz, A.: Four decades of Mizar. J. Autom. Reason. 55(3), 191–198 (2015). doi:10.1007/s10817-015-9345-1
Korniłowicz, A., Kryvolap, A., Nikitchenko, M., Ivanov, I.: Formalization of the algebra of nominative data in Mizar. In: 2017 Federated Conference on Computer Science and Information Systems (2017, accepted)
Bancerek, G., Byliński, C., Grabowski, A., Korniłowicz, A., Matuszewski, R., Naumowicz, A., Pąk, K., Urban, J.: Mizar: state-of-the-art and beyond. In: Intelligent Computer Mathematics – International Conference, CICM 2015, Proceedings, Washington, DC, USA, pp. 261–279 (2015). http://dx.doi.org/10.1007/978-3-319-20615-8_17
Grabowski, A., Korniłowicz, A., Schwarzweller, C.: Equality in computer proof assistants. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) Proceedings of the 2015 Federated Conference on Computer Science and Information Systems. Annals of Computer Science and Information Systems, vol. 5, pp. 45–54. IEEE (2015). http://dx.doi.org/10.15439/2015F229
Byliński, C.: Partial functions. Formaliz. Math. 1(2), 357–367 (1990)
Byliński, C.: Some basic properties of sets. Formaliz. Math. 1(1), 47–53 (1990)
Bancerek, G., Trybulec, A.: Miscellaneous facts about functions. Formaliz. Math. 5(4), 485–492 (1996)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG
About this paper
Cite this paper
Korniłowicz, A., Kryvolap, A., Nikitchenko, M., Ivanov, I. (2018). Formalization of the Nominative Algorithmic Algebra in Mizar. In: Świątek, J., Borzemski, L., Wilimowska, Z. (eds) Information Systems Architecture and Technology: Proceedings of 38th International Conference on Information Systems Architecture and Technology – ISAT 2017. ISAT 2017. Advances in Intelligent Systems and Computing, vol 656. Springer, Cham. https://doi.org/10.1007/978-3-319-67229-8_16
Download citation
DOI: https://doi.org/10.1007/978-3-319-67229-8_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-67228-1
Online ISBN: 978-3-319-67229-8
eBook Packages: EngineeringEngineering (R0)