Elements of Specifications


A Gentle specification is a list of declarations.

A declaration may introduce a data type as in

   'type' Expr

      plus(Expr, Expr)
      minus(Expr, Expr)
      mult(Expr, Expr)
      div(Expr, Expr)
a predicate as in

   'action' eval (Expr -> INT)

      'rule' eval(plus(X1, X2) -> N1+N2): eval(X1 -> N1) eval(X2 -> N2)
      'rule' eval(minus(X1, X2) -> N1-N2): eval(X1 -> N1) eval(X2 -> N2)
      'rule' eval(mult(X1, X2) -> N1*N2): eval(X1 -> N1) eval(X2 -> N2)
      'rule' eval(div(X1, X2) -> N1 / N2): eval(X1 -> N1) eval(X2 -> N2)
      'rule' eval(neg(X) -> -N): eval(X -> N)
      'rule' eval(num(N) -> N)
a global variable as in

   'var' CurLoopContext: LoopContext
or a global table as in

   'table' Label (Address: INT)
Declarations may be given in any order.

The Root Definition

One of the declarations must be a root definition. It consists of the the keyword 'root' followed by one or more statements. The program generated from the specification elaborates these statements.


  'root' expression(-> X) code(X)
Here, expression is elaborated first yielding a value X, then code is elaborated with X as an argument. expression and code must be declared as predicates.

Here is a complete Gentle specification

  'root' print("Hello World!")
using the predefined predicate print.


Comments may be interspersed into the specification. They allow documentation to be included for a human reader and are ignored by the compiler. There are two forms of comments in Gentle.

Comments of the first form start with `` -'' and finish at the end of the line. For example,

   -- this comment extends to the end of the line
The second form is text enclosed in `` /*'' and `` */'', these comments can range over several lines. E.g.

   /* this comment 
      ranges over two lines */
Comments of the second form may be nested. This is of particular value because it allows us to ``comment out'' a text without bothering whether the text contains comments.