lgallet/epicours
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

vault backup: 2023-10-04 12:10:12

Browse Source
This commit is contained in:
Louis Gallet
2023-10-04 12:10:12 +02:00
parent 58fd976855
commit f7e4ce0d46
1 changed files with 27 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

28
Algo/CM/CM du 04 octobre.md
View File

@ -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
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