Objects as algebras

Instructor's Guide

intro, types, algebra, modules, classes, summary, Q/A, literature
The types for which we have thus far seen algebraic specifications (including Bool, Seq, Set and Nat) are all types of a mathematical kind, which (by virtue of being mathematical) define operations without side-effects. Dynamic state changes, that is side-effects, are often mentioned as determining the characteristics of objects in general. In the following we will explore how we may deal with assigning meaning to dynamic state changes in an algebraic framework. Let us look first at the abstract data type stack. The type stack may be considered as one of the `real life' types in the world of programming. See slide 8-Stack.

Abstract Data Type -- applicative

Stack 


  functions
    new : stack;
    push : element * stack  -> stack; 
    empty : stack -> boolean;
    pop : stack -> stack;
    top : stack -> element;
  axioms
    empty( new ) = true
    empty( push(x,s) ) = false
    top( push(x,s) ) = x
    pop( push(x,s) ) = s
  preconditions
    pre: pop( s : stack ) = not empty(s)
    pre: top( s : stack ) = not empty(s)
  end
slide: The ADT Stack
 Above, a stack has been specified by giving a signature (consisting of the functions new, push, empty, pop and top). In addition to the axioms characterizing the behavior of the stack, we have included two pre-conditions to test whether the stack is empty in case pop or top is applied. The pre-conditions result in conditional axioms for the operations pop and top. Conditional axioms, however, do preserve the initial algebra semantics. The specification given above is a maximally abstract description of the behavior of a stack. Adding more implementation detail would disrupt its nice applicative structure, without necessarily resulting in different behavior (from a sufficiently abstract perspective). The behavior of elements of abstract data types and objects is characterized by state changes. State changes may affect the value delivered by observers or methods. Many state changes (such as the growing or shrinking of a set, sequence or stack) really are nothing but applicative transformations that may mathematically be described by the input-output behavior of an appropriate function. An example in which the value of an object on some attribute is dependent on the history of the operations applied to the object, instead of the structure of the object itself (as in the case of a stack) is the object account, as specified in slide 8-account. The example is taken from  [Goguen].

Dynamic state changes -- objects

account 


  object account is
  functions
   bal : account -> money
  methods
   credit : account * money -> account
   debit : account * money -> account
  error
   overdraw : money -> money
  axioms
   bal(new(A)) = 0
   bal(credit(A,M)) = bal(A) + M
   bal(debit(A,M)) = bal(A) - M if bal(A) >= M
  error-axioms
   bal(debit(A,M)) = overdraw(M) if bal(A) < M
  end
slide: The algebraic specification of an account
 An account object has one attribute function (called bal) that delivers the amount of money that is (still) in the account. In addition, there are two method functions, credit and debit that may respectively be used to add or withdraw money from the account. Finally, there is one special error function, overdraw, that is used to define the result of balance when there is not enough money left to grant a debit request. Error axioms are needed whenever the proper axioms are stated conditionally, that is contain an if expression. The conditional parts of the axioms, including the error axioms, must cover all possible cases. Now, first look at the form of the axioms. The axioms are specified as fn(method(Object,Args)) = expr where fn specifies an attribute function (bal in the case of account) and method a method (either new, which is used to create new accounts, credit or debit). By convention, we assume that method(Object,...) = Object, that is that a method function returns its first argument. Applying a method thus results in redefining the value of the function fn. For example, invoking the method credit(acc,10) for the account acc results in modifying the function bal to deliver the value bal(acc) + 10 instead of simply bal(acc). In the example above, the axioms define the meaning of the function bal with respect to the possible method applications. It is not difficult to see that these operations are of a non-applicative nature, non-applicative in the sense that each time a method is invoked the actual definition of bal is changed. The change is necessary because, in contrast to, for example, the functions employed in a boolean algebra, the actual value of the account may change in time in a completely arbitrary way. A first order framework of (multi sorted) algebras is not sufficiently strong to define the meaning of such changes. What we need may be characterized as a multiple world semantics, where each world corresponds to a possible state of the account. As an alternative semantics we will also discuss the interpretation of an object as an abstract machine, which resembles an (initial) algebra with hidden sorts.

Multiple world semantics

From a semantic perspective, an object that changes its state may be regarded as moving from one world to another, when we see a world as representing a particular state of affairs. Take for example an arbitrary (say John's) account, which has a balance of 500. We may express this as balance(accountJohn) = 500. Now, when we invoke the method credit, as in credit(accountJohn, 200), then we expect the balance of the account to be raised to 700. In the language of the specification, this is expressed as bal(credit(accountJohn,200)) = bal(accountJohn) + 200 Semantically, the result is a state of affairs in which bal(accountJohn) = 700. In  [Goguen] an operational interpretation is given of a multiple world semantics by introducing a database D (that stores the values of the attribute functions of objects as first order terms) which is transformed as the result of invoking a method, into a new database D' (that has an updated value for the attribute function modified by the method). The meaning of each database (or world) may be characterized by an algebra and an interpretation as before. The rules according to which transformations on a database take place may be formulated as in slide 8-multiple.
   - inference rules
  • 〈 f(t1,…,tn),D 〉 → 〈 v, D 〉

  • 〈 m(t1,…,tn),D 〉 → 〈 t1, D′〉

  • 〈 t , D 〉 → 〈 t′, D′〉 ⇒ 〈 e(…,t,…), D 〉 → 〈 e(…,t′,…), D′〉

slide: The interpretation of change
 The first rule (attribute) describes how attribute functions are evaluated. Whenever a function f with arguments    - inference rules
  • 〈 f(t1,…,tn),D 〉 → 〈 v, D 〉

  • 〈 m(t1,…,tn),D 〉 → 〈 t1, D′〉

  • 〈 t , D 〉 → 〈 t′, D′〉 ⇒ 〈 e(…,t,…), D 〉 → 〈 e(…,t′,…), D′〉

evaluates to a value (or expression) v, then the term    - inference rules
  • 〈 f(t1,…,tn),D 〉 → 〈 v, D 〉

  • 〈 m(t1,…,tn),D 〉 → 〈 t1, D′〉

  • 〈 t , D 〉 → 〈 t′, D′〉 ⇒ 〈 e(…,t,…), D 〉 → 〈 e(…,t′,…), D′〉

may be replaced by v without affecting the database D. (We have simplified the treatment by omitting all aspects having to do with matching and substitutions, since such details are not needed to understand the process of symbolic evaluation in a multiple world context.) The next rule (method) describes the result of evaluating a method. We assume that invoking the method changes the database D into D'. Recall that, by convention, a method returns its first argument. Finally, the last rule (composition) describes how we may glue all this together. No doubt, the reader needs an example to get a picture of how this machinery actually works.

Example - a counter object

 
  object ctr is 
   ctr  

  function n : ctr -> nat
  method incr : ctr -> ctr
  axioms 
     n(new(C)) = 0
     n(incr(C)) = n(C) + 1
  end
slide: The object ctr
 In slide 8-ctr, we have specified a simple object ctr with an attribute function value (delivering the value of the counter) and a method function incr (that may be used to increment the value of the counter).

Abstract evaluation

  <n(incr(incr(new(C)))),{ C }> -[new]-> 
  <n(incr(incr(C))),{ C[n:=0] }> -[incr]-> 
  <n(incr(C)),{ C[n:=1] }> -[incr]-> 
  <n(C), { C[n:=2] }> -[n]->
  <2, { C[n:=2] }>
slide: An example of abstract evaluation
 The end result of the evaluation depicted in slide 8-ctr-evl is the value 2 and a context (or database) in which the value of the counter C is (also) 2. The database is modified in each step in which the method incr is applied. When the attribute function value is evaluated the database remains unchanged, since it is merely consulted.

Objects as abstract machines

Multiple world semantics provide a very powerful framework in which to define the meaning of object specifications. Yet, as illustrated above, the reasoning involved has a very operational flavor and lacks the appealing simplicity of the initial algebra semantics given for abstract data types. As an alternative,  [Goguen] propose an interpretation of objects (with dynamic state changes) as abstract machines. Recall that an initial algebra semantics defines a model in which the elements are equivalence classes representing the abstract values of the data type. In effect, initial models are defined only up to isomorphism (that is, structural equivalence with similar models). In essence, the framework of initial algebra semantics allows us to abstract from the particular representation of a data type, when assigning meaning to a specification. From this perspective it does not matter, for example, whether integers are represented in binary or decimal notation. The notion of abstract machines generalizes the notion of initial algebras in that it loosens the requirement of (structural) isomorphism, to allow for what we may call behavioral equivalence. The idea underlying the notion of behavioral equivalence is to make a distinction between visible sorts and hidden sorts and to look only at the visible sorts to determine whether two algebras |A and |B are behaviorally equivalent. According to  [Goguen], two algebras |A and |B are behaviorally equivalent if and only if the result of evaluating any expression of a visible sort in |A is the same as the result of evaluating that expression in |B. Now, an abstract machine (in the sense of Goguen and Meseguer, 1986) is simply the equivalence class of behaviorally equivalent algebras, or in other words the maximally abstract characterization of the visible behavior of an abstract data type with (hidden) states. The notion of abstract machines is of particular relevance as a formal framework to characterize the (implementation) refinement relation between objects. For example, it is easy to determine that the behavior of a stack implemented as a list is equivalent to the behavior of a stack implemented by a pointer array, whereas these objects are clearly not equivalent from a structural point of view. Moreover, the behavior of both conform (in an abstract sense) with the behavior specified in an algebraic way. Together, the notions of abstract machine and behavioral equivalence provide a formalization of the notion of information hiding in an algebraic setting. In the chapters that follow we will look at alternative formalisms to explain information hiding, polymorphism and behavioral refinement.