Signature -- names and profiles

$%S$


  • $ f : s_1 \* ... \* s_n -> s $

Functions -- for $T$
  • constants -- $c : -> T$
  • producers -- $g : s_1 \* ... \* s_n -> T$
  • observers -- $f : T -> s_i$

Type -- generators

  • $ %S_T = P_T \cup O_T$, $C_T \subset P_T$, $P_T \cap O_T = \emptyset$
slide: Algebraic specification