Towards Modular
Evolving Algebras

   It is shown that Evolving Algebras describing Algebraic Operational semantics of various fragments of Prolog can be constructed incrementally. The correctness of Evolving algebras and their extensions corresponding to larger fragments of the language is proved. In particular, the Evolving Algebra for pure Prolog is described and compared with its extension (due to Börger) for pure Prolog with the cut operator. It is shown that there is a homomorphism that maps the latter algebra onto the former one. This homomorphism extends to a homomorphism of the evolution steps of both algebras during computations of pure Prolog programs. Moreover, the cut operator can be represented as an external dynamic function (oracle) of the algebra for pure Prolog.

1 Introduction

   Evolving algebras were proposed by Gurevich [1988] (see also Gurevich 1991 for a more recent account) as a framework for Algebraic operational semantics of programming languages. Evolving algebras are (essentially first-order) finite structures that evolve with time in the same way as a computer executing commands of a program in a programming language. Evolving algebras are many-sorted partial structures i.e. they are using a finite number of universes some of witch may be empty at certain steps and functions which need not be defined on all the elements of their domains.

An Evolving algebra is an abstract mathematical object amenable to a rigorous mathematical analysis that describes various aspects of the corresponding programming language or of a corresponding subset of it. Each evolving algebra is defined on a certain level of abstraction and some of its universes are dynamically changed and functions dynamically updated during transitions from one state to another while some universes and function are considered static in the process. The static functions and universes correspond to abstract notions and operations that are intuitively known but are not actually the subject of analysis.

There are several possible interpretations of static functions and universes:

(i) static functions correspond to implementation dependent features of the language and are not a part of the semantics of the language while dynamic functions represent implementation independent features that determine the semantics of the language.

(ii) static functions correspond to features of the language that will be analyzed later in more detail as a part of the modular construction of the language.

(iii) static functions correspond to hidden operations e.g. garbage collection, unification etc. in Prolog.

next page

contents

The aim of this paper is to describe the new concept of a module over an Evolving Algebra. By their nature, modules are evolving algebras sharing certain functions and universes with the given algebra using as well some other dynamic functions and universes of their own.

The paper concentrates on the Algebraic Operational Semantics of full Prolog that was described by an evolving algebra in a sequence of papers by Börger [1990a, 1990b and 1990c]. It will analyze modules over this algebra supporting the approach (i) and (iii) mentioned above. The modular description of Prolog will be the subject of a subsequent paper.

The modules over the above mentioned algebra are supporting the above interpretations (i), (iii) and:

a) are mathematical objects representing implementations dependent features or hidden operations of Prolog amenable to rigorous mathematical study,

b) give a simple and unambiguous description of these operations,

c) make it possible to verify correctness of implementation of these operations.

The paper is organized as follows. Section 2 recall the concept of Evolving Algebras and introduces the concept of the modules over an evolving algebra. Section 3 describes a simple motivating example of such a module and shows more complicated examples of nesting such modules.

The paper is self-contained. The knowledge of [Börger 1990a] is recommendable, although not necessary.

2 Evolving Algebras and Modules

Let us recall the basic concept of evolving algebra [Gurevich 1988, 1991]:

2.1 Definition An evolving algebra A is a triple A,F,T consisting of a non-empty finite, many sorted, partial first order algebra A,F of the signature F and a finite set T of transition rules of the same signature F.

The transition rules of T are all of the form

IF b(x) THEN U₁(x)

previous page

next page

contents

.

.

.

U_k(x) ENDIF

where b(x) is a boolean expression of the signature F of , k is a natural number and

U₁(x),...,U_k(x)

are updates and x is a tuple of variables ranging over some of the universes of the algebra A.

There are three possible types of updates:

1. A function update is an equation of the form

(1) f(t₁,...,t_n):=t

where

(2) t₁,...,t_n,t

are terms and f is a function of the signature F. The function update (1) is executed in A if the terms (2) are evaluated in A to resulting elements e₁,...,e_n,e, respectively, and the element e is assigned as a new value of f of the n-tuple e₁,...,e_n. As a result, we get a new algebra A' of the same signature F.

2. A universe extension is an update of the following form:

TAKE temp_i = NEW(U_i) WHERE i = (1,...,t) IN F₁

.

.

.

F_k ENDTAKE

where U_i are universes of A, k is a natural number, t is a closed term of the signature of A and F₁,...,F_k is a set of function updates.

