2.2 KiB
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 nthaxioms 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, nthis 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