Advertisement

Statically Safe Program Generation with SafeGen

  • Shan Shan Huang
  • David Zook
  • Yannis Smaragdakis
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3676)

Abstract

SafeGen is a meta-programming language for writing statically safe generators of Java programs. If a program generator written in SafeGen passes the checks of the SafeGen compiler, then the generator will only generate well-formed Java programs, for any generator input. In other words, statically checking the generator guarantees the correctness of any generated program, with respect to static checks commonly performed by a conventional compiler (including type safety, existence of a superclass, etc.). To achieve this guarantee, SafeGen supports only language primitives for reflection over an existing well-formed Java program, primitives for creating program fragments, and a restricted set of constructs for iteration, conditional actions, and name generation. SafeGen’s static checking algorithm is a combination of traditional type checking for Java, and a series of calls to a theorem prover to check the validity of first-order logical sentences constructed to represent well-formedness properties of the generated program under all inputs. The approach has worked quite well in our tests, providing proofs for correct generators or pointing out interesting bugs.

Keywords

Theorem Prover Logic Formula Static Check Type Check Program Language Design 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Andreka, H., van Benthem, J., Nemeti, I.: Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic 27(3), 217–274 (1998)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Bachrach, J., Playford, K.: The Java syntactic extender (JSE). In: Proceedings of the OOPSLA 2001 conference on Object Oriented Programming Systems Languages and Applications, pp. 31–42. ACM Press, New York (2001)Google Scholar
  3. 3.
    Baker, J., Hsieh, W.C.: Maya: multiple-dispatch syntax extension in Java. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, pp. 270–281. ACM Press, New York (2002)CrossRefGoogle Scholar
  4. 4.
    Batory, D., Lofaso, B., Smaragdakis, Y.: JTS: tools for implementing domain-specific languages. In: Proceedings Fifth International Conference on Software Reuse, pp. 143–153. IEEE, Los Alamitos (1998)Google Scholar
  5. 5.
    Batory, D., Sarvela, J.N., Rauschmayer, A.: Scaling step-wise refinement. In: Proceedings of the 25th International Conference on Software Engineering, pp. 187–197. IEEE Computer Society, Los Alamitos (2003)CrossRefGoogle Scholar
  6. 6.
    Bryant, A., Catton, A., De Volder, K., Murphy, G.C.: Explicit programming. In: Proceedings of the 1st international conference on Aspect-Oriented Software Development, pp. 10–18. ACM Press, New York (2002)CrossRefGoogle Scholar
  7. 7.
    Calcagno, C., Taha, W., Huang, L., Leroy, X.: Implementing multi-stage languages using ASTs, gensym, and reflection. In: Pfenning, F., Smaragdakis, Y. (eds.) GPCE 2003. LNCS, vol. 2830, pp. 57–76. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  8. 8.
    Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Conference on Programming Language Design and Implementation (PLDI), pp. 234–245. ACM Press, New York (2002)Google Scholar
  9. 9.
    Ganzinger, H., de Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: Logic in Computer Science conference (LICS), pp. 295–304 (1999)Google Scholar
  10. 10.
    Pasalic, E., Taha, W., Sheard, T.: Tagless staged interpreters for typed languages. In: International Conference on Functional Programming (ICFP), pp. 218–229. ACM Press, New York (2002)Google Scholar
  11. 11.
    Sheard, T., Jones, S.P.: Template meta-programming for Haskell. In: Proceedings of the ACM SIGPLAN workshop on Haskell, pp. 1–16. ACM Press, New York (2002)CrossRefGoogle Scholar
  12. 12.
    Stevens, A., et al.: XDoclet, Web site, http://xdoclet.sourceforge.net/
  13. 13.
    Taha, W., Sheard, T.: Multi-stage programming with explicit annotations. In: Partial Evaluation and Semantics-Based Program Manipulation, pp. 203–217. ACM, New York (1997)CrossRefGoogle Scholar
  14. 14.
    Tilevich, E., Urbanski, S., Smaragdakis, Y., Fleury, M.: Aspectizing server-side distribution. In: Proceedings of the Automated Software Engineering (ASE) Conference. IEEE Press, Los Alamitos (2003)Google Scholar
  15. 15.
    Visser, E.: Meta-programming with concrete object syntax. In: Batory, D., Consel, C., Taha, W. (eds.) GPCE 2002. LNCS, vol. 2487, pp. 299–315. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  16. 16.
    Weidenbach, C.: SPASS: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning. Elsevier, Amsterdam (1999)Google Scholar
  17. 17.
    Weise, D., Crew, R.F.: Programmable syntax macros. In: SIGPLAN Conference on Programming Language Design and Implementation, pp. 156–165 (1993)Google Scholar
  18. 18.
    Zook, D., Huang, S.S., Smaragdakis, Y.: Generating AspectJ programs with Meta-AspectJ. In: Karsai, G., Visser, E. (eds.) GPCE 2004. LNCS, vol. 3286, pp. 1–18. Springer, Heidelberg (2004)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Shan Shan Huang
    • 1
  • David Zook
    • 1
  • Yannis Smaragdakis
    • 1
  1. 1.College of ComputingGeorgia Institute of TechnologyAtlantaUSA

Personalised recommendations