Improving the

Algebraic Specification Language ASF^{+}

Claus-Peter Wirth

cp@ags.uni-sb.de

http://ags.uni-sb.de/˜ cp/welcome.html

Research Report

http://ags.uni-sb.de/˜ cp/p/asf/all.ps.gz

!!! !!! !!! !!! preliminary version !!! !!! !!! !!! !!!

December 14, 1999 Typos corrected, July 30, 2001

FR Informatik, Universität des Saarlandes, D–66041 Saarbrücken, Germany

Abstract:

Contents

1 Introduction 1 2 Minor Syntactic Changes 2 3 Basic Specifications 4 4 The Problems with ASF^{+} in Practice 7

4.1 Explicit Renaming . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 4.2 Sharing Structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 4.3 Higher-Order Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

5 Syntax 20 References and Notes 23

1 Introduction

The algebraic specification language ASF was presented in Bergstra &al. (1989). What makes ASF interesting is that it provides the possibility to structure and parameterize a specification without any reference to the semantics. Instead, there is a translation function that maps any structured ASF specification without any unbound parameters to a basic flat unstructured specification. Note that this function maps syntax to syntax. Although such an approach may make theoreticians unhappy; regarding all the open questions on how to use algebraic specification successfully in practice, the flexible syntax-to-syntax approach seems to be the proper way for our time to structure algebraic specifications.

While ASF as defined in Bergstra &al. (1989) was a first step into the right direction, it had several shortcomings, most of them already listed in section 1.4.1 of Bergstra &al. (1989) “Known defects and limitations of ASF”.

Maintaining the main aspects of ASF, in ASF^{+} defined in Lunde & Wirth (1994) we have extended ASF with the following concepts:

1. While once exported names in ASF must stay visible up to the top of the module hierarchy, ASF^{+} permits a more sophisticated hiding of signature names.

2. The erroneous merging of distinct structures that occurs when importing different actualizations of the same parameterized module in ASF is avoided in ASF^{+} by a more adequate form of parameter binding.

3. A new concept of ASF^{+} called name-space (“Namensraum” in German) permits the specifier on the one hand directly to identify the origin of hidden names and on the other hand to decide whether an imported module is only to be accessed or whether an important property of it is to be modified. In the first case he can access one single globally provided version; in the second he has to import a copy of the module.

Just like ASF, ASF^{+} still supports the following:

• Import of Modules with unbound parameters into other modules

• Overloading of (possibly infix) operators

While we think that ASF^{+} is an improvement of ASF, in practice it has also shown some shortcomings. These shortcomings can be summarized: It takes to much time to write and read typical things. In the following we will demonstrate these shortcomings and try to solve them.

2 Minor Syntactic Changes

Note that we have already done some simplifications and little changes to the syntax of ASF^{+} here:

• The the repeated occurrences of the keyword “import” are omitted and “import” is replaced with “imports”.

• When renaming a signature symbol, we write

                            “Y renames X”

instead of

                          “X renamed to Y ”.

• If a parameter block (that requires the parameters to be bound to symbols of the same module) contains only one parameter, the enclosing parentheses may be omitted everywhere.

• In order to bind the parameters X and Y (captured in a parameter block) to A and

B of module M, we write

                    “(X, Y) bound to (A, B) of M”

instead of

                “(X bound to A, Y bound to B) of M”.

Moreover, we may write

                         “X bound to A of M”

instead of

                       “(X) bound to (A) of M”.

• The keyword non-constructors has been changed into functions in the signature section and into general variables in the variables section.

• The keyword equations starting the definitions has been changed into axioms for the definitions of a restricted format and into lemmas for any format.

• The keyword goals starting the properties that should follow from the definitions (axioms, lemmas) has been renamed into theorems.

• We omit the enclosing parentheses ‘{’ and ‘}’ for the body of a module, the signature

section, and the variables, axioms, lemmas, and theorems sections.

• Nullary function symbols and variables are now declared with a simple “:” instead of the previous “: ->”.

• The former ‘#’, separating multiple argument sorts in a function declaration is omitted now: Any white-space is sufficient for the separation.

• Names introduced by the user may now even contain a hyphen ‘-’. This is possible because the hyphen is not generated anymore by the translation of the structured specifications into basic flat unstructured specifications. Instead of