The update 2.1.2 (ii) is executed in A if the term t is evaluated to a natural number n , new

previous page

next page

contents

elements temp₁,...,temp_n are added to the universes U₁,...,U_n respectively, and the function updates F₁,...,F_k are executed simultaneously for each i=1,...,n. If t always evaluates to 1, we write

TAKE temp = NEW(U) IN F₁

.

.

.

F_k ENDTAKE

3. A universe contraction is an update of the form:

DISPOSE(s)

where s is a term of the signature of A. This update is executed on A if the term is evaluated to an element e of some universe U of A , the element e is deleted from U and each function f of the signature F of A gets undefined on every tuple (t₁,...,t_m) of its domain, whenever the term s occurs in one of the terms t_i, i=1,...,m.

2.2 Definition Let A = A,F,Tbe an evolving algebra. A module A' over A is an evolving algebra A',F',T'with the following properties:

1. If the signature F' shares some universes and functions with the signature F of the algebra A and if some shared universe or function is dynamically updated (defined) by the algebra A , then all transition rules of T describing these updates are transition rules of T'.

2. If the signature F' contains some universes and function both static and dynamic of its own, the dynamic functions and universes of A are updated by the rules of T'.

3. Some of the rules of T' are updating the values of static functions of the algebra A using the dynamic and static functions of A'.

If the values of a static function f of A are fully determined by A' , we say that the module A' computes f. It should be noted that a module A' is a non-empty algebra according to the definition 2.1.

2.3 Remark Note that static functions or universes of the main algebra A corresponds to a

previous page

next page

contents

certain level of abstraction. If the static function f of A is computed by a module A' = A',F',T', then f does not belong to the signature F'. On the other hand, different modules computing different static functions of the main algebra, can have some internal functions and universes in common.

2.4 The evolving algebra for Prolog

In what follows, we shall use the following universes for description of evolving algebra for Prolog:

STACK, PROGRAM, TERM, SUBST, INTEGER, BOOLEAN, IDENT

The universe STACK describes the resolution stack during Prolog computations. Functions on universe STACK save information about state of a Prolog computation. They are as follows.

First : STACK

NextStack: STACK STACK

for representing the stack structure of the choice points. Each element of STACK saves information using functions

Goal : STACK TERM

CurClause : STACK PROGRAM

CurSubst : STACK SUBST

about current goal, clause to be tried next and current substitution, respectively.

The universe PROGRAM is used to describe the status of the database. We will use the functions

ProgBegin : PROGRAM

NextClause : PROGRAM PROGRAM

TheClause : PROGRAM TERM

The functions ProgBegin and NextClause are used for ordering of clauses in the database. For the purposes of this paper, we will not distinguish between clauses and terms.

The universes TERM and SUBST represent terms and substitutions. The former includes all types of terms, i.e. variables, atoms, integers and structures. Distinguishing among the types

previous page

next page

contents

is not necessary on this level of abstraction. It will be described later. The functions, that have a meaning only for some type of terms, e.g. the arity and arguments are defined only for structures, have as theirs domain the whole universe of TERM, but on the rest are undefined. The undefined values are denoted by the symbol undef.

The universes TERM and SUBST are manipulated by the following functions, that are static in the algebra for Prolog:

Mgu : TERM ´ TERM SUBST

Rename : TERM TERM

ApplySub : TERM ´ SUBST TERM

AppendSub: SUBST ´ SUBST SUBST

where the function Mgu computes a most general unifier for two terms, and Rename creates a copy of the term with new (renamed) variables. The function ApplySub finds a term after applying the substitution on the given term and AppendSub computes a composition of given substitutions.

The universes INTEGER, BOOLEAN and IDENT are used as basic domains with the usual meaning.

We use five more functions for manipulating the goals and clauses, that are represented by terms. They support gaining of the first literal from a goal, the rest of a goal and appending goals after resolution step:

FirstGoal : TERM TERM

RestGoal : TERM TERM

AppendGoal : TERM ´ TERM TERM

and accessing the head and the body of the clause:

ClauseHead : TERM TERM

ClauseBody : TERM TERM

The main algebra will use only these functions. Some of them are static and will be described dynamically in modules which are defined later.

We describe one rule of the main algebra to see situations when static functions are used. The rule shows evolving of the algebra in case of unsuccessful resolution.

