An explanation of error messages of ASF

Consider the specification in BlackOrWhite.sdf and BlackOrWhite.asf. They define a sort BlackOrWhite which contains the values black and white and a flip function to switch colors.

module BlackOrWhite
exports
   sorts BlackOrWhite
   context-free syntax
     "white" -> BlackOrWhite
     "black" -> BlackOrWhite

    flip(BlackOrWhite) -> BlackOrWhite

equations
[1] flip(black) = white
[2] flip(white) = black

After carefully designing this specification, you save it. To your distress, you get an error message that resembles the following:

character '' expected, line 2, column 0

What is going on here? Well, actually two things:

This is easily corrected as shown in BlackOrWhiteCorrected.sdf and BlackOrWhiteCorrected.asf.

Example 1.3. BlackOrWhiteCorrected.sdf

module BlackOrWhiteCorrected
exports
   imports basic/Comments              
   sorts BlackOrWhite
   context-free syntax
     "white" -> BlackOrWhite
     "black" -> BlackOrWhite

    flip(BlackOrWhite) -> BlackOrWhite

Note:

The missing import is inserted here.

equations
[1] flip(black) = white
[2] flip(white) = black

Now let's embellish the previous example further by giving better names to the equations. See BlackOrWhiteWithTags.asf.

equations
[flip] flip(black) = white
[flip] flip(white) = black

Unfortunately, this leads to an error message in the following spirit:

character ']' unexpected, line 2, column 6

The explanation is that the tag of an equation (here: flip) and a function name in the specification (here also flip) interfere with each other. The simple solution is shown in BlackOrWhiteWithCorrectedTags.asf. Whether you change [flip] to [flip1], [flip-1], [flipa], or something else is not important as long as you avoid the tag [flip] itself.

equations
[flip-1] flip(black) = white
[flip-2] flip(white) = black

It is not unusual to equate the Boolean values true and false with the respective integers 1 and 0. You specify this in BoolAsInt.sdf and BoolAsInt.asf.

module BoolAsInt
exports
  imports basic/Comments

equations
[t1] true  = 1
[f0] false = 0

You are confident that you did a good job: a proper tag, a Boolean constant on the left-hand side and Integer constant on the right-hand side of each equation. Unfortunately, this experiment ends prematurely in the following error message:

character '1' unexpected, line 2, column 14

The story behind this error is as follows. The implementors of The Meta-Environment are clever (maybe too clever?) and they use the parser to do the type checking of equations as well. In this example, the left-hand side is of type Boolean and the right-hand side of type Integer, a clear type error. Unfortunately, the system reports this type error as a parse error. A likely solution for this problem is to introduce a new sort BoolOrInt that contains both Booleans and Integers. Now, the above equations can be parsed as equations over this new sort.

It is sometimes hard to find syntax errors in conditional equations with many, complex, conditions. Here are the most likely causes:

When you have completed your specification you want to write some input terms and parse and reduce them in order to validate your specification. As in ordinary programming when you are hit by a syntax error detected by the compiler, you can also get a parse error after entering an input term. There are three possible explanations for this:

Can we give some hints here?

If the normal form of a term still contains function symbols that should have been removed during rewriting, you probably have

A typical example of a forgotten equation is shown in FacError1.asf.

equations
[fac1] fac(succ(0)) = succ(0)
[fac2] X != 0 ===> fac(succ(X)) = mul(X,fac(X))

Trying to reduce fac(0) will now yield fac(0) instead of succ(0).

If the left-hand sides of two equations can match the same term, then two reductions are possible and the outcome of rewriting becomes uncertain. Consider the example in FacError2.asf where the condition in equation [fac2] is forgotten. Now the left-hand sides of both[fac1] and [fac2] can match the term fac(succ(0)) and lead to different outcomes depending on the implementation. Always make sure that such overlapping left-hand sides are guarded by a condition that determines which equation to apply.

equations
[fac0] fac(0)       = succ(0)
[fac1] fac(succ(0)) = succ(0)
[fac2] fac(succ(X)) = mul(X,fac(X))

As in any language, if the equations that describe the induction over a given structure are wrong, this may lead to infinite recursion. Consider the erroneous definition of the factorial function in FacError3.asf.

equations
[fac0] fac(0)       = succ(0)
[fac1] fac(succ(0)) = succ(0)
[fac2] X != 0 ===> fac(succ(X)) = mul(X,fac(succ(X)))

Some operators are inherently commutative, i.e., it does not matter in which order the arguments occur. It is tempting to express this in a specification.

Consider the following, extended, definition of addition in AdderError.asf. Mathematically, this is a fine specification. However, executing may lead to non-termination. The careful reader will observe that equation [0] also overlaps with equations [1] and [2], therefore the outcome is uncertain as explained above.

Example 1.14. AdderError.asf

equations                             

[0] add(X, Y) = add(Y, X)   
[1] add(0, X) = X                     
[2] add(succ(X), Y) = succ(add(X,Y))  

Notes:

New equation that expresses commutativity of addition.

Commutative equations may also occur in the disguise of an equation containing list matching.

The specification of sets in ItemSet.sdf and ItemSet.asf illustrates a specification that leads to non-termination since equation[2], which expresses that two elements in a set may be exchanged, will lead to an infinite rewriting loop.

module ItemSet

imports basic/Whitespace

exports
  context-free start-symbols Set
  sorts Item Set 

  lexical syntax
    [a-z]+ -> Item 

  context-free syntax
    Set[Item] -> Set

hiddens
  variables
    "I"[0-9]* -> Item
    "L"[0-9]* -> {Item ","}*

equations
[1] {L1, I, L2, I, L3}   = {L1, I, L2, L3} 
[2] {L1, I1, L2, I2, L3} = {L1, I2, L2, I1, L3} 

Add examples here.

There are a few issues to be aware of when writing conditions: