Motivated by the proliferation and usefulness of Domain Specific Languages as well as the demand for enriching well established languages by high level capabilities like pattern matching or invariant checking, we introduce the Formal Islands framework.
The main idea consists to integrate, in existing programs, formally defined parts called islands, on which proofs and tests can be meaningfully developed. Then, Formal Islands could be safely dissolved into their hosting language to be transparently integrated in the existing development environment.
The paper presents this generic framework and shows that the properties valid on the Formal Islands are also valid on the corresponding dissolved host codes. Formal Islands can be used as a general methodology to develop new DSLs and we show that language extensions like SQLJ —embedding SQL capabilities in Java —, or Tom —a Java language extension allowing for pattern matching and rewriting—are indeed islands.
KeywordsFormal Island Language Extension Abstract Syntax Tree Abstraction Function Predicate Mapping
Unable to display preview. Download preview PDF.
- 2.Baader, F., Nipkow, T.: Term Rewriting and all That. Cambridge University Press, Cambridge (1998)Google Scholar
- 3.Balland, E., Kirchner, C., Moreau, P.-E.: Formal Islands. Technical report, LORIA (2006), available at http://hal.inria.fr/inria-00001146
- 5.Clossman, G., Shaw, P., Hapner, M., Klein, J., Pledereder, R., Becker, B.: Java and relational databases (tutorial): SQLJ. In: Proceedings of the ACM SIGMOD International Conference on Management of Data, p. 500. ACM Press, New York (1998)Google Scholar
- 9.Melton, J., Eisenberg, A.: Understanding SQL and Java Together: A Guide to SQLJ, JDBC, and Related Technologies. Morgan Kaufmann, San Francisco (2000)Google Scholar
- 10.Mernik, M., Heering, J., Sloane, A.M.: When and how to develop domain-specific languages. Technical report, CWI (2003)Google Scholar