This rule applies if the resolution stack is not empty (3.1), the goal on the top of stack is not empty (3.2), there is a clause to be tried next (3.3) and unification between current first goal

previous page

next page

contents

under substitution (3.4) and rename head of current clause (3.5) fails (3.6). In such case the update increment the clause counter (3.7).

(3.1) IF (First ą undef) and

(3.2) (FirstGoal(First) ą undef) and

(3.3) (CurClause(First) ą undef) and

(3.4) (Mgu(ApplySub(FirstGoal(Goal(First)),CurSubst(First)),

(3.5) ClauseHead(Rename(TheClause(CurClause(First)))))

(3.6) = undef)

THEN

(3.7) CurClause(First) := NextClause(CurClause(First))

We can see the static functions Mgu, Rename and ApplySub in the rule.

3. Modules manipulating terms

In this part, modules are described for static functions used on terms, namely for functions Rename, Mgu, ApplySub used in the Prolog algebra. For this level of abstraction, we choose the functions describing the structure of terms. These functions are dynamic and internal, so the module operates them itself.

The new internal universes of the module type TYPE and AUXSTACK, where

TYPE = { tvar, tint, tatom, tstruct }

is used to distinguish among type of terms and AUXSTACK for auxiliary manipulations terms during the evolution of the module.

The dynamic internal functions are as follows:

Type : TERM TYPE

Functor : TERM TERM

(1) Arity : TERM INTEGER

Args : TERM ´ INTEGER TERM

Ivalue : TERM INTEGER

Name : TERM IDENT

The auxiliary stack AUXSTACK is represented by the internal dynamic functions

Aux : AUXSTACK for top of the stack

previous page

next page

contents

(2) NextAux : AUXSTACK AUXSTACK for next element of the stack

Term1,Term2: AUXSTACK TERM denoting the terms we are working with

The modules for Rename, Mgu, ApplySub use the functions (1) for passing information about terms. The auxiliary functions (2) can be viewed as local in each module.

Evolution of the module (algebra) is data driven. But there is no syntactic reflection of hidden operations. Functions of lower levels of abstraction are in this case hidden from general view, but modules working on data structure use these functions during evolution (computation).

The parameter passing to and from a module is in the standard way. The module starts to evolve in some state of the main algebra and after finishing this process, it is possible to obtain the results from its final state. We use the special constant functions in the module to make the (input) elements of the universe(s) and the output accessible. They are denoted by InTerm, InSubst, OutTerm, OutSubst etc.

To get better formalization of a module we use the constant functions

Start, Done : BOOLEAN

where Start gets the value true in the initial state of the module and the value false in the subsequent states. Similarly, Done gets the value false through the evolution process of the module and true after the process is finished. All rules of the module have a condition of the form

IF (not Done) and ... THEN ...

which means, that the evolution of the module stops when Done is true.

3.1. Module Rename

The function Rename: TERM TERM , which builds a new term with the same structure and renamed variables is static in the main algebra. We describe this function dynamically by the module Rename. The module uses the internal constants

InTerm,

OutTerm : TERM

to represent the input and output elements.

The module updates values of the dynamic functions (1) on newly created elements of the universe TERM.

We shall replace the following two updates

previous page

next page

contents

Aux := NextStack(Aux) next element of stack

Dispose(Aux) dispose top, done

by symbolic expression shorten auxstack.

Here are the corresponding internal rules:

IF (not Done) THEN general condition to continue

IF (Aux = undef) THEN stack is empty

IF Start THEN distinguishing start and end

TAKE = tempTerm = New(TERM), universe extension

tempStack = New(AUXSTACK) IN new element of the auxiliary stack

Term1(tempStack) := InTerm copying the input term

Term2(tempStack) := tempTerm the resulting term

OutTerm := tempTerm output

Aux := tempStack setting the auxiliary stack

NextAux(tempStack) := undef the rest is free

Start := false algebra begins to evolve

ENDTAKE

The rule extends the auxiliary stack by one element and creates a new copy of the input term. The pair consisting of the copied term and the new term are accessible by Term1 and Term2 on the stack, where the latter is a new element of the universe TERM, but its structure is not described since the functions (1) have not been updated yet. This is done by the next rules.

IF (not Done) and (Aux = undef) and (not Start) THEN

Done := true stop the evolution process

In case of cleaning of the auxiliary stack, the rule stops the module evolution process.

IF (not Done) and (Aux ą undef) THEN

