Executable specification ..? how executable specifications can be used for rapid prototyping?

527 Views Asked by At

After reading these books

Bertrand Meyer, Introduction to the Theory of Programming Languages &

J.D. Ullman, Elements of ML Programming

I have read some papers also, tried to find on google also but I still don't understand this concept. 'executable language semantic specification in functional languages as a rapid prototyping'

I have some questions .. I don't understand meaning of some lines and I have some questions also.. what does this mean and what is 'executable specification'

(1) executable language semantic specification in SML as a rapid prototype of the language implementation

(2)how executable specifications can be used for rapid prototyping

(3)Denotational semantics provides the “oracle” of the implementation for imperative programming languages on available architecture/machines.

1

There are 1 best solutions below

0
On

I'm really just guessing as I haven't read the books you're talking about, but I suspect it is referring to the practice of encoding the semantics of some language as a set of SML functions. This provides a quick and easy means of playing with the semantics of a language in an executable setting without having to implement all the messy front- and back-end compiler or interpreter artifacts. For example:

datatype value = Int of int
               | String of string

datatype ast = Seq of ast * ast
             | Print of ast
             | Value of value
             | Assign of string * ast
             | Variable of string

fun value_printer (Int i) = print (Int.toString i)
  | value_printer (String s) = print s

fun execute env (Seq (a, b)) = (execute env a; execute env b)
  | execute env (Print a) = value_printer (execute env a)
  | execute env (Value _) = ()
  | execute env (Assign (s, a)) = ...
    etc, etc.

You basically define a datatype with which to represent your abstract syntax tree, and then define a function that performs rewriting on this AST (or which reduces AST sub-trees to some value datatype that represents values in your language).

If the execute function looks vaguely familiar, it's because it resembles more traditional semantic definitions that you might see in a textbook, just with some funny syntax.

You could imagine that we could experiment for building type-checkers, static analyses, or optimizations in this setting without ever having to move out of our "rapid prototyping" environment (which happens to be SML). SML is really well-suited to these kinds of tasks, which is (I assume) why the books you've read suggest this approach.