!!! This text has been created automatically from the original framemaker script !!! The formatting is poor we know. If you need a better one print the postscript !!! version. ASpecT Version 2.0 Quick starter Richard Seifert and Jorn von Holten University of Bremen October 1992 1. Introduction This manual is intended to give a quick introduction to the ASpecT programming language. For further details consider the ASpecT language reference and the ASpecT system reference manual. The ASpecT language was initially developed in 1986 as an attempt to provide an implemen- tation for (a subset of) Algebraic Specifications of Abstract Datatypes. Also parametrized mod- ules were supported. From the beginning the system was designed to be as user-friendly as pos- sible, including overloading facilities and a source-level debugger. Efficiency called for by val- ue evaluation and reference counting memory management. Over the years more and more features were added, including subsorting, functionals and re- stricted polymorphism. Still the language is under development. Current plans include views and object-oriented lan- guage extensions. 2. Language description A module (specification) consists of imported modules, signatures and axioms. It can be divided into a global interface and a local implementation. For parametrized modules an additional formal parameter part is present. Note that 'GLOBAL' is only valid if a formal part exist. Example: SPEC TEST = END. Syntax: specification ::= SPEC '=' ((FORMAL body [GLOBAL body]) | body) [LOCAL body] END '.' . body ::= {import '+'} {part}. part ::= include | sorts | opns | macros | forall axioms | forall theorems. ::= [A-Za-z0-9]* | [A-Z0-9_]*. 2.1. Signature The signature of a module consists of datatype (sort) and function (operation) declarations. 2.1.1. Datatypes (Sorts) Datatypes declarations (Sorts) are introduced starting with their name and followed by their data creating (constructor) functions. Names of sorts and constructors begin with a lower case letter. The constructor functions have an associated type declaration. Sorts (except formal, external and forward declared sorts (see 2.4 and 2.5)) must always have at least one associated constructor. Example: SORTS nat ::= zero | succ nat. Here the sort nat is declared together with the two constructors zero :: nat and succ:: nat -> nat (the constructor declarations are abbreviated). This means, that every term of sort nat can be represented as either zero (meaning 0) or succ(succ(...(zero)..)) (n times succ meaning n). The often used sort list of xx can be abbreviated by [xx]. Example: nats ::= [nat]. This makes the constructors [] :: nats and (:) :: nat -> nats -> nats available. Here the infix-con- structor (:) is a curried function which needs two arguments to actually build a list. Lists of El- ements x1:(x2:(x3:[])) can also be written as [x1,x2,x3]. To abbreviate structured types, type synonyms can be introduced: Example: SORTS relation ::= (data -> datas,datas). Here relation is a synonym for a tuple of a functional data -> datas and additional datas. Sorts can also be build by joining several existing sorts (subsorts). Example: SORTS int ::= (pos) | (neg). Here the sort int comprises both sorts pos and neg. In fact two unnamed constructors (coer- cions) of type :: pos -> int resp. :: neg -> int are declared. Those coercions should be carefully used, as they can easily introduce ambiguities when writing axioms (see 2.2). To extract components of constructor terms it is possible to declare additional data selectors/ modifiers. A data selector (projection) retrieves a component of a constructor term, a modifier changes a component of a constructor term. Any selector/modifier must be declared in every constructor present. Example: SORTS chunk ::= small(head :: data,datas) | big(head :: data,data,datas). Here a sort chunk with two constructors small :: (data,datas) -> chunk and big :: (data,data,da- tas) -> chunk is declared as well as the selector head :: chunk -> data and the modifier head :: (chunk,data) -> chunk. Syntax: sorts ::= SORTS {sort '.'}. sort ::= '[' type' ']' | sortcons. sortcons ::= ( cons | '(' types' ')' ) [ "|" sortcons ]. cons ::= ( | '(' ')' ) { type } | type0 type0 | '(' cons ')' type { type } type ::= type0 [ '->' type ]. type0 ::= [ '::'] | '(' types ')' . types ::= [ '::' ] type' [ ',' types ]. type' ::= type0' [ '->' type' ]. type0' ::= | '(' types' ')'. types' ::= type' [ ',' types' ]. See 2.2. for and . Note the difference between type' and type especially the usage of type' in types. 2.1.2. Functions Function declarations denote derived functions (operations) which operate on / yield construc- tor terms. Function names begin with a lower case letter (except for infix-functions, see below). Example: OPNS nat + nat :: nat. split:: nat -> nats -> (nats,nats). Here two derived functions (+) :: nat -> nat -> nat and split are declared. (+) is an infix-function for which infix-notation is available. It is assumed that axioms (see 2.2) are provided later on which describe the functions' behav- iour. Infix function names are sequences of special characters (excluding .,()[]{}#_" ). In addition for any curried function infix notation is available by prepending a '_' before the actual func- tion name. For convenience tuple selectors are implicitly declared to extract components of tuple results computed by functions. The selectors are named according to the name of the sort of the result they extract. In case of ambiguities these selectors can be differentiated by additional numbers. In the exam- ple the implicit selectors are nats[.1] :: (nats,nats) -> nats and nats.2 :: (nats,nats) -> nats which extract the first resp. the second component of their argument tuple. Several functions with identical types can be enumerated, separated by commata. Syntax: opns ::= OPNS {decl '.'}. decl ::= items '::' type' '.'. items ::= [ EXTERN ] item [ ',' items ]. item ::= type0' type0' | | '(' ')' | | . 2.2. Axioms The axioms describe the behaviour of the derived functions. They are understood as rewrite rules from left to right. Several restrictions are imposed (loosened only for the non-operational theorems (see 2.2.2)). - The axioms must be unambiguously typeable, type variables eliminated. - Only axioms for derived functions may be written - The left-hand-side (lhs) arguments of the derived functions must consist of variables and constructors only. Variable names always begin with a capital letter. - The axioms must be left-linear. This means, no variable may occur more than once in an axioms lhs. - All the variables of the axioms right hand side (rhs) must also occur in the axiom's lhs. - All the variables of the axioms lhs must also occur in the axiom's rhs. This means that variables occurring only in the lhs must be anonymised (written as _). - The axioms for a derived function must be grouped together - The axioms lhss for a derived function must cover all possible cases of argument terms. - The axioms lhss for a derived function must not overlap, i.e. there must not be argument terms for which more than one axiom is applicable. The variables always begin with a capital letter. Example: (continued) EQNS X + zero = X. X + succ Y = succ(X + Y). Here the function (+) is described by two axioms. The first means that adding any term (denot- ed by variable X) to zero will result in X. The second axiom means that adding any term X to another term of form succ Y results in a term succ Z where Z is obtained by adding X and Y. There are no builtin operator precedences in ASpecT, infix-terms associate from left to right. Function application always binds higher than infix-operators. To resolve ambiguities it is possible to declare functions' and variables' types. In addition any term can be annotated with its presumed type. Example: FORALL X :: nat. EQNS X + (zero :: nat) = X. For the conditional if_then_else :: (boolean,data,data) -> data (see 2.6.2) a 'mixfix' - notation is available. The if-then-else name parts bind less than any other function application or infix- operator. Example: EQNS abs X = if X >= zero then X else neg X. As an abbreviation there is a case-construct dealing with multiple conditions involving the buil- tin equality (see 2.6.2). Example: EQNS g X = case X of 0: 0 | 1,2: 1 | 3: 2 else X. This is equivalent to the nested conditionals (where elsif is an abbreviation of 'else if'). g X = if X == 0 then 0 elsif (X == 1) || (X == 2) then 1 elsif X == 3 then 2 else X. Sometimes it is more convenient to write overlapping axioms, violating restriction (vi). For this purpose axioms may be annotated to be catch-all axioms (by a preceding '$'). These catch-all axioms may overlap with normal axioms and by definition only deal with cases not covered by the normal axioms. Catch-all axioms may not overlap with other catch-all axioms though. Example: EQNS f zero = zero. $f X = X. As an abbreviation previously declared macros (see 2.2.1) may also occur in the axioms. In the current version macros may only occur in the axioms' rhs. Syntax: forall ::= [FORALL {decl '.'}]. axioms ::= EQNS {axiom '.'}. axiom ::= ['$'] term '=' term. term ::= simple { ('::' | '``') type }{ infix term }. terms ::= term { ',' term }. simple ::= simple1 | '-' | term_oph term_args. simple0 ::= simple1 | term_oph. simple1 ::= 'if' term 'then' term else | 'case' term 'of' case { '|' case } else | 'let' eqn { eqn } 'in' term | '[' [ terms [ '|' term ] ] ']' | | | . term_oph ::= | '_' | '.' | '(' terms ')' | | | '(' ')'. term_args ::= [ ('(' terms ')' | simple0) term_args ]. case ::= terms ':' term. else ::= { 'elsif' term 'then' term } 'else' term. Note that names in <> stand for lexicalic elements such as string lexemes (,2.6.1), character lexemes (,2.6.1), integer lexemes (,2.6.1), variable identifiers (), normal identifiers (), macro identifiers () and infix identifiers (). ::= [a-z][A-Za-z0-9_]* ::= [A-Z][A-Za-z0-9_]* ::= '_' | '_' | [!#$%&*+,-/:;<=>?@^`|~]* ::= '#' | '#' . The sequences '/*', '=', '``' and '::' are not regarded as as well as a single '#' imedia- telly followed by a letter which leds to a . In the cases where starts with a '_' this leading character is omited (i.e. '_mod' is actually the identifier 'mod'). 2.2.1. Macros and Lets Macros can be understood as intermediate variables denoting terms. They correspond to LET- or WHERE-clauses in functional programming languages. In contrast they are not associated with a particular rule, but are valid for all rules following the macro declaration up to the next macro block which hides all previously declared macros. Macro names are distinguished by a leading '#' followed by or . Example: MACROS #XX = X * X. EQNS f X = #XX + #XX. Here a macro #XX standing for the term X * X is introduced. It is used by function f which thus returns (X * X) + (X * X). Macros also may be parametrised to allow for a more general usage. Macro argument variables also begin with a '#'. Example: MACROS #XX(#Z) = #Z * #Z. EQNS g(X,Y) = #XX(X) + #XX(Y). Here the parametrised macro #XX is instantiated twice (by X and Y). Thus function g yields (X * X) + (Y * Y). Macros are especially useful in connection with functions yielding tuple results, the compo- nents of which can be given explicit names. Example: MACROS (#sum,#sums) = sigma(X,Y). EQNS sigma(_,zero) = (zero,zero). sigma(X,succ Y) = (X + #sum,#sum + #sums). Here the function sigma returns a tuple of two (nat) result terms. The macro declaration could also be written as MACROS #sum = nat.1(sigma(X,Y)). #sums = nat.2(sigma(X,Y)). Parametrized macros may not contain (nested) tuples or unnamed variables ('_'). All of the macro's parameters must be used in its right hand side. The left hand side of a macro equation may only contain macro identifiers. The let...in construct on the other hand is in this language version a shorthand for macros. Re- strictions layed on macros are true for lets too. But unlike macros, this construct is part of the right hand side of an equation (equation or theorem) - lets may not be written in macros or at any right hand side of an equation. The scope of the definitions made in the let construct is lim- ited to the term following the 'in'. There are several restrictions and abbreviations in this ver- sion. Semantically there may be only one equation per let construct. If you write more than one equa- tion as in let X = Y+1. Z = A+1. in X+Z this is regared as a nested let construct let X = Y + 1. in let Z = A + 1. in X+Z As a consequence it is possible to redefine variables as in goal S = let S = S + "Hello ". S = S + "world\n". in S. The left hand side of lets may only consist of variables or (nested) tuples of variables. No ap- plications (as allowed for macros) are possible. One should keep in mind that the local variables are not visible in macros. Lets are translated to macros and therefore some error messages may be irritating. Syntax: macros ::= MACROS {macro '.'}. macro ::= term '=' term. 2.2.2. Theorems It is possible to write axioms without any restriction (except being unambiguously typeable). They are for specification purposes only and are not further considered by the compiler. Example: THEOREMS X + (Y + Z) = (X + Y) + Z. X + Y = Y + X. Syntax: theorems ::= THEOREMS {axiom '.'} 2.3. Imports A hierarchy of specifications can be built by importing specifications. Specifications may be imported more than once (perhaps via different paths) but cyclic imports are forbidden. Example: SPEC NAT = ... END. SPEC BOOL = ... END. SPEC NAT_OPS = NAT + BOOL + ... END. Here the specifications NAT and BOOL are imported by the specification NAT_OPS. Modules can be imported at the beginning of a global and local part or they can be inserted at any place of the program (headed by the keyword IMPORTS). Syntax: import ::= specid [instantiation]. include ::= IMPORTS import '+' {import '+'} 2.4. Parametrisation To enhance the reusability of specifications it is possible to abstract some details (which are declared formal) to be instantiated (actualized) differently for different usages. Example: SPEC LIST = FORMAL SORTS data. GLOBAL SORTS list :: [data]. OPNS concat :: (list,list) -> list. ... END. Here the specification LIST contains the formal parameter sort data. It declares a sort list as a list of datas and also a function concat operating on such lists. By different instantiations it is thus possible to generate e.g. lists of nat or list of boolean values together with the respective concat functions (see below). Example: (continued) SPEC LISTS = LIST ACTUAL SORTS data = nat. list = nats. END + LIST ACTUAL SORTS data = boolean. list = bools. END + ... Here the parametrized specification LIST is instantiated twice: first the formal sort data is in- stantiated (actualized) by nat and the generated list sort is renamed to nats to avoid name clash- es with the second instantiation in which data is instantiated by sort boolean. The formal parameters can also be functions, actual parameters can also be formal, thus allow- ing for nested instantiations. Example: SPEC SET = FORMAL SORTS data. OPNS eq::(data,data) -> boolean. GLOBAL SORTS set. ... LOCAL LIST ACTUAL SORTS data = data. list = set. END + ... Here the parametrized specification SET contains a formal sort data together with a function eq to compare data values. The generated sort set is implemented locally (see 2.5) as a list of data values. The formal data sort data from LIST is actualized by the formal sort data from SET. In the current version there is restriction concerning the instantiation of formal sorts with for- mal constructors by actual sorts containing tuple sorts in places where the formal sorts only have a formal sort. Instantiation with tuple sorts requires a quite expensive implementation and several implicit translation functions. This translation does not consider tuple sorts within datastructures in the current version. Example: SPEC PAR = FORMAL SORTS data. list ::= [data]. ... END. SPEC ACT = PAR ACTUAL SORTS data = (integer,integer). datas = ii. END + SORTS ii ::= [(integer,integer)]. ... END. Here the formal sort data of PAR is instantiated with a tuple of integers. This is not forbidden by itself, but the following instantiation of datas by ii is, because it creates an instantiation of a datastructure (list of data) by a tuple. Syntax: instantiation ::= ACTUAL [SORTS {actsort '.'}] [OPNS {actopn '.'}] END. actsort ::= sortid '=' sortid. actopn ::= opname ['::' type] = opname ['::' type]. 2.4.1. Polymorphism In some cases it is possible to omit the instantiation of parametrized modules and let it be in- ferred by the ASpecT parser. This mechanism is called polymorphic import. In the current version only parametrized modules without formal operations can be polymor- phically imported. Furthermore all actual parameter sorts must be inferable when using any of the generated global functions. Example: SPEC LISTOPS = FORMAL SORTS data. datas ::= [data]. GLOBAL OPNS datas ++ datas :: datas. ... END. SPEC USE = LISTOPS + SORTS ints ::= [integer]. OPNS f :: ints -> ints. EQNS f XX = XX ++ XX. END. Here the module LISTOPS is polymorphically imported by USE. In the axiom for f the poly- morphic function (++) is used. The instantiation inferred is LISTOPS ACTUAL SORTS data = integer. datas = ints. END + If LISTOPS contained e.g. another function g :: data -> data, LISTOPS could no longer be polymorphically imported, because by using g in any axiom the instantiation of datas could not be uniquely inferred. 2.5. Scoping rules Specifications may be split into globally visible and local parts. Only the global parts can be accessed from other specifications. The same holds for globally and locally imported specifi- cations. Example: SPEC NAT_OP = NAT + OPNS f :: nat. LOCAL BOOL + OPNS g :: nat -> boolean. END. Here the specification NAT_OP globally imports specification NAT and declares function f. The locally imported specification BOOL as well as the local function g are not visible outside this specification. It is possible to hide the sorts representation (constructors) by making global only the sort name (a kind of forward declaration) and putting the complete sort declaration into the local part. Example: SPEC TABLE = SORTS table. ... LOCAL SORTS table ::= mt | b(data,table,table). END. Here only the sort name table is visible outside, its concrete representation by the constructors mt and b is hidden. In the current version it is not possible to forward declare synonyms or sorts containing sub- sorts. A forward declaration is implicit in certain instantiations of parametrized modules, when not yet declared sorts and functions are used as actual parameters. In the current version forward declared functions and sorts must be declared later in the same module (they may not be imported). All imported modules in the global (local) part of a module are visible from the beginning of the global (local) part but their order is not changed. All sort blocks and all function declarations are treated in the same way. For sort declarations there is a linear visibility constraint which is disabled within a sort block to allow for mutually recursive sorts. Macro definitions are visible until the next macro block which hides all preceding macro defi- nitions. Macros cannot be (mutually) recursive and must be declared in order of usage. 2.6. Builtins 2.6.1. Builtin sorts The sorts boolean, integer, char, string and system are builtin. The sort boolean is declared as boolean ::= true | false. The sort integer consists of the constants () -maxint, .. -2,-1,0,1,2,..,maxint. You may write octal ('0'[0-7]*) and hexadecimal (0[xX][0-9a-fA-F]*) constants too. Note that the mi- nus sign is not part of the lexeme and that constants which are too large (system depended) are no lexemes. The sort char consists of all character constants (), e.g. 'a','A','0'. Special characters are represented as described below (2.6.1.1). The character '\t' which is normally invisible is re- placed by up to eight blanks depending on its position. The sort string consists of all string constants (), e.g. "ASpecT", "A b c". Special char- acters are represented as described below. The character '\t' which is normally invisible is re- placed by up to eight blanks depending on its position. Do not use a '\NUL' character within strings (implementation restriction). The sort system is not further specified and represents the operating system state. It is used in the operating system interface (see 2.6.3). 2.6.1.1. Special Characters We support various possibilities to build special characters. These possibilities can be divided in several categories. All these characters have in common that they begin with a backslash (\) known as escape character. Therefor the special characters are sometimes called escape se- quences. In describing the possible sequences we name the decimal value of the sequence. The well know set of escape sequences of the C language are supported. \a 7 \b 8 \f 12 \n 10 \r 13 \t 9 \v 11 \\ stands for \ \" stands for ". Need not be escaped in character constants. \' stands for '. Need not be escaped in string constants. The so called controll sequences are supported. \^@ 0 \^H 8 \^P 16 \^X 24 \^A 1 \^I 9 \^Q 17 \^Y 25 \^B 2 \^J 10 \^R 18 \^Z 26 \^C 3 \^K 11 \^S 19 \^[ 27 \^D 4 \^L 12 \^T 20 \^\ 28 \^E 5 \^M 13 \^U 21 \^] 29 \^F 6 \^N 14 \^V 22 \^^ 30 \^G 7 \^O 15 \^W 23 \^_ 31 The ASCII standard names can be used. \NUL 0 \BS 8 \DLE 16 \CAN 24 \SOH 1 \HT 9 \DC1 17 \EM 25 \STX 2 \LF 10 \DC2 18 \SUB 26 \ETX 3 \VT 11 \DC3 19 \ESC 27 \EOT 4 \FF 12 \DC4 20 \FS 28 \ENQ 5 \CR 13 \NAK 21 \GS 29 \ACK 6 \SO 14 \SYN 22 \RS 30 \BEL 7 \SI 15 \ETB 23 \US 31 and \DEL 127 You can represent these values by giving their numerical value directly. Decimal, octal and hexadecimal values can be used. Octal values start with \o and are followed by at least one octal digit (0-7). Hexadecimal values start with \x and are followed by at least one hexadecimal digit (0-9,A-F,a-f) and decimal values just start with a backslash and are followed by at least one decimal digit (0-9). The value ends if an illegal character appears. The value may not exceed 127. In strings you may use the escape sequence \& to end values if needed. This sequence is omitted whereever it is written. If a backslash in string constants is followed by whitespace (' ', '\t', '\n') and later another backslash this sequence is omitted as well. This construct is know as gap and can be used to write string constants which exceed one line (formatting purpose). All other escaped characters stand for themselves meaning the backslash is omitted. 2.6.2. Builtin functions For every sort s, builtin or user declared, there is a builtin equality (==):: s -> s -> boolean. For convenience there is also a builtin conditional if_then_else :: (boolean,s,s) -> s. written mixfix. Other functions on builtin sorts are external (see 2.7) and could be replaced by user implemen- tations. 2.6.3. Operating system interface The operating system is represented by the builtin sort system. Functions which change the op- erating system state (e.g. i/o- functions) thus get and return a system parameter. It is not allowed to 'backtrack' on the operating system, that is to manipulate a system state and later refer to its old value. The basic functions to read and write terms can be found in the standard modules READ- WRITE, STREAM and SYSTEM. The root module of a specification is assumed to contain a user defined function goal :: system -> system which is called by the ASpecT runtime system after initialization with the initial system state. Example: SPEC HELLO = STREAM + OPNS goal :: system -> system. EQNS goal S = S + "Hello world !\n". END. Here the string "Hello world!" is written to the standard output. 2.7. External sorts and functions To allow for the usage of functions and sorts implemented in other languages it is possible to qualify sorts and functions as external. Nevertheless their usage should be minimized as they require profound knowledge of ASpecT implementation and leave the firm ground of the AS- pecT specification language. It is not allowed to declare constructors for external sorts nor to write axioms for external func- tions. Example: SPEC ARRAY = ... SORTS EXTERN array. OPNS EXTERN create_array::(integer,data) -> array. ... Here the implementations of sort array as well as of function create_array are assumed to be external (written in another language, preferably C). If a module contains external sorts and/or functions the compiler assumes the presence of ad- ditional files with suffix .xh / .xc where their implementions in C should be present (in the ex- ample ARRAY.xh and ARRAY.xc). For every external sort s at least five external functions must be implemented, that is functions to read, write, compare for equality, copy and free terms of sort s. The latter two functions refer to the memory management (see 4.5) and are used to create or destroy a reference to a term of sort s. The external functions must also take care of the memory management and be careful to insert the appropriate copy and free function calls (see 4.5). 3. Tools 3.1. Program generator The ASpecT program generator is called gen. First it (recursively) scans ASpecT modules (.AS) and computes the import hierarchy describ- ing global and local module dependencies, which are stored in associated .IMP files. The AS- pecT intermediate forms produced by the scanner have the suffix .AS0. Files are searched according to the ASpecT environment variable ASPECT in which directo- ries containing ASpecT modules are listed. Gen needs a so-called command template file (see 5.1). In this file the different commands to be issued are listed, together with the suffixes of the files they need and produce. To create an executable program from an ASpecT source, calls to the ASpecT parser (asp, see 3.2), the ASpecT translator (sc, see 3.2), the C compiler (cc or gcc) and the linker (ld) must be present in the command template file. The -n and -d options force the translation of the given files with (-d) or without (-n) debugging information. With -u it is possible to remove all debugger calls by retranslating the respective files. By -o an alternative name for the generated executable file may be given (default is lower case of root module name). To show the issued commands without executing them the -s option is provided. Example: gen HELLO -ohy generates an executable file called hy. Gen is capable of using several machines in a network. For this purpose a file containing the names of the machines to be used (net.cfg) is needed. Gen is then called with option -p. 3.2. Parser The parser (asp) expects a .AS0 file and assumes that all imported files are already parsed. It produces a .AS1 and a .IDS file if successful. The number of different parses (due to overloading of identifiers) considered is set to 40 but may be changed by supplying a -m parameter to asp in the command template file (see 5.1). 3.3. Program translator The ASpecT program translator is called sc. It translates ASpecT internal representations (.AS1) to C programs (.c and .h) and is normally called by the ASpecT program generator gen (see 3.1). sc reads ASpecT internal files with suffix .AS1 and generates two C source files with .h and .c suffix. The -db option causes the insertion of debugging information (see 3.4). The maximal depth (-td) and size (-ts) of generated C program terms may be given to cope with C compiler limitations (default is depth=10 and size=20). Example: sc FILE -db reads the internal form FILE.AS1 and generates the corresponding C program FILE.h and FI- LE.c containing debugger calls. The termination checker (see 3.3.1) can be enabled by supplying the -t option. 3.3.1. Termination checker Build into the program translator are various program analyses. One of them is the so-called termination checker which tries to verify the termination of func- tions. It builds a program call graph and constructs a termination ordering according to the axioms. External and imported functions are assumed to terminate. Termination checking proceeds even if some underlying functions cannot be shown to be terminating. Calls which do not obey the constructed termination ordering are indicated as 'probably non- terminating'. In the current version of ASpecT functionals are not correctly handled by the termination checker (in a conservative way, though). 3.4. Runtime debugger The runtime debugger is part of the runtime system and allows for the separate debugging of program modules. Calls into modules to be debugged as well as calls from these modules are displayed. Displayed function calls are headed by a call level (increased by recursive calls) and printed only up to a given (adjustable) term depth. Argument and result terms may be examined by navigating along them. Their type can be dis- played. Function calls may be skipped or stepped into, it also possible to skip until a given call level is reached. Breakpoints on specific functions may be set or removed. Call statistics about function calls may be displayed. For an overview of available debugger commands type '?' when running a program including debugger calls. 3.4.1. Interpreter When running a program including debugger calls it is possible to evaluate function calls in a restricted way: all of a functions arguments must already be evaluated, i.e. consist of construc- tors only. To enter interpreter mode simply type 'i'. In the current version this feature is not quite stable (unfortunately). 4. Language implementation All of the ASpecT tools have been written in the ASpecT language comprising about 25000 lines of ASpecT specifications in more than 150 modules. A small runtime kernel (including the runtime debugger and interpreter) has been implemented in C. The resulting C programs (more than 100000 lines) bootstrap themselves on a SUN SLC in about one hour to executable code requiring about 1 Megabyte of heap space. In what follows some of the used implementation techniques are described. They should be taken into account by experienced ASpecT programmers in order to achieve maximum efficiency. 4.1. Pattern matching The defining equations for a given function are grouped together and a corresponding C func- tion is generated. The patterns occurring on the equations left hand sides are compiled into case cascades. The order in which argument patterns are scanned is determined by a simple heuristic: they are scanned in order of descending frequency of occurrence in the defining equations. 4.2. Common subexpression elimination Calls of non-constructor (derived) functions are extracted from the equations and replaced by intermediate variables. Calls appearing more than once are collapsed and represented by the same intermediate vari- able. 4.3. Unfolding Certain derived functions are unfolded, their definitions are inserted in place of their call. This is especially useful for functions which do not evaluate all of their parameters (non-strict func- tions). After unfolding an attempt is made to move calls into the case cascades of the unfolded calls to avoid some computations. In the current version unfolding takes place inside a module if the right hand side of the defi- nition(s) consist of a constant expression or a single call to another definition. This must be true for all equations. Intermodular unfolding is somewhat more restricted. The unfolded calls have to be visible meaning they have to be global and for specific reasons string constants are not unfolded now. Look into the standard module BOOLEAN for three examples of unfoldable operations. 4.4. Recursion removal Function calls are more costly than simple gotos (jumps). Therefore the ASpecT-translator at- tempts to transform recursive functions into iterative ones. This is possible for (constructor) tail recursive functions. These functions allow the recursive function call(s) to be moved to the end of the function code. In this situation the recursive calls can be changed into simple gotos. 4.5. Memory management Any term contains a reference count, denoting how many references to it exist. When e.g. in an axioms rhs a variable occurs more than once, the term bound to this variable must be copied when executing this rule. It is not physically copied, but it's reference count is increased. When leaving a function, all terms not occurring in the functions result can be destroyed. This is achieved by decreasing their reference counts. When a reference count reaches 0, the term be- comes garbage and is inserted in a so-called free list. When new terms are constructed, they are preferably taken from this free list. The signature of the modules is held in a separate data structure, which is needed for reading, writing and freeing terms. This data structure is allocated during initialization. 5. Installation The ASpecT system consists of - the runtime system, - the runtime debugger and interpreter, - the ASpecT server for distributed program generation, - the ASpecT tools (generator, parser, translator), - the command template file (default.cmd, see 5.1), - various standard modules - manual entries for the ASpecT tools and - this manual. The ASpecT runtime system, debugger and server should be copied in a separate directory (e.g. ASpecT/runtime). The ASpecT tools should be placed in a directory which is included in the search path for ex- ecutable files (e.g. ASpecT/bin). The standard modules should also have their own directory (e.g. ASpecT/standard). The environment variable ASPECT should be set to contain all directories where ASpecT source modules (inclusive the standard directory) and the command template file shall be searched. The ASpecT program translator creates ANSI-C source files. If needed also non-ANSI-C is supported by simply not defining the C-constant '__STDC__' (which is automatically defined by e.g. GNU-C). The support for both ANSI-C and non-ANSI-C is enabled by using the macros defined in the file ansidecl.h . 5.1. Command template file The command template file (default.cmd) required by the ASpecT program generator (gen) de- scribes the commands to be issued for generating an executable program from ASpecT source modules. The different entries in the command template file may contain placeholders (%p, %f, %i, %d, %m and %l). The %p placeholder can be used to prepend a base path before another path. %f stands for the current file for which commands are issued by gen. %i stands for a given destination directory when installing the ASpecT system on a new ma- chine. %d stands for optional debug parameters when needed. %m stands for a string which is substituted differently for imported files and for the root module, which is thus marked as main file. %l stands for all library modules which are the concatenation of the leading modules, the program specific modules and the trailing modules (see below). The command template file has the format (in ASpecT syntax) : template ::= cmd( string, {Header message} string, {Suffix of file containing module dependencies} strings, {Suffixes of needed and produced files} string, {Base path to be inserted in place of %p} string, {Program to check for presence of debugger calls} string, {Name of server for distributed generation} integer, {Min. nro. of processes for distributed generation} string, {Message issued when linking} string, {Base linker call} string, {Suffix of library modules to be linked} string, {Separator between library modules} strings, {leading library modules} strings, {trailing library modules} commands).{Commands to be issued} strings ::= [string]. commands ::= [command]. command ::= com(boolean, { net-able command } string, { Message to be printed on execution } string, { Command template } strings, { source-suffixes of this file } strings, { special source-suffixes of this file } strings, { source-suffixes of the imported files } strings, { spec. source-suffixes of imported files} strings, { target-suffixes } string, { %m-replace if handling the main file } string, { %m-replace otherwise } string, { %d-replace if debug-mode is on } string, { %d-replace otherwise } boolean, { indicates that this command is used for including/excluding debugger } mode). { mode for installation-handling } mode ::= always | {Indifferent of installation mode} not_install | {Command issued when not installing} install. {Command issued when installing} Example: (for SUN/Unix with GNU-C) cmd( "GNU-C Version (SPARC)", ".IMP", [".AS0",".IMP",".AS1",".OPD",".c",".h",".4.o"], "/user/aspect", "%p/bin.4/sc -q -dbtest %f", "aspserv",4, "Linking", "/bin/gcc-ld -e start -dc -dp %l -o %f", ".4.o", " ", ["/usr/lib/crt0.o", "%p/ASpecT/runtime/runtime.4.o", "%p/ASpecT/runtime/rts_db.4.o"], ["/usr/local/lib/gcc-gnulib", "/usr/lib/libc.a", "/usr/lib/libg.a"], [com(true,"Parsing","%p/bin.4/asp -q %f", [".IMP"],[],[".AS1"],[],[".AS1"], "","","","", false,always), com(true,"Generating","%p/bin.4/sc -q %d %f", [".AS1"],[],[".OPD"],[],[".c",".h",".OPD"], "","","-db","", false,not_install), com(true,"Generating","%p/bin.4/sc -q -noheader %d %f", [".AS1"],[],[".OPD"],[],[".c"], "","","-db","", true,not_install), com(true,"Installing","%p/bin.4/sc -q -todir %i %d %f", [".AS1"],[],[],[],[".c",".h"], "","","-db","", true, install), com(true,"Compiling", "/bin/gcc -g -c -O %m -I%p/ASpecT/runtime %f.c -o %f.4.o", [".c",".h"],[".xc",".xh"],[".h"],[".xh"],[".4.o"], "-DMAIN","", "","", false,not_install)] ) Appendix A: System Messages In the following table the messages generated by the ASpecT system are listed in alphabetical order. To express varying parts of the messages placeholders enclosed in pointed brackets (<>) are inserted. Many of the messages are preceded by the specification the message refers to and are followed by "at line in column " to state the exact position in the file. This is missing in the table. The messages are described in two parts. The first one (introduced by a "") describes the cause of the error and the second (introduced by a "") offers possible solutions how to handle the message. Table A.1: The System Messages -db and -stat turned off due -opt option This information is written by the C paraphraser when the -opt option is set and at least one of the options -db or -stat is set too. The -opt option enables the optimizer mode. This is in contrast to -db and -stat which disable the optimizer mode. Since this is just an information the system continues working. expected A syntax error occurred at the specified location. Correct the syntax error considering the tokens expected. Actual sort must have constructors A formal sort is restricted by some constructors. An actualization of this sort has been performed with a sort not having such restrictions. Enter the constructors for the actual sort too. Ambiguous equation: A definition has been formulated which cannot be fixed to a single interpretation. Some of the possible interpretations are given as fully typed terms. The place of first difference is marked. Use the FORALL declaration or type annotations to remove the ambiguities. Ambiguous formal opn An overloading on the names of formal operations exist. At time of instantiation only their name is given. In the current version of the compiler this situation is not resolved. The user has to give the whole argument and domain sort of the formal operation too to resolve it. Ambiguous projection : An explicit projection has been defined on the constructors of a sort which overlaps with other explicit projections with that name projecting the same sort. Since explicit projections are equivalent to operations they cannot be overloaded on the name and the projected sort at the same time too. Bad position of actual constructor A formal sort has been actualized by an actual sort but the order of the constructors is different. In the current version the number, the structure and the order of the constructors of formal and actual sort has to be identical. Please consider this restriction. Bad projection A projection is applied to a term but the specified type is not contained in it or the term does not have a tuple type. Bad renaming A sort or an operation has been renamed to something which is not a name but a tuple or a functional. Constructor eqns not allowed The compiler had detected some axioms with a constructor on top of their lhs. Constructors are free in ASpecT. Remove the respective equations or redefine them as theorems. Constructor may not be assigned An actualization of a constructor has been made. The actualization of an constructor is done with the actualization of the formal sort it is bound to. ASpecT does not allow direct actualization of a constructor. Constructor may not be renamed A renaming of a constructor has been made. In the current version the renaming of constructors is not permitted. Constructor mismatch (formal: :, actual: :) A formal sort has been actualized by an actual sort but the structure or name of one of the constructors is different In the current version the number, the structure and the order of the constructors of formal and actual sort has to be identical. Please consider this restriction. Constructor undeclared An unknown constructor was used at time of actualization Declare the constructor. (Cyclic) Type mismatch (assumed: , got: ) The ASpecT parser failed to determine the type of an expression. The error may only occur when using nested macros. Check the expression for the right type. The parser offers a possible error. Because of some theoretical problems to determine the right position of such an error the actual error may be elsewhere in the expression. Eqns for the same opn should be grouped The specification contains several definitions of an operation which are not grouped. All definitions belonging to an operation must be grouped. This means that no other definitions may separate them and they have to be collected in one equation block. Error reading The stated file could not be read by the ASpecT system. There may be several reasons dealing with specific details of the used operating system. Test whether the file exists (in the search path) and the permission to read is given. Error reading command template file The gen tool was either unable to find a command template file or the command template file found is erroneous. Follow the search path contained in the ASPECT environment variable and try to localize a command template file (default.cmd). If there is none make some command template file available, otherwise correct the contents of the command template file. Error removing defective file The gen tool tries to delete this file Check write protection Error removing file The gen tool tries to delete this file Check write protection Error writing The stated file could not be written by the ASpecT system. There may be several reasons dependent of the operating system. Test whether there is enough space and the permission to write is given. External sort may not have constructors A sort has been declared as extern and some constructors have been given. Extern sorts may not have constructors since their construction is not performed by ASpecT. A pattern matching on the structure of extern sorts is only possible by means of user defined matching functions. Remove either the constructors or the keyword EXTERN. FATAL ERROR (too many args). EXECUTION STOPS HERE! This fatal error does not occur on running the ASpecT system. It may occur if a user program is executed. A call to an operation has occurred with more than a specific amount of arguments. Due to problems with the manipulation of the call stack in C the maximal number of arguments plus results an operation may have is limited to currently 25. If required the user may change the limit by patching the callswitch-macro in the file runtime.h and rebuild the runtime system. The user program has to be retranslated with an increased -ma parameter to the ASpecT program translator (see 3.3) in the command template file (see 5.1). Fatal error: cannot schedule a job! This should be an error in the gen tool. The gen tool collected some jobs but cannot solve the dependencies. Report the error to the ASpecT group. Formal imports not supported The compiler has detected an import declaration in the formal part of a specification. The current release of the ASpecT language does not support formal imports. You should expand the file textually. Formal opn may not be external A formal operation is declared to be extern. This is unreasonable in ASpecT. Remove the keyword EXTERN. Formal opn not actualized An instantiation has been made without assigning all formal operations. Give the missing actualizations. Formal opns must be actualized A specification has been included polymorphically which contains formal operations. Such specifications are not allowed to be used polymorphically. Actualize the specification or redefine the specification without formal operations by using functional parameters for example. Formal sort may not be extern A formal sort is declared to be extern. This is unreasonable in ASpecT. Remove the keyword EXTERN. Formal sort not actualized An actualization has been made without assigning all formal sorts. Give the missing actualizations. Formal sort(s) are not reachable by If the operation with the stated name is used from the polymorphically imported specification the given sorts cannot be inferred. The specification may not be imported polymorphically. Forward declared sort must not contain formal parts A sort has been declared globally without constructors or has been used as an instantiation. Later it is defined as a sort containing formal sorts. This is an implementation restriction of ASpecT to be removed soon. Forward declaration of synonym/supersort not allowed A sort has been declared globally without constructors or has been used as an instantiation. Later it is defined as synonym sort or as sort containing subsorts. This is an implementation restriction of ASpecT to prevent costly calculations. Found specification instead of in The expected specid differs from the actual one. Correct the specid in the file specified by . Higher-order pattern matching not allowed A pattern of an equation is higher order. This is not allowed in ASpecT since higher order pattern matching normally leads to non deterministic pattern matching. Import cycle between and The two given specifications import each other. Resolve the import cycle. Import cycle involving The stated specification imports itself somewhere in the import graph. Resolve the import cycle. Inconsistent actual opn, should be There is a inconsistency between the sorts of a formal and an actual operation. The sorts of formal and actual operation should be identical after actualization. Otherwise they are incompatible. job(s) canceled The gen tool canceled some collected jobs. This normally occurs if depended files could not be generated or some files are missing Act as required, i.e. correct mistakes, create files. Local sort must have constructors A local sort has been detected without any constructors. Local sorts must have constructors unless they are not declared extern. Rephrase the respective declaration. Macro argument not used Some of the macro arguments are not used on the right hand side of a macro definition. Unlike normal operations all arguments of a macro have to be used in the macro definition. Anonym macro arguments are not allowed. Macro declared twice A macro identifier is declared which has been declared before. Macro identifiers cannot be overloaded in a scope of visibility. Rename the macro identifier. Macro undeclared A macro or macro variable has been used but not defined. Define the macro or macro variable. Macro used with different types A macro is used more than once in an equation but the type of the usages is different. A macro must have a unique sort in an equation. Memory full !!! This message comes from the ASpecT runtime system. It may occur while running user programs too. The obvious reason is that no more memory can be allocated. If this error occurs while running the ASpecT system there is less what can be done. To save memory it is a good idea to keep the interfaces between the specifications as small as possible. Very large specification modules should be split up. If this does not help you may perhaps run into a currently unknown feature (bug) of the system or simply your computer's memory is really not big enough. If this error occurs while running a user program one should run the termination check first to detect possible sources of non-terminations. If this does not help check your data structures and algorithms.. Missing arguments An operation has not been given all its arguments required from the context. The missing argument is stated by the sort. Enter the missing argument, change the context of the operation usage or use another operation (misspelling?). Missing Eqns for : An operation has not been totally declared. The lhs patterns of all axioms for an operation have to cover all possible cases since partially undefined operations would construct new data in the goal domain. The missing cases should be considered too. Missing macro parameters A macro is used without assigning all of the parameters. Macros can only be used with all of the arguments given. No equations allowed for formal opn There are some definitions detected for an operation declared in the formal part of a specification. The operations in the formal part may not be restricted by definitions. Either remove the definitions or redefine them as theorems. Non-constructor argument The pattern of an equation contains an operation. Such non-constructor equations are not allowed in ASpecT. Non left-linear definition A variable is used more than once on the left hand side of an equation. Such non left-linear definitions are not allowed in ASpecT since it is sometimes impossible to define the missing cases without using catchall equations. Move the test for equality to the right side of the equation using the if then else construct and the "==" operation. Opn already declared implicitly An operation has been declared which was already declared implicitly as projection or a projection is used as actual operation. Since projections have the name of an existing sort change the name of the operation or change the arguments. Opn assigned twice In an actualization of an imported specification you have actualized (renamed) an operation more than once. An operation can only be actualized (renamed) once. Throw away all but one of the conflicting actualizations (renamings). Opn declared twice A declaration of an operation occurred which was already declared in the current scope of visibility. Operation must be distinguished by either the name, the argument domain or the goal domain. Search the scope of visibility for the conflicting operation and redeclare one of them. If the error occurs in a FORALL declaration remove all but one of the conflicting declarations. Opn undeclared An operation has been used which is not declared. All operations being used have to be declared. If it is not a case of misspelling declare the missing operation. Overlapping Catch-all Eqns for A catchall equation for an operation overlaps with another catchall equation. The overlapping of the patterns of the definition is forbidden in ASpecT since the rewrite system has to be deterministic. Find the overlapping pair and merge the definitions or specialize the equations and write an additional catch-all equation. Overlapping Lhs for : An equation for an operation overlaps with another equation. The overlapping of the patterns of the definition is forbidden in ASpecT since the rewrite system has to be deterministic. Find the overlapping pair and merge the definitions. Polymorphic opn not allowed as actual opn An operation of a polymorphically imported specification is used to actualize a formal parameter operation. In this version of the compiler the automatic actualization inference is limited to the equations. In an actualization block no polymorphic operations are allowed. Actualize the polymorphic specification or declare a new operation which is defined by the polymorphic operation. Polymorphic sorts not supported A specification with formal parts is imported polymorphically but it contains a global sort declaration. This is currently not supported in the ASpecT system since the compiler does not automatically rename polymorphic sorts. Either actualize the specification explicitly or split the desired module into parts. Some of the part may be used polymorphically (those which do not contain global sorts) others may not. Polymorphic subterm A subterm of a term remains polymorphic after the typing finished. This may happen too, if then nesting of polymorphic functions is complex. All terms of an ASpecT specification must get just one sort. Polymorphic subterms may have several sorts. Use the FORALL declaration or type annotations to remove the polymorphism. Projection : has to be defined for all constructors of An explicit projection has been defined only on some of the constructors of a sort. Explicit projections must be defined on all constructors of a sort. Projection needs one argument An operation has been used which the ASpecT compiler identifies as projection but none or more than one argument has been given. A projection cannot be used as a functional. It must have exactly one argument. Projection on tuples not supported A projection has been applied to an explicitly written tuple term. It is unreasonable to apply this projection since the result can be written directly (and the rest of the tuple can be omitted). Scanning This is an information of the ASpecT system stating that the syntax check of that file is currently running. Sort declared twice The stated identifier has been declared twice as sort identifier. Check the scope (including the imported specifications) for the candidate and rename one of the two. A sort identifier has to be unique in any scope of visibility. Sort must have constructors A sort is declared without constructors. This is only allowed for external sorts and global sorts which are also defined locally - but this time with its constructors. Rephrase the respective declaration. Sort undeclared The stated identifier has been used as sort identifier but it is not declared as such in the current scope of visibility. You may have misspelled the identifier or you forgot to declare it or some specification module has to be included. Specification imported from different files (,) There are two modules with different filenames and the same module name (specid). Module names must be unique within a specification including all imported modules. Change the module name of one of the files or import only one of them. Too few constructors (formal sort: , actual sort: ) A formal sort is restricted by some constructors. The actual sort assigned has less constructors than the formal sort. An actual sort must have at least the restrictions which have been imposed on the respective formal sort. Too many () arguments An operation has been used with too many arguments. The number of supernumerary arguments is stated. Delete the arguments or use another operation (misspelling?). Too many constructors (formal sort: , actual sort: ) A formal sort is restricted by some constructors. The actual sort assigned has more constructors than the formal sort. In the current version the number, the structure and the order of the constructors of formal and actual sort has to be identical. Please consider this restriction. Too many parses The system tries to calculate the sort of a term. The number of possibilities for some subterms exceeds a given limit. Use the FORALL declaration or type annotations to limit the number of possibilities. If nothing helps you may increase the maximum number of parses by increasing the -m parameter to asp (see 3.2) in the command template file (see 5.1). Type mismatch (assumed: , got: ) The ASpecT parser failed to determine the type of an expression. Check the expression for the right type. The parser offers a possible error. Because of some theoretical problems to determine the right position of such an error the actual error may be elsewhere in the expression. Unable to locate The gen tool cannot find this source file Check if the file is present. If it is present check if the ASPECT environemt is set apropriatly. Variable declared twice A variable in a FORALL declaration has been declared twice. Remove one of the declarations. Variable only occurs in rhs A variable in the right hand side of an equation does not find its equivalent in the left hand side. Rename the variable or add it to the left hand side. Variable should be anonymous A variable in the left hand side of an equation is named but it is not used on the right hand side. To enhance readability and to prevent the wasting of identifiers ASpecT forces the programmer to anonymize the variables only occurring on the left hand side of an equation. Anonymize ('_') the respective variable.