Pasted

fmod NAT-ADD is
 	sort Nat .			--- hva vi opererer med
 	op 0 : -> Nat [ctor] .		--- tar en ikkenoe, lager s� et naturlig tall
	op s : Nat -> Nat [ctor] .	--- gj�r om en nat til en annen nat
	op _+_ : Nat Nat -> Nat .	--- legger sammen to nat, og returnerer en annen nat.
 	vars M N : Nat .		--- variabler m og n blir deklareret som naturlige tall
 	eq 0 + M = M .			--- null pluss noe er noe
	eq s(M) + N = s(M + N) .	--- en mer enn m pluss n er det samme som en mer enn m og n
 endfm
 fmod NAT-MULT is
 	protecting NAT-ADD .
 	op _*_ : Nat Nat -> Nat [prec 31] .
 	vars M N : Nat .
 	eq 0 * M = 0 .
	eq s(M) * N = N + M * N .
 endfm
 fmod NAT-MINUS is
 	protecting NAT-MULT .
 	op _-_ : Nat Nat -> Nat .
 	vars M N : Nat .
 	eq 0 - N = 0 .
	eq s(M) - 0 = s(M) .
	eq s(M) - s(N) = M - N .
 endfm
 fmod MONUS is
 	protecting NAT-MINUS .
 	op _monus_ : Nat Nat -> Nat .
 	vars M N : Nat .
 	eq M monus 0 = M .
	eq 0 monus M = 0 .
	eq s(M) monus s(N) = M monus N .
 endfm
 fmod BOOLEAN is
 	sort Boolean .
 	op true : -> Boolean .
	op false : -> Boolean .
	op not_ : Boolean -> Boolean .
	op _and_ : Boolean Boolean -> Boolean .
	op _or_ : Boolean Boolean -> Boolean .
 	var A : Boolean .
 	eq not true = false .
	eq not false = true .
	eq true and A = A .
	eq false and A = false .
	eq true or A = true .
	eq false or A = A .
 endfm
 fmod LIST is
 	protecting BOOLEAN .
	protecting MONUS .
 	sorts List .
 	op nil : -> List [ctor] .
	op __ : List Nat -> List [ctor] .
 	op length : List -> Nat .
	op concat : List List -> List .
	op insertFront : Nat List -> List .
	ops first last : List -> Nat .
	op rest : List -> List .
	op empty? : List -> Boolean .
	op reverse : List -> List .
 	vars N N' : Nat .
	vars L L' : List .
	---vars true false : Boolean .
 	eq length(nil) = 0 .
	eq length(L N) = s(length(L)) .
	eq concat(L, nil) = L .
	eq concat(L, L' N) = concat(L, L') N .
	eq first(nil) = 0 .                 *** Default/error value
	eq first(nil N) = N .
	eq first(L N N') = first(L N) .
 	--- oppgave 20 (empty?, rest, last, reverse) ---
 	eq last(nil) = 0 .
	eq last(nil N) = N .
	eq last(L N' N) = last(L N) .
 	eq rest(nil) = nil .
	eq rest(nil N) = nil .
	eq rest(L N) = rest(L) N .
 	eq reverse(nil) = nil .
	eq reverse(L)  = reverse(rest(L)) first(L) .
 	eq empty?(nil) = true .
	eq empty?(L) = false .
 endfm
 fmod BST is
 	protecting LIST .
 	sort BinTree .
 	op niltree : -> BinTree [ctor] .
	op bintree : BinTree Nat BinTree -> BinTree [ctor] .
	ops preorder inorder postorder : BinTree -> List . *** Traverse the tree
	ops size weight : BinTree -> Nat .
	op isSearchTree : BinTree -> Boolean .
	op reverse : BinTree -> BinTree .
 	vars BT BT' : BinTree .
	vars N N' : Nat .
 	eq preorder(niltree) = nil .
	eq preorder(bintree(BT, N, BT')) =
		insertFront(N,           *** Root first, then left and right subtrees:
			concat(preorder(BT), preorder(BT'))) .
 	eq size(niltree) = 0 .
	eq size(bintree(BT, N, BT')) = s(size(BT) + size(BT')) .
 	--- ====================================================
 	eq inorder(niltree) = nil .
	eq inorder(bintree(BT, N, BT')) = insertFront(N, concat(preorder(BT), preorder(BT'))) .
  	eq postorder(niltree) = nil .
  	eq reverse(niltree) = niltree .
  	eq weight(niltree) = 0 .
 endfm