[]
readme
course(s)
preface
I
1
2
II
3
4
III
5
6
7
IV
8
9
10
V
11
12
afterthought(s)
appendix
reference(s)
example(s)
resource(s)
_

intro, types, algebra, modules, classes, summary, Q/A, literature

- Signatures -- generators and observers
- Equations -- specifying constraints
- Initial algebra semantics
- Objects as algebras

Algebraic specification techniques have been developed as a means to specify the design of complex software systems in a formal way. The algebraic approach has been motivated by the notion of

** Bool**

adtboolis functions true : bool false : bool and, or : bool * bool -> bool not : bool -> bool axioms [B1] and(true,x) = x [B2] and(false,x) = false [B3] not(true) = false [B4] not(false) = true [B5] or(x,y) = not(and(not(x),not(y))) end

intro, types, algebra, modules, classes, summary, Q/A, literature

Abstract data types may be considered as modules specifying the values and functions belonging to the type. In

intro, types, algebra, modules, classes, summary, Q/A, literature

The specification of the signature of a type (which lists the

** Nat**

functions 0 : Nat S : Nat -> Nat mul : Nat * Nat -> Nat plus : Nat * Nat -> Nat axioms [1] plus(x,0) = x [2] plus(x,Sy) = S(plus(x,y)) [3] mul(x,0) = 0 [4] mul(x,Sy) = plus(mul(x,y),x) end

mul(plus(S 0,S 0),S 0) -[2]-> mul(S(plus(S 0,0)), S 0) -[1]-> mul(SS 0,S 0) -[4]-> plus(mul(SS0,0),SS0) -[3]-> plus(0,SS0) -[2*]-> SS0

** Set**

intro, types, algebra, modules, classes, summary, Q/A, literature

In the previous section we have given a rather operational characterization of the equivalence relation induced by the equational theory and the process of term rewriting that enables us to purge the generator universe of a type, by eliminating redundant elements. However, what we actually strive for is a mathematical model that captures the meaning of an algebraic specification. Such a model is provided (or rather a class of such models) by the mathematical structures known as (not surprisingly) algebras. A

intro, types, algebra, modules, classes, summary, Q/A, literature

The types for which we have thus far seen algebraic specifications (including

** Stack**

functionsnew : stack; push : element * stack -> stack; empty : stack -> boolean; pop : stack -> stack; top : stack -> element;axiomsempty( new ) =trueempty( push(x,s) ) =falsetop( push(x,s) ) = x pop( push(x,s) ) = spreconditionspre: pop( s : stack ) =notempty(s)pre: top( s : stack ) =notempty(s)end

** 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

object ctr is## function n : ctr -> nat method incr : ctr -> ctr axioms n(new(C)) = 0 n(incr(C)) = n(C) + 1 end

ctr

<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]}>

[]
readme
course(s)
preface
I
1
2
II
3
4
III
5
6
7
IV
8
9
10
V
11
12
afterthought(s)
appendix
reference(s)
example(s)
resource(s)
_

(C) Æliens 04/09/2009

You may not copy or print any of this material without explicit permission of the author or the publisher. In case of other copyright issues, contact the author.