Verifying an infinite systolic algorithm using third-order equational methods. (English) Zbl 1101.68056
Summary: We consider using third-order equational methods to formally verify that an infinite systolic algorithm correctly implements a family of convolution functions. The detailed case study we present illustrates the use of third-order algebra as a formal framework for developing families of computing systems. It also provides an interesting insight into the use of infinite algorithms as a means of verifying a family of finite algorithms. We consider using purely equational reasoning in our verification proofs and in particular, using the rule of free variable induction. We conclude by considering how our verification proofs can be automated using rewriting techniques.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68M07 | Mathematical problems of computer architecture |
Software:
ELANReferences:
| [1] | Allenby, R. B.J. T., Rings, Fields and Groups: An Introduction to Abstract Algebra (1991), Edward Arnold: Edward Arnold Hodder and Stoughton · Zbl 0726.00001 |
| [2] | Broy, M., Equational specification of partial higher-order algebras, (Broy, M., Logic of Programming and Calculi of Discrete Design (1987), Springer-Verlag: Springer-Verlag Berlin) · Zbl 0625.68022 |
| [5] | Ehrig, H.; Mahr, B., (Fundamentals of Algebraic Specification 1—Equations and Initial Semantics. Fundamentals of Algebraic Specification 1—Equations and Initial Semantics, EATCS Monographs on Theoretical Computer Science, vol. 6 (1985), Springer-Verlag: Springer-Verlag Berlin) · Zbl 0557.68013 |
| [6] | Gougen, J. A., Proving and rewriting, (Second International Conference on Algebraic and Logic Programming. Second International Conference on Algebraic and Logic Programming, Lecture Notes in Computing Science, vol. 463 (1990), Springer-Verlag: Springer-Verlag Berlin), 1-24 · Zbl 1496.03045 |
| [7] | Kosiuczenko, P.; Meinke, K., On the power of higher-order algebraic specifications, Information and Computation, 124, 1, 85-101 (1995) · Zbl 0844.68082 |
| [8] | Kung, H. T., Why systolic architectures?, Computer, 15, 1, 37-46 (1982) |
| [9] | Loeckx, J.; Ehrich, H.-D.; Wolf, M., Specification of Abstract Data Types (1996), Wiley: Wiley New York · Zbl 0868.68077 |
| [10] | Maibaum, T. S.E.; Lucena, C. J., Higher-order data types, International Journal of Computer and Information Sciences, 9, 31-53 (1980) · Zbl 0425.68026 |
| [12] | McConnell, B.; Tucker, J. V., Infinite synchronous concurrent algorithms: the specification and verification of a hardware stack, (Bauer, F. L.; Brauer, W.; Schwichtenberg, H., Proceedings of NATO Summer School 1991 at Marktoberdorf, in Logic and Algebra of Specification (1993), Springer-Verlag: Springer-Verlag Berlin), 321-375 |
| [13] | Meinke, K., Universal algebra in higher types, Theoretical Computer Science, 100, 385-417 (1992) · Zbl 0777.08008 |
| [14] | Meinke, K., Higher-order equational logic for specification, simulation and testing, (Dowek, G.; etal., Proceedings of HOA ’95. Proceedings of HOA ’95, Lecture Notes in Computing Science, vol. 1072 (1996), Springer-Verlag: Springer-Verlag Berlin), 124-143 · Zbl 1407.68310 |
| [15] | Meinke, K., A completeness theorem for the expressive power of higher-order algebraic specifications, Journal of Computer and System Sciences, 54, 3, 502-519 (1997) · Zbl 0906.68095 |
| [16] | Meinke, K.; Tucker, J. V., Universal algebra, (Abramsky, S.; Gabbay, D.; Maibaum, T. S.E., Handbook of Logic in Computer Science, vol. I (1993), Oxford University Press: Oxford University Press Oxford), 189-412 |
| [17] | Meinke, K.; Steggles, L. J., Specification and verification in higher order algebra: a case study of convolution, (Heering, J.; etal., Proceedings of HOA ’93. Proceedings of HOA ’93, Lecture Notes in Computing Science, vol. 816 (1994), Springer-Verlag: Springer-Verlag Berlin), 189-222 |
| [18] | Meinke, K.; Steggles, L. J., Correctness of dataflow and systolic algorithms using algebras of streams, Acta Informatica, 38, 45-88 (2001) · Zbl 1032.68106 |
| [19] | Möller, B., Algebraic specifications with higher-order operators, (Meertens, L. G.L. T., Program Specification and Transformation (1987), North-Holland: North-Holland Amsterdam) |
| [20] | Möller, B.; Tarlecki, A.; Wirsing, M., Algebraic specifications of reachable higher-order algebras, (Sannella, D.; Tarlecki, A., Recent Trends in Data Type Specification. Recent Trends in Data Type Specification, Lecture Notes in Computing Science, vol. 332 (1988), Springer-Verlag: Springer-Verlag Berlin), 154-169 · Zbl 0659.68027 |
| [21] | Poigné, A., Higher-order data structures—Cartesian closure versus \(λ\)-calculus, (Proceedings of Symposium on Theoretical Aspects of Computer Science. Proceedings of Symposium on Theoretical Aspects of Computer Science, Lecture Notes in Computing Science, vol. 166 (1984), Springer-Verlag: Springer-Verlag Berlin), 174-185 · Zbl 0575.68018 |
| [22] | Poigné, A., On specifications, theories and models with higher types, Information and Control, 68, 1-46 (1986) · Zbl 0591.68019 |
| [23] | Qian, Z., An algebraic semantics of higher-order types with subtypes, Acta Informatica, 30, 569-607 (1993) · Zbl 0790.68079 |
| [25] | Steggles, L. J., Parameterised higher-order algebraic specifications, (Hanus, M.; Heering, J.; Meinke, K., Proceedings of HOA ’97. Proceedings of HOA ’97, Lecture Notes in Computing Science, vol. 1298 (1997), Springer-Verlag: Springer-Verlag Berlin), 76-98 · Zbl 0884.68087 |
| [26] | Steggles, L. J., Specifying and verifying real-time systems using second-order algebraic methods: a case study of the railroad crossing controller, Journal of Universal Computer Science, 6, 4, 460-473 (2000) · Zbl 0960.68114 |
| [27] | Stephens, R., A survey of stream processing, Acta Informatica, 34, 7, 491-541 (1997) · Zbl 0879.68026 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
