diff --git a/Algo/CM/CM du 04 octobre.md b/Algo/CM/CM du 04 octobre.md index 244d9cc..3cde621 100644 --- a/Algo/CM/CM du 04 octobre.md +++ b/Algo/CM/CM du 04 octobre.md @@ -28,4 +28,30 @@ 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 \ No newline at end of file +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 +