20 lines
706 B
Markdown
20 lines
706 B
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). 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
|