The Feasibility of Interactively Probing Quiescent Properties of GUI Applications

  • Peter Achten
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3474)


In this paper we explore how application-users can, in an interactive way, test properties about the state of GUI applications that can be classified as local state transition systems with quiescence. These properties can be added and removed at run-time. It is guaranteed that they are type-correct. We investigate the consequences of such an approach for one particular functional GUI library, Object I/O. The goal is to gain confidence in the quality of interactive applications, and to seek properties that can be proven correct, perhaps using formal proof tools.


Graphical User Interface Concrete Object Proof Obligation Functional Language Dynamic Type 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Achten, P., Jones, S.P.: Porting the Clean Object I/O library to Haskell. In: Mohnen, M., Koopman, P. (eds.) IFL 2000. LNCS, vol. 2011, pp. 194–213. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  2. 2.
    Achten, P., Plasmeijer, R.: Interactive Functional Objects in Clean. In: Clack, C., Hammond, K., Davie, T. (eds.) IFL 1997. LNCS, vol. 1467, pp. 304–321. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  3. 3.
    Achten, P., Plasmeijer, R.: The implementation of interactive local state transition systems in Clean. In: Koopman, P., Clack, C. (eds.) IFL 1999. LNCS, vol. 1868, pp. 115–130. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  4. 4.
    Achten, P., Wierich, M.: A Tutorial to the Clean Object I/O Library - Version 1.2. Technical Report CSI-R0003, Computing Science Institute, Faculty of Mathematics and Informatics, University of Nijmegen, The Netherlands, p. 294 (February 2000)Google Scholar
  5. 5.
    Angelov, K.: ObjectIO for Haskell. Description and Sources at,, Applications at, / (2003)
  6. 6.
    Barendsen, E., Smetsers, S.: Uniqueness typing for functional languages with graph rewriting semantics. Mathematical Structures in Computer Science 6, 579–612 (1996)zbMATHMathSciNetGoogle Scholar
  7. 7.
    Chitil, O., McNeill, D., Runciman, C.: Lazy Assertions. In: Trinder, P., Michaelson, G.J., Peña, R. (eds.) IFL 2003. LNCS, vol. 3145, pp. 31–46. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  8. 8.
    Chitil, O., Runciman, C., Wallace, M.: Freja, Hat and Hood – A Comparative Evaluation of Three Systems for Tracing and Debugging Lazy Functional Programs. In: Mohnen, M., Koopman, P. (eds.) IFL 2000. LNCS, vol. 2011, pp. 176–193. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  9. 9.
    de Mol, M., van Eekelen, M., Plasmeijer, R.: Theorem proving for functional programmers - Sparkle: A functional theorem prover. In: Arts, T., Mohnen, M. (eds.) IFL 2002. LNCS, vol. 2312, pp. 55–72. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  10. 10.
    Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the Design of JML Accomodates Both Runtime Assertion Checking and Formal Verification. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 262–284. Springer, Heidelberg (2003); Also available as Technical Report TR 03-04a, Department of Computer Science, 226 Atanasoff Hall, Iowa State University, Ames, Iowa, USAGoogle Scholar
  11. 11.
    Leroy, X.: The Objective Caml system – release 3.08; Documentation and user’s manual. Institut National de Recherche en Informatique et en Automatique (July 2004)Google Scholar
  12. 12.
    Meyer, B.: Eiffel: The Language. Prentice-Hall, Englewood Cliffs (1992)zbMATHGoogle Scholar
  13. 13.
    Jones, S.P., Gordon, A., Finne, S.: Concurrent Haskell. In: 23rd ACM Symposium on Principles of Programming Languages (POPL 1996), St.Petersburg Beach, Florida, pp. 295–308. ACM, New York (1996)CrossRefGoogle Scholar
  14. 14.
    Jones, S.P., Hughes, J., et al.: Report on the programming language Haskell 98. University of Yale (1999),
  15. 15.
    Pil, M.: Dynamic types and type dependent functions. In: Hammond, K., Davie, T., Clack, C. (eds.) IFL 1998. LNCS, vol. 1595, pp. 169–185. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  16. 16.
    Plasmeijer, R., van Eekelen, M.: Concurrent CLEAN Language Report (version 2.0) (December 2001),
  17. 17.
    Tretmans, J.: Test Generation with Inputs, Outputs, and Quiescence. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 127–146. Springer, Heidelberg (1996)Google Scholar
  18. 18.
    Vervoort, M., Plasmeijer, R.: Lazy dynamic input/output in the lazy functional language Clean. In: Peña, R., Arts, T. (eds.) IFL 2002. LNCS, vol. 2670, pp. 101–117. Springer, Heidelberg (2003)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Peter Achten
    • 1
  1. 1.Department of Software TechnologyRadboud University NijmegenNijmegenThe Netherlands

Personalised recommendations