IF (Type(Term1(Aux)) = tvar) THEN variable

Type(Term2(Aux)) := tvar type of created term is also var

shorten auxstack

In case of variable we need not to create a new structure, we have only to assign a new variable. By this rule, new variable was created extending the universe TERM.

previous page

next page

contents

IF (not Done) and (Aux ą undef) THEN

IF (Type(Term1(Aux)) = tint) THEN integer

Type(Term2(Aux)) := tint type of created term is also int

Ivalue(Term1(Aux)) := Ivalue(Term2(Aux)) copy the value

shorten auxstack

The rule is used for integers, it copies the value and disposes the top element. We have a similar rule for atoms.

IF (not Done) and (Aux ą undef) THEN

IF (Type(Term1(Aux)) = tatom) THEN atom

Type(Term2(Aux)) := tatom type of created term is also atom

Name(Term1(Aux)) := Name(Term2(Aux)) copy the value

shorten auxstack

The rule for creating a structure is not so simple. First, we create an appropriate number of elements on the stack and of the universe TERM, which will be assigned the subterms of the currently copied term. We set the functions Term1 and Term2 of the new stack elements to the subterms of the copied term and to the created terms, respectively. The latter are linked to subterms of the newly created structure.

IF (not Done) and (Aux ą undef) THEN

IF (Type(Term1(Aux)) = tstruct) THEN structure

Type(Term2(Aux)) := tstruct type of created term is structure

TAKE tempTerm(i) = New(TERM),

tempStack(i) = New(AUXSTACK)

WHERE i = 1... Arity(Term1(Aux)) IN

Functor(Term1(Aux)) := Functor(Term2(Aux))

Arity(Term1(Aux)) := Arity(Term2(Aux))

Args(Term1(Aux),i) := Args(Term2(Aux),i) i = 1... Arity(Term1(Aux))

Aux := tempStack(1) new top of the auxiliary stack

NextStack(tempStack(i)) := tempStack(i+1) i = 1... Arity(Term1(Aux))-1

NextStack(tempStack(Arity(Term1(Aux)))) := NextStack(Aux)

Term1(tempStack(i)) := Args(Term1(Aux),i) i = 1... Arity(Term1(Aux))

Term2(tempStack(i)) := tempTerm(i) i = 1... Arity(Term1(Aux))

Dispose(Aux) dispose top, done

ENDTAKE

previous page

next page

contents

These are rules for the module Rename. The new term and its structure are created and it is accessible in OutTerm after the algebra stops evolving.

3.2. Module Mgu

The static function Mgu: TERM ´ TERM SUBST of the main algebra computes the most general unifier of the input terms. The structure of the module Mgu is similar to the one of the module Rename. Using the universe AUXTERM, it traverses recursively the structure of terms and creates the new substitution. It uses static functions handling substitutions, which need not be specified on this level of abstraction. These functions are:

ApplySub : TERM ´ SUBST TERM

AppendSub : SUBST ´ SUBST SUBST

They are shared with the main algebra and the module Mgu. The internal static function of the module is

MakeSub : TERM ´ TERM SUBST

which creates a new substitution from a variable (the first argument) and a term. If the first argument is different from a variable, i.e. if Type(_) ą tvar, then the function MakeSub is undefined.

We suppose, that Mgu returns undef if the terms are not unifiable. We suppose as well, that the empty substitution is included in the universe SUBST.

We show only the two most important rules of the module Mgu. The first one (4.1) is performing one step in the unification algorithm, when a variable from first term should be unified with something from second term. A similar rule not shown here covers the symmetric situation. The rule uses an internal constant of the module Mgu

tempSub : SUBST

for saving the created substitution during the process. The rule omitts the occur-check, however it is possible to describe the module with the occur-check, as well.

The rule (4.2) solves one of the cases, when the two given terms are not unifiable. Then the rule aborts the evolution process by setting the function Done to the value true and the result of unification to undef.

previous page

next page

contents

IF (not Done) and (Aux ą undef) THEN

(4.1) IF (Type(ApplySub(Term1(Aux),tempSub)) = tvar) THEN

TempSub := AppendSub(TempSub,

MakeSub(ApplySub(Term1(Aux),TempSub),

ApplySub(Term2(Aux),TempSub)))

shorten auxstack

(4.2) IF (Type(ApplySub(Term1(Aux),TempSub)) ą tvar) and

