Abstract
In a pure functional language a series of values computed from one another can be considered as different states of the same “abstract object”. For this abstract object temporal properties (e.g. invariants) can be formulated and proved. This paper explains how to define and prove certain kinds of temporal properties of programs written in the pure functional language Clean. Sparkle, a theorem prover designed for Clean, is applied as a tool. Since Sparkle is not capable of handling temporal logical properties, its original version has been extended to support object abstraction, certain temporal properties and a new form of theorems which includes hypotheses. The resulting system is called Sparkle-T. The examples presented in this paper illustrate how object abstraction and the definition and proof of temporal properties can be carried out in Sparkle-T. Furthermore, some novel features of the Sparkle-T system are demonstrated as well.
Supported by the Hungarian National Science Research Grant (OTKA), Grant Nr.T037742 and by the Bolyai Research Scholarship of the Hungarian Academy of Sciences.
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 subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abadi, M., Lamport, L.: Composing specifications. ACM Trans. Program. Lang. Syst. 15(1), 73–132 (1993)
Achten, P., Plasmeijer, R.: Interactive Objects in Clean. In: Clack, C., Hammond, K., Davie, T. (eds.) IFL 1997. LNCS, vol. 1467, pp. 304–321. Springer, Heidelberg (1998)
Butterfield, A.: Reasoning about I/O and Exceptions. In: Grelck, C., Huch, F., Michaelson, G.J., Trinder, P. (eds.) IFL 2004. LNCS, vol. 3474, pp. 33–48. Springer, Heidelberg (2005)
Chandy, K.M., Misra, J.: Parallel Program Design: a Foundation. Addison-Wesley, Reading (1989)
Dam, M., Fredlund, L., Gurov, D.: Toward Parametric Verification of Open Distributed Systems. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, p. 150. Springer, Heidelberg (1998)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall Inc., Englewood Cliffs (1976)
Daxkobler, K., Horváth, Z., Kozsik, T.: A Prototype of CPPCC - Safe Functional Mobile Code in Clean. In: Proceedings of Implementation of Functional Languages 2002, Madrid, Spain, September 15–19, pp. 301–310 (2002)
Dowse, M., Strong, G., Butterfield, A.: Proving Make Correct: I/O Proofs in Haskell and Clean. In: Peña, R., Arts, T. (eds.) IFL 2002. LNCS, vol. 2670, pp. 68–83. Springer, Heidelberg (2003)
Dowse, M., Butterfield, A., van Eekelen, M., de Mol, M., Plasmeijer, R.: Towards Machine-Verified Proofs for I/O. In: Grelck, C., Huch, F., Michaelson, G.J., Trinder, P. (eds.) IFL 2004. LNCS, vol. 3474. Springer, Heidelberg (2005)
Dowse, M., Butterfield, A.: A Language for Reasoning about Concurrent Functional I/O (Draft). In: Grelck, C., Huch, F., Michaelson, G.J., Trinder, P. (eds.) IFL 2004. LNCS, vol. 3474, pp. 129–141. Springer, Heidelberg (2005)
Dowse, M., Butterfield, A., van Eekelen, M.: Reasoning About Deterministic Concurrent Functional I/O. In: Grelck, C., Huch, F., Michaelson, G.J., Trinder, P. (eds.) IFL 2004. LNCS, vol. 3474, pp. 177–194. Springer, Heidelberg (2005)
Home of Clean, http://www.cs.kun.nl/~clean/
Horváth, Z.: The Formal Specification of a Problem Solved by a Parallel Program—a Relational Model. Annales Universitatis Scientiarum Budapestinensis de Rolando Eötvös Nominatae, Sectio Computatorica, Tomus XVII, pp. 173–191 (1998)
Horváth, Z., Achten, P., Kozsik, T., Plasmeijer, R.: Proving the Temporal Properties of the Unique World. In: Proceedings of the Sixth Symposium on Programming Languages and Software Tools, Tallin, Estonia, pp. 113–125 (August 1999)
Horváth, Z., Achten, P., Kozsik, T., Plasmeijer, R.: Verification of the Temporal Properties of Dynamic Clean Processes. In: Koopman, P., Clack, C. (eds.) IFL 1999. LNCS, vol. 1868, pp. 203–218. Springer, Heidelberg (2000)
Horváth, Z., Kozsik, T., Tejfel, M.: Proving Invariants of Functional Programs. In: Proceedings of Eighth Symposium on Programming Languages and Software Tools, Kuopio, Finland, June 17–18, pp. 115–126 (2003)
Horváth, Z., Kozsik, T., Tejfel, M.: Verifying Invariants of Abstract Functional Objects - a case study. In: 6th International Conference on Applied Informatics, Eger, Hungary, January 7–31 (2004)
Kozsik, T., van Arkel, D., Plasmeijer, R.: Subtyping with Strengthening Type Invariants. In: Mohnen, M., Koopman, P. (eds.) IFL 2000. LNCS, vol. 2011, pp. 315–330. Springer, Heidelberg (2001)
Kozsik, T.: Reasoning with Sparkle: a case study. Technical Report, Faculty of Informatics, Eötvös Loránd University, Budapest, Hungary
de Mol, M.: PhD thesis, Radboud University Nijmegen (in preparation)
de Mol, M., van Eekelen, M., Plasmeijer, R.: Theorem Proving for Functional Programmers. In: Arts, T., Mohnen, M. (eds.) IFL 2002. LNCS, vol. 2312, p. 55. Springer, Heidelberg (2002)
Peyton Jones, S., Hughes, J., et al.: Report on the Programming Language Haskell 98, A Non-strict, Purely Functional Language (February 1999)
Plasmeijer, R., van Eekelen, M.: Concurrent Clean Version 2.0 Language Report (2001), http://www.cs.kun.nl/~clean/Manuals/manuals.html
Tejfel, M., Horváth, Z., Kozsik, T.: Extending the Sparkle Core language with object abstraction. Acta Cybernetica 17, 419–445 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tejfel, M., Horváth, Z., Kozsik, T. (2006). Temporal Properties of Clean Programs Proven in Sparkle-T. In: Horváth, Z. (eds) Central European Functional Programming School. CEFP 2005. Lecture Notes in Computer Science, vol 4164. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11894100_6
Download citation
DOI: https://doi.org/10.1007/11894100_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-46843-1
Online ISBN: 978-3-540-46845-5
eBook Packages: Computer ScienceComputer Science (R0)