Alphabet
Description
Basic type to provide when working with Sigma.
This is the type of the "letters" (used to label the transition of an automaton).
Refinement of
Associated types
Notation
A 
A type that is a model of Alphabet 

a, b 
objects of type A 

Definitions
Valid expressions
the following expressions must be valid.
Name 
Expression 
Type requirements 
Return type 
Write 
out<<a 
out is an ostream 
ostram& 
Read 
in>>>a 
in is an istream 
istream& 
Asignement 
a=b 

A 
Equal 
a==b 

bool 
Less 
a<b 

bool 
Expression semantics
Name 
Expression 
Precondition 
Semantics 
Postcondition 
Write 
out<<a 

write a to the output stream out 

Read 
in>>a 

read a from the input stream in 

Assignement 
a=b 

Set a as a copy of b 

Equal 
a==b 



Less 
a<b 



Complexity guarantees
Invariants
Models
User can make its own, Nevertheless int, char and long
perfectly fit in, and are usually sufficients.