(Type(ApplySub(Term2(Aux),TempSub)) ą tvar) THEN

Done := true stop the evolving

Aux := undef clean the stack

OutSubst := undef output sign failing

3.3. Module ApplySub

The module describes the static function ApplySub: TERM ´ SUBST TERM working with substitutions on an abstract level. The new internal functions are

DomainSub : TERM ´ SUBST BOOLEAN

RangeSub : TERM ´ SUBST TERM

where the former one checks for each variable, represented by the first argument, whether it is in the domain of the substitution, and the latter (given a variable and a substitution) returns a term, which is substituted to the variable by the substitution.

Again, the structure of the rules is very similar to the structure of rules of the previous modules. The main idea is to traverse the term and create the resulting new term.

The rule (5.1) is responsible for creating the auxiliary stack and the passing the parameters. The new term is prepared, at this time without its structure and without the correct values of the functions (5.1), which are updated by the following rules.

The rule (5.2) finishes the evolving.

The rule (5.3) reflects the case of a variable. We have to check, whether the variable is in the domain of the substitution and then we let it be (5.3a) or change it to a new term according the substitution (5.3b).

The rules (5.4) and (5.5) cover the case of integers and atoms, they copy the relevant functions to a new term.

The part (5.6) copes with the most complicated case namely, with the case when the term is a structure. We create the new elements of the stack and new terms, which are subterms of the created term from the top of the auxiliary stack.

previous page

next page

contents

IF (not Done) THEN general condition to continue

IF (Aux = undef) THEN stack is empty

IF Start THEN distinguishing of start and end

(5.1) TAKE tempTerm = New(TERM), new term

tempStack = New(AUXSTACK) IN new element of stack

Term1(tempStack) := InTerm copied term

Term2(tempStack) := tempTerm created term

OutTerm := tempTerm created term is output

Aux := tempStack setting the auxiliary stack

NextAux(tempStack) := undef the rest is free

Start := false algebra begins to evolve

ENDTAKE

ELSE

(5.2) Done := true

ELSE IF (Type(Term1(Aux)) = tvar) THEN variable

(5.3) IF DomainSub(Term1(Aux),InSubst) THEN

(5.3a) Type(Term2(Aux)) := Type(RangeSub(Term1(Aux),InSubst))

Functor(Term2(Aux)) := Functor(RangeSub(Term1(Aux),InSubst))

Arity(Term2(Aux)) := Arity(RangeSub(Term1(Aux),InSubst))

Args(Term2(Aux),i) := Args(RangeSub(Term1(Aux),InSubst),i)

i = 1... Arity(Term1(Aux))

Ivalue(Term2(Aux)) := Ivalue(RangeSub(Term1(Aux),InSubst))

Name(Term2(Aux)) := Name(RangeSub(Term1(Aux),InSubst))

shorten auxstack

(5.3b) ELSE

Type(Term2(Aux)) := tvar type of created term is var

shorten auxstack

ELSE IF (Type(Term1(Aux)) = tint) THEN

(5.4) Type(Term2(Aux)) := tint type of created term is int

Ivalue(Term2(Aux)) := Ivalue(Term1(Aux))

shorten auxstack

ELSE IF (Type(Term1(Aux)) = tatom) THEN

(5.5) Type(Term2(Aux)) := tatom type of created term is atom

Name(Term2(Aux)) := Name(Term1(Aux))

shorten auxstack

ELSE term is the structure

(5.6) Type(Term2(Aux)) := tstruct type of created term is structure

previous page

next page

contents

TAKE tempTerm(i) = New(TERM),

tempStack(i) = New(AUXSTACK)

WHERE i = 1... Arity(Term1(Aux)) IN

Functor(Term1(Aux)) := Functor(Term2(Aux))

Arity(Term1(Aux)) := Arity(Term2(Aux))

Args(Term1(Aux),i) := Args(Term2(Aux),i) i = 1... Arity(Term1(Aux))

Aux := tempStack(1) new top of stack

NextStack(tempStack(i)) := tempStack(i+1) i = 1... Arity(Term1(Aux))-1

NextStack(tempStack(Arity(Term1(Aux)))) := NextStack(Aux)

Term1(tempStack(i)) := Args(Term1(Aux),i) i = 1... Arity(Term1(Aux))

Term2(tempStack(i)) := tempTerm(i) i = 1... Arity(Term1(Aux))

Dispose(Aux) dispose top, done

ENDTAKE

