×

zbMATH — the first resource for mathematics

Statically safe program generation with SafeGen. (English) Zbl 1215.68054
Summary: 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.

MSC:
68N15 Theory of programming languages
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Java Collections Framework Web site. http://java.sun.com/j2se/1.4.2/docs/guide/collections/
[2] Andreka, H.; Van Benthem, J.; Nemeti, I.: Modal languages and bounded fragments of predicate logic, Journal of philosophical logic 27, No. 3, 217-274 (1998) · Zbl 0919.03013
[3] Bachrach, J.; Playford, K.: The Java syntactic extender (JSE), , 31-42 (2001)
[4] Baker, J.; Hsieh, W. C.: Maya: multiple-dispatch syntax extension in Java, , 270-281 (2002)
[5] Batory, D.; Lofaso, B.; Smaragdakis, Y.: JTS: tools for implementing domain-specific languages, , 143-153 (1998)
[6] Batory, D.; Sarvela, J. N.; Rauschmayer, A.: Scaling step-wise refinement, , 187-197 (2003)
[7] Bryant, A.; Catton, A.; De Volder, K.; Murphy, G. C.: Explicit programming, , 10-18 (2002)
[8] B. Burke, et al. JBoss AOP Web site. http://labs.jboss.com/portal/jbossaop (accessed April 2007)
[9] Calcagno, C.; Taha, W.; Huang, L.; Leroy, X.: Implementing multi-stage languages using asts, gensym, and reflection, Lncs 2830, 57-76 (2003)
[10] D. Draheim, C. Lutteroth, G. Weber, A type system for reflective program generators, in: Generative Programming and Component Engineering, GPCE, 2005 · Zbl 1215.68062
[11] Fahndrich, M.; Carbin, M.; Larus, J. R.: Reflective program generation with patterns, , 275-284 (2006)
[12] Flanagan, C.; Leino, K. R. M.; Lillibridge, M.; Nelson, G.; Saxe, J. B.; Stata, R.: Extended static checking for Java, , 234-245 (June 2002)
[13] Gamma, E.; Helm, R.; Johnson, R.: Design patterns. Elements of reusable object-oriented software, Addison-wesley professional computing series (1995)
[14] Ganzinger, H.; De Nivelle, H.: A superposition decision procedure for the guarded fragment with equality, , 295-304 (1999)
[15] J. Gosling, et al. The Java Language Specification, GOTOP Information Inc., 5F, No.7, Lane 50, Sec.3 Nan Kang Road Taipei, Taiwan · Zbl 0865.68001
[16] E. Grädel, Decidable fragments of first-order and fixed-point logic, From prefix-vocabulary classes to guarded logics, in: Proceedings of Kalmár Workshop on Logic and Computer Science, Szeged, 2003
[17] Huang, S. S.; Smaragdakis, Y.: Easy language extension with meta-aspectj, , 865-868 (2006)
[18] Huang, S. S.; Zook, D.; Smaragdakis, Y.: Cj: enhancing Java with safe type conditions, , 185-198 (2007)
[19] Kiczales, G.; Hilsdale, E.; Hugunin, J.; Kersten, M.; Palm, J.; Griswold, W. G.: An overview of aspectj, , 327-353 (2001) · Zbl 0982.68552
[20] Kiczales, G.; Lamping, J.; Menhdhekar, A.; Maeda, C.; Lopes, C.; Loingtier, J. -M.; Irwin, J.: Aspect-oriented programming, Proceedings European conference on object-oriented programming 1241, 220-242 (1997)
[21] M. Mohnen, Interfaces with default implementations in Java, in: Proceedings of the Inaugural Conference on the Principles and Practice of Programming, 2002, pp. 35–40, Maynooth, County Kildare, Ireland, Ireland, 2002. National University of Ireland
[22] Pasalie, E.; Taha, W.; Sheard, T.: Tagless staged interpreters for typed languages, , 218-229 (2002) · Zbl 1322.68033
[23] Sheard, T.; Jones, S. P.: Template meta-programming for haskell, , 1-16 (2002)
[24] A. Stevens, et al. XDoclet Web site. http://xdoclet.sourceforge.net/ (accessed April 2007)
[25] Taha, W.; Sheard, T.: Multi-stage programming with explicit annotations, , 203-217 (1997) · Zbl 0949.68047
[26] Tilevich, E.; Urbanski, S.; Smaragdakis, Y.; Fleury, M.: Aspectizing server-side distribution, (October 2003)
[27] Visser, E.: Meta-programming with concrete object syntax, Lncs 2487, 299-315 (2002) · Zbl 1028.68921
[28] Warth, A.; Stanojevic, M.; Millstein, T.: Statically scoped object adaptation with expanders, , 37-56 (2006)
[29] C. Weidenbach, The theory of SPASS Version 2.0., Technical Report, Max-Planck Institute fur Informatik · Zbl 1072.68596
[30] D. Weise, R.F. Crew, Programmable syntax macros, in: SIGPLAN Conference on Programming Language Design and Implementation, 1993, pp. 156–165
[31] Zook, D.; Huang, S. S.; Smaragdakis, Y.: Generating aspectj programs with meta-aspectj, , 1-18 (2004)
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.