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

vault backup: 2023-10-11 11:33:06

Browse Source
This commit is contained in:
Louis Gallet 2023-10-11 11:33:06 +02:00
parent ec8c78cf4e
commit 745172f553
Signed by: lgallet
SSH Key Fingerprint: SHA256:qnW7pk4EoMRR0UftZLZQKSMUImbEFsiruLC7jbCHJAY
1 changed files with 10 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
Algo/CM/Lists.md
View File

@ -14,7 +14,7 @@ USES
OPERATIONS OPERATIONS
emptylist : -> list (* Internal operations of list*) emptylist : -> list (* Internal operations of list*)
cons : list x element -> list (* Internal operations of list *) cons : element x list -> list (* Internal operations of list *)
tail : list -> list (* Internal operations of list *) tail : list -> list (* Internal operations of list *)
head : list -> box (* Internal operations of box *) head : list -> box (* Internal operations of box *)
contents : box -> element (* Observer of box *) contents : box -> element (* Observer of box *)
@ -22,17 +22,17 @@ OPERATIONS
next : box -> box (* Internal operation of box *) next : box -> box (* Internal operation of box *)
PRECONDITIONS PRECONDITIONS
tail(_l_) is-defined-iaoi _l_ ≠ emptylist tail(l) is-defined-iaoi l ≠ emptylist
head(_l_) is-defined-iaoi _l_ ≠ emptylist head(l) is-defined-iaoi l ≠ emptylist
first(_l_) is-defined-iaoi _l_ ≠ emptylist first(l) is-defined-iaoi l ≠ emptylist
AXIOMS AXIOMS
first(_l_) = contents(head(_l_)) first(_l_) = contents(head(l))
tail(cons(_e,l_)) = _l_ tail(cons(_e,l_)) = l
first(cons(_e,l_)) = _e_ first(cons(_e,l_)) = e
next(head(_l_)) = head(tail(_l_)) next(head(_l_)) = head(tail(l))
WITH WITH
list _l_ list l
element _e_ element e
``` ```