An abstract type have a signature, which contains types, uses and operations, and have some axioms. 

An axiom let us determine the value of the application of the observers with the internal operations (in the example below, the operation modify). We can see that as a validation. An axiom must be precise. 

```
Types
	vector
Uses
	integer, element
Operations
	Modify : vector x integer x element -> vector /*internal operation*/
	Nth: vector x integer -> element /* Observers */
	Lowerlimit: vector -> integer /* Observers */
	Upperlimit: vector -> integer /* Observers */

Axioms
	lowerlimit(v) =< i =< upperlimit(v) -> nth(modify(v,i,e), i) = e
```
In this example, the axiom explain that it check nth position in the modified vector