This concludes the description of module ApplySub.

Conclusions

We have shown the possibility of modular approach in algebraic operational semantics. This was illustrated by examples from the language Prolog. Such approach seems to be very fruitful in the case when they are many hidden operations, that are not reflected by the syntactical structure of the language. It enables us to choose among various levels of abstraction. The level of abstraction is reflected by the choice of static functions, that enable one to work with informally described objects, the behaviour of which is supposed to be known and correct.

By choosing the data structures at some level, we can describe explicitly operations (static functions) on these structures using modules. The modules can be made one after another, as it is shown in the paper, or one inside another. For instance, the universum SUBST, which is static on the level of a known term structure in the module Mgu, can be described by a module, which is a submodule of Mgu.

Using modules as described above gives one the tools for describing the static functions of the main algebra dynamically. The description is then based on internal data structures of the modules. From this points of view, discovering the internal data structure wipes out the difference between the operations based on the syntactic structure of the language and the hidden operations. Modules and rules for both types of operations are data-driven.

It is supposed that the values of all dynamic functions in the initial state of the algebra are tabulated. The values of dynamic functions are given for the elements of the universes, which

previous page

next page

contents

appears in the initial state, in a program and a goal in our case. This can be seen as a part of initial presentation. During the evolution process new values of relevant dynamic functions for new elements are explicitly computed and assigned. On the other hand it it supposed that static functions are given (tabulated) at whole (potentially infinite) universes including all potentially created elements and that they work correctly. The above examples of the modules show that different modules can use the same static and dynamic functions. The use of some static function in different modules is coherent, because the function yields the same correct results on the same elements.

The reader should note that the modules are mathematical objects amenable to rigorous mathematical analysis. Hence they make it possible to verify the correctness of the implementation of the static functions they are describing.

As in other programming languages, the modules with their concept of locality make the description of the language and of its operational semantics easily understandable.

All modules described in the paper are concerned with the data flow during computation. In a subsequent paper we shall show how modules can be used to describe the control structures.

REFERENCES

Apt, K. R.: Introduction to Logic Programming, In: Handbook of Theoretical Computer Science (J. van Leeuwen, editor), North Holland, Amsterdam, 1990

Bjørner, D., Jones, C. J.: Formal Specification and Software Development. Prentice Hall

previous page

next page

contents

International, 1982

Börger, E.: A Logical Operational Semantics of Full Prolog. Part I. Selection Core and Control. In: CSL'89. 3rd Workshop on Computer Science Logic, Springer Verlag LNCS 440, 1990.

Börger, E.: A Logical Operational Semantics of Full Prolog. Part II. Built-in Predicates for Database Manipulations. In: MFCS'90. Proc. of the International Symposium on Mathematical Foundation of Computer Science, Springer Verlag LNCS, 1990.

Börger, E.: A Logical Operational Semantics of Full Prolog. Part III. Built-in Predicates for Files, Terms,In-Output and Arithmetic. In: Proc. Workshop Logic for Computer Science, Berkeley, MSRI, November, 1989 (to appear with Springer Verlag, ed. Y. Moschovakis)

Deransart, P., Folkjaer, P., Pique, J.-F., Scowen, R. S.: Prolog. Draft for Working Draft 3.0. ISO/IEC JTC1 SC22 WG17 No. 53, 1990.

Gurevich, Y.: Evolving Algebras. A Tutorial Introduction. Bull. EATCS, No 2., February 1991.

Gurevich, Y., Morris, J.: Algebraic Operational Semantics and Modula-2. In: CSL'87. 1st Workshop on Computer Science Logic (Eds. E. Börger, H. Kleine-Büning, M. Richter), Springer Verlag LNCS 329, 1988.

Hric, J., Štěpánek, P.: Remarks on the Algebraic Operational Semantics of Prolog, LOP'91, Masaryk University, Brno, 1991

Hric, J., Štěpánek, P.: Fragments of Prolog and Evolving Algebras. In: From the Logical Point of View 3/92, Czech Academy of Sciences, Prague, 1993.

Jones, C.B.: Systematic Software Development Using VDM. Prentice Hall International, 1986

Lloyd, J. W.: Foundations of Logic Programming, Springer-Verlag, Berlin, Heidelberg, 1984

Morris, J.: Algebraic Operational Semantics for Modula-2, Ph.D. Thesis, The University of Michigan, 1988.

previous page

contents