Subsections:
Bool">

Algebraic specification -- ADT

Bool 


  adt bool is
  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
slide: The ADT
slide: Algebraic specification
slide: Generators -- basis and universe
Seq">
slide: The ADT
slide: Equivalence
Nat">

Natural numbers

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
slide: The ADT 
  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
slide: Symbolic evaluation
Set">

Sets

Set


Axioms
slide: The ADT
Set">
slide: Equivalence classes for
slide: Interpretations and models
Bool and Nat">
slide: Interpretations of
slide: Initial models
slide: Structure and interpretation
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

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
slide: The interpretation of change
ctr">

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

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