This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Domain-Specific Language for Regular Sets of Strings and Trees
May/June 1999 (vol. 25 no. 3)
pp. 378-386

Abstract—We propose a new high-level programming notation, called FIDO, that we have designed to concisely express regular sets of strings or trees. In particular, it can be viewed as a domain-specific language for the expression of finite-state automata on large alphabets (of sometimes astronomical size). FIDO is based on a combination of mathematical logic and programming language concepts. This combination shares no similarities with usual logic programming languages. FIDO compiles into finite-state string or tree automata, so there is no concept of run-time. It has already been applied to a variety of problems of considerable complexity and practical interest. In the present paper, we motivate the need for a language like FIDO, and discuss our design and its implementation. Also, we briefly discuss design criteria for domain-specific languages that we have learned from the work with FIDO. We show how recursive data types, unification, implicit coercions, and subtyping can be merged with a variation of predicate logic, called the Monadic Second-order Logic (M2L) on trees. FIDO is translated first into pure M2L via suitable encodings, and finally into finite-state automata through the MONA tool.

[1] A. Ayari, D. Basin, and A. Podelski, “Lisa: A Specification Language Based on WS2S,” Proc. CSL'97, BRICS, 1997.
[2] D. Basin and N. Klarlund, “Hardware Verification Using Monadic Second-Order Logic,” Proc: Seventh Int'l Conf, Computer Aided Verification, CAV'95, Lecture Notes in Computer Science 939, 1995.
[3] M. Biehl, N. Klarlund, and T. Rauhe, “Algorithms for Guided Tree Automata,” Proc. WIA'96, Springer-Verlag, 1996.
[4] R.E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, Vol. C-35, No. 8, Aug. 1986, pp. 667-690.
[5] J.G. Henriksen, M. Jørgensen, J. Jensen, N. Klarlund, B. Paige, T. Rauhe, and A. Sandholm, “Mona: Monadic Second-Order Logic in Practice,” Proc. TACAS'95, Lecture Notes in Computer Science 1,019, May 1995.
[6] G.J. Holzmann, “The Model Checker SPIN,” IEEE Trans. Software Eng., vol. 23, May 1997.
[7] J.L. Jensen, M.E. Jørgensen, N. Klarlund, and M.I. Schwartzbach, “Automatic Verification of Pointer Programs Using Monadic Second-Order Logic,” Proc. PLDI'97, 1997.
[8] N. Klarlund, M. Nielsen, and K. Sunesen, “A Case Study in Automated Verification Based on Trace Abstractions,” Technical Report RS-95-54, BRICS, Aarhus Univ., 1995.
[9] N. Klarlund, M. Nielsen, and K. Sunesen, “Automated Logical Verification Based on Trace Abstraction,” Proc. PODC'96 1996.
[10] N. Klarlund, J. Koistinen, and M.I. Schwartzbach, “Formal Design Constraints,” Proc. OOPSLA'96, Oct. 1996.
[11] N. Klarlund and T. Rauhe, “BDD Algorithms and Cache Misses,” Technical Report RS-96-05, BRICS, 1996, to appear.
[12] J.C. Reynolds, “Three Approaches to Type Structure,” Math. Foundations of Software Development, Lecture Notes in Computer Science 185, 1985.

Index Terms:
Domain-specific languages, regular sets, trees, strings, logic.
Citation:
Nils Klarlund, Michael I. Schwartzbach, "A Domain-Specific Language for Regular Sets of Strings and Trees," IEEE Transactions on Software Engineering, vol. 25, no. 3, pp. 378-386, May-June 1999, doi:10.1109/32.798326
Usage of this product signifies your acceptance of the Terms of Use.