62 lines
2.2 KiB
Markdown
62 lines
2.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
|
|
|
|
```
|
|
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 |