32 lines
1.2 KiB
Markdown
32 lines
1.2 KiB
Markdown
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
|
|
|
|
To use partial operations we have to create some preconditions
|