Abstract
RISCAL is a language for describing mathematical algorithms and formally specifying their behavior with respect to user-defined theories in first-order logic. This language is based on a type system that constrains the size of all types by formal parameters; thus a RISCAL specification denotes an infinite class of models of which every instance has finite size. This allows the RISCAL software to fully automatically check in small instances the validity of theorems and the correctness of algorithms. Our goal is to quickly detect errors respectively inadequacies in the formalization by falsification in small model instances before attempting actual correctness proofs for the whole model class.
Supported by the Johannes Kepler University, Linz Institute of Technology (LIT), project LOGTECHEDU, and by the OEAD WTZ project SK 14/2018 SemTech.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131–146. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14052-5_11
Butler, M., et al. (eds.): Abstract State Machines, Alloy, B, TLA, VDM, and Z. LNCS, vol. 9675. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-319-33600-8
RISCAL: The RISC Algorithm Language (RISCAL), March 2017. https://www.risc.jku.at/research/formal/software/RISCAL
Runciman, C., Naylor, M., Lindblad, F.: Smallcheck and lazy smallcheck: automatic exhaustive testing for small values. In: First ACM SIGPLAN Symposium on Haskell, Haskell 2008, pp. 37–48. ACM, New York (2008). https://doi.org/10.1145/1411286.1411292
Schreiner, W.: The RISC Algorithm Language (RISCAL) – Tutorial and Reference Manual (Version 1.0). Technical report, RISC, Johannes Kepler University, Linz, Austria, March 2017. download from [3]
Schreiner, W., Brunhuemer, A., Fürst, C.: Teaching the formalization of mathematical theories and algorithms via the automatic checking of finite models. In: Post-Proceedings ThEdu’17, Theorem proving components for Educational software. EPTCS, vol. 267, pp. 120–139 (2018). https://doi.org/10.4204/EPTCS.267.8
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Schreiner, W. (2018). Validating Mathematical Theorems and Algorithms with RISCAL. In: Rabe, F., Farmer, W., Passmore, G., Youssef, A. (eds) Intelligent Computer Mathematics. CICM 2018. Lecture Notes in Computer Science(), vol 11006. Springer, Cham. https://doi.org/10.1007/978-3-319-96812-4_21
Download citation
DOI: https://doi.org/10.1007/978-3-319-96812-4_21
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-96811-7
Online ISBN: 978-3-319-96812-4
eBook Packages: Computer ScienceComputer Science (R0)