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

Signature -- names and profiles

%S


Functions -- for $T$

Type -- generators

slide: Algebraic specification

Generators -- values of $T$

T


Examples
slide: Generators -- basis and universe
Seq">

Sequences

  • %e : seq T

    empty


  • _ |> _ : seq T \* T -> seq T

    right append


  • _ <| _ : T \* seq T -> seq T

    left append


  • _ \. _ : seq T \* seq T -> seq T

    concatenation


  • << _ >> : T -> seq T

    lifting


  • << _,...,_ >> : T^{n} -> seq T

    multiple arguments


Generator basis -- preferably one-to-one

  • G_{seq T } = { %e, |> }, GU_{seq T } = { %e, %e |> a, %e |> b, ..., %e |> a |> b, ... }
  • G'_{seq T } = { %e, <| }, GU'_{seq T } = { %e, a <| %e , b <| %e, ..., b <| a <| %e, ... }
  • G''_{seq T } = { %e, \. , << _ >> }, GU''_{seq T } = { %e, <>, <>, ,..., %e \. %e, ..., %e \. <> , ... }

Infinite generator basis
  • G'''_{seq T } = { %e, << _ >>, << _ , _ >>, ... }, GU'''_{seq T } = { %e, <>, <>, ,..., <> , ... }
slide: The ADT

The equivalence relation -- congruence
  • x = x \zline{reflexivity}
  • x = y => y = x \zline{symmetry}
  • x = y /\ y = z => x = z \zline{transitivity}
  • x = y => f(...,x,...) = f(...,y,...)

Equivalence classes -- representatives

  • abstract elements -- GU_T /=
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


  • G_{Set_{A} = { \emptyset, add }
  • GU_{Set_{A} } = { 0, add(0,a), ..., add(add(0,a),a), ... }

Axioms

 

  [S1] add(add(s,x),y) = add(add(s,y),x) 
 commutativity

  [S2] add(add(s,x),x) = add(s,x) 
 idempotence
slide: The ADT
Set">

Equivalence classes

GU_{ Set _{A} }/=


  • { \emptyset }
  • { add(0,a), add(add(0,a),a), ... }
  • ...
  • { add(add(0,a),b), add(add(0,b),a), ... }
slide: Equivalence classes for

Mathematical model -- algebra

  • %S-algebra -- |A = ( { A_s }_{s \e S }, %S )
  • interpretation -- eval : T_{%S} -> |A
  • adequacy -- |A |= t_1 = t_2 <=> E |- t_1 = t_2
slide: Interpretations and models
Bool and Nat">

Booleans

  • |B = ( { tt, ff }, { \neg, / \/ } )
  • eval_{|B} : T_{Bool} -> |B = { or |-> \/, and |-> / not |-> \neg }

Natural numbers

  • |N = ( \nat , { ++ , + , \star } )
  • eval_{|N} : T_{Nat} -> |N = { S |-> ++ , mul |-> \star, plus |-> + }
slide: Interpretations of

Initial algebra

  • %S E-algebra -- |M = ( T_{%S}/=, %S/=)

Properties
  • no junk -- \A a : T_{%S}/= \E t \dot eval_{|M}(t) = a
  • no confusion -- |M |= t_1 = t_2 <=> E |- t_1 = t_2
slide: Initial models

Structure -- $ |B = ( {{ tt, ff }}, {{ \neg, /\, \/ }} )$

|B


  • eval_{|B} : T_{%S_{Bool} -> |B = { or |-> \/, not |-> \neg }
  • eval_{|B} : T_{%S_{Nat} -> |B = { S |-> \neg, mul |-> / plus |-> xor }
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

Multiple world semantics -- inference rules

  • << f(t_1,...,t_n),D >> -> << v, D >>

    • attribute


  • << m(t_1,...,t_n),D >> -> << t_1, D' >>

    • method


  • << t , D >> -> << t', D' >> => << e(...,t,...), D >> -> <>
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


   -[new]-> 
   -[incr]-> 
   -[incr]-> 
   -[n]->
  <2, { C[n:=2] }>
slide: An example of abstract evaluation