Executable Specification Languages

We believe that a new software development paradigm is struggling to be born. It appears in many guises and contexts, under many names, and is as yet still unformed and incomplete. We are not surprised at the struggles, for we do not believe that paradigms arise from a single blinding flash of insight, but rather they come about by careful assembly of many good ideas into a package that makes sense and works, as a whole, in some profound way. We believe we see initial attempts at creating such an assemblage. On the other hand, we suspect that some of birth pains are self-inflicted, because of confusion about the goal and narrow-mindedness in approaches to achieving this goal.

To us, the essence of this new paradigm is a shift toward descriptions of what software should do and away from how it should do it, while still providing enough operational information so that the desired behavior can be generated automatically.

A description of “what a system should do” is normally called a specification. Thus it would be natural to assume we are talking about general-purpose specification languages, for example CASL or B/Z, as the foundation for this new paradigm. But this is not the case, because of the requirement that desired behaviors can be generated automatically. By this, we mean that the specifications must be executable, so that the generated behaviors are sufficiently efficient and reliable to be usable in practice. There is as yet no general way to convert from a specification in a general-purpose specification language to an executable program. Note that this kind of synthesis is an important research area (my student Srinivas Nedunuri working with Doug Smith on it, but this is another topic), but it is not not yet ready for widespread adoption.

One way to solve this problem in the short term is to limit the expressiveness of the languages to a particular kind of problem. We believe that executable special-purpose specification languages will be the foundation of the next widely-used programming paradigm. Here is one way to see how this approach fits into the landscape of computer science research:

There has been great success exploring lightweight verification techniques. The key point is that these approaches narrow the expressiveness of the properties that can be specified, then apply powerful automation technology to verify the limited theorems. We believe that equal progress can be made by narrowing the expressiveness of the specification languages used for synthesis, and applying powerful optimization techniques to the problem.

There are already many successful examples of this approach, including grammars (Yacc), databases (SQL), spreadsheets (Excel), security (XACML), state machines (StateCharts), network protocols (NDLog, Frenentic),  user interfaces (XUL), and many more. These systems all allow users to specify what a computation should do, without saying exactly how to do it. Most of them have deep theory and optimization techniques that make them expressive and efficient. But they are also specialized to a particular task. There are many more examples in practical use, or experimental design.

There is a subtle point in our initial statement. We emphasize that behavior is generated automatically, but this does not necessarily mean that code is generated. The behavior may be generated by an interpreter. The examples mentioned above span the spectrum between interpretation and compilation.

The key question, for the development of a new paradigm, is whether this approach can be generalized so that it can be used to build complete (or nearly complete) systems. Currently specialized specification languages are used as small components of systems, but the majority of the system is created using general-purpose code. The question is whether this emphasis can be inverted, so that most of a system is build with specialized languages, with general-purpose used for the underlying language engines, or as application-specific code plugged in where necessary. The success of this approach will depend in part on the amount of regularity in the systems we want to build.

Given the goal, to move from how towards what while still supporting executability, it is not surprising that there is a lot of experimentation necessary. There are many problems that must be solved before this vision is realized. In this blog we will elaborate on these themes and also discuss our specific work on realizing this vision in Ensō.

We apologize for continuing to blog at the level of polemic, rather than giving more examples of code in Ensō. The reason is that blogs are well-suited to polemic, and our technical results are going into academic papers. When we have the papers ready (and the first one should be done soon) we will post a summary here. We were giving demos at SPLASH, so if you want to know more you should come next year.

Comments (3)

  1. Freddy Mallet wrote::

    Thanks for sharing your thoughts. According to your definition of what are Executable Specification Languages, I don’t see the difference with the definition of DSL ? For me Executable Specifications Languages are a way to automatically test the expected behavior of an application : the what and not the how.

    Wednesday, November 9, 2011 at 2:12 pm #
  2. w7cook wrote::

    See my next blog post for a response to your question. Thanks for writing.

    Wednesday, November 9, 2011 at 4:32 pm #
  3. Freddy Mallet wrote::

    Thanks for this so detailed answer. Indeed, as I’m a big fan of executable specifications, I was mainly confused by the use of such terms in another different context.

    Wednesday, November 9, 2011 at 5:33 pm #
Get plugin http://www.fastemailsender.com