“<module-name>[<instance-name>,…,<instance-name>]-<name>” the translation function should simply produce

“<module-name>[<instance-name>,…,<instance-name>]<name>”, and instead of

“<module-name>-<name>”

the translation function simply should produce “<module-name>[]<name>”.

• Moreover, names introduced by the user that do not denote modules or instances may even contain brackets ‘[’ and ‘]’ provided that there is no module name that is equal to the prefix up to the first occurrence of an opening bracket ‘[’.

The complete new syntax is defined in Sect. 5.

3 Basic Specifications

In the following section we will need some specifications to build on. We present them here in advance because the reader should get an intuitive understanding of ASF^{+} simply by reading specifications of well-known structures.

Specification 3.1 (Boolean Values) module Booleans

short B
add signature
public:
 sorts

bool

 constructors

true, false : bool

 functions

and : bool bool -> bool

general variables

X : bool

axioms

and(true, X) = X
and(X, true) = X
and(false, X) = false
and(X, false) = false

Specification 3.2 (Natural Numbers, 1^{st} version) module Naturals

short N
add signature
public:
 sorts

nat, [nat x nat] to nat

 constructors

0 :  nat
s : nat -> nat

 functions

1, 2, 3 : nat
max : [nat x nat] to nat
apply : [nat x nat] to nat nat nat -> nat

variables

m, n : nat

axioms

1 = s(0)
2 = s(1)
3 = s(2)
apply(max, 0, n)  = n
apply(max, m, 0)  = m
apply(max, s(m), s(n)) = s(apply(max, m, n))

Specification 3.3 (Lists, 1^{st} version) module Lists <LISTITEM>

short L
imports

Booleans { public: bool, true, false } Naturals { public: nat, 0, s }

add signature
parameters:
(
sorts

LISTITEM

)
public:
sorts

list, list to bool

constructors

[] :  list
:: : LISTITEM list -> list

functions

hd : list -> LISTITEM
tl  : list -> list
length : list -> nat
null : list -> bool
dl, rc : LISTITEM list -> list
∈ : LISTITEM list -> bool
nth : nat list -> LISTITEM
append : list list -> list
isprefix, isproperprefix : list -> list to bool
apply : list to bool list -> bool

variables

n : nat
i, j : LISTITEM
k, l : list

axioms

\begin{matrix}hd(i:: l) = & i \\ tl(i:: l) = & l \end{matrix}

null([]) = true
null(i:: l) = false

nth(0, i:: l) = i
nth(s(n), i:: l) = nth(n, l)

/* dl(i, l) deletes any occurrence of i in l, rc(i, l) only the repeated occurrences, i.e. it removes copies of i in l */

[dl1] dl(i, []) = []
[dl2] dl(i, j :: l) = dl(i, l)  if i=j
[dl3] dl(i, j :: l) = j :: dl(i, l) if i≠j
[rc1] rc(i, [])  = []
[rc2] rc(i, (j :: l)) = (j :: dl(i, l)) if i=j
[rc3] rc(i, (j :: l)) = (j :: rc(i, l)) if i≠j
[∈1] i ∈ []  = false
[∈2] i ∈ (j :: l) = true if i=j
[∈3] i ∈ (j :: l) = i ∈ l if i≠j
length([]) = 0
length(i:: l) = s(length(l))
append([], l) = l
append(i:: k, l) = i:: append(k, l)
apply(isprefix([]), l)  = true
apply(isprefix(i:: k), []) = false
apply(isprefix(i:: k), j :: l) = false  if i≠j
apply(isprefix(i:: k), j :: l) = apply(isprefix(k), l) if i=j
apply(isproperprefix(k), [])  = false
apply(isproperprefix([]), j :: l) = true
apply(isproperprefix(i:: k), j :: l) = false  if i≠j
apply(isproperprefix(i:: k), j :: l) = apply(isproperprefix(k), l) if i=j

4 The Problems with ASF^{+} in Practice

4.1 Explicit Renaming

In ASF^{+} a module for sets could look the following way.

Specification 4.1 (Sets, 1^{st} version) module Sets <SETITEM>

short S
imports

Booleans { public: bool, true, false, and } Lists[S]<SETITEM renames LISTITEM> { public: dl, ∈, null,

set renames list,

     {} renames [],

choose renames hd, chooserest renames tl, card renames length

 private: ::

}

add signature
public:
 functions

insert : SETITEM set -> set
∪ , ∩ , \ : set set -> set
⊆ , equal  : set set -> bool

variables

i : SETITEM  s, t, u : set

axioms

insert(i, s) = s  if (i ∈ s)=true
insert(i, s) = i:: s if (i ∈ s)=false

\begin{matrix}s ∪ \{\} = & s \\ s ∪ (i:: t) = & insert(i, s) ∪ t \end{matrix}

s ∩ {} = {}
s ∩ (i:: t) = i:: (dl(i, s) ∩ t) if (i ∈ s)=true
s ∩ (i:: t) = s ∩ t  if (i ∈ s)=false

\begin{matrix}s \ \{\} = & s \\ s \ (i:: t) = & dl(i, s) \ t \end{matrix}

{} ⊆ t = true
(i:: s) ⊆ t = false if (i ∈ t)=false
(i:: s) ⊆ t = s ⊆ t if (i ∈ t)=true
equal(s, t) = and(s ⊆ t, t ⊆ s)

theorems

[⊆reflexive]  s ⊆ s
[⊆transitive]  s ⊆ u, \overline{s ⊆ t}, \overline{t ⊆ u}
[equalreflexive] equal(s, s)
[equalsymmetric] equal(s, t), \overline{equal(t, s)}
[equaltransitive] equal(s, u), \overline{equal(s, t)}, \overline{equal(t, u)}

When we want to use these sets in some other module, there will most likely be other sets around with visible names. Thus, in order to avoid name conflicts, we have to rename ‘{}’ and the sort ‘set’ like in the following example.

Specification 4.2 (Sets of Natural Numbers, 1^{st} version)

module SetNat
short SNat
imports

Sets[SNat]<SETITEM bound to nat of Naturals> {public: insert, choose, chooserest, null, ∪, ∩, \,

setnat renames set,

emptysetnat renames {} }

This renaming has to be done for every instantiation of ‘Sets’ and has been reported to us to be a real nuisance. Since it can be overcome in a way that will also solve the problem of Sect. 4.2, we should do the following changes.

Specification 4.3 (Sets, 2^{nd} version) module Sets <SETITEM>

short S
imports

Booleans { public: bool, true, false, and } Lists[S]<SETITEM renames LISTITEM> { public: dl, ∈, null,

set<SETITEM> renames list, {}<SETITEM> renames [], choose renames hd, chooserest renames tl, card renames length

 private: ::

} … (cf. Spec. 4.1)

Note that the true name of ‘set’ has been changed into the qualified name ‘set<SETITEM>’. Nevertheless, we may use ‘set’ as a nickname as long as it cannot be confused. Similarly, ’{}<SETITEM>’ replaced ’{}’. This becomes advantageous, when instantiating ‘Sets’ like before:

Specification 4.4 (Sets of Natural Numbers, 2^{nd} version)

module SetNat
short SNat
imports

Sets[SNat]<SETITEM bound to nat of Naturals> {public: insert, choose, chooserest, null, ∪, ∩, \, set<nat>, {}<nat> }

This does not seem to be much of a change, but note that the renaming has become more systematic and that we still may use ‘set’ and ‘{}’ as nicknames as long there cannot be any confusion. Note that we may even use ‘{}’ as nickname for different true names as long as we can find out what it is by the context; e.g., when ‘{}’ is an argument of a function whose argument sorts are known, or when ‘{}’ occurs on the right-hand side of an equation where we know the sort of the left-hand side.

4.2 Sharing Structures

When we instantiate a parameter in ASF^{+}, we must provide a unique instance name (“Instanzbezeichnung” in German). E.g., in Spec. 4.4, we reused the short name ‘SNat’ for the module name as instance name when instantiating the parameter ‘SETITEM’ with ‘nat’. As a result of this, ‘null’ belongs to the name-space ‘Sets[SNat]’ instead of simple ‘Sets’. A closer inspection of the module ‘Sets’ tells us that ‘null’ actually belongs to the name-space ‘Lists[S,SNat]’ because it is imported from the name-space ‘Lists[S]’. This, however, is not our point here. Our point is the following: When we instantiate the parameter ‘SETITEM’ a second time with ‘nat’, ASF^{+} requires a new instance name, say ‘SNat2’. Note that ‘SNat’ cannot be used again because each instantiation requires a unique instance name. The resulting function ‘null’ belongs to the name-space ‘Lists[S,SNat2]’ and has nothing to do with the function of the same name from above. This is a nice and useful feature because in different parts of the specification different destructive changes to the sets of natural numbers may be needed. When we designed ASF^{+}, we thought that if some set of natural numbers should be shared, then it should be instantiated only once and then imported in the instantiated form. Theoretically, this is fine. Practically, it furthers a good structure of the specification. It may, however, be quite hard to use. Suppose we want to define a module that provides the possibility to use functions from ‘ITEMS1’ to ‘ITEMS2’ (having sort ‘ITEMS1 to ITEMS2’) for constructing new functions from the power-set ‘S1’ of ‘ITEMS1’ to the power-set ‘S2’ of ‘ITEMS2’ as in the following example ‘Mapch’. Note that it is of no use importing the module ‘Sets’ into ‘Mapch’: We should not import an instantiated version because we want to use the module ‘Mapch’ for sets over an arbitrary sort. When we import the parameterized versions and later instantiate the parameters with say ‘nat’, the whole module ‘Mapch’ becomes useless because it operates on a copy of ‘SNat’ and cannot cooperate with it. So the only possible solution in ASF^{+} is not to import ‘Sets’ at all and parameterize every set function. This is hard to understand. Moreover, any instantiation of the the module ‘Mapch’ will take half a page and be very hard to read.

Specification 4.5 (Mapping Sets, 1^{st} version)

module Mapch <

ITEMS1 (S1, emptyS1, insertS1, nullS1, chooseS1, chooserestS1) ITEMS2 (S2, emptyS2, insertS2, nullS2, chooseS2, chooserestS2) (ITEMS1 to ITEMS2, APPLY1to2)>

short 2S
imports

Booleans { public: bool, true, false }

add signature
parameters:
(
 sorts

ITEMS1

)
(
 sorts

S1

 functions

emptyS1 :  S1
insertS1 : ITEMS1 S1 -> S1
nullS1  : S1 -> bool
chooseS1 : S1 -> ITEMS1
chooserestS1 : S1 -> S1

)
(
 sorts

ITEMS2

)
(
 sorts

S2

 functions

emptyS2 :  S2
insertS2 : ITEMS2 S2 -> S2
nullS2  : S2 -> bool
chooseS2 : S2 -> ITEMS2
chooserestS2 : S2 -> S2

)
(
 sorts

ITEMS1 to ITEMS2

 functions

APPLY1to2 : ITEMS1 to ITEMS2 ITEMS1 -> ITEMS2

)
public:

 functions

mapch : ITEMS1 to ITEMS2 S1 -> S2

variables

C : S1
f : ITEMS1 to ITEMS2

axioms

mapch(f, C) = emptyS2

if nullS1(C)=true

mapch(f, C) = insertS2(APPLY1to2(f, chooseS1(C)), mapch(f, chooserestS1(C)))

if nullS1(C)=false

We may use our new qualified names from Sect. 4.1 to define Sets in a structural way (cf. Def. 4.6) that then will make it possible to import Sets into Mapch in the intended and useful way.

Definition 4.6 (Structural modules) A module is called structural if it does not have any parameters; or if all imported modules are structural and not instantiated with instance names, any new (added in add signature) sort and any new function that does not have all parameters as argument sort or qualification of an argument sort are qualified with the complete list of parameter blocks following the module name. Moreover, when a renaming occurs in an import, the qualification of the new name must be the (renamed) qualification of the old name.

The good thing with parameterized structural modules is that we can instantiate them without providing any instance name, because the names of the instantiated module can belong to the names of the parameterized module without any erroneous symbol identifications.

Now is Spec. 4.3 structural? No, it is not. It imports ‘Lists’ that is not structural. Thus, let us first redefine ‘Lists’ in a structural way:

Specification 4.7 (Lists, 2^{nd} version) module Lists <LISTITEM>

short L
imports

Booleans { public: bool, true, false } Naturals { public: nat, 0, s }

add signature
parameters:
(
 sorts

LISTITEM

)
public:
 sorts

list<LISTITEM>, list to bool<LISTITEM>

 constructors

[]<LISTITEM> :  list
::  : LISTITEM list -> list

 functions

hd : list -> LISTITEM
tl  : list -> list
length : list -> nat
null : list -> bool
dl, rc : LISTITEM list -> list
∈ : LISTITEM list -> bool
nth : nat list -> LISTITEM
append : list list -> list
isprefix, isproperprefix : list -> list to bool
apply : list to bool list -> bool

… (cf. Spec. 3.3)

Now we can define ‘Sets’ and ‘SetNat’ in a structural way:

Specification 4.8 (Sets, final version) module Sets <SETITEM>

short S
imports

Booleans { public: bool, true, false, and } /* Note that in the following line there is non instance name given to ‘Lists’ as before, although the parameter ‘LISTITEM’ is renamed. This is possible because ‘Lists’ is structural now. */

Lists<SETITEM renames LISTITEM> { public: dl, ∈, null,

set<SETITEM> renames list<LISTITEM>, {}<SETITEM> renames []<LISTITEM>, choose renames hd, chooserest renames tl, card renames length

 private: ::

}

add signature
public:
 functions

insert : SETITEM set -> set
∪ , ∩ , \ : set set -> set
⊆ , equal  : set set -> bool

variables

i : SETITEM  s, t, u : set

axioms

insert(i, s) = s  if (i ∈ s)=true
insert(i, s) = i:: s if (i ∈ s)=false

\begin{matrix}s ∪ \{\} = & s \\ s ∪ (i:: t) = & insert(i, s) ∪ t \end{matrix}

s ∩ {} = ∅
s ∩ (i:: t) = i:: (dl(i, s) ∩ t) if (i ∈ s)=true
s ∩ (i:: t) = s ∩ t  if (i ∈ s)=false

\begin{matrix}s \ \{\} = & s \\ s \ (i:: t) = & dl(i, s) \ t \end{matrix}

{} ⊆ t = true
(i:: s) ⊆ t = false if (i ∈ t)=false
(i:: s) ⊆ t = s ⊆ t if (i ∈ t)=true
equal(s, t) = and(s ⊆ t, t ⊆ s)

theorems

[⊆reflexive]  s ⊆ s
[⊆transitive]  s ⊆ u, \overline{s ⊆ t}, \overline{t ⊆ u}
[equalreflexive] equal(s, s)
[equalsymmetric] equal(s, t), \overline{equal(t, s)}
[equaltransitive] equal(s, u), \overline{equal(s, t)}, \overline{equal(t, u)}

Specification 4.9 (Sets of Natural Numbers, final version)

module SetNat
short SNat
imports

/* Note that the instance name SNat has been removed from the following line! */ Sets<SETITEM bound to nat of Naturals> { public: insert, choose, chooserest, null, ∪, ∩, \, set<nat>, {}<nat> } Finally, we redefine Mapch as intended.

Specification 4.10 (Mapping Sets, 2^{nd} version) module Mapch <ITEMS1 ITEMS2 (ITEMS1 to ITEMS2, APPLY1to2)>

short 2S
imports

Booleans { public: bool, true, false } Sets<ITEMS1 renames SETITEM> { public: set<ITEMS1> , {}<ITEMS1> , insert, null, choose, chooserest } Sets<ITEMS2 renames SETITEM> { public: set<ITEMS2> , {}<ITEMS2> , insert, null, choose, chooserest }

add signature
parameters:
(
 sorts

ITEMS1 to ITEMS2

 functions

APPLY1to2 : ITEMS1 to ITEMS2 ITEMS1 -> ITEMS2

)
public:
 functions

mapch<ITEMS1 ITEMS2 (ITEMS1 to ITEMS2, APPLY1to2)>

: ITEMS1 to ITEMS2 set<ITEMS1> -> set<ITEMS2>

variables

C : set<ITEMS1>
f : ITEMS1 to ITEMS2

axioms

mapch(f, C) = {}
if null(C)=true
mapch(f, C) = insert(APPLY1to2(f, choose(C)), mapch(f, chooserest(C)))
if null(C)=false

4.3 Higher-Order Functions

Another problem in practice is the restriction of ASF^{+} to first-order function symbols. E.g. in Spec. 3.2 we had to define a function ‘max’ as a nullary function of the sort ‘[nat x nat] to nat’. We would have preferred to define it as a function of type ‘nat nat -> nat’. But then we could not use it in Spec. 4.10 in the form of ‘mapch(max, C)’. Functional objects are needed very often in practice. It frequently happens that one needs some function as a functional object that was, however, defined as a function. Then one has to change the signature, the definition and any call of the function in any module. This is definitely not appropriate.

In order to free the specifier from the decision whether to specify a function or a corresponding functional object, we introduce the following convention:

1. All non-constructor non-nullary function declarations are meant to declare the Cur-

ried^{1} nullary function symbol. Thus,

max : nat nat -> nat

is taken as syntactic sugar for

max : nat -> (nat -> nat) ,

which again is taken as syntactic sugar for max : nat to [nat to nat] .

2. The function application to a non-singleton tuple of the form

max(i, j)

is taken to be syntactic sugar for

(max(i))(j).

3. The function application to a singleton tuple of the form

max(i)

is taken to be syntactic sugar for apply(max, i).

Thus

max(i, j)

finally denotes apply(apply(max, i), j).

Let us now see what the specifications ‘Naturals’ and ‘Mapch’ will look like now:

1A motivation for this is given before Spec. 4.13.

Specification 4.11 (Natural Numbers, final version) module Naturals

short N
add signature
public:
 sorts

nat

 constructors

0 :  nat
s : nat -> nat

 functions

1, 2, 3 : nat
max : nat nat -> nat

variables

m, n : nat

axioms

1 = s(0)
2 = s(1)
3 = s(2)
max(0, n)  = n
max(m, 0)  = m
max(s(m), s(n)) = s(max(m, n))

Specification 4.12 (Mapping Sets, final version) module Mapch <ITEMS1 ITEMS2>

short 2S
imports

Booleans { public: bool, true, false } Sets<ITEMS1 renames SETITEM> { public: set<ITEMS1> , {}<ITEMS1> , insert, null, choose, chooserest } Sets<ITEMS2 renames SETITEM> { public: set<ITEMS2> , {}<ITEMS2> , insert, null, choose, chooserest }

add signature
public:
 functions

mapch : (ITEMS1 -> ITEMS2) set<ITEMS1> -> set<ITEMS2>

variables

C : set<ITEMS1>  f : ITEMS1 -> ITEMS2

axioms

mapch(f, C) = {}
if null(C)=true
mapch(f, C) = insert(f(choose(C)), mapch(f, chooserest(C)))
if null(C)=false

Also the other specifications look more beautiful now. Take, e.g., the Spec. 4.7 of Lists that is redefined below. Note that item 1 in the enumeration above plays an essential role here, because we had specified the functional object ‘isprefix’ as

isprefix, isproperprefix : list -> list to bool

and not as isprefix, isproperprefix : -> [list x list] to bool .

We made this choice because we wanted to apply it in forms like ‘mapch(isprefix(l), C)’.

Specification 4.13 (Lists, final version) module Lists <LISTITEM>

short L
imports

Booleans { public: bool, true, false } Naturals { public: nat, 0, s }

add signature
parameters:
(
 sorts

LISTITEM

)
public:
 sorts

list<LISTITEM>

 constructors

[]<LISTITEM> :  list
::  : LISTITEM list -> list

 functions

hd : list -> LISTITEM
tl  : list -> list
length : list -> nat
null : list -> bool
dl, rc : LISTITEM list -> list
∈ : LISTITEM list -> bool
nth : nat list -> LISTITEM
append : list list -> list
isprefix, isproperprefix : list list -> bool

variables

n : nat
i, j : LISTITEM
k, l : list

axioms

\begin{matrix}hd(i:: l) = & i \\ tl(i:: l) = & l \end{matrix}

null([]) = true
null(i:: l) = false
nth(0, i:: l) = i
nth(s(n), i:: l) = nth(n, l)

/* dl(i, l) deletes any occurrence of i in l, rc(i, l) only the repeated occurrences, i.e. it removes copies of i in l */

[dl1] dl(i, []) = []
[dl2] dl(i, j :: l) = dl(i, l)  if i=j
[dl3] dl(i, j :: l) = j :: dl(i, l) if i≠j
[rc1] rc(i, [])  = []
[rc2] rc(i, (j :: l)) = (j :: dl(i, l)) if i=j
[rc3] rc(i, (j :: l)) = (j :: rc(i, l)) if i≠j
[∈1] i ∈ []  = false
[∈2] i ∈ (j :: l) = true if i=j
[∈3] i ∈ (j :: l) = i ∈ l if i≠j
length([]) = 0
length(i:: l) = s(length(l))
append([], l) = l
append(i:: k, l) = i:: append(k, l)
isprefix([], l)  = true
isprefix(i:: k, []) = false
isprefix(i:: k, j :: l) = false  if i≠j
isprefix(i:: k, j :: l) = isprefix(k, l) if i=j
isproperprefix(k, [])  = false
isproperprefix([], j :: l) = true
isproperprefix(i:: k, j :: l) = false  if i≠j
isproperprefix(i:: k, j :: l) = isproperprefix(k, l) if i=j

Note that we also could introduce λ-terms now as a syntactic sugar for anonymous function definitions. We, however, do not do this on purpose, because specifications are easier to read if any function has a name. Moreover, one of the design decisions of ASF^{+} was that anything must have a name that can be understood and deduced from the structured specification.^{2}

Note that the fact that the last line of the above specification actually reads

apply(apply(isproperprefix, i:: k), j :: l) = apply(apply(isproperprefix, k), l) if i=j

is only relevant for the automated admissibility check of the defining rules, including an effectively testable confluence criterion that guarantees consistency of the specification. The specifier only has to realize the actual form of the rule in the rare cases where this check fails. Note that the admissibility check of Kühler & Wirth (1996) has no problems with any of the specifications above.

2E.g., the anonymous renaming of hidden clashing names of ASF has been replaced in ASF^{+} by appending the name-space names to the front of the clashing names, resp..

Finally, we have to remark that there are also some problems introduced by this solution:

1. Overloaded function names may only be used with sufficiently many arguments to

disambiguate them. E.g., if we have two function declarations

\begin{matrix}f : & s s′_{0} & -> & s′′ \\ f : & s s′_{1} & -> & s′′ \end{matrix}

Then it is illegal to write f(x) or f(x)(x′) but legal to write f< : s s′_{0}>(x) or f(x, x′).

2. Suppose we would use the function

insert : nat set<nat> -> set<nat>

in Spec. 4.9 as functional object in a function

f : (nat set<nat> -> set<nat>) -> s

then it is illegal to write f(insert) but legal to write f(insert<nat>) although ‘insert’ was not qualified in Spec. 4.8. The reason for this is that ‘insert’ belongs to the name-space ‘Sets’ and is overloaded with the ‘insert’ from all other instantiations of ‘Sets’.

5 Syntax

The syntax of ASF^{+} is given by the following context-free grammar.

We denote terminal symbols with quotation marks and typewriter font, non-terminal symbols with <…>. x* means zero, one, or several repetitions of x. x^{+} means one or several repetitions of x. (x “t”)* and (x “t”)^{+} denote repetitions of x, separated by the terminal symbol t. Optional parts are put into brackets […].

<specification> ::= <module>^{+}
<module> ::= “module” <module-name>[<parameter-blocks>]

[“short” <short-module-name>] [<imports>] [<add-signature>] [<variables>] [<general-variables>] [<axioms>] [<lemmas>] [<theorems>]

<parameter-blocks> ::= “<” <parameter-block>^{+} “>”
<parameter-block> ::= “(” (<sort-or-func-name> “,”)^{+} “)”
| <sort-or-func-name>
<sort-or-func-name> ::= <sort-name> | <function-name>
<qualified-sort-or-func-name> ::= <qualified-sort-name> | <qualified-func-name>
<qualified-sort-name> ::= <sort-name>[<parameter-blocks>]
<qualified-func-name> ::= <function-name>[<parameter-blocks>]
<imports> ::= “imports” <import>^{+}
<import> ::= <module-name>

[“[”<instance-name>“]”] [“<” <ext-para-block>^{+} “>”] [“{” <import-block> “}”]

<ext-para-block> ::= “(”(<name-with-ren> “,”)^{+} “)”
| <name-with-ren>
| “(”(<sort-or-func-name> “,”)^{+} “)”

“bound to”

“(”(<qualified-sort-or-func-name> “,”)^{+} “)” “of” <module-name>[<parameter-blocks>]

| <sort-or-func-name>

“bound to”

<qualified-sort-or-func-name> “of” <module-name>[<parameter-blocks>]

<name-with-ren> ::= <sort-or-func-name>

[“renames” <sort-or-func-name>]

<import-block> ::=

[ “public:” (<qualified-name-with-ren> “,”)^{+} ]
[ “private:” (<qualified-name-with-ren> “,”)^{+} ]
<qualified-name-with-ren> ::= <qualified-sort-or-func-name>

[“renames” <qualified-sort-or-func-name>]

| “copy of” <qualified-sort-or-func-name>

<add-signature> ::= “add signature”
[ “parameters:” <para-block-sig>^{+} ]
[ “public:”  <signature> ]
[ “private:”  <signature> ]
<para-block-sig> ::= “(” <signature> [<conditions>] “)”
<signature> ::= [ “sorts” (<qualified-sort-name> “,”)^{+} ]
[ “constructors” <function-dec>^{+} ]
[ “functions”  <function-dec>^{+} ]
<function-dec> ::= (<ext-func-name> “,”)^{+} “ : ” <sort-dec>
<ext-func-name> ::= <qualified-func-name> [“ ”]
| “ ” <qualified-func-name> “ ”
<sort-dec> ::= <qualified-sort-name>
| <ext-sort-name>^{+} “ -> ” <ext-sort-name>
<ext-sort-name> ::= <qualified-sort-name>
| “(” <ext-sort-name>^{+} “ -> ” <ext-sort-name> “)”
<eq> ::= <term> [“=” <term>]
<term> ::= [<term> <function-name>] <primary>
<primary> ::= <qualified-func-name>

<primary>

| <qualified-func-name>

[“< : ” <ext-sort-name>^{+} “>”] [“(” (<term> “,”)^{+} “)”]

| <variable-name>

[“(” (<term> “,”)^{+} “)”]

| “(”<term>“)”
<variables> ::= [“constructor”] “variables” <variable-dec>^{+}
<general-variables> ::= “general-variables” <variable-dec>^{+}
<variable-dec> ::= (<variable-name> “,”)^{+} “ : ” <sort-dec>
<axioms> ::= “axioms” <axiom>^{+}
<axiom> ::= “[” <label-name> “]” <eq> [“ if ” (<eq> “,”)^{+}]
| <macro-equation>
<lemmas> ::= “lemmas” <lemma>^{+}
<lemma> ::= “[” <label-name> “]” <formula>
<theorems> ::= “theorems” <theorem>^{+}
<theorem> ::= “[” <label-name> “]” <formula>
<conditions> ::= “conditions” <condition>^{+}
<condition> ::= “[” <label-name> “]” <formula>

The lexical conventions of ASF^{+} are the following:

• The usual white-space characters separate tokens.

• The names introduced by the user (i.e. <module-name>, <short-module-name>, <instance-name>, <label-name>, <sort-name>, <function-name>) consist of an arbitrary sequence of numbers, letters, prime (′), and underscore ( ). But the underscore must not appear at the very beginning or ending of a name because this is used for defining infix operators.

• The keywords, however, cannot be used as names. Moreover, “<” and “>” must not appear in names because they are reserved to enclose the lists of parameter blocks. Furthermore, “(”, “,”, and “)” must not appear in names for similar reasons.

• (Short) names of modules (<module-name>, <short-module-name>) and instance names (<instance-name>) must not contain the symbols “[” and “]” because this can be confused with the brackets enclosing the instance names.

• At least the following ASCII-characters may additionally appear in names of sorts or functions (<sort-name>, <function-name>): “:”, “-”,“+”, “*”, “!”, “$”, “%”, “&”, “;”, “?”, “∼”, “\”, “|”, “/”, “.”, “[”, “]”. The opening bracket (“[”), however, may not occur if there is a module name that is equal to the prefix up to the first occurrence of an opening bracket. Moreover, the name “:” must not be any user name.

References and Notes

Jan A. Bergstra, Jan Heering, Paul Klint (1989). Algebraic Specification. ACM Press.

Ulrich Kühler, Claus-Peter Wirth (1996). Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving. SEKI-Report SR–96–11, Univ. Kaiserslautern. Short version in: 8^{th} RTA 1997, LNCS 1232, pp. 38-52, Springer.

Rüdiger Lunde, Claus-Peter Wirth (1994). ASF+ – eine ASF-ähnliche Spezifikationssprache. SEKI-Working-Paper SWP–94–05 (SFB), Univ. Kaiserslautern.

Acknowledgements: