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. An axiom is the application of the observer on an internal operation : `observer(internal operation)`

```
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

The axiom can't be contradictory. Two (or more) contradictory axioms are call the consistency. When we create the axiom, we have to remove all the consistency. 
Example: 
```
nth(v,1)=0
nth(v,i)=i
```
That an consistency, because the two `nth`axioms are contradictory

The completeness is when we have enough axioms for our abstract type :
1. **Completeness**: Axioms should provide a complete and unambiguous specification of the ADT's behavior. This means that they should cover all possible scenarios and outcomes for the ADT's operations. Users of the ADT should be able to rely on these axioms to understand how the ADT behaves in different situations.

2. **Consistency**: Axioms should be consistent with each other and with the intended behavior of the ADT. This means that the axioms should not contradict each other, and they should accurately reflect the expected behavior of the ADT's operations. Inconsistent axioms can lead to confusion and incorrect usage of the ADT.


To use partial operations we have to create some preconditions

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

Preconditions
	nth(v,i) is-defined-iaoi lowerlimit(v) =< (i) =< upperlimit(v) & isinit(v,i) = true

Axioms
	lowerlimit(v) =< i =< upperlimit(v) -> nth(modify(v,i,e), i) = e
	lowerlimit(v) =< i =< upperlimit(v) & lowerlimit(v) =< j =< upperlimit(v) & i≠j -> nth(modifiy(v,i,e), j) = nth(v,j)
	isinit(vect(i,j),k)= false
	lowerlimit(v) =< i =< upperlimit(v) -> isinit(modifiy(v,i,e),i)= true
	... (all the other axioms)
```
Here, `nth`is a partial operation and `isinit` is a auxiliary operation

## Important things to create a abstract type
- What we want to create
- Add all necessary operations
- Preconditions